論文の概要: Event-B Agent: Towards LLM Agent for Formal Model Synthesis and Repair

• arxiv url: http://arxiv.org/abs/2605.17475v1
• Date: Sun, 17 May 2026 14:23:45 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-05-19 17:57:48.110081
• Title: Event-B Agent: Towards LLM Agent for Formal Model Synthesis and Repair
• Title（参考訳）: Event-B Agent:形式的モデル合成と修復のためのLLM Agentを目指して
• Authors: Hongshu Wang, Xinyue Zuo, Yuhan Sun, Qin Li, Yamine Ait Ameur, Jin Song Dong,
• Abstract要約: Event-B Agentは、ソフトウェア設計のインターリーブな性質にインスパイアされた、新しいフレームワークである。 Event-B Agentは、エンド・ツー・エンドの形式モデル合成と修復において、ベースラインを大幅に上回ることを示す。 以上の結果から,Event-B Agent は形式的モデル合成と修復の修正に向けた有望なステップであることが示唆された。
• 参考スコア（独自算出の注目度）: 13.777416057673761
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Building software that is correct by construction is a long-standing goal in software engineering, as it ensures reliability during design and development rather than after deployment. Formal methods realize this vision by enabling the expression of system behavior and requirements in mathematics, thereby guaranteeing correctness through formal verification, including theorem proving and model checking. However, the steep learning curve and demand for mathematical expertise hinder the widespread adoption of formal methods. Large language models (LLMs) have recently shown promise in bridging this gap through autoformalization. However, existing LLM-based approaches are largely limited to isolated tasks, such as theorem proving without formalization or model synthesis with insufficient verification. While valuable, these efforts do not fully exploit the potential of a more comprehensive framework in which models and proofs evolve together, a process that closely reflects real-world development practice. To address this gap, we propose Event-B Agent, a novel framework inspired by the interleaved nature of software design. Given natural language requirements, Event-B Agent constructs an initial model and iteratively repairs and refines it using formal verification feedback. Refinement simplifies proof discharge, while repair of models and proofs ensures the soundness of each refinement step. Together, these two components reinforce each other to progressively improve the model quality. Evaluation across systems of varying complexity demonstrates that Event-B Agent substantially outperforms baselines in end-to-end formal model synthesis and repair, while maintaining reasonable efficiency. These results suggest that Event-B Agent is a promising step toward correct-by-construction formal model synthesis and repair.
• Abstract（参考訳）: ビルドによって正しいソフトウェアを構築することは、ソフトウェアエンジニアリングにおける長年の目標であり、デプロイ後にではなく、設計と開発の間の信頼性を保証する。 形式的手法は、数学におけるシステム行動と要求の表現を可能にし、定理証明やモデル検査を含む形式的検証を通じて正当性を保証することによって、このビジョンを実現する。 しかし、急勾配の学習曲線と数学的専門知識の需要は、形式的手法の普及を妨げている。 大規模言語モデル(LLM)は、最近、オートフォーマル化によってこのギャップを埋めることを約束している。 しかし、既存の LLM ベースのアプローチは、形式化のない定理証明や不十分な検証を伴うモデル合成のような孤立したタスクに限られている。 価値はあるものの、これらの取り組みは、モデルと証明が共に進化するより包括的なフレームワークの可能性を十分に活用していない。 このギャップに対処するために、ソフトウェア設計のインターリーブな性質に着想を得た新しいフレームワークであるEvent-B Agentを提案する。 自然言語の要求を前提として、Event-B Agentは初期モデルを構築し、形式的な検証フィードバックを使用して反復的に修正し、洗練する。 リファインメントは証明放電を単純化し、モデルと証明の修復は各精製工程の健全性を保証する。 これら2つのコンポーネントは相互に強化され、モデルの品質が徐々に向上する。 複雑さの異なるシステム間での評価は、Event-B Agentが、適切な効率を維持しながら、エンドツーエンドの形式モデル合成と修復において、ベースラインを大幅に上回っていることを示している。 これらの結果から,Event-B Agent は形式的モデル合成と修復の修正に向けた有望なステップであることが示唆された。

関連論文リスト

• 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)
• Understanding by Reconstruction: Reversing the Software Development Process for LLM Pretraining [66.89012795621349]
  大規模言語モデル(LLM)は、複雑なソフトウェア工学に必要な、深く、長期にわたる推論に苦しむことが多い。 本稿では,再構築による理解という,新しいパラダイムを提案する。 マルチエージェントシミュレーションを用いて潜在エージェント軌道を合成するフレームワークを提案する。
  論文  参考訳（メタデータ） (2026-03-11T09:23:20Z)
• Rethinking Scientific Modeling: Toward Physically Consistent and Simulation-Executable Programmatic Generation [8.067859101380389]
  非実行可能または物理的に一貫性のない出力は、厳密な工学的制約の下では依然として一般的である。 物理に一貫性のある自動建築モデリングのための枠組みを提案する。 CivilInstructは、構造工学の知識と制約推論を形式化するドメイン固有のデータセットとして導入された。 MBEvalは、実行可能性と構造的ダイナミクスの一貫性を評価する検証駆動ベンチマークとして提示される。
  論文  参考訳（メタデータ） (2026-02-06T06:57:04Z)
• Veri-Sure: A Contract-Aware Multi-Agent Framework with Temporal Tracing and Formal Verification for Correct RTL Code Generation [4.723302382132762]
  シリコングレードの正しさは、 (i) シミュレーション中心の評価の限られたカバレッジと信頼性、 (ii) 回帰と修復幻覚、 (iii) エージェントハンドオフ間で意図が再解釈される意味的ドリフトによってボトルネックが残っている。 エージェントの意図を整合させる設計契約を確立するマルチエージェントフレームワークであるVeri-Sureを提案する。
  論文  参考訳（メタデータ） (2026-01-27T16:10:23Z)
• 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)
• Step-Aware Policy Optimization for Reasoning in Diffusion Large Language Models [57.42778606399764]
  拡散言語モデル(dLLM)は、テキスト生成に有望で非自己回帰的なパラダイムを提供する。 現在の強化学習アプローチは、しばしばスパースで結果に基づく報酬に頼っている。 これは推論の自然な構造との根本的なミスマッチに由来すると我々は主張する。
  論文  参考訳（メタデータ） (2025-10-02T00:34:15Z)
• PAT-Agent: Autoformalization for Model Checking [17.082027022913998]
  PAT-Agentは自然言語の自動形式化と形式モデル修復のためのエンドツーエンドフレームワークである。 これは、大きな言語モデルの生成能力と形式的検証の厳密さを組み合わせたものである。
  論文  参考訳（メタデータ） (2025-09-28T06:32:14Z)
• Solving Formal Math Problems by Decomposition and Iterative Reflection [30.54275542622631]
  textbfDelta Proverは汎用LLMとLean 4の実証環境とのインタラクションを編成します。 bftextDelta Proverは、miniF2F-testベンチマークで、最先端の95.9%の成功率を達成した。
  論文  参考訳（メタデータ） (2025-07-21T03:56:35Z)

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

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