要約
LLMSを通じて自動化された定理証明（ATP）の最近の進歩は、LEAN 4コードを使用した正式な推論の可能性を強調しています。
ただし、ATPは、Open AI O1/O3およびDeepSeek R1によって実証されているように、最近のトレーニング後のスケーリングによってまだ革命されていません。
この作業では、ATPのポストトレーニング全体を調査し、自然言語の推論モデルのブレークスルーと整列することを目指しています。開始するには、現在のATPモデルを継続的に訓練します。
次に、Lean 4 Compilerによって返された結果報酬を使用して、補強学習を検討します。
設計された継続的なトレーニングと強化学習プロセスを通じて、DeepSeek-Prover-V1.5とGoedel-Proverの両方を含む既存の正式なプロバーを成功裏に改善し、全装飾の分野で最先端のパフォーマンスを達成しました。
たとえば、MINIF2Fで59.8％の合格率（Pass@32）を達成します。
これは進行中のプロジェクトであり、調査結果を徐々に更新し、データとトレーニングの詳細を公開します。
要約(オリジナル)
Recent advances in automated theorem proving (ATP) through LLMs have highlighted the potential of formal reasoning with Lean 4 codes. However, ATP has not yet be revolutionized by the recent posttraining scaling as demonstrated by Open AI O1/O3 and Deepseek R1. In this work, we investigate the entire posttraining of ATP, aiming to align it with breakthroughs in reasoning models in natural languages.To begin, we continual train current ATP models with a hybrid dataset, which consists of numerous statement-proof pairs, and additional data aimed at incorporating cognitive behaviors that emulate human reasoning and hypothesis refinement. Next, we explore reinforcement learning with the use of outcome reward returned by Lean 4 compiler. Through our designed continual training and reinforcement learning processes, we have successfully improved existing formal provers, including both DeepSeek-Prover-v1.5 and Goedel-Prover, achieving state-of-the-art performance in the field of whole-proof generation. For example, we achieve a 59.8% pass rate (pass@32) on MiniF2F. This is an on-going project and we will progressively update our findings, release our data and training details.
arxiv情報
| 著者 | Jingyuan Zhang,Qi Wang,Xingguang Ji,Yahui Liu,Yang Yue,Fuzheng Zhang,Di Zhang,Guorui Zhou,Kun Gai |
| 発行日 | 2025-04-08 15:15:26+00:00 |
| arxivサイト | arxiv_id(pdf) |
提供元, 利用サービス
arxiv.jp, Google