DeepTheorem: Advancing LLM Reasoning for Theorem Proving Through Natural Language and Reinforcement Learning

要約

定理証明は、大規模な言語モデル（LLM）の複雑な推論能力を評価するための主要なテストベッドとして機能します。
ただし、従来の自動化された定理（ATP）アプローチは、トレーニング前に獲得した非公式の自然言語知識から派生したLLMSの強度とは不十分な正式な証明システムに大きく依存しています。
この作業では、LLM数学的推論を強化するために自然言語を活用する包括的な非公式の定理枠組みである深い理論を提案します。
Deeptheoremには、121kの高品質のIMOレベルの非公式定理と、正確さ、難易度、およびトピックカテゴリに厳密に注釈が付けられた多様な数学ドメインにまたがる証明で構成される大規模なベンチマークデータセットが含まれています。
私たちは、堅牢な数学的推論を奨励するために、検証された定理バリアントを活用して、非公式の定理を実証するために明示的に調整された新しい強化学習戦略（RL-Zero）を考案します。
さらに、証明の正確性と推論ステップの質を調べる包括的な結果とプロセス評価メトリックを提案します。
広範な実験分析により、深部理論により、既存のデータセットや監視された微調整プロトコルと比較してLLM定理プロービングパフォーマンスが大幅に向上し、最先端の精度と推論品質を達成します。
私たちの調査結果は、自動化された非公式の定理と数学的探査を根本的に前進させる深い理論の可能性を強調しています。

要約(オリジナル)

Theorem proving serves as a major testbed for evaluating complex reasoning abilities in large language models (LLMs). However, traditional automated theorem proving (ATP) approaches rely heavily on formal proof systems that poorly align with LLMs’ strength derived from informal, natural language knowledge acquired during pre-training. In this work, we propose DeepTheorem, a comprehensive informal theorem-proving framework exploiting natural language to enhance LLM mathematical reasoning. DeepTheorem includes a large-scale benchmark dataset consisting of 121K high-quality IMO-level informal theorems and proofs spanning diverse mathematical domains, rigorously annotated for correctness, difficulty, and topic categories, accompanied by systematically constructed verifiable theorem variants. We devise a novel reinforcement learning strategy (RL-Zero) explicitly tailored to informal theorem proving, leveraging the verified theorem variants to incentivize robust mathematical inference. Additionally, we propose comprehensive outcome and process evaluation metrics examining proof correctness and the quality of reasoning steps. Extensive experimental analyses demonstrate DeepTheorem significantly improves LLM theorem-proving performance compared to existing datasets and supervised fine-tuning protocols, achieving state-of-the-art accuracy and reasoning quality. Our findings highlight DeepTheorem’s potential to fundamentally advance automated informal theorem proving and mathematical exploration.

arxiv情報

提供元, 利用サービス

arxiv.jp, Google