DeepSeek-Prover-V2: Advancing Formal Mathematical Reasoning via Reinforcement Learning for Subgoal Decomposition

要約

Lean 4で証明する正式な定理用に設計されたオープンソースの大型言語モデルであるDeepSeek-Prover-V2を導入します。初期化データは、DeepSeek-V3を搭載した再帰定理証明パイプラインを通じて収集されます。
コールドスタートトレーニング手順は、DeepSeek-V3に複雑な問題を一連のサブゴールに分解するよう促すことから始まります。
解決されたサブゴールの証明は、補強学習のための最初のコールドスタートを作成するために、DeepSeek-V3の段階的な推論と組み合わせて、考え方のプロセスに合成されます。
このプロセスにより、非公式および正式な数学的推論の両方を統一モデルに統合することができます。
結果のモデルであるDeepSeek-Prover-V2-671Bは、神経定理が証明する最先端のパフォーマンスを実現し、MINIF2Fテストで88.9％のパス比に達し、Putnambenchの658の問題のうち49件を解きました。
標準のベンチマークに加えて、325の正式な問題のコレクションであるProverbenchを紹介し、最近のAIMEコンペティションから選択された15の問題を含む評価を充実させます（24〜25年）。
これらの15のAIME問題に関するさらなる評価は、モデルがそれらの6つを正常に解決することを示しています。
それに比べて、DeepSeek-V3は多数決を使用してこれらの問題の8つを解決し、大規模な言語モデルにおける正式な数学的推論と非公式の数学的推論のギャップが実質的に狭くなっていることを強調しています。

要約(オリジナル)

We introduce DeepSeek-Prover-V2, an open-source large language model designed for formal theorem proving in Lean 4, with initialization data collected through a recursive theorem proving pipeline powered by DeepSeek-V3. The cold-start training procedure begins by prompting DeepSeek-V3 to decompose complex problems into a series of subgoals. The proofs of resolved subgoals are synthesized into a chain-of-thought process, combined with DeepSeek-V3’s step-by-step reasoning, to create an initial cold start for reinforcement learning. This process enables us to integrate both informal and formal mathematical reasoning into a unified model. The resulting model, DeepSeek-Prover-V2-671B, achieves state-of-the-art performance in neural theorem proving, reaching 88.9% pass ratio on the MiniF2F-test and solving 49 out of 658 problems from PutnamBench. In addition to standard benchmarks, we introduce ProverBench, a collection of 325 formalized problems, to enrich our evaluation, including 15 selected problems from the recent AIME competitions (years 24-25). Further evaluation on these 15 AIME problems shows that the model successfully solves 6 of them. In comparison, DeepSeek-V3 solves 8 of these problems using majority voting, highlighting that the gap between formal and informal mathematical reasoning in large language models is substantially narrowing.

arxiv情報

提供元, 利用サービス

arxiv.jp, Google