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.

I previously worked on AI for Math and self-evolving intelligence at PrincetonPLI, Princeton, advised by Prof. Chi Jin. I've also worked in Tsinghua NLP Lab, advised by Prof. Zhiyuan Liu, and Spatiotemporal Learning 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-11 Finalist for the Tsinghua University Top Grade Scholarship (15 out of ~3,600, highest honor).
  • 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-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