論文の概要: Formal Model Construction Guided by Model-Based Proof Sketches
- arxiv url: http://arxiv.org/abs/2609.29870v1
- Date: Thu, 24 Sep 2026 14:26:46 GMT
- ステータス: 翻訳完了
- システム内更新日: 2026-09-25 21:10:10.004196
- Title: Formal Model Construction Guided by Model-Based Proof Sketches
- Title（参考訳）: モデルベースプロフスケッチによる形式モデル構築
- Abstract要約: 本稿では,プロフスケッチ型形式モデル合成法を提案する。
モデルに基づく証明スケッチを中心にした自動形式化手法である。
ProGSは、構文的妥当性、推論的妥当性、行動的正当性において、最先端のエージェント形式モデリングアプローチよりも改善されている。
- 参考スコア（独自算出の注目度）: 9.855306583270414
- License: http://creativecommons.org/licenses/by/4.0/
- Abstract: Formal modeling provides strong guarantees about system correctness, but developing and repairing formal models remains labor-intensive and requires substantial expertise in logic and formal reasoning. Recent LLM-based autoformalization agents seek to reduce this burden by generating candidate formal models and revising them using feedback from formal tools. However, the existing approaches follow a generate-and-repair paradigm, in which repairs are driven by verification failures of the generated model and therefore depend heavily on both the granularity of the feedback and the LLM's repair capability. As a consequence, a repair targeting one level of verification may invalidate properties at another level, which requires reasoning over the complete set of event guards. To address these limitations, we propose Proof-Sketch-Guided Formal Model Synthesis (ProGS), an autoformalization method centered on model-based proof sketches. A model-based proof sketch represents the proof structure of the target formal system as a tree. Internal nodes capture case splits and inductive reasoning steps, while leaf nodes correspond to concrete state-transition events that realize individual subgoals. ProGS uses LLMs to generate and repair these sketches, with verification failures mapped back to specific nodes and subtrees to provide structured guidance for iterative repair. Our evaluation on a benchmark of 27 formal systems shows that ProGS improves over state-of-the-art agentic formal modeling approaches in syntactic validity, deductive verifiability, and behavioral correctness, demonstrating the benefit of organizing formal model construction around hierarchical proof sketches.
- Abstract（参考訳）: 形式的モデリングはシステム正当性について強い保証を提供するが、形式的モデルの開発と修復は労働集約的であり、論理学と形式的推論においてかなりの専門知識を必要とする。
近年のLSMベースの自動形式化エージェントは、候補となる形式モデルを生成し、形式ツールからのフィードバックを用いて修正することで、この負担を軽減しようとしている。
しかし、既存のアプローチは、生成モデルの検証失敗によって修復が駆動されるジェネレーション・アンド・リペアのパラダイムに従うため、フィードバックの粒度とLLMの修理能力の両方に大きく依存する。
結果として、あるレベルの認証を対象とする修復は、他のレベルでプロパティを無効にし、イベントガードの完全なセットを推論する必要がある。
これらの制約に対処するために,モデルに基づく証明スケッチを中心にした自動形式化手法ProGS(Proof-Sketch-Guided Formal Model Synthesis)を提案する。
モデルに基づく証明スケッチは、対象の形式システムの証明構造を木として表現する。
内部ノードはケース分割と帰納的推論ステップをキャプチャし、一方リーフノードは個々のサブゴールを実現する具体的な状態遷移イベントに対応する。
ProGSはLSMを使用してこれらのスケッチを生成し、修復し、検証の失敗を特定のノードやサブツリーにマップして、反復的な修正のための構造化されたガイダンスを提供する。
本稿では,27の形式体系のベンチマークから,構文的妥当性,帰納的妥当性,行動的正当性といった,最先端のエージェント型モデルアプローチよりも優れた手法が提案され,階層的証明スケッチを中心に形式的モデル構築を組織化することのメリットが示された。
関連論文リスト
- Gatekeepers and Hallucinations: A Layered Evaluation Framework for LLM-Driven Quantum Circuit Generation [0.0]
材料インフォームド変分量子固有解器(VQE)回路生成のための階層評価フレームワークを提案する。
5つの異なるLCM障害モード(幾何学幻覚、存在しないAPI使用、統合障害、制約違反、検証不可能な出力)を分類する。
評価プラットフォーム自身のソースコードの法医学的な監査により、サイレントフォールバック・テンプレート置換によって、ハーネスに2つの明らかなモデル障害が生じたことが確認された。
論文 参考訳（メタデータ） (2026-06-16T19:17:54Z) - Event-B Agent: Towards LLM Agent for Formal Model Synthesis and Repair [13.777416057673761]
Event-B Agentは、ソフトウェア設計のインターリーブな性質にインスパイアされた、新しいフレームワークである。
Event-B Agentは、エンド・ツー・エンドの形式モデル合成と修復において、ベースラインを大幅に上回ることを示す。
以上の結果から,Event-B Agent は形式的モデル合成と修復の修正に向けた有望なステップであることが示唆された。
論文 参考訳（メタデータ） (2026-05-17T14:23:45Z) - CellScientist: Dual-Space Hierarchical Orchestration for Closed-Loop Refinement of Virtual Cell Models [62.281480231694]
VCM(Virtual Cell Modeling)は、摂動応答を予測できるだけでなく、予測が失敗した場合にターゲットリビジョンをサポートするモデルを必要とする。
現在のLCM支援モデリングでは、予測誤差が実行可能実装を通して観測されるという改善ルーティング問題に直面している。
提案するCellScientistは,高レベル仮説空間と低レベル実行可能実装空間を結合した,二重空間階層型フレームワークである。
論文 参考訳（メタデータ） (2026-05-08T06:40:24Z) - 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) - X-RAY: Mapping LLM Reasoning Capability via Formalized and Calibrated Probes [11.988348978958376]
大規模言語モデル(LLM)は有望な性能を達成するが、その推論能力はいまだによく分かっていない。
我々は、校正された正式に検証されたプローブを用いてLCM推論能力をマッピングする説明可能な推論分析システムであるX線について述べる。
数学,物理学,化学の分野において,中等レベルから高度な問題に対する現状のLSMの評価を行った。
論文 参考訳（メタデータ） (2026-03-05T15:34:22Z) - ReForm: Reflective Autoformalization with Prospective Bounded Sequence Optimization [73.0780809974414]
本稿では,意味的整合性評価を自己形式化プロセスに統合する反射的自己形式化手法を提案する。
これにより、モデルが形式的なステートメントを反復的に生成し、セマンティックな忠実さを評価し、自己修正された特定エラーを発生させることができる。
実験の結果、ReFormは最強のベースラインに対して平均22.6ポイントの改善を達成した。
論文 参考訳（メタデータ） (2025-10-28T16:22:54Z) - Autoformalizer with Tool Feedback [52.334957386319864]
自動形式化は、数学的問題を自然言語から形式的ステートメントに変換することによって、ATP(Automated Theorem Proving)のデータ不足に対処する。
既存のフォーミュラライザは、構文的妥当性とセマンティック一貫性を満たす有効なステートメントを一貫して生成することに苦慮している。
本稿では,ツールフィードバックを用いたオートフォーマライザ (ATF) を提案する。
論文 参考訳（メタデータ） (2025-10-08T10:25:12Z) - PAT-Agent: Autoformalization for Model Checking [17.082027022913998]
PAT-Agentは自然言語の自動形式化と形式モデル修復のためのエンドツーエンドフレームワークである。
これは、大きな言語モデルの生成能力と形式的検証の厳密さを組み合わせたものである。
論文 参考訳（メタデータ） (2025-09-28T06:32:14Z) - Lean-STaR: Learning to Interleave Thinking and Proving [53.923617816215774]
証明の各ステップに先立って,非公式な思考を生成するために,言語モデルをトレーニングするフレームワークであるLean-STaRを紹介します。
Lean-STaRは、Lean定理証明環境内のminiF2F-testベンチマークで最先端の結果を達成する。
論文 参考訳（メタデータ） (2024-07-14T01:43:07Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。