💻 computer science

The Machine Proposes. The Proof Disposes: Neuro-Symbolic Synthesis of Formally Verified Markov Usage Models from Natural Language Requirements

本論文は、L*学習、文法制約付きLLM、および凸最適化を統合することで、自然言語による要件から形式的に検証可能なマルコフ使用モデルの合成を自動化し、純粋なニューラルベースラインを大幅に上回る高忠実度な故障検出とカバレッジを実現するとともに、安全性が極めて重要なシステムにおける手動モデリングのボトルネックを排除するフレームワークであるNeuro-Symbolic MBSTを導入するものである。

原著者： Nathan Ginting

公開日 2026-07-28

📖 1 分で読めます☕ さくっと読める

CC BY 4.0

原著者： Nathan Ginting

原論文は CC BY 4.0 (https://creativecommons.org/licenses/by/4.0/) でライセンスされています。 ✨ これは以下の論文のAI生成解説です。著者が執筆または承認したものではありません。技術的な正確性については原論文を参照してください。免責事項の全文を読む

ロボットに車の運転やウェブサイトの操作を教えようとしている場面を想像してみてください。これを安全に行うためには、ロボットが取り得るすべての動きのマップ（地図）が必要です。ソフトウェアテストの世界では、このマップは「使用モデル（usage model）」と呼ばれます。それは、システムがどのような状態（例えば「ブレーキ中」や「ショッピングカートが満杯」など）になり得るか、そしてある状態から別の状態へ移動する確率（例えば「ユーザーが『購入』をクリックする確率は80%」など）を示すフローチャートのようなものです。

何十年もの間、専門家たちはこれらのマップを用いて「統計的テスト」を行ってきました。単にコードが一度動作するかどうかを確認するのではなく、マップに基づいて、システム内を数千回のラン・ランダムな旅をシミュレートします。もしマップが正確であれば、テストは、非常に稀でトリッキーな状況でのみ発生する隠れたバグを見つけ出すことができます。しかし、ここには大きな問題があります。これらのマップを手作業で作成するのは、時間がかかり、退屈で、ヒューマンエラーが起きやすいのです。それは、目隠しをしたまま街全体の詳細な地図を描こうとするようなものです。最近、私たちは新しいツールを手に入れました。それは、テキストを読み取ってマップがどうあるべきかを推測できる人工知能（AI）です。しかし、ここには落とし穴があります。AIはマップの「形」を推測することには長けていますが、「数値」を正しく出すことは苦手なのです。AIは存在しない道を勝手に描いたり、「降水確率が150%」といった不可能な数値を提示したりすることがあります。この論文は、次のように問いかけています。「AIの創造性と、厳格な数学的な『ルールブック』を組み合わせることで、自動的に完璧なマップを構築できるだろうか？」

「The Machine Proposes. The Proof Disposes（機械が提案し、証明が処分する）」と題されたこの論文は、NeSy-MBSTと呼ばれる新しいシステムを紹介しています。これは、クリエイティブな作家と厳格な数学教師のチームアップと考えてください。「作家」は大規模言語モデル（LLM）であり、自然言語による要件（例：「ユーザーはカートにアイテムを追加できること」）を読み取り、システムのドラフトマップを提案します。一方、「数学教師」は記号ソルバー（symbolic solver）であり、そのドラフトを数学の法則に照らしてチェックするコンピュータプログラムです。

このチームはどのように連携しているのでしょうか：

提案（The Proposal）: AIが要件を読み取り、状態と遷移のスケッチを作成します。これは高速で、人間の言語をよく理解しています。
証明（The Proof）: 数学教師が即座にそのスケッチをチェックします。AIが物理的に不可能な遷移を捏造していないか？ステップを忘れていないか？教師は「その道は存在しません」とか「曲がり角を飛ばしています」と指摘します。
修正（The Fix）: AIはそのフィードバックを受け取り、マップを修正して、再度試行します。
数値（The Numbers）: マップの形が完璧になったら、数学教師が引き継いで確率を割り当てます。AIに数値を推測させる（これはエラーの原因になります）代わりに、教師は「凸最適化（convex optimizer）」を使用して、確率が正確に合計100%になり、現実の使用状況を反映するように計算します。

研究者たちは、このシステムを2種類の課題、すなわち自動運転車（自律走行車システム）と、2つのeコマースサイト（ユーザー用ショッピングページと管理者用ダッシュボード）でテストしました。彼らは、この新しい「チームアップ」システムを、AI単独での使用、および従来の人の手による手法と比較しました。

結果は素晴らしいものでした。AI単独で使用した場合、システムは重要な経路の約半分を見逃し、マップの構造にエラーが生じました。しかし、このNeSy-MBSTのチームアップを用いることで、システムは、自動運転車のようなクリティカルなシステムに求められる安全基準である0.90という閾値に対し、0.9125というスコアを達成しました。これは、AI単独では不十分であったものの、このチームアップであれば安全テストに合格できることを意味しています。

具体的には、新システムは可能な遷移（システムが辿り得る経路）の85.7%をカバーできましたが、AI単独バージョンでは50%しかカバーできませんでした。これは35.7パーセントポイントの大幅な向上です。平たく言えば、新しいシステムは、AI単独では陥りがちな「行き止まり」や「存在しない道」を幻覚として作り出すことがなかったため、より幅広い潜在的なバグを見つけ出すことができたのです。

また、論文では数値がどれほど正確であったかについても調査しています。AIの確率の推測が実際の数学にどれだけ近いかを測定するために、イェンセン・シャノン・ダイバージェンス（Jensen–Shannon divergence）という指標を用いました。新システムは0.012という、完璧に極めて近いスコアを達成しましたが、AI単独バージョンは0.157と、かなり離れた数値でした。これは、数学教師がAIの誤った計算を正しく修正したことを証明しています。

研究者たちは、どの部分が最も大きな役割を果たしているのかを特定するために、「アブレーション研究（ablation study）」と呼ばれる特別な実験を行いました。その結果、記号検証ループ（マップの構造をチェックする数学教師）が、より多くの経路を見つける主な要因であったことがわかりました。また、凸最適化（確率計算を行う数学教師）が、数値の正確さの主な要因でした。クローズドループのフィードバック（テスト実行から学習する仕組み）も少し貢献してはいますが、核心となる魔法は、初期段階のチームアップにありました。

結論として、この論文は、AIのスピードと人間の専門家の安全性、どちらか一方を選ぶ必要はないことを示唆しています。AIにアイデアを提案させ、厳格な数学的システムにそれを検証・修正させることで、作成が迅速でありながら、クリティカルなシステムにも耐えうる安全なソフトウェアテスト用マップを構築できるのです。著者らは、今回テストしたシステム（最大42の状態）については非常にうまく機能しているものの、巨大で複雑な産業用システムへとスケールアップできるかどうかについては、さらなる研究が必要であると述べています。しかし現時点では、「機械が提案する」ことは素晴らしい出発点であり、最終的なマップが使用される前に「証明がミスを処分する」ことが重要であるということを、彼らは証明しました。

技術要約：形式検証されたマルコフ使用モデルのニューロ・シンボリック合成

1. 問題提起

**モデルベース統計的テスト（MBST）**の普及を妨げている主要なボトルネックは、マルコフ連鎖使用モデルの手動構築にあります。これらのモデルは、テスト目的を絶対的なコードカバレッジから、期待されるフィールド品質に関する統計的推論へと移行させるために不可欠です。しかし、曖昧で非構造化された自然言語の要件を、検証済みの状態遷移トポロジーおよび数学的に一貫した確率行列へと翻訳するには、高度な形式手法の専門知識が必要となります。

大規模言語モデル（LLM）は構文抽出能力を示していますが、MBSTに適用する場合、純粋なニューラルアプローチには以下の4つの決定的な限界が存在します：

確率的揮発性とハルシネーション（幻覚）： LLMは重要なエッジケースを見落としたり、不可能な遷移を構築したり、システムの不変条件を違反したりすることがあり、無効なテストケースを生成する可能性があります。
キャリブレーションの失敗： LLMは精密な数値推論に苦しみ、行の確率和が1となる制約（ $\sum_j p_{ij} = 1$ ）や、有効なマルコフ連鎖に必要な複雑な多変数制約を満たせないことがよくあります。
状態空間の爆発： 有限のコンテキストウィンドウ内で動作するLLMは、構造的な一貫性を失うことなく、高度に並列化されたマルチストリームの遷移モデルを効果的に追跡または生成することができません。
意味的・実現可能性の乖離： LLMは意味的な進行には優れていますが、物理的および論理的な実現可能性の制約（例：空のカート状態でチェックアウトの遷移を実行する）を頻繁に違反し、意味的には論理的であっても物理的には実行不可能なパスを生成します。

既存の文献では、自動化されたモデル構築が、MBSTの欠陥検出保証に必要な構造的および確率的特性を保持できるかどうかについての、エンドツーエンドの評価が欠けています。

2. 手法：NeSy-MBST フレームワーク

本論文では、意味解析と数学的制約解決を分離するハイブリッドフレームワークである Neuro-Symbolic Model-Based Statistical Testing (NeSy-MBST) を導入しています。このアーキテクチャは、密接に結合した5つのステージで構成されています。

A. プログレス・フィジビリティ（進行・実現可能性）二重メモリ・アーキテクチャ

システムはモデル構築を、2つの補完的なメモリシステムに分割します：

Neural Progress Memory（ニューラル進行メモリ）： 微調整されたLLMが自然言語の要件を解析して、意図された振る舞いのトポロジーを捉える意味的フローグラフ（「何を行うか」）をドラフトします。
Symbolic Feasibility Memory（シンボリック実現可能性メモリ）： ルールベースのエンジンが、厳格な論理的不変条件、前提条件、および遷移ガード（「どのように行うか」）を強制し、候補となるすべての遷移を承認前に検証します。

B. LLMオーラクルを用いた $L^*$ による能動的オートマトン学習

フレームワークは、状態空間を発見するために、 $L^*$ 能動的オートマトン学習アルゴリズムの特殊な変形を採用しています。

メンバーシップクエリ： アルゴリズムは、文法制約付きのLLMオーラクル（出力は Yes, No, Unsure に限定）に対して、候補となる入力シーケンスが受理されるかどうかを照会します。
等価クエリ： 現在の仮説オートマトンが実際のシステム（SUT）に対してテストされます。乖離が発生した場合、それは仮説を洗練するための反例として使用されます。
エスカレーション： LLMが「Unsure（不明）」を返した場合、そのクエリは人間の専門家またはSUTのランタイム実行へとエスカレーションされ、学習ループに未検証の情報が組み込まれることを確実に防ぎます。

C. パス依存型階層モデリング

パス依存性による組合せ爆発に対処するため、NeSy-MBSTは2層の階層を使用します：

上位ツリー構造： 頻繁に発生するパス依存シーケンスは、ツリー内に埋め込まれた高次マルコフ連鎖としてモデル化されます。
下位マルコフモデル： 稀なケースや例外パスは、標準的な一次マルコフ連鎖を使用してモデル化されます。

D. 数学的制約最適化

LLMに数値を直接生成させるのではなく、フレームワークはこの作業をシンボリックソルバーにオフロードします：

制約抽出： LLMは要件から比較関係（例： $P(\text{checkout}|\text{cart}) > P(\text{browse}|\text{cart})$ ）を抽出します。
凸計画法： 凸計画エンジン（SLSQP）が、抽出されたすべての制約、行の確率和、およびドメイン固有の境界条件を満たしつつ、不当なバイアスを避けるためにエントロピーを最大化するように、遷移確率行列 $P$ を解きます。

E. クローズドループ・モデル適応

フレームワークは、使用モデルを「生きている成果物」として扱います。ランタイムのテレメトリ（実行ログ、カバレッジ指標、失敗データ）がモデリングエンジンにフィードバックされます。LLMは予測された振る舞いと観察された振る舞いの間の乖離を分析し、シンボリックソルバーは確率を再校正することで、モデルが現実世界の利用パターンへと収束することを保証します。

3. 主な貢献

NeSy-MBST フレームワーク： $L^*$ 能動学習、文法制約付きLLMオーラクル、シンボリックソルバー、およびクローズドループ・フィードバックを組み合わせ、使用モデルの合成を自動化する新しいアーキテクチャ。
LLM出力の形式検証： 構造的違反（到達不能な状態、欠落した自己ループ）を検出し、ターゲットを絞った再プロンプトをトリガーするシンボリック検証ループを導入することで、想起制限のある生成問題を、検証ガイド型の補完問題へと変換しました。
誤差の直交分解： 本論文は、構造的完全性（トポロジー）と確率的キャリブレーション（重み）が、それぞれシンボリックループと凸最適化によって個別に処理される直交する特性であることを確立しています。
実証的検証： 自動運転車（AV）のCPSベンチマークおよび2つのeコマース仕様を用いた包括的な評価を行い、NeSy-MBSTを純粋なニューラル・ベースラインおよび従来の徒手的なアプローチと比較しました。

4. 実験結果

AV CPSベンチマーク（9状態、13遷移）およびeコマースモデル（最大42状態、218遷移）で評価した結果、NeSy-MBSTは以下を達成しました：

抽出精度 (RQ1): システムレベルの F1スコア 0.9125 を達成し、安全クリティカルな閾値である0.90を超えました。これは、最高のGPT-4oベースライン（Hybrid SMF）に対して39.1%の向上、最も強力な単一モデルベースライン（Claude 3.5 Sonnet）に対して14.8%の向上を示しています。
欠陥検出カバレッジ (RQ2): 85.7% の遷移カバレッジを達成し、純粋なニューラル・ベースライン（50%）に対して35.7パーセントポイントの利得を得ました。これは、欠陥を明らかにするパスの多様性が大幅に増加したことを示唆しています。
確率的キャリブレーション (RQ3): イェンセン・シャノン・ダイバージェンス (JSD) 0.012 を達成（純粋なニューラル・ベースラインの0.157と比較）し、凸最適化が運用テスト割り当ての忠実度を保持していることを確認しました。正規化フロベニウス距離は0.0654であり、参照分布との高い構造的類似性を示しています。
効率性： 最大42の状態を持つモデルに対して、フルモデルカバレッジのテストスイートを6分未満で生成しました。
アブレーション研究 (RQ4):
- シンボリックループが、構造的完全性の主要な推進力（遷移F1を0.78から0.96へ向上）であることが特定されました。
- 凸最適化は、構造的指標を変更することなく、確率的キャリブレーションを制御していることが示されました。
- クローズドループ・フィードバックは、分布の忠実度に対して、主に長期的なテストキャンペーンにおいて価値のある、わずかな改善を提供しました。

5. 意義と主張

本論文は、NeSy-MBSTが、安全クリティカルなサイバー物理システム（CPS）に求められる統計的厳密さを損なうことなく、手動モデリングのボトルネックを解消すると主張しています。

ギャップの解消： 結果は、ニューロ・シンボリックな統合が、純粋なニューラル・アプローチでは達成できない、MBSTに必要な構造的忠実度（F1 $\ge$ 0.90）と確率的キャリブレーションを実現できることを示しています。
欠陥検出のプロキシ（代理指標）： 本研究では、シードされた欠陥コーパスに対する直接的な欠陥検出率を測定していませんが、論文では、観察された35.7%の遷移カバレッジの増加は、欠陥検出の強力なプロキシであり、産業用MBT展開文献で報告されている25〜40%の向上と一致していると論じています。
エンジニアリング標準： 著者らは、LLMによる形式テストモデル生成の拡張が、以下の2つの条件が満たされる場合に限り、研究上の好奇心から標準的なエンジニアリング慣行へと移行すべきであると提案しています。(1) ハルシネーションを防ぐために、LLMが構造的制約（文法制約付き出力、シンボリック検証）の下で動作すること、および(2) 数値パラメータがLLMによって直接ではなく、認定されたソルバーによって割り当てられること。

結論として、本アプローチは厳格な統計的テストを、専門的な安全クリティカル・チームを超えて、より幅広いソフトウェア開発の実践へと開放するものであるとしつつ、より大規模な産業システムや多様な要件スタイルにおけるこれら知見の検証に向けた今後の課題も認めています。