Organizer: 张泽宝

Speaker: 辛华剑（爱丁堡大学）

Time: 17:00-18:00, Mar. 18  2025

Online: Zoom: 811 5638 1768（Password: msrc）

Venue: 至善楼602

Title: Frontier of Formal Theorem Proving with Large Language Models: Insights from the DeepSeek-Prover Series

Abstract:

Recent advances in large language models have markedly influenced mathematical reasoning and automated theorem proving within artificial intelligence. Yet, despite their success in natural language tasks, these models face notable obstacles in formal theorem proving environments such as Lean and Isabelle, where exacting derivations must adhere to strict formal specifications. Even state-of-the-art models encounter difficulty generating accurate and complex formal proofs, revealing the unique blend of mathematical rigor required in this domain. In the DeepSeek-Prover series (V1 and V1.5), we have explored specialized methodologies aimed at addressing these challenges. This talk will delve into three foundational areas: the synthesis of training data through autoformalization, reinforcement learning that utilizes feedback from proof assistants, and test-time optimization using Monte Carlo tree search. I will also provide insights into current model capabilities, persistent challenges, and the future potential of large language models in automated theorem proving.

Cirriculum Vitae:

Huajian Xin is currently a PhD student at the University of Edinburgh under Professor Li Wenda. His research focuses on enabling large language models (LLMs) to perform formalized mathematical theorem proving, with a particular emphasis on autoformalization tasks that bridge natural language and formal language, as well as agent tasks that leverage computer algebra systems and other tools. He is also interning with the ByteDance Doubao/Seed Team and previously interned at DeepSeek, where he led the research on the DeepSeek Prover series of models. For more information, please visit his personal homepage at https://xinhuajian.wordpress.com.