Bohan Lyu

I'm a first-year PhD student at UC Berkeley EECS, and a member of BAIR.

Previously, I worked on AI for Math and self-improving AI systems at PLI, Princeton, advised by Prof. Chi Jin. I've also worked in Tsinghua NLP Lab, advised by Prof. Zhiyuan Liu, and Spatiotemporal Learning Lab, UCSD UCSD, advised by Prof. Rose Yu.

I received my double bachelor's degree in Computer Science and Economics from Tsinghua University in 2026.

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

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

News

2026-10 Releasing RAX! Scaling online exploration achieves SOTA results across 5 benchmarks and enables robots to learn complex real-world tasks without human demonstrations.
2026-09 MLS-Bench is accepted as an Oral at NeurIPS 2026 (top 0.4%)! It has also been featured in model releases from AI labs like Qwen.
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 highlight indicates representative papers

	FrontierCS 2: A Benchmark for Computer Science R&D FrontierCS 2 Team Preprint, 2026 arXiv / Code / Website / BibTeX / We introduce FrontierCS 2, a benchmark of 48 open-ended computer science R&D tasks across 13 domains. Agents reconstruct the key contribution removed from a paper’s released code and pass only when their implementation beats the human reference on every metric and hidden workload.
	Scaling Online Exploration for Robot Agents Runhan Huang, Xiangcheng Zhang, Haoyu Chen, Yitong Li, Yen-Jen Wang, Bohan Lyu, Haotian Ye, Chuye Hong, Yixuan Wang, Chloe Su, Haoyu Xiong, Yangzhen Wu, Enze Xie, Travis Manderson, Stefano Ermon, Pieter Abbeel, Antonio Torralba, Dawn Song, Weirui Ye, Yilun Du Preprint, 2026 arXiv / Code / Website / BibTeX / We introduce RAX (Robot Agent eXploration), an open-source framework that scales online exploration for robot agents: a frozen LLM coding agent acquires online experience and compiles it into executable programs, learning new tasks with no demonstrations, no teleoperation, and no policy training.
	Agents' Last Exam ALE Team NeurIPS 2026 E&D Track 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.
	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 NeurIPS 2026 E&D Track (Oral, Top 0.4%)* 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.
	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.
	Ineq-Comp: Benchmarking Human-Intuitive Compositional Reasoning in Automated Theorem Proving on Inequalities Haoyu Zhao, Yihan Geng, Shange Tang, Yong Lin, Bohan Lyu, Hongzhou Lin, Chi Jin, Sanjeev Arora NeurIPS 2025 D&B Track arXiv / Code / BibTeX / LLM-based proof assistants struggle with compositional reasoning in inequalities. The Ineq-Comp benchmark reveals that even strong models like DeepSeek-Prover-V2-7B falter, despite having proofs of subparts. This highlights a key gap between AI and human mathematical intuition.
	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.
	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.
	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.
	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.