Is Behavior Cloning All You Need? Understanding Horizon in Imitation Learning

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.

In person and on Zoom:

https://harvard.zoom.us/j/92220006185?pwd=V3mrb4cNSbgRXtNJtRJkTvWFVhmbI5.1
Password: cmsa