技術概要：Event-B エージェント

問題定義

「構築によって正しさが保証される（correct by construction）」ソフトウェアの開発は、形式手法に依存しており、そこではシステムの動作と要件が数学的に表現され、定理証明とモデル検査を通じて検証されます。しかし、学習曲線の急峻さと数学的専門知識への需要が、これらの手法の広範な普及を妨げてきました。大規模言語モデル（LLM）は自動形式化において有望な成果を示していますが、既存のアプローチは、形式化なしの定理証明や、有界モデル検査のみで検証されたモデル合成など、孤立したタスクに大きく限定されています。

重要なのは、現在の LLM ベースの手法が、形式モデルとその関連する証明の反復的な共進化を支援できていない点です。実際には、形式開発において、定理証明器が証明義務（PO）の discharge に失敗した場合、システムは形式モデルとその証明アーティファクトの両方に対する修正を可能にする必要があります。既存のツールは、固定されたモデルを前提として証明を検索する（LLM 証明支援ツール）か、厳密な証明ベースの検証なしにモデルを構築する（自動形式化）かのいずれかです。モデルと証明の結合状態空間における協調プロセスとして形式開発を定式化し、反復的な洗練と修復を可能にするフレームワークの欠如があります。

手法：Event-B エージェント

これらのギャップに対処するため、著者は、エンドツーエンドの形式モデル合成と修復のための新しい神経記号フレームワークであるEvent-B エージェントを提案します。このフレームワークは、自然言語の要件を受け取り、洗練、合成、修復を統合する反復プロセスを通じて、形式 Event-B モデルを構築するように設計されています。

手法は以下の 3 つの主要段階から構成されます：

1. 洗練戦略の計画

複雑なシステムにおける自動推論は、探索空間の急速な拡大により困難であるという認識に基づき、Event-B エージェントは LLM を用いて洗練戦略を計画します。

• 分解: エージェントは自然言語の要件の集合を互いに排他的な部分集合に分割し、これらを複数の洗練ステップに分散します。
• 結合不変条件（Gluing Invariants）: 各洗練ステップ間の遷移に対して、LLM は抽象変数と具体変数を関連付ける「結合不変条件」を提案します。これにより一貫性が保証されます。
• 検証: これらの不変条件は、モデルチェッカーを用いた反例チェックと証明試行を通じて検証され、承認される前に、以前のステップで証明された性質が保持されていることを保証します。

2. モデル合成

各洗練ステップにおいて、エージェントは割り当てられた要件と結合不変条件に基づいて形式モデルを合成します。

• スキーマガイド生成: LLM 生成に共通する構文エラーを軽減するため、システムは Event-B 文法をエンコードした JSON スキーマを使用します。これにより、構造的な正しさ（必須イベント、変数宣言など）が保証されます。
• 妥当性ループ: 生成されたモデルはコンパイルされます。コンパイルエラー（型不一致、未宣言変数など）は LLM にフィードバックされ、モデルが構文的に有効かつ型が正しいまで反復的に修復されます。

3. モデルおよび証明の修復

これはフレームワークの中核的な貢献であり、モデルと証明の共進化を処理するように設計されています。

• 検証ループ: 合成されたモデルは、まずモデルチェッカー（ProB）によって有界状態内での不変条件違反がチェックされます。反例が見つかった場合、モデルは修復されます。
• 定理証明: 次に、モデルは非有界の定理証明に付されます。証明が失敗した場合、システムは証明状態を分析して問題を診断します。
• 修復ルール推奨: システムは、証明状態を特定の修復ルール（例：「矛盾するゴール」、「存在量化ゴール」、「量化された不変条件の保持」）にマッピングする新しいコンポーネントを採用します。これらのルールは、手動での証明 discharge の経験から経験的に導き出されたものです。
• 原子修復の実行: 「修正戦略決定」を行う LLM が、原子修復関数（例：StrengthenGuard、AddInvariant、InstantiateHypothesis）のライブラリから選択し、それらを実行します。これにより、LLM の修正が健全で検証可能な操作に制限されます。
• 健全性: システムは、モデルの修正後にすべての証明を再生することで健全性を保証します。ターゲットの PO が discharge されるという結合効果が、SMT ソルバーと定理証明器によって検証された場合にのみ、修復は承認されます。

主要な貢献

論文は、以下の 3 つの主要な貢献を概説しています：

1. フレームワーク: Event-B エージェントは、協調的なモデル構築と証明導出による洗練ベースの開発を支援し、「構築によって正しさが保証される」という原則を体現する、初のエンドツーエンド形式モデル合成および修復フレームワークです。
2. ツール: 証明の概念実証ツールであり、Event-B の標準環境である Rodin IDE に統合されています。モデル検査には ProB を、定理証明には標準的な Rodin 証明器を利用しています。
3. 評価: シンプルなものから複雑なものまで 27 の形式システムを対象とした包括的な評価。ベースラインとの比較、アブレーション研究、効率性分析が含まれています。

実験結果

このフレームワークは、システムあたり平均 182.41 の証明義務を持つ 27 の形式システムで評価されました。結果は、ベースライン（LLM + 自動証明器、Cursor、PAT-Agent）に対して大幅な改善を示しています：

• 一貫性（証明義務 discharge 率 - PDR）: Event-B エージェントは**97.86%**の PDR を達成し、ベースライン（89.20% から 95.56%）を大幅に上回りました。すべての複雑さレベルで 97.0% 超の PDR を維持しましたが、ベースラインは複雑さが高まるにつれて変動が大きく、性能が低下しました。
• 正しさ（要件カバレッジ - RC と充足 - RF）:
  • RC: Event-B エージェントは**97.13%**を達成し、2 番目に良い手法を 4.63% 上回りました。
  • RF: Event-B エージェントは**93.79%**を達成し、2 番目に良い手法を 18.01% 上回りました。
  • RF/RC の比率（0.97）は、要件が捕捉されれば、エージェントが関連する証明を正常に discharge することを示しており、ベースラインでは捕捉された要件が証明されずに残ることが多かったのと対照的です。
• 効率性: システムを合成および修復する平均時間は74.45 分でした。単一の PO の discharge を試行する平均時間は0.24 分であり、修復のオーバーヘッドはシステム複雑さとともに爆発するのではなく、PO の数に比例して線形にスケールすることを示唆しています。
• アブレーション研究: 洗練戦略または修復ガイダンスコンポーネントのいずれかを除去すると性能が低下し、これら 2 つのコンポーネントが相互に強化し合っていることが確認されました。洗練は証明の複雑さを軽減し、修復ガイダンスは洗練ステップの正しさを保証します。

意義と主張

著者は、Event-B エージェントが、実用的で健全な LLM 支援形式開発に向けた有望な一歩であると主張しています。形式開発をモデルと証明の結合状態空間として扱うことで、このフレームワークは、孤立した自動形式化または定理証明の限界を克服します。

論文は以下の点を強調しています：

• 洗練は不可欠であり、複雑さを管理し、エージェントが困難な問題を管理可能なステップに分解しながら正しさを保持することを可能にします。
• 証明ガイド修復は必要です。なぜなら、モデル検査（有界）だけでは一般的な正しさを保証できず、定理証明（非有界）が必要ですが、自動推論が失敗した際にモデルと証明の両方を修復するメカニズムが必要だからです。
• 神経記号アプローチは、LLM の意味的な柔軟性と、記号的検証ツールの厳密な健全性を成功裡に組み合わせました。

著者は現在の範囲については謙虚であり、修復ルールのライブラリは経験的に導き出されたものであり網羅的ではないこと、および矛盾する自然言語要件の処理は今後の課題であることを指摘しています。しかし、結果は、提案されたフレームワークが自然言語の要件と「構築によって正しさが保証される」形式モデルの間のギャップを効果的に埋めていることを示唆しています。