論文の概要: ProofOptimizer: Training Language Models to Simplify Proofs without Human Demonstrations

• arxiv url: http://arxiv.org/abs/2510.15700v1
• Date: Fri, 17 Oct 2025 14:45:30 GMT
• ステータス: 翻訳完了
• システム内更新日: 2025-10-20 20:17:34.66035
• Title: ProofOptimizer: Training Language Models to Simplify Proofs without Human Demonstrations
• Title（参考訳）: ProofOptimizer:人間の指示なしに証明をシンプルにするための言語モデルを訓練する
• Authors: Alex Gu, Bartosz Piotrowski, Fabian Gloeckle, Kaiyu Yang, Aram H. Markosyan,
• Abstract要約: Proofrは、人間の監督を必要とせず、リーンの証明を単純化するために訓練された最初の言語モデルです。 Provrは専門家の反復と強化学習を通じてトレーニングされ、リーンを使って単純化の検証とトレーニング信号を提供する。 Provrは、最先端のRL訓練プローバーが標準ベンチマークで生成した証明を実質的に圧縮する。
• 参考スコア（独自算出の注目度）: 14.748476989228214
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Neural theorem proving has advanced rapidly in the past year, reaching IMO gold-medalist capabilities and producing formal proofs that span thousands of lines. Although such proofs are mechanically verified by formal systems like Lean, their excessive length renders them difficult for humans to comprehend and limits their usefulness for mathematical insight. Proof simplification is therefore a critical bottleneck. Yet, training data for this task is scarce, and existing methods -- mainly agentic scaffolding with off-the-shelf LLMs -- struggle with the extremely long proofs generated by RL-trained provers. We introduce ProofOptimizer, the first language model trained to simplify Lean proofs without requiring additional human supervision. ProofOptimizer is trained via expert iteration and reinforcement learning, using Lean to verify simplifications and provide training signal. At inference time, it operates within an iterative proof-shortening workflow, progressively reducing proof length. Experiments show that ProofOptimizer substantially compresses proofs generated by state-of-the-art RL-trained provers on standard benchmarks, reducing proof length by 87% on miniF2F, 57% on PutnamBench, and 49% on Seed-Prover's IMO 2025 proofs. Beyond conciseness, the simplified proofs check faster in Lean and further improve downstream prover performance when reused as training data for supervised finetuning.
• Abstract（参考訳）: ニューラル定理の証明は、過去1年間に急速に進歩し、IMOゴールドメダリストの能力に到達し、数千行に及ぶ公式な証明を生み出した。 このような証明は、Leanのような形式的なシステムによって機械的に検証されているが、その過剰な長さは、人間が数学的洞察のために有用性を理解し、制限することを困難にしている。 したがって、証明の単純化は重要なボトルネックである。 しかし、このタスクのトレーニングデータは乏しく、既存の手法(主に既成のLLMを持つエージェント的な足場)は、RL訓練プローバーが生成する極めて長い証明と競合する。 ProofOptimizerを紹介します。これは、人間の監督を必要とせず、リーンの証明を単純化するために訓練された最初の言語モデルです。 ProofOptimizerは、専門家の反復と強化学習を通じてトレーニングされ、リーンを使用して単純化の検証とトレーニング信号を提供する。 推論時に反復的な証明ショートニングワークフロー内で動作し、証明の長さを徐々に削減する。 実験の結果、ProofOptimizerは標準ベンチマークで最先端のRL訓練プロバーによって生成された証明を実質的に圧縮し、miniF2Fでは87%、PatnamBenchでは57%、Seed-Proverでは49%の証明を削減した。 簡潔さの他に、単純化された証明はリーンでより高速にチェックし、教師付き微調整のためのトレーニングデータとして再利用された場合、下流の証明器のパフォーマンスをさらに向上する。

関連論文リスト

• LeanProgress: Guiding Search for Neural Theorem Proving via Proof Progress Prediction [74.79306773878955]
  証明の進捗を予測する手法であるLeanProgressを紹介します。 実験の結果、LeanProgressは全体の予測精度が75.1%に達することがわかった。
  論文  参考訳（メタデータ） (2025-02-25T07:46:36Z)
• Generating Millions Of Lean Theorems With Proofs By Exploring State Transition Graphs [6.65877320351217]
  我々はLeanNavigatorを開発した。これはリーンの定理と証明の大規模なデータセットを生成する新しい方法だ。 我々は10億のトークンを合計470万の定理で生成し、以前のデータセットを桁違いに上回った。 この広範なデータセットを使用して、我々は、定理証明タスクにおいて最先端のReProverモデルより優れたAIモデルを訓練した。
  論文  参考訳（メタデータ） (2025-02-16T06:20:39Z)
• Next-Token Prediction Task Assumes Optimal Data Ordering for LLM Training in Proof Generation [27.60611509339328]
  1つのトレーニングデータサンプルの最適順序は、特定の証明ステップの関連中間監督が、その証明ステップの左側に常に配置されているときに発生すると論じる。 証明が直感的に逐次順序にある場合、トレーニングが最も効果的であることを示す。
  論文  参考訳（メタデータ） (2024-10-30T18:00:04Z)
• Lean-STaR: Learning to Interleave Thinking and Proving [53.923617816215774]
  証明の各ステップに先立って,非公式な思考を生成するために,言語モデルをトレーニングするフレームワークであるLean-STaRを紹介します。 Lean-STaRは、Lean定理証明環境内のminiF2F-testベンチマークで最先端の結果を達成する。
  論文  参考訳（メタデータ） (2024-07-14T01:43:07Z)

関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。

指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。