論文の概要: PROMISE: Proof Automation as Structural Imitation of Human Reasoning
- arxiv url: http://arxiv.org/abs/2604.05399v2
- Date: Thu, 09 Apr 2026 00:24:10 GMT
- ステータス: 翻訳完了
- システム内更新日: 2026-04-10 14:10:47.876791
- Title: PROMISE: Proof Automation as Structural Imitation of Human Reasoning
- Title（参考訳）: PROMISE:人間推論の構造的模倣としての証明自動化
- Authors: Youngjoo Ahn, Sangyeop Yeo, Gijung Im, Jongmin Lee, Jinyoung Yeo, Jieung Kim,
- Abstract要約: ProMISEは,証明状態遷移に対するステートフルな探索として,証明生成を再構成する構造認識フレームワークである。
複数のLLMバックエンドにまたがるSEL4ベンチマークのPROMISEを評価し,SeleneやRangoといった先行システムと比較した。
- 参考スコア（独自算出の注目度）: 15.113069562646302
- License: http://creativecommons.org/licenses/by/4.0/
- Abstract: Automated proof generation for formal software verification remains largely unresolved despite advances in large language models (LLMs). While LLMs perform well in NLP, vision, and code generation, formal verification still requires substantial human effort. Interactive theorem proving (ITP) demands manual proof construction under strict logical constraints, limiting scalability; for example, verifying the seL4 microkernel required decades of effort. Existing LLM-based approaches attempt to automate this process but remain limited. Most rely on single-shot generation or shallow retrieval, which may work for small proofs but fail to scale to large, interdependent verification tasks with deep structural dependencies. We present PROMISE (PROof MIning via Structural Embeddings), a structure-aware framework that reframes proof generation as a stateful search over proof-state transitions. Instead of surface-level retrieval, PROMISE mines structural patterns from proof states and tactic transitions, enabling retrieval and adaptation of compatible proof fragments during iterative search. We evaluate PROMISE on the seL4 benchmark across multiple LLM backends and compare it with prior systems such as Selene and Rango. PROMISE consistently outperforms prior methods, achieving up to +26 point improvements (186% relative gain) while maintaining robustness across models, demonstrating the effectiveness of structure-aware proof mining for scalable theorem proving.
- Abstract（参考訳）: 大規模言語モデル(LLM)の進歩にもかかわらず、形式的ソフトウェア検証のための自動証明生成はほとんど未解決のままである。
LLMはNLP、ビジョン、コード生成でよく機能するが、正式な検証には相当な人的努力が必要である。
対話的定理証明(ITP)では、厳密な論理的制約の下で手動による証明を要求され、スケーラビリティが制限される。
既存のLLMベースのアプローチは、このプロセスを自動化しようとするが、制限されている。
多くの場合、シングルショット生成や浅い検索に依存しており、小さな証明のためには機能するが、深い構造的依存関係を持つ大規模で相互依存の検証タスクにはスケールできない。
ProMISE(PROof MIning via Structure Embeddings)は,証明状態遷移に対するステートフルな探索として,証明生成を再構成する構造認識フレームワークである。
表面レベルの検索の代わりに、ProMISEは証明状態と戦術遷移から構造パターンを抽出し、反復探索中に互換性のある証明フラグメントの検索と適応を可能にする。
複数のLLMバックエンドにまたがるSEL4ベンチマークのPROMISEを評価し,SeleneやRangoといった先行システムと比較した。
PROMISE は従来の手法を一貫して上回り、モデル間の堅牢性を維持しつつ、+26点の改善(相対利得)を達成し、スケーラブルな定理証明のための構造対応の証明マイニングの有効性を実証した。
関連論文リスト
- Stepwise: Neuro-Symbolic Proof Search for Automated Systems Verification [21.423111823947867]
本稿では,システムレベルの検証プロジェクトの証明検索の自動化を目的とした,ニューロシンボリックな証明生成フレームワークを提案する。
このフレームワークは、証明状態に対して最優先のツリー探索を行い、次の候補証明ステップのためにLLMを何度もクエリする。
さらなるベンチマークの結果は強力な一般化を示し、スケーラブルな自動ソフトウェア検証への道のりを示している。
論文 参考訳（メタデータ） (2026-03-20T07:45:49Z) - Prism: Efficient Test-Time Scaling via Hierarchical Search and Self-Verification for Discrete Diffusion Language Models [96.0074341403456]
LLM推論を改善するための実用的な方法として、推論時計算が再導入されている。
テスト時間スケーリング(TTS)アルゴリズムの多くは、自動回帰デコーディングに依存している。
そこで我々は,dLLM のための効率的な TTS フレームワーク Prism を提案する。
論文 参考訳（メタデータ） (2026-02-02T09:14:51Z) - BRIDGE: Building Representations In Domain Guided Program Verification [67.36686119518441]
BRIDGEは、検証をコード、仕様、証明の3つの相互接続ドメインに分解する。
提案手法は, 標準誤差フィードバック法よりも精度と効率を著しく向上することを示す。
論文 参考訳（メタデータ） (2025-11-26T06:39:19Z) - Dynamic Generation of Multi-LLM Agents Communication Topologies with Graph Diffusion Models [99.85131798240808]
我々はtextitGuided Topology Diffusion (GTD) と呼ばれる新しい生成フレームワークを導入する。
条件付き離散グラフ拡散モデルにインスパイアされたGTD式は、反復的な構成過程としてトポロジー合成を行う。
各ステップで生成は、多目的報酬を予測する軽量プロキシモデルによって制御される。
実験により、GTDは高いタスク適応性、スパース、効率的な通信トポロジを生成できることが示されている。
論文 参考訳（メタデータ） (2025-10-09T05:28:28Z) - MPS-Prover: Advancing Stepwise Theorem Proving by Multi-Perspective Search and Data Curation [48.22540519786074]
本稿では,制限を克服する新しいATPシステムであるMPS-Proverを紹介する。
MPS-Proverには、パフォーマンスを犠牲にすることなく、冗長なトレーニングデータの約40%を産み出す、非常に効果的なポストトレーニングデータキュレーション戦略と、多目的のツリーサーチメカニズムの2つの重要なイノベーションが含まれている。
大規模な評価では、MPS-Proverは、miniF2FやProofNetなど、複数の挑戦的なベンチマークで最先端のパフォーマンスを達成している。
論文 参考訳（メタデータ） (2025-05-16T07:56:03Z) - 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) - APE-Bench I: Towards File-level Automated Proof Engineering of Formal Math Libraries [5.227446378450704]
APE-Bench Iは、Mathlib4の実際のコミット履歴から構築された最初の現実的なベンチマークである。
Eleansticはスケーラブルな並列検証インフラストラクチャで、Mathlibの複数バージョンにわたる検証に最適化されている。
論文 参考訳（メタデータ） (2025-04-27T05:04:02Z) - ProofAug: Efficient Neural Theorem Proving via Fine-grained Proof Structure Analysis [50.020850767257095]
本稿では,LLMに様々な粒度で自動化手法を付加するProofAugを提案する。
本手法は,オープンソースのDeep-math-7bベースモデルとIsabelle証明アシスタントを用いて,MiniF2Fベンチマークで検証した。
また、ProofAugのLean 4バージョンを実装し、Kimina-Prover-seek-Distill-1.5Bのパス@1のパフォーマンスを44.3%から50.4%に改善します。
論文 参考訳（メタデータ） (2025-01-30T12:37:06Z) - Reference Trustable Decoding: A Training-Free Augmentation Paradigm for Large Language Models [79.41139393080736]
大規模言語モデル(LLM)は急速に進歩し、印象的な機能を示している。
In-Context Learning (ICL) など。
効率的なファインチューニング(PEFT)は、現在2つの主要な拡張方法である。
下流タスクへのLLM。
我々は、モデルが微調整なしで新しいタスクに迅速に適応できるパラダイムである参照信頼復号(RTD)を提案する。
論文 参考訳（メタデータ） (2024-09-30T10:48:20Z) - Proof Automation with Large Language Models [6.587933406842906]
大規模言語モデル(LLM)は、自然言語で非公式な証明を自動的に生成する可能性を示している。
本稿では,まず LLM に初期証明を生成することを促し,次に目標とする記号法を利用して低レベルの問題を反復的に修復する,新しい生成・修復手法である PALM を提案する。
その結果、PALMは他の最先端の手法よりも大幅に優れており、76.6%から180.4%の定理を証明できた。
論文 参考訳（メタデータ） (2024-09-22T00:19:27Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。