An Empirical Study of LLM-Generated Specifications for VeriFast
本論文は、303個のC言語関数に対するVeriFast仕様書の生成において、8つのプロンプティング戦略にわたる10個の大規模言語モデルの有効性を実証的に評価しており、LLMは機能的な振る舞いは維持するものの、主にドメイン固有の分離論理に関する知識の誤りに起因して、検証の成功率はわずか31.4%にとどまっていることを明らかにしている。
原論文は CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/) でライセンスされています。 これは以下の論文のAI生成解説です。著者が執筆または承認したものではありません。技術的な正確性については原論文を参照してください。 免責事項の全文を読む
想像してみてください。あなたの手元には、VeriFastという名の、非常に厳格で極めて賢いロボット検査官がいます。その仕事は、コンピュータコードをチェックし、決してクラッシュせず、データを失わず、約束通りに正確に動作することを確認することです。しかし、ここには落とし穴があります。VeriFastは人間の言葉を話しません。それは、**分離論理（Separation Logic）**と呼ばれる、非常に複雑な数学的方言を話します。VeriFastに仕事をさせるためには、人間が、メモリがどのように扱われるかを説明する膨大な「取扱説明書（仕様書）」、つまり都市の交通ルールを詳細に記した地図のようなものを書かなければなりません。
このマニュアルを書くことは、信じられないほど困難で時間がかかる作業です。それは、ロードトリップ中のドライバーが行う一つひとつの曲がり角に対して、詳細な法的契約書を作成しようとするようなものです。
大きな問い
この論文の著者たちは、こう問いかけました。「人工知能（具体的には大規模言語モデル、LLM）は、この複雑な取扱説明書をVeriFastのために書くことができるのだろうか？」
彼らは、LLMを「コードは書けるが、VeriFastの厳格な方言を学ぶ必要がある新しい見習い」として扱いました。彼らは10種類の異なるAIモデルを、303個の異なるコンピュータ関数（コードの断片）に対してテストし、AIがマニュアルを書き、そしてVeriFastがそれを受理できるかどうかを検証しました。
実験： 「3ステップ」テスト
研究者たちは、大規模なテスト走行を用意しました。
- 入力： 彼らはAIに対し、各タスクについて3種類の「ブリーフィング（指示）」を与えました。
- 自然言語： 単なる平易な英語による説明（例：「この関数はリストの末尾にノードを追加する」）。
- 形式的振る舞い： コードといくつかの数学記号を組み合わせたもの。
- 形式的プラス： コードに加え、非常に詳細で、ほぼ完成に近い数学的マニュアル。
- プロンプト： 彼らは、AIに仕事を依頼する方法として、8つの異なる方法（例：ステップバイステップのレシピを与えるのか、単に「やれ」と言うのか）を試しました。
- モデル： 彼らは、GPT-4oからGemini 2.5 Proに至るまで、10種類の異なるAIの脳をテストしました。
結果： 良かった点、悪かった点、そして「惜しい」点
良いニュース（見習いは正直である）：
AIは、コードの「意図」を理解することにおいて、驚くほど優秀でした。**91%**以上のケースにおいて、AIはコードが本来すべきことを誤って変更してしまうことはありませんでした。コードを証明しやすくするために、元の説明を欺こうとすることはありませんでした。AIは元のジョブ記述に忠実でした。悪いニュース（見習いはルールに疎い）：
AIは仕事の内容は理解していましたが、VeriFastに受理されるマニュアルを書くことには失敗しました。AIが生成したマニュアルが検査に合格したのは、わずか約**31%**でした。これは、およそ3回の試行のうち1回程度です。「なぜ」なのか（それは論理の問題ではなく、構文の問題である）：
AIが失敗した場合、それは通常、AIが「愚か」だったり数学ができなかったりしたからではありません。AIがVeriFastの特定の文法やルールを知らなかったために失敗したのです。- 比喩： AIが、完璧なステーキを調理できる素晴らしいシェフだと想像してください。しかし、VeriFastは、特定の、非常に難解なフランス語の方言で書かれたレシピしか受け付けない保健所の検査官です。シェフはレシピを英語やスペイン語で書いてしまいます。料理自体は素晴らしいのですが、フォーマットが間違っているために検査官に拒否されてしまうのです。
- 論文によると、エラーの**94%**はこれらの特定のルール（例えば、メモリブロックを「開く」または「閉じる」のを忘れたり、特定のキーワードが欠けていたりすること）に関するものであり、プログラム自体の論理に関するものではありませんでした。
誰が勝ったのか？
- 最高のAI： Gemini 2.5 Proが明確な勝者でした。他のモデルよりもミスが少なく、より多くの検査に合格しました。
- 最高の入力： 研究者がAIに「形式的プラス」のブリーフィング（非常に詳細な出発点）を与えたとき、成功率は上がりました。逆に、単なる英語の説明だけを与えた場合、AIは最も苦戦しました。
まとめ
この論文の結論は、AIはコードが「何を」すべきかを理解することには長けているものの、VeriFastのような高度な検証ツールが要求する「特定の、厳格な指示」を書くことには、現時点ではまだ不得意であるということです。
AIは推論できないために失敗しているのではなく、その「方言」を知らないために失敗しているのです。これを解決するためには、以下のいずれかが必要であると研究者たちは示唆しています。
- VeriFastの特定のルールをより良くAIに教えること。
- AIが間違いを犯したときに、より良いフィードバックを与えること（単に「間違い」と言うのではなく、文法を添削する教師のように）。
- AIと従来のツールを組み合わせて、ギャップを埋めること。
要するに、AIの見習いは才能があり誠実ですが、一人で仕事をこなせるようになる前に、ロボット検査官の特定の「言語」について、もっと多くの訓練を受ける必要があるのです。
自分の分野の論文に埋もれていませんか？
研究キーワードに一致する最新の論文のダイジェストを毎日受け取りましょう——技術要約付き、あなたの言語で。