Bohan Lyu

I'm an incoming PhD student at UC BerkeleyUC Berkeley EECS. I received my double bachelor's degree in Computer Science and Economics from TsinghuaTsinghua University in 2026.

Now I'm working on self-evolving intelligence at PrincetonPLI, Princeton, advised by Prof. Prof. Chi Jin. Prior to it, I've worked in Tsinghua NLP Lab, advised by Prof. Zhiyuan Liu, and Rose-STL-Lab, UCSDUCSD, advised by Prof. Rose Yu.

Feel free to reach out if you want to chat about research or collaboration!

Contact Info  /  Google Scholar  /  Twitter  /  Where is Bohan?

   

profile photo

News

  • 2026-05 Releasing MLS-Bench!
  • 2025-07 Releasing Goedel-Prover-V2!
  • 2025-05 Enhancing LLM's Capabilities in Open Domains via Autonomous Tool Integration is accepted to ACL 2025 Main!
  • 2025-05 Adapting while Learning is accepted to ICML 2025!
  • 2024-05 Awarded Spark Scientific and Technological Innovation Fellowship (Top 1% in Tsinghua).

Research (* indicates equal contribution, highlight indicates representative papers)
project image

Agents' Last Exam


ALE Team
arXiv 2026
arXiv / Code / Website / BibTeX /

We introduce Agents’ Last Exam (ALE), a benchmark of 1K+ long-horizon, economically valuable, real-world tasks across 55 subfields and 13 industry clusters, and find that current frontier agents remain far from saturating the hardest tier.
project image

MLS-Bench: A Holistic and Rigorous Assessment of AI Systems on Building Better AI


Bohan Lyu*, Yucheng Yang*, Siqiao Huang*, Jiaru Zhang*, Qixin Xu*, Xinghan Li*, Xinyang Han*, Yicheng Zhang*, Huaqing Zhang*, Runhan Huang, Kaicheng Yang, Zitao Chen, Wentao Guo, Junlin Yang, Xinyue Ai, Wenhao Chai, Yadi Cao, Ziran Yang, Kun Wang, Dapeng Jiang, Huan-ang Gao, Shange Tang, Chengshuai Shi, Simon S. Du, Max Simchowitz, Jiantao Jiao, Dawn Song, Chi Jin
AI4Math @ ICML2026 (Honorable Mention Award)
arXiv / Code / Website / BibTeX /

We introduce MLS-Bench, a benchmark of 140 tasks across 12 domains for evaluating whether AI systems can invent generalizable and scalable ML methods, and find that current agents remain far from reliably surpassing human-designed methods.
project image

Goedel-Prover-V2: Scaling Formal Theorem Proving with Scaffolded Data Synthesis and Self-Correction


Yong Lin*, Shange Tang*, Bohan Lyu*, Ziran Yang*, Jui-Hui Chung*, Haoyu Zhao*, Lai Jiang*, Yihan Geng*, Jiawei Ge, Jingruo Sun, Jiayun Wu, Jiri Gesi, Ximing Lu, David Acuna, Kaiyu Yang, Hongzhou Lin, Yejin Choi, Danqi Chen, Sanjeev Arora, Chi Jin
ICLR 2026, AI4MATH @ ICML 2025 (Oral)
arXiv / Code / Slides / Website / BibTeX /

Goedel-Prover-V2 sets new state-of-the-art in automated proof generation with dramatically smaller models, using scaffolded training, self-correction, and model averaging to outperform systems 20-100x larger on key mathematical benchmarks.
project image

SURGE: On the Potential of Large Language Models as General-Purpose Surrogate Code Executors


Bohan Lyu*, Siqiao Huang*, Zichen Liang*
EMNLP 2025 (Main, meta score top 0.3%)
arXiv / Code / Website / BibTeX /

SURGE evaluates LLMs’ ability to predict code execution across eight key areas. While they show promise, limitations prevent general-purpose surrogate execution. This is an extension of a course project that does not reflect the focus of my research.
project image

Goedel-Prover: A Frontier Model for Open-Source Automated Theorem Proving


Yong Lin*, Shange Tang*, Bohan Lyu, Jiayun Wu, Hongzhou Lin, Kaiyu Yang, Jia Li, Mengzhou Xia, Danqi Chen, Sanjeev Arora, Chi Jin
COLM 2025
arXiv / Code / Website / YouTube / BibTeX /

The new 7B Goedel-Prover sets a new state-of-the-art in open-source automated theorem proving, beating previous records with a 7% improvement on miniF2F, topping the PutnamBench Leaderboard, and solving nearly twice as many problems on Lean Workbook.
project image

Adapting While Learning: Grounding LLMs for Scientific Problems with Tool Usage Adaptation


Bohan Lyu*, Yadi Cao*, Duncan Watson-Parris, Leon Bergen, Taylor Berg-Kirkpatrick, Rose Yu
ICML 2025, AAAI 2024 FSS (Oral)
arXiv / Code / Slides / Website / YouTube / BibTeX /

This work proposes a fine-tuning method where LLMs internalize tool-generated solutions (World Knowledge Distillation) and learn to switch between direct answers and tool use for complex problems (Tool Usage Adaptation). It outperforms GPT-4 and Claude-3.5 across six scientific benchmarks.
project image

Enhancing Open-Domain Task-Solving Capability of LLMs via Autonomous Tool Integration from GitHub


Bohan Lyu*, Xin Cong*, Heyang Yu, Pan Yang, Cheng Qian, Zihe Wang, Yujia Qin, Yining Ye, Yaxi Lu, Chen Qian, Zhong Zhang, Yukun Yan, Yankai Lin, Zhiyuan Liu, Maosong Sun
ACL 2025 (Main)
arXiv / Code / Slides / Website / YouTube / BibTeX /

Constructed OpenAct benchmark for complex open-domain task-solving. Developed a novel LLM agent system, OpenAgent, which leverages GitHub repositories to extend its capabilities to address diverse user queries.

Talks

Towards AI Systems That Build Better AI  [Video (in Chinese)]

  • 2026-05TsinghuaTsinghua University
  • 2026-05Moonshot AIMoonshot AI (Kimi)
  • 2026-05Zhipu AIZhipu AI (GLM)
  • 2026-06Peking UniversityPeking University
  • 2026-06TencentTencent

Fantastic CS PhD Opportunities and Where to Find Them  [Slides]

  • 2026-03TsinghuaTsinghua University

The Curious Landscape of LLM Reasoning: An Overview of Techniques, Research Directions, and Challenges  [Slides]

  • 2025-10TsinghuaTsinghua University

LLM Reasoning: From Informal to Formal  [Slides]

  • 2025-07TsinghuaTsinghua University

Resources

Some tools and resources I've developed for the research community:

  • jload - A Python package for convenient JSON/JSONL data loading and saving. PyPI version
  • vlllm - A Python package for convenient text generation with multiprocessing support. PyPI version





Design and source code from Leonid Keselman's website