Can LLMs Write Correct TLA+ Specifications? Evaluating Natural-Language-to-TLA+ Generation

あなたは、非常に賢く、博識なロボットに、複雑な機械の厳格で数学的なレシピを書く方法を教えようとしていると想像してください。この機械は「分散システム」（AmazonやMicrosoftを動かしているクラウドサーバーのようなもの）です。そして、そのレシピは**TLA+**と呼ばれる特別な言語で書かれています。

この言語は、ハイリスクなパズルのようなものです。もし記号を一つでも書き漏らしたり、論理を少しでも間違えたりすると、レシピ上では正しく見えても、現実の世界ではシステムがクラッシュしてしまいます。問題は、これらのレシピを手書きするのは難しく、時間がかかるということです。そこで研究者たちは、こう問いかけました。「最新のAI（大規模言語モデル、またはLLM）に、私たちの代わりにこれらのレシピを書かせることができるだろうか？」

この論文は、その問いに対する最初の大きな成績表です。以下に、その内容を分かりやすく説明します。

1. 「文法と意味」のギャップ

研究者たちは、30種類の異なるAIに対し、自然言語による説明に基づいたTLA+のレシピを書かせました。

• 良いニュース（文法）： 約**26%**の確率で、AIは表面上は正しく見えるレシピを作成しました。「スペルチェッカー」（SANYと呼ばれます）は、「単語や記号の順序は正しい」と判定しました。
• 悪いニュース（意味）： しかし、実際にレシピを「論理テスター」（TLCと呼ばれます）に通して、それが本当に機能するかどうかを確認したところ、合格したのはわずか**8.6%**でした。

例え話： ある学生に法律の契約書を書くよう頼んだと想像してください。その学生は完璧な綴りと文法を使っていますが（成功率26%）、書かれた契約書の内容は意図とは逆であったり、重要な条項が欠落していたりして、法的には全く役に立たないものです（成功率8.6%）。AIは言語の「見た目」を模倣することには長けていますが、その背後にある「論理」を理解することにはしばしば失敗します。

2. 大きければ大きいほど良いわけではない

通常、より大きく強力なAIほど優れた仕事ができると想定されがちですが、この研究ではそうではありませんでした。

• 驚きの事実： 小規模なAIモデル（DeepSeek r1:8b）が、その巨大な「兄貴分」（DeepSeek r1:70b）よりもはるかに優れた仕事を行いました。
• 理由： 小規模なモデルは、数学の生徒が計算過程を示すように、「ステップ・バイ・ステップで考える（思考プロセスを示す）」ように訓練されていたためです。一方で、大規模なモデルはインターネット上の膨大な一般データで学習されているため、TLA+の厳格なルールによって混乱してしまいました。これは、正確なスフレの作り方を知っている専門のシェフと、あらゆる料理を知っているが特定のレシピに対しては考えすぎてしまうジェネラリストの違いのようなものです。

3. 「コードの専門家」は失敗した

研究者たちは、コンピュータコード（PythonやJavaなど）を書くことで有名なAIをテストしました。驚くべきことに、これらの「コードの専門家」は、汎用AIよりも成績が悪かったのです。

• 理由： これらのモデルは、セミコロン（;）や波括弧（{}）を用いたコーディングに慣れすぎているため、TLA+のレシピの中にそれらを誤って入れてしまう癖がありました。TLA+にはこれらの記号は存在しないため、レシピは即座に壊れてしまいます。これは、時計を修理しようとしている大工が、普段使っているハンマーを誤って使おうとするようなものです。

4. 「ステップ・バイ・ステップ」の手法が最も効果的だった

研究者たちは、AIに助けを求める4つの異なる方法を試しました。最も成功した方法は、**「プログレッシブ・プロンプティング（段階的プロンプト）」**と呼ばれる手法でした。

• 仕組み： AIに一度にレシピ全体を書かせるのではなく、パーツごとに構築させていく方法です。「まず、タイトルを書いてください。次に、変数を書いてください。次に、ルールを書いてください」という具合です。
• 結果： これが、完全に動作するレシピを生み出した唯一の方法でした（成功率は8.6%）。これは家の建築と同じです。屋根、壁、基礎を一気に作ろうとすれば失敗する可能性が高いですが、一室ずつ丁寧に作っていけば、成功の確率は高まります。

5. AIの「ハルシネーション（幻覚）」

論文では、AIが繰り返してしまう5つの具体的な間違い（ハルシネーション）が特定されました。

1. 記号の間違い： 特殊な数学記号（∧など）を、TLA+が要求するプレーンテキストの記号（/\など）の代わりに使ってしまう。
2. 言語の混同： 他のプログラミング言語のセミコロンやバッククォートを誤って混ぜてしまう。
3. 思考の垂れ流し： AIが自身の「思考プロセス」（...など）を最終的なレシピの中にそのまま貼り付けてしまい、エラーを引き起こす。
4. 長さの不一致： レシピが通常の9倍の長さになったり、逆にほとんど何も書かれなかったりする。
5. 構造の崩壊： レシピの「終了」マーカーを書き忘れ、文書が未完成のまま終わってしまう。

まとめ

この論文の結論は、現在のAIは、単独で信頼できるTLA+仕様を書くことはまだできないということです。AIは言語の「見た目」を模倣することはできますが、人間による一行ごとのチェックなしでは信頼できないほど、論理的なエラーを多発させます。

研究者たちは、これを解決するために以下のことが必要だと示唆しています。

• 「ステップ・バイ・ステップ」のプロンプティング手法を用いること。
• 巨大な汎用モデルではなく、推論に特化した小規模なモデルを使用すること。
• AIがレシピを実行する前に、一般的な間違い（誤った記号の除去など）を自動的に修正するツールを構築すること。

それまでは、これらの極めて重要なシステムのレシピを書くことは依然として人間の専門家の仕事であり、AIはあくまで「有用だが間違いを犯しやすい助手」に留まります。