論文の概要: Proof-Refactor: Refactoring Generated Formal Proofs into Modular Artifacts

• arxiv url: http://arxiv.org/abs/2606.03743v1
• Date: Tue, 02 Jun 2026 14:56:10 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-06-03 22:00:05.091477
• Title: Proof-Refactor: Refactoring Generated Formal Proofs into Modular Artifacts
• Title（参考訳）: Proof-Refactoring Refactoring Generated Formal Proofs into Modular Artifacts
• Authors: Yiming Fu, Peixuan Liu, Zichen Wang, Kun yuan,
• Abstract要約: このギャップは,ほとんどのエビデンス生成パイプラインにおいて,コンパイル優先の目的が暗黙的であることに起因している,と我々は主張する。 本稿では,人間の証明リファクタリングに触発されたプロセス誘導アプローチを提案する。
• 参考スコア（独自算出の注目度）: 19.455779459310982
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: While Large Language Models (LLMs) have shown strong performance in generating formal proofs, their outputs often remain less readable, modular, maintainable, and reusable than proofs in mature formal mathematics libraries. We argue that this gap stems in part from the compile-first objective implicit in most proof-generation pipelines, which encourages monolithic or ad hoc proof scripts rather than library-quality artifacts. Existing approaches to proof-quality improvement often rely on explicit, computable optimization objectives. In practice, however, the most tractable and experimentally validated objectives are largely length-based, while higher-level qualities such as readability, modularity, maintainability, and reusability are difficult to reduce to reliable automatic metrics. Instead of optimizing proof improvement against a single proxy metric, we take a process-guided approach inspired by human proof-refactoring workflows. We propose an agentic framework $\textbf{Proof-Refactor}$ that decomposes proof refactoring into four phases: extracting candidate proof fragments, designing helper declarations, formally proving the extracted and designed components, and repairing the original proof using the verified components. On generated Lean proofs from PutnamBench and Putnam2025, Proof-Refactor improves rubric-based refactoring scores over a strong Claude Code refactoring baseline, with the largest gains in signature quality and human readability. These results suggest that process-guided refactoring can improve proof structure without treating proof length as the primary objective.
• Abstract（参考訳）: LLM(Large Language Models)は形式的証明の生成において高い性能を示しているが、その出力は成熟した形式的数学ライブラリの証明よりも可読性、モジュール性、保守性、再利用性が低い。 このギャップは,ライブラリ品質のアーティファクトではなく,モノリシックあるいはアドホックな証明スクリプトを推奨する,ほとんどの実証生成パイプラインにおいて,コンパイルファーストの目標が暗黙的に存在することから生じるものだ,と我々は主張する。 証明品質の改善への既存のアプローチは、しばしば明示的で計算可能な最適化目標に依存している。 しかし実際には、最もトラクタブルで実験的に検証された目的は主に長さに基づくものであり、可読性、モジュール性、保守性、再利用性といった高レベルな品質は、信頼性の高い自動メトリクスに還元することが困難である。 ひとつのプロキシメトリックに対して証明の改善を最適化する代わりに、人間の証明リファクタリングワークフローにインスパイアされたプロセス指向のアプローチを採用します。 提案するエージェントフレームワーク $\textbf{Proof-Refactor}$ は,検証のリファクタリングを4つのフェーズに分解する。 PutnamBench氏とPatnam2025氏が生成したリーンの証明について、Proof-Refactorは、強力なClaude Codeリファクタリングベースラインよりもルックスベースのリファクタリングスコアを改善し、署名品質と人間の可読性において最大の成果を上げている。 これらの結果から, プロセス誘導リファクタリングは, 証明長を主目的として扱うことなく, 証明構造を改善できることが示唆された。

関連論文リスト

• PROMISE: Proof Automation as Structural Imitation of Human Reasoning [15.113069562646302]
  ProMISEは,証明状態遷移に対するステートフルな探索として,証明生成を再構成する構造認識フレームワークである。 複数のLLMバックエンドにまたがるSEL4ベンチマークのPROMISEを評価し,SeleneやRangoといった先行システムと比較した。
  論文  参考訳（メタデータ） (2026-04-07T03:49:12Z)
• ExVerus: Verus Proof Repair via Counterexample Reasoning [8.819482630789217]
  大規模言語モデル(LLM)のための逆例誘導フレームワークであるEXVERUSを提案する。 証明が失敗すると、EXVERUSは反例を自動生成して検証し、LSMを誘導して誘導不変量に一般化し、これらの障害を阻止する。 評価の結果,EXVERUSは最先端のプロンプトベースのVerus証明生成器よりも証明精度,堅牢性,トークン効率を著しく向上することがわかった。
  論文  参考訳（メタデータ） (2026-03-26T18:14:34Z)
• Compile to Compress: Boosting Formal Theorem Provers by Compiler Outputs [48.390500145598544]
  大型言語モデル (LLM) は形式定理の証明において大きな可能性を証明している。 我々は形式的検証において情報的構造を利用する: コンパイラが多様な証明の試みの広大な空間をマッピングする観察である。 我々は,この圧縮を利用して効率的な学習と証明探索を行う,学習と再定義のためのフレームワークを提案する。
  論文  参考訳（メタデータ） (2026-03-13T01:33:20Z)
• Proof-RM: A Scalable and Generalizable Reward Model for Math Proof [67.53066972145183]
  大規模言語モデル(LLM)は,*検証リワード*(RLVR)を用いた強化学習を通じて,強力な数学推論能力を示した。 多くの先進的な数学的問題は証明ベースであり、単純な解マッチングによって証明の真性を決定するための保証された方法はない。 自動検証を実現するには、完全な証明プロセスを確実に評価できるリワードモデル(RM)が必要である。
  論文  参考訳（メタデータ） (2026-02-02T17:42:53Z)
• BRIDGE: Building Representations In Domain Guided Program Verification [67.36686119518441]
  BRIDGEは、検証をコード、仕様、証明の3つの相互接続ドメインに分解する。 提案手法は, 標準誤差フィードバック法よりも精度と効率を著しく向上することを示す。
  論文  参考訳（メタデータ） (2025-11-26T06:39:19Z)
• ImProver: Agent-Based Automated Proof Optimization [18.315243539816464]
  リーンの任意のユーザ定義メトリクスを最適化するために、証明を書き換える大規模な言語モデルエージェントであるImProverを紹介します。 我々は、現実世界の学部生、競争、研究レベルの数学定理の書き換えについてImProverをテストする。
  論文  参考訳（メタデータ） (2024-10-07T05:14:18Z)
• Lean-STaR: Learning to Interleave Thinking and Proving [53.923617816215774]
  証明の各ステップに先立って,非公式な思考を生成するために,言語モデルをトレーニングするフレームワークであるLean-STaRを紹介します。 Lean-STaRは、Lean定理証明環境内のminiF2F-testベンチマークで最先端の結果を達成する。
  論文  参考訳（メタデータ） (2024-07-14T01:43:07Z)

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

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