論文の概要: Mechanic: Sorrifier-Driven Formal Decomposition Workflow for Automated Theorem Proving

• arxiv url: http://arxiv.org/abs/2603.24465v1
• Date: Wed, 25 Mar 2026 16:12:08 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-03-26 21:06:11.37794
• Title: Mechanic: Sorrifier-Driven Formal Decomposition Workflow for Automated Theorem Proving
• Title（参考訳）: メカニック:Sorrifier-Driven Formal Decomposition Workflow for Automated Theorem Proving
• Authors: Ruichen Qiu, Yichuan Cao, Junqi Liu, Dakai Guo, Xiao-Shan Gao, Lihong Zhi, Ruyong Feng,
• Abstract要約: メカニック(Mechanic)は、謝罪駆動の形式的分解戦略を採用した新しいエージェントシステムである。 未解決のサブゴールを正確に分離するために、リーンの残念なプレースホルダーを活用することで、Mechanicは失敗するサブプロブレムを、クリーンで自己完結したコンテキストに抽出し、独立して解決する。
• 参考スコア（独自算出の注目度）: 13.446180044466324
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Recent advances in large language models (LLMs) and LLM-based agents have substantially improved the capabilities of automated theorem proving. However, for problems requiring complex mathematical reasoning, current systems rarely succeed on the first try and must repeatedly modify their proof strategies. Existing approaches for handling failed attempts typically either discard the entire proof and regenerate it from scratch or iteratively fix errors within the proof. The former is inefficient, as it may abandon mostly correct reasoning due to localized errors, while the latter, although preserving prior progress, leads to progressively longer contexts which progressively degrades the model's ability to attend to the remaining unresolved subproblems. To address this dilemma, we propose Mechanic, a novel agent system that employs a sorry-driven formal decomposition strategy. By leveraging the sorry placeholder in Lean to precisely isolate unresolved subgoals while preserving the surrounding verified proof structure, Mechanic extracts each failed subproblem into a clean, self-contained context and resolves it independently. This avoids both the waste of full regeneration and the excessive context length induced by repeated repairs. Experimental results on challenging mathematical competition benchmarks, including IMO 2025 and Putnam 2025, demonstrate that our agent achieves significant advantages in proving efficiency.
• Abstract（参考訳）: 大規模言語モデル(LLM)とLLMベースのエージェントの最近の進歩は、自動定理証明の能力を大幅に改善している。 しかし、複雑な数学的推論を必要とする問題に対して、現在のシステムは最初の試みで成功することはめったになく、証明戦略を何度も修正しなければならない。 失敗した試みに対処するための既存のアプローチは、典型的には証明全体を破棄し、それをスクラッチから再生するか、または証明内のエラーを反復的に修正する。 前者は局所的な誤りのためにほとんど正しい推論を放棄するが、後者は事前の進歩を保っているが、徐々に長い文脈をもたらし、残りの未解決のサブプロブレムへのモデルの適用能力は徐々に低下する。 このジレンマに対処するために,謝罪駆動型形式分解戦略を用いた新しいエージェントシステムであるMechanicを提案する。 リーンの気の毒なプレースホルダーを利用して、解決されていないサブゴールを正確に分離し、周囲の証明された構造を保存することで、Mechanicは失敗したサブプロブレムをクリーンで自己完結したコンテキストに抽出し、独立して解決する。 これにより、完全再生の無駄と、繰り返しの修復によって引き起こされる過度なコンテキスト長の両方を避けることができる。 IMO 2025 や Putnam 2025 などの数学コンペティションベンチマークによる実験結果から,我々のエージェントが効率を立証する上で大きな優位性を発揮することが示された。

関連論文リスト

• Dynamic analysis enhances issue resolution [53.50448142467294]
  DAIRA(Dynamic Analysis-enhanced Issue Resolution Agent)は、エージェントの推論サイクルに動的解析を組み込む自動修復フレームワークである。 テストトレース駆動の方法論によって駆動されるDAIRAは、軽量モニタを使用して重要なランタイムデータを抽出する。 Gemini 3 Flash Previewを使用すると、DAIRAは新たな最先端(SOTA)パフォーマンスを確立し、SWE-bench Verifiedデータセットで79.4%の解像度を達成する。
  論文  参考訳（メタデータ） (2026-03-23T14:48:54Z)
• Test-Time Scaling with Diffusion Language Models via Reward-Guided Stitching [66.39914384073145]
  本稿では,安価な拡散サンプリング推論をステップレベル候補の再利用プールに変換する自己整合性フレームワークを提案する。 ステップレベルの再結合は、難しい問題に対して最も有益であることがわかった。 トレーニング不要のフレームワークは、6つの数学およびコーディングタスクの平均精度を最大2倍改善します。
  論文  参考訳（メタデータ） (2026-02-26T11:08:39Z)
• Gödel's Poetry [0.0]
  本稿では,Lean4の証明生成に特殊言語モデルを用いるコンピュータ定理証明の新しいアプローチを提案する。 分解せずにMiniF2Fの90.4%のパスレートを達成する。 重要な技術的貢献は、抽象構文木(AST)解析機能を備えたKimina Lean Serverの拡張にあります。
  論文  参考訳（メタデータ） (2025-12-16T10:00:01Z)
• Metacognitive Self-Correction for Multi-Agent System via Prototype-Guided Next-Execution Reconstruction [58.51530390018909]
  大規模言語モデルに基づくマルチエージェントシステムは、協調的な問題解決において優れているが、エラーのカスケードには脆弱である。 我々は,MASにリアルタイム,教師なし,ステップレベルの誤り検出と自己補正を付与するメタ認知フレームワークMASCを提案する。
  論文  参考訳（メタデータ） (2025-10-16T05:35:37Z)
• Towards Solving More Challenging IMO Problems via Decoupled Reasoning and Proving [48.22540519786074]
  最近の研究では、非公式な精度は80%を超え、公式な成功はPutnamBenchのようなベンチマークで8%以下である。 低レベルの証明生成から高レベルの推論を分離する新しいフレームワークを提案する。 提案手法は,2000年以降のIMO問題に対して,従来のオープンソース証明者が未報告の課題として評価した。
  論文  参考訳（メタデータ） (2025-07-07T22:38:49Z)
• 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)
• A Theoretical Analysis of the Repetition Problem in Text Generation [55.8184629429347]
  我々は、繰り返しの問題が、残念ながら、我々の言語自体の特性によって引き起こされていることを示す。 一つの大きな理由は、その後の単語と同じ単語を高い確率で予測する単語が多すぎるという事実に起因する。 高インフロー問題を軽減するための新しい再バランス符号化手法を提案する。
  論文  参考訳（メタデータ） (2020-12-29T08:51:47Z)

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

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