教科書を超えて：実世界のTLA+モデリングにおけるLLMの評価

長年、TLA+は並行および分散システムの仕様策定におけるゴールドスタンダードであり、エンジニアがコードを一行も書く前に、重大な設計上の欠陥を特定することを可能にしてきました。大規模言語モデル（LLM）の台頭により、この厳格なプロセスをAIに委ねたいという誘惑が高まっています。しかし、重要な疑問が残ります。AIは実際に目の前のシステムをモデリングしているのでしょうか、それとも単に学習データにある有名な教科書的な実装を暗唱しているだけなのでしょうか？

Speculaチームによる最近の研究は、"教科書的なモデリング"と忠実なシステム表現との間のギャップを明らかにするために設計された自動ベンチマークであるSysMoBenchを導入しています。並行同期プリミティブからEtcdやZooKeeperのような複雑な分散プロトコルに至るまで、11の実世界のシステムをLLMで評価することで、チームは現在のLLMが形式仕様策定にどのように取り組むかにおける体系的な失敗を明らかにしました。

正解性の錯覚

EtcdのRaft実装のためのTLA+仕様を記述するよう求められた際、主要なLLMは、構文チェックを通過し、TLCモデルチェッカーでエラーなく実行できるコードを生成することがよくあります。一見すると、その結果は洗練されているように見えます。しかし、詳しく調査すると、その仕様はEtcdの実際の実装における特定のアーキテクチャ上の選択を反映しているのではなく、元のRaft論文の付録を反映していることが多いのです。

これがLLMベースのモデリングにおける核心的な課題です。LLMはオンライン上のほぼすべてのTLA+の例を見てきているため、「Raftの仕様」を求めると、抽象化メカニズムではなく想起メカニズムが作動してしまいます。システムを真にモデリングするためには、LLMは複雑なソースコードから論理を抽象化し、その抽象化を正しい形式モデルへと変換できなければなりません。

SysMoBenchの仕組み

想起とモデリングを区別するために、SysMoBenchは4段階の評価パイプラインを採用しています：

Syntax Phase: 仕様がコンパイルできるかを確認します。
Runtime Phase: TLCモデルチェッカーがクラッシュせずに仕様を実行できるかを確認します。
Conformance Phase: トレース検証を使用して、実際のコードからの実行トレースをモデルと比較します。
Invariant Phase: 仕様が主要な安全性（safety）および活性（liveness）の特性を満たしているかを確認します。

最先端のLLMはSyntax Phaseでは100%に近いスコアを獲得しますが、Conformance PhaseとInvariant Phaseのテストではパフォーマンスが急落します。複雑な分散システムにおいては、最も強力なモデルであっても、総合スコアはしばしば10%から50%の間まで低下します。

「教科書的なモデリング」の2つのパターン

研究では、LLMが実装の詳細ではなく一般的なテンプレートに依存してしまう、2つの繰り返される失敗モードを特定しています：

1. 不可能な状態の許容

LLMは、システムの実際のデータ構造と一致しない形式化テンプレートを使用することがよくあります。例えば、ZooKeeperのFast Leader Election (FLE) の仕様において、Claude Sonnetはサーバーのrecvsetを集合の和集合として扱い、すべての投票を証拠として蓄積することを可能にしていました。実際のZooKeeperのコードでは、これは送信者によってキー付けされたマップであり、新しい投票は古い投票を上書きします。この不一致により、仕様は実際のシステムが到達決してできない状態に進入することが可能になります。

2. 到達可能な状態の消失

逆に、LLMは複数の実装ステップを単一の原子的なガード（atomic guard）に統合してしまうことがよくあります。同じZooKeeperの例では、LLMはローカルな論理時計の更新とメッセージの処理という行為を一つのステップに融合させていました。実際のコードでは、これらは逐次的に発生します。これらを融合させることで、LLMは、実際のシステムがすべての選挙ラウンドで進入する状態を消失させてしまい、仕様において特定の遷移が不可能になってしまいます。

遷移検証：きめ細かなアプローチ

これらの失敗を特定するために、SysMoBenchはTransition Validationを利用しています。モジュール全体に対する二値的な合格/不合格ではなく、システムは実際の実行からの実行トレースを収集中、それらを「遷移ウィンドウ」（事前状態、アクション、事後状態）に分割します。

各ウィンドウは、TLCに供給され、仕様のアクションが実際にシステムを事前状態から事後状態へ移動させることができるかを確認します。これにより、アクションごとのスコアカードが提供され、開発者は、粗い集計スコアに頼るのではなく、どの特定の状態遷移が失敗しているのか、そしてなぜ失敗しているのかを正確に把握することができます。

より広範な影響と未解決の課題

この結果は、LLMがTLA+の言語には優れているものの、特定の実装の論理には苦戦することを示唆しています。これは、形式手法の未来に関するより広範な議論を巻き起こしています：

Coupled Verification: Verusのような、実装と検証を結合させることで、モデルがコードから乖離することを防ぐアプローチを主張する人々もいます。
Human Intent: 設計プロセスを自動化することは、人間の意図を排除してしまうという哲学的な懸念があります。あるコメント投稿者は、もしLLMが設計とコードの両方を生成する場合、「証明」には意味のある人間の保証が欠かせない可能性があると指摘しました。
Liveness Properties: ユーザーは、LLMが安全性（safety）特性と比較して、活性（liveness）特性（「何か良いことが最終的に起こる」ことを保証すること）に特に苦戦することに気づきました。

これらの障害があるにもかかわらず、Speculaチームは、リポジトリを自律的に読み取り、仕様策定のワークフローを推進できる特化型エージェントを開発しています。彼らの特化型エージェントであるSpeculaは、現在のSysMoBenchのタスクにおいて、すでに完全な適合性と不変量特性のスコアを達成する能力を示しており、これは、単なるLLMプロンプトではなく、エージェント的ワークフローが今後の道筋であることを示唆しています。

結論

コンパイル可能なTLA+モジュールを書くことは、低いハードルです。そのモジュールを特定のシステムの実際の挙動と一致させることは、真の挑戦です。私たちがエージェント的モデルチェッキングへと移行するにつれ、焦点は構文（syntax）から適合性（conformance）へと移らなければなりません。目標は、Raftがのように見える仕様を作成することではなく、システムそのものとなる仕様を作成することです。