TLA-Prover：LLMに「正しそうな仕様」ではなく「検査に通る仕様」を書かせる研究

今日は、6月4日にarXivへ投稿された「TLA-Prover」を取り上げます。テーマはかなり地味に見えます。TLA+という形式仕様言語で、分散システムや安全クリティカルなプロトコルの仕様をLLMに合成させる研究です。でも、これはAIコーディングの次の段階を考える上で重要です。コードを書けるAIから、設計の前提そのものを検査可能な形で書けるAIへ、という話だからです。(arxiv.org)

ポイントは、単に「TLA+を書けるモデルを作った」ことではありません。著者らは、既存の25モデルを調べたところ、最良の公開ベースラインでも構文的に通る出力が26.6%、意味的にTLCモデルチェッカーを通る出力が8.6%だったと報告しています。つまり、LLMはそれらしい形式仕様を出せても、モデルチェッカーにかけると多くが落ちる。自然言語やPythonなら雰囲気でごまかせる部分が、形式仕様ではすぐ露呈します。(arxiv.org)

TLA-Proverの面白さは、報酬を人間の好みや別のLLMジャッジに頼らず、TLCという検査ツールから直接取っている点です。訓練は、検証済み例によるSFTに加え、失敗した仕様を修復させるGRPOで構成されています。つまり「人間が良さそうと言ったから正しい」ではなく、「検査器が拒否したので直す」というループです。これは、AIエージェントに外部ツールを使わせる研究の中でも、かなり健全な方向に見えます。(arxiv.org)

さらに重要なのがDiamond評価です。単にTLCを通るだけだと、モデルは中身の薄い仕様や、常に真になる性質を書いて逃げる可能性があります。そこで著者らは、正しさの性質を少し改変し、その改変に対してTLCが違反を検出できるかを確認します。もしそれでも通ってしまうなら、その仕様は検査として意味が薄い。TLA-Proverは30問の保持ベンチマークでGoldとDiamondのpass@1がどちらも30%となり、8.6%の未調整ベースラインに対して約3.5倍と報告されています。(arxiv.org)

ここで冷静に見たいのは、これは「AIが分散システムを自動で安全に設計できるようになった」という話ではないことです。評価セットは30問で、論文はプレプリント段階です。TLA+自体も、コードを生成する言語ではなく、システムの振る舞いを数学的に記述し、設計レベルの欠陥を見つけるための道具です。Leslie LamportのTLA+公式ページでも、TLA+とTLCは根本的な設計ミスを早期に見つけるためのものとして位置づけられています。(lamport.org)

それでも、この研究が示す方向は大きいです。今のAIコーディングは「実装を速くする」方向に寄りがちですが、本当に難しいのは、そもそも何を満たすべきかを曖昧にしたままコードを量産してしまうことです。TLA-Proverのようなアプローチは、AIに仕様を書かせ、外部検査器で落とし、修復させるという閉じた訓練ループを作ります。これは、将来の開発エージェントが「コードを書く前に検査可能な設計仮説を出す」方向へ進むための小さな足場です。

実務的には、すぐに本番の分散プロトコル設計を任せるというより、仕様作成のたたき台、学習支援、CIに組み込む形式検査の補助として見るのが妥当だと思います。AIが書いたものをAIが褒める世界ではなく、外部の厳密な検査器が失敗を返す世界へ。LLMの信頼性を上げる鍵は、モデルを万能にすることだけではなく、モデルが間違えた時に逃げられない環境を作ることなのかもしれません。