論文の概要: AIProver: Agentic Auto-Formalization of Mathematical Research via Certificate-Driven Evolving Harness

• arxiv url: http://arxiv.org/abs/2610.05367v1
• Date: Sun, 04 Oct 2026 16:48:12 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-10-10 14:20:18.336996
• Title: AIProver: Agentic Auto-Formalization of Mathematical Research via Certificate-Driven Evolving Harness
• Title（参考訳）: AIProver: Certificate-Driven Evolving Harnessによる数学研究のエージェントオートフォーマル化
• Abstract要約: 本稿では,自律的証明自動形式化と証明合成のためのエージェントフレームワークであるAIProverを提案する。 119Bのオープンウェイト言語モデルを共同で訓練し、HarnessEvolveとのエージェント的ツールコールハーネスを進化させた。 研究レベルのトレーニングと評価のために,RoCoBench,Mathlib,CSLib,Mizar Math Libraryの58.9kインスタンス,および有界算術教科書を紹介する。
• 参考スコア（独自算出の注目度）: 10.0330160351666
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: Proof auto-formalization translates natural-language (NL) theorems and proofs into a formal language (FL) such as Lean, enabling mechanical verification. Despite rapid progress, research-level proofs often depend on concepts missing from leading proof assistant libraries (e.g., Lean's Mathlib), and successful compilation does not guarantee that a translation preserves the theorem's meaning or the proof's reasoning. Furthermore, aligned NL-FL training data are scarce, and leading agents often rely on costly frontier models and manually engineered harnesses. To address the above issues, we present AIProver, an agentic framework for autonomous proof auto-formalization and proof synthesis (AFPS) that jointly post-trains a 119B open-weight language model and evolves its agentic, tool-calling harness with HarnessEvolve. Verifiers assess type correctness, proof completeness, and semantic correctness, returning rewards and diagnostic certificates that drive model fine-tuning and alternating reinforcement learning via symbolic feedback and HarnessEvolve, a certificate-driven evolutionary search over the whole harness control flow that re-tailors the harness to the updated model. For research-level training and evaluation, we introduce LoCoBench, 58.9k instances from Mathlib, CSLib, Mizar Math Library, and a bounded-arithmetic textbook, with a 771-instance validation split whose theorem-proof pairs have no public Lean formalization. Against 39 frameworks spanning AFPS agents, frontier LLMs, and coding agents, AIProver lifts pass@4 semantic correctness over its Leanstral-1.5 base from 15.7% to 36.7% and outperforms every other open-weight system and Aristotle. As a Claude Code and Codex skill, it lifts their semantic correctness from 41.9% and 34.1% to 79.8% and 62.4%, respectively. Further, it is also 24% cheaper than Numina-Lean-Agent, pushing the accuracy-cost frontier of research-level AFPS.
• Abstract（参考訳）: 証明自己形式化(Proof auto-formalization)は、自然言語(NL)の定理と証明をリーンのような形式言語(FL)に変換し、機械的検証を可能にする。 急激な進歩にもかかわらず、研究レベルの証明は、主要な証明補助ライブラリ(例えば、リーンのMathlib)から欠落している概念に依存しており、成功しているコンパイルは、翻訳が定理の意味や証明の推論を保存することを保証しない。 さらに、調整されたNL-FL訓練データは乏しく、先導エージェントはコストのかかるフロンティアモデルや手作業によるハーネスに依存していることが多い。 上記の問題に対処するため、AIProverは、自律的証明の自動形式化と証明合成(AFPS)のためのエージェントフレームワークであり、119Bのオープンウェイト言語モデルを共同で訓練し、HarnessEvolveでエージェント的ツールコールハーネスを進化させる。 検証者は、タイプ正当性、証明完全性、意味的正当性を評価し、モデルの微調整とシンボルフィードバックによる強化学習を駆動する報酬と診断証明書を返却する。 研究レベルのトレーニングと評価には、Mathlib, CSLib, Mizar Math Library, and a bounded-arithmetic textbook, with a 771-instance validation split that the theorem-proof pairs have not public Lean formalization. 58.9k instances from Mathlib, CSLib, Mizar Math Library, and a bounded-arithmetic textbook。 AFPSエージェント、フロンティアLDM、コーディングエージェントにまたがる39のフレームワークに対して、AIProverは、Leanstral-1.5ベースを15.7%から36.7%に引き上げ、他のすべてのオープンウェイトシステムとアリストテレスを上回ります。 クロード・コードとコーデックスのスキルとして、それぞれ41.9%と34.1%から79.8%、62.4%に意味的正しさを引き上げている。 さらに、Numina-Lean-Agentよりも24%安く、研究レベルのAFPSの精度とコストの面でも優れている。

関連論文リスト

• ProofLoom: Proof-Obligation-Driven Theory Construction for Autoformalizing Research-Level Stochastic Optimization [5.053793874612475]
  本稿では,ProofLoomを紹介した。Proof-Obligation-Driven Theory Constructionのための,完全に自動化されたLLMエージェントシステムである。 ProofLoomは、公開されたアルゴリズム、ターゲット定理、およびソース証明を与えられた後、リーンモデルとサポート理論を自律的に構築する。 33の開発で、490,693行のアルゴリズムローカルなリーンコードを生成する。
  論文  参考訳（メタデータ） (2026-09-28T11:45:27Z)
• OProver: A Unified Framework for Agentic Formal Theorem Proving [33.14658302112269]
  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%)で上位にランクインしている。
  論文  参考訳（メタデータ） (2026-05-17T06:39:05Z)
• 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)
• APOLLO: Automated LLM and Lean Collaboration for Advanced Formal Reasoning [16.8655558789989]
  本稿では,自動定理証明のためのモデルに依存しないエージェントフレームワークであるAPOLLO (Automated PrOof repair viaLLM and Lean cOllaboration)を提案する。 エージェントのセットは、証明を分析し、シンタックスのエラーを修正し、リーンを使って証明の誤りを特定し、失敗するサブレムマを分離し、自動化されたソルバを利用し、残りの目標に対してLLMを呼び出す。 この結果から,LLM出力を目標としたコンパイラ誘導型修復は,効率と正確性の両方において劇的に向上することが示された。
  論文  参考訳（メタデータ） (2025-05-09T03:38:31Z)
• Formal Theorem Proving by Rewarding LLMs to Decompose Proofs Hierarchically [29.908878832382523]
  本稿では,自動検証/評価を可能にする形式言語による証明記述能力の向上に焦点をあてる。 我々は、定理に直接関係する補題がテスト時の定理証明者に与えられないより自然な設定で作業する。 我々は、モデルが定理を補題に分解し、補題を証明し、補題を用いて定理を証明することを奨励するRLベースの訓練アルゴリズムを設計する。
  論文  参考訳（メタデータ） (2024-11-04T05:57:40Z)
• 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)

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

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