論文の概要: 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:人間推論の構造的模倣としての証明自動化
• 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点の改善(相対利得)を達成し、スケーラブルな定理証明のための構造対応の証明マイニングの有効性を実証した。

関連論文リスト

• Beyond LLM-Based Reasoning: Lightweight GNNs for Agent Failure Attribution [47.70578021328887]
  大規模言語モデル(LLM)ベースのマルチエージェントシステムは、しばしば複雑な障害モードを示す。 AFANetは、ステップレベルの意味信号とエージェントレベルの関係を通して相互作用軌跡をモデル化する軽量なグラフベースのフレームワークである。 以上の結果から, エージェント障害の効果的な帰属は大きな推論を必要とせず, 軽量で構造化されたアプローチで高い性能を達成できることが示唆された。
  論文  参考訳（メタデータ） (2026-08-19T06:16:09Z)
• PROVE-RT: Generating Mechanized Theorem Prover Scripts for Real-Time Systems using LLMs [2.6015820133532137]
  本稿では, PROSA/ROCQ スクリプトを生成する LLM 支援フレームワーク PROVE-RT を紹介する。 我々は,1,191のリアルタイムシステム論文から機械化指向コーパスを構築し,134の非公式スケッチと依存関係情報を含む。 キュレートされた評価セットでは、最先端のLLMの直接的なプロンプトは有効なPROSA機構を確実に生成することができず、PROVE-RTは44.7%の成功率を達成する。
  論文  参考訳（メタデータ） (2026-08-13T03:12:17Z)
• LiveFMBench: Unveiling the Power and Limits of Agentic Workflows in Specification Generation [75.05397479715576]
  大規模言語モデル(LLM)とエージェントは有望な進歩を示しているが、その真の能力と失敗モードは未だ不明である。 CプログラムのためのLCMおよびエージェントベースの形式仕様生成に関する、最初の体系的および汚染に配慮した研究を提案する。
  論文  参考訳（メタデータ） (2026-05-02T11:31:33Z)
• DocSeeker: Structured Visual Reasoning with Evidence Grounding for Long Document Understanding [63.257540233507626]
  本稿では、構造化解析、局所化、推論のワークフローを実行するためにモデルを必要とするパラダイムを提案する。 ショートページトレーニングから超長文書への堅牢な一般化を示し、視覚的検索・拡張生成システムと自然に相乗効果を示す。
  論文  参考訳（メタデータ） (2026-04-14T14:39:26Z)
• Stress-Testing the Reasoning Competence of LLMs With Proofs Under Minimal Formalism [2.215655942741476]
  本稿では,機械チェック可能な証明を通じて推論を評価するベンチマークスイートProofGridを紹介する。 ProofGridには、証明記述、証明チェック、証明マスキング、証明ギャップ埋めを含む15のタスクが含まれている。 タスクは最小の形式表記、特に短いプロンプトに適合するコンパクトな自然言語推論言語であるNDLで表現される。
  論文  参考訳（メタデータ） (2026-04-07T01:19:41Z)
• 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)

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

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