論文の概要: OProver: A Unified Framework for Agentic Formal Theorem Proving

• arxiv url: http://arxiv.org/abs/2605.17283v1
• Date: Sun, 17 May 2026 06:39:05 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-05-19 17:57:47.828161
• Title: OProver: A Unified Framework for Agentic Formal Theorem Proving
• Title（参考訳）: OProver: エージェント形式定理証明のための統一フレームワーク
• Authors: David Ma, Kaijing Ma, Shawn Guo, Yunfeng Shi, Enduo Zhao, Jiajun Shi, Zhaoxiang Zhang, Gavin Cheung, Jiaheng Liu, Zili Wang,
• Abstract要約: OProverは、Lean 4.0で証明された代理的な形式的な反復定理のための統一されたフレームワークである。 エージェント証明を実行し、新たに証明された証明をOProofsと検索メモリにインデックスし、修理軌跡をSFTデータとして使用し、未解決のハードケースをRLに使用する。 OProver-32BはMiniF2F (93.3%)、ProverBench (58.2%)、PutnamBench (11.3%)で最高のパス@32を獲得し、MathOlympiad (22.8%)、ProofNet (33.2%)で上位にランクインしている。
• 参考スコア（独自算出の注目度）: 33.14658302112269
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Recent progress in formal theorem proving has benefited from large-scale proof generation and verifier-aware training, but agentic proving is rarely integrated into prover training, appearing only at inference time. We present OProver, a unified framework for agentic formal theorem proving in Lean 4, in which failed proof attempts are iteratively revised using retrieved compiler verified proofs and Lean compiler feedback. OProver is trained through continued pretraining followed by iterative post-training: each iteration runs agentic proving, indexes newly verified proofs into OProofs and the retrieval memory, uses repair trajectories as SFT data, and uses unresolved hard cases for RL. OProofs is built from public Lean resources, large-scale proof synthesis, and agentic proving traces, containing 1.77M Lean statements, 6.86M compiler-verified proofs, and serialized trajectories with retrieved context, failed attempts, feedback, and repairs. Across five benchmarks, OProver-32B attains the best Pass@32 on MiniF2F (93.3%), ProverBench (58.2%), and PutnamBench (11.3%), and ranks second on MathOlympiad (22.8%) and ProofNet (33.2%) more top placements than any prior open-weight whole-proof prover.
• Abstract（参考訳）: 近年の形式的定理証明の進歩は、大規模な証明生成と検証者対応訓練の恩恵を受けているが、エージェント的証明は推論時にのみ現れる証明者訓練に統合されることは滅多にない。 OProver(リンク)は、Lean 4で証明されたエージェント形式定理の統一フレームワークで、取得したコンパイラ検証証明とLeanコンパイラフィードバックを使用して、失敗した証明の試みを反復的に修正する。 各イテレーションはエージェントによる証明を実行し、新たに証明された証明をOProofsと検索メモリにインデックスし、修理軌跡をSFTデータとして使用し、未解決のハードケースをRLに使用する。 OProofsは、パブリックなリーンリソース、大規模な証明合成、エージェントによる証明トレースから構築されており、リーンステートメント1.77M、コンパイラが検証した証明6.86M、検索されたコンテキスト、失敗した試み、フィードバック、修正を含むシリアライズされたトラジェクトリを含んでいる。 5つのベンチマークで、OProver-32BはMiniF2F (93.3%)、ProverBench (58.2%)、PutnamBench (11.3%)で最高のPass@32を獲得し、MathOlympiad (22.8%)、ProofNet (33.2%)の上位にランクインした。

関連論文リスト

• ProofOptimizer: Training Language Models to Simplify Proofs without Human Demonstrations [14.748476989228214]
  Proofrは、人間の監督を必要とせず、リーンの証明を単純化するために訓練された最初の言語モデルです。 Provrは専門家の反復と強化学習を通じてトレーニングされ、リーンを使って単純化の検証とトレーニング信号を提供する。 Provrは、最先端のRL訓練プローバーが標準ベンチマークで生成した証明を実質的に圧縮する。
  論文  参考訳（メタデータ） (2025-10-17T14:45:30Z)
• ProofBridge: Auto-Formalization of Natural Language Proofs in Lean via Joint Embeddings [9.764411884491052]
  ProofBridgeは、NLの定理と証明を自動的にリーン4に翻訳するフレームワークです。 中心となるのは、NL と FL (NL-FL) の定理対を共有意味空間で整列する合同埋め込みモデルである。 我々の訓練は、NL-FL 対が意味論的に同値である場合に限り、この空間において NL-FL の定理が密接にマッピングされることを保証する。
  論文  参考訳（メタデータ） (2025-10-17T14:20:50Z)
• LeanProgress: Guiding Search for Neural Theorem Proving via Proof Progress Prediction [74.79306773878955]
  証明の進捗を予測する手法であるLeanProgressを紹介します。 実験の結果、LeanProgressは全体の予測精度が75.1%に達することがわかった。
  論文  参考訳（メタデータ） (2025-02-25T07:46:36Z)
• Goedel-Prover: A Frontier Model for Open-Source Automated Theorem Proving [72.8626512877667]
  我々は,2025年4月5日現在,数学問題の自動証明生成における最先端(最先端)性能を実現する,オープンソースの言語モデルであるGoedel-Proverを紹介した。 まず、自然言語の数学問題をNuminaデータセットからLean 4で等価な形式ステートメントに変換するためにLLMをトレーニングします。 次に,一連のプロデューサをトレーニングすることで,形式証明の大規模なデータセットを開発する。 最後に、Goedel-Pset-v1-solvedというデータセットを取得し、Goedel-Pset-v1から800K以上のステートメントの証明を含む。
  論文  参考訳（メタデータ） (2025-02-11T15:27:35Z)
• STP: Self-play LLM Theorem Provers with Iterative Conjecturing and Proving [33.61458249318183]
  セルフプレイ・セオレム・プロバー(STP)は、予想と証明という2つの役割を担っている。 STPは同時に、予想と証明という2つの役割を担っている。 私たちはLeanとIsabelleの2つの形式的検証ツールで評価します。
  論文  参考訳（メタデータ） (2025-01-31T23:01:48Z)
• Lean-STaR: Learning to Interleave Thinking and Proving [53.923617816215774]
  証明の各ステップに先立って,非公式な思考を生成するために,言語モデルをトレーニングするフレームワークであるLean-STaRを紹介します。 Lean-STaRは、Lean定理証明環境内のminiF2F-testベンチマークで最先端の結果を達成する。
  論文  参考訳（メタデータ） (2024-07-14T01:43:07Z)
• DeepSeek-Prover: Advancing Theorem Proving in LLMs through Large-Scale Synthetic Data [65.5290035371111]
  本稿では,高校・学部レベルの数学競争問題から得られたリーン4証明データを生成する手法を提案する。 この合成データセットでDeepSeekMath 7Bモデルを微調整します。 我々のモデルは、Lean 4 Formalized International Mathematical Olympiad (FIMO)ベンチマークで148の問題を5つ証明しましたが、GPT-4は証明できませんでした。
  論文  参考訳（メタデータ） (2024-05-23T09:03:42Z)

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

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