論文の概要: Efficient Test-Time Optimization for Multi-Agent Proof Autoformalization
- arxiv url: http://arxiv.org/abs/2607.11307v1
- Date: Mon, 13 Jul 2026 09:21:15 GMT
- ステータス: 翻訳完了
- システム内更新日: 2026-07-14 17:47:21.415942
- Title: Efficient Test-Time Optimization for Multi-Agent Proof Autoformalization
- Title（参考訳）: マルチエージェントオートフォーマライゼーションのための効率的なテスト時間最適化
- Abstract要約: ToMapは、Decomposer-Formalizer-Proverパイプラインとして自動形式化の証明を構築するフレームワークである。
ToMapは,構文的正当性と意味的忠実性の両方で評価すると,最善前の手法よりも19.0%向上することを示す。
- 参考スコア（独自算出の注目度）: 20.22828310618122
- License: http://creativecommons.org/licenses/by/4.0/
- Abstract: Full-proof autoformalization bridges extensive mathematical proofs in natural language with formally validated reasoning, offering a pathway to elevate the ceiling of verifiable mathematical reasoning. Unlike statement-level formalization, proof autoformalization is a long-horizon challenge requiring coordination of claims, contexts, and dependencies across many proof steps, yet has only recently come under focused study. Current approaches either rely on costly model training or apply excessive, unguided repair at inference time. To this end, we introduce ToMap, a multi-agent framework that structures proof autoformalization as a Decomposer-Formalizer-Prover pipeline with efficient test-time optimization guided by formal verification and semantic rubrics for proof quality. Rather than distributing test-time compute across all agents, we perform bottleneck analysis and identify the Decomposer as the critical bottleneck: the quality of its atomic, self-contained proof units directly determines whether downstream agents can successfully formalize and prove each step. ToMap therefore treats the Formalizer and Prover as downstream executors and efficiently focuses test-time compute on Decomposer refinement. This refinement follows a loop inspired by GEPA, evolving prompts over candidate decompositions and using formal verification progress together with semantic proof rubrics to define a Pareto frontier that guides the next decomposition update. Experiments on ProofFlowBench show that ToMap improves over the best previous method by 19.0% when evaluated by both syntactic correctness and semantic faithfulness, while requiring lower test-time cost. Scaling analysis shows that most gains emerge within a few iterations of decomposition evolution, guiding test-time budget selection.
- Abstract（参考訳）: 完全な自己形式化は、公式に検証された推論を持つ自然言語の広範な数学的証明を橋渡しし、検証可能な数学的推論の天井を高くする経路を提供する。
ステートメントレベルの形式化とは異なり、証明オートフォーマル化は主張、文脈、依存関係の調整を必要とする長期的課題である。
現在のアプローチは、コストのかかるモデルトレーニングに依存するか、あるいは推論時に過度にガイドなしの修復を適用するかのどちらかです。
そこで本研究では,自動形式化の証明をデコンポサフォーマライザ・プロバーパイプラインとして構築するマルチエージェントフレームワークToMapを紹介する。
全てのエージェントにテスト時間計算を分散するのではなく、ボトルネック解析を行い、Decomposerを重要なボトルネックとして識別する。
そこでToMapは、FormalizerとProverを下流のエグゼキュータとして扱い、Decomposerの改良にテストタイムの計算を効率よくフォーカスする。
この改良は、GEPAにインスパイアされたループに従って、候補の分解を先導し、セマンティックな証明ルーブリックと共に形式的な検証の進歩を使用して、次の分解アップデートを導くパレートフロンティアを定義する。
ProofFlowBenchの実験では、ToMapは、テスト時間コストを低くしながら、構文的正確性と意味的忠実性の両方で評価すると、最良前のメソッドよりも19.0%改善している。
スケール分析によると、ほとんどの利得は、数回の分解進化のイテレーションで発生し、テストタイムの予算選択を導く。
関連論文リスト
- From Verdict to Process: Agentic Reinforcement Learning for Multi-Stage Fact Verification [4.539896456749749]
本稿では,多段階事実検証トラジェクトリのエンドツーエンド最適化のためのエージェント強化学習フレームワークProFactを提案する。
ProFactは、クレームの分解、証拠探索、回答生成、検証予測を協調する統一的なポリシーを訓練する。
実証評価の結果,ProFactは検証性能と推論効率の両方において,高いベースラインを一貫して上回っていることがわかった。
論文 参考訳（メタデータ） (2026-06-11T12:17:18Z) - Learning to Generate Formally Verifiable Step-by-Step Logic Reasoning via Structured Formal Intermediaries [18.744562922743405]
PRoSFI(Process Reward over Structured Formal Intermediates)は、精度を損なうことなく推論信頼性を高める新しい報奨法である。
完全に検証された推論チェーンのみが高い報酬を受け取る。
形式的検証の統合は、ステップバイステップのマシンチェック可能な証明を生成するためのモデルを導く。
論文 参考訳（メタデータ） (2026-03-31T09:42:13Z) - Compile to Compress: Boosting Formal Theorem Provers by Compiler Outputs [48.390500145598544]
大型言語モデル (LLM) は形式定理の証明において大きな可能性を証明している。
我々は形式的検証において情報的構造を利用する: コンパイラが多様な証明の試みの広大な空間をマッピングする観察である。
我々は,この圧縮を利用して効率的な学習と証明探索を行う,学習と再定義のためのフレームワークを提案する。
論文 参考訳（メタデータ） (2026-03-13T01:33:20Z) - Decompose-and-Formalise: Recursively Verifiable Natural Language Inference [34.505373718498014]
ニューロシンボリックパイプラインにおける定理プロバー(TP)を持つ大言語モデル(LLM)は、自然言語推論(NLI)の検証と証明誘導による説明の洗練に役立つ
本稿では,前提と仮説のペアを包含木に分解する分解・形式化フレームワークを提案する。
また、一貫性のある引数-ロールバインディングを強制するために、イベントベースの論理形式に$-substitutionを導入します。
論文 参考訳（メタデータ） (2026-01-27T13:43:30Z) - BRIDGE: Building Representations In Domain Guided Program Verification [67.36686119518441]
BRIDGEは、検証をコード、仕様、証明の3つの相互接続ドメインに分解する。
提案手法は, 標準誤差フィードバック法よりも精度と効率を著しく向上することを示す。
論文 参考訳（メタデータ） (2025-11-26T06:39:19Z) - Provable Benefit of Curriculum in Transformer Tree-Reasoning Post-Training [76.12556589212666]
学習後のカリキュラムは指数関数的複雑性のボトルネックを回避していることを示す。
結果のみの報酬信号の下では、強化学習の微調整は、サンプルの複雑さを高い精度で達成する。
カリキュラムを意識したクエリにより、報奨託書の呼び出しとサンプリングコストの両方を指数関数的に削減するテストタイムスケーリングの保証を確立する。
論文 参考訳（メタデータ） (2025-11-10T18:29:54Z) - ReForm: Reflective Autoformalization with Prospective Bounded Sequence Optimization [73.0780809974414]
本稿では,意味的整合性評価を自己形式化プロセスに統合する反射的自己形式化手法を提案する。
これにより、モデルが形式的なステートメントを反復的に生成し、セマンティックな忠実さを評価し、自己修正された特定エラーを発生させることができる。
実験の結果、ReFormは最強のベースラインに対して平均22.6ポイントの改善を達成した。
論文 参考訳（メタデータ） (2025-10-28T16:22:54Z) - ProofFlow: A Dependency Graph Approach to Faithful Proof Autoformalization [10.021930888250546]
現在のアプローチでは、オリジナルの人間による議論の意味的意味と論理的構造を保存できない。
本稿では,構造的忠実度を主目的とする新しいパイプラインであるProofFlowを紹介する。
我々は184人の学部レベルの問題に対して,ステップバイステップのソリューションを手動でアノテートした新しいベンチマークを提示する。
また,構文的正しさ,意味的忠実度,構造的忠実度を評価するための新しい合成指標ProofScoreを導入する。
論文 参考訳（メタデータ） (2025-10-13T10:20:11Z) - Autoformalizer with Tool Feedback [52.334957386319864]
自動形式化は、数学的問題を自然言語から形式的ステートメントに変換することによって、ATP(Automated Theorem Proving)のデータ不足に対処する。
既存のフォーミュラライザは、構文的妥当性とセマンティック一貫性を満たす有効なステートメントを一貫して生成することに苦慮している。
本稿では,ツールフィードバックを用いたオートフォーマライザ (ATF) を提案する。
論文 参考訳（メタデータ） (2025-10-08T10:25:12Z) - Alchemy: Amplifying Theorem-Proving Capability through Symbolic Mutation [71.32761934724867]
この研究は、記号的突然変異を通じて形式的な定理を構成するデータ合成のフレームワークであるAlchemyを提案する。
マドリブにおける各候補定理について、書き直しや適用に使用できるすべてのイベーシブルな定理を同定する。
その結果、マドリブの定理の数は110kから6Mへと桁違いに増加する。
論文 参考訳（メタデータ） (2024-10-21T08:04:21Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。