
自分が3ヶ月前に書いたコードを、自分で見返して「これ、どういう時にどう動くんだっけ」と一瞬固まったこと、ありませんか。
書いた本人の頭の中には、書いた当時の「こう動くはず」という暗黙のお約束があったはずです。けれど時間が経つと、その記憶は薄れていきます。ドキュメントに残しておけばいいのですが、書く時間も、書いたあと最新状態に保つ時間も、現場ではなかなか取れません。
ここで「テストはすでに書かれていますよね?じゃあ、そのテストを走らせて観察すれば、コードが守っているお約束を機械が自動で抜き出せるのでは?」という発想があります。実は数十年前から続く研究の流れで、テストの実行結果から「このコードはこういう性質を持つ」というルールを自動で引っ張り出してくれるツールが、すでにいくつも作られています。
便利そうな話なのですが、実際にやってみると一つ大きな困りごとにぶつかります。機械が引っ張り出してきたルールのなかに、嘘が混じるのです。しかも、人間が一つずつ振り分けるしかない、という嘘が。
本記事では、その振り分け作業をLLMに手伝わせたら何が起きたか、という研究を紹介します。
※スキルファイルあり
そもそも「プログラムの仕様」って何のこと?
話を始める前に、この記事でずっと出てくる「仕様」という言葉を、共通認識にしておきます。
ここでの仕様というのは、たとえばこんなお約束のことです。
- このメソッドは、サイズが0以上の値を返す
- このキューにaddを呼んだら、サイズが1増える
- このsortを呼んだ後、配列は昇順になっている
- 返り値がnullになるのは、入力が空のときだけ
コードのコメントに書くような、ふんわりした注意書きを、もっと機械が読める形にしたもの、と思ってもらえれば大きく外れません。実際のコードでは、assert文の形で書かれたり、ドキュメントコメントのなかに特別な書式で書かれたりします。
こういうお約束がコードに添えられていると、いいことがたくさんあります。お約束と実際の動きがズレていたらバグとわかる。お約束をもとに自動でテストを作れる。他の人が安心してそのコードを使える。
便利なのに、なぜ現場で書かれないのか。答えはシンプルで、書くのが面倒だからです。コード自体を書くので手一杯なのに、そのうえ「どう振る舞うべきか」を別言語で書き下すなんて、余計な仕事が増えるだけに感じます。
そこで昔から、「じゃあ、テストを走らせて実際の動きを観察すれば、機械がお約束を勝手に拾ってくれるのでは?」という発想の研究が続いてきました。
機械にお約束を拾わせる仕組み
やっていることを噛み砕くと、こんな流れです。
まず、機械が「こうなるはず」という仮説をたくさん作ります。「サイズは0以上のはず」「返り値はnullじゃないはず」「AとBは等しいはず」のような調子で、コードに関係しそうな候補を大量に並べます。
次に、手元にあるテストを片っ端から走らせて、その仮説が一度でも破られないか確かめます。途中で破られたら「これは違うな」と外す。最後まで破られなかったものだけを「たぶん本当のお約束ですね」と報告する。それだけです。
この仕組みの大きな落とし穴
困るのは、テストが見ていない場所では、仮説が破られようがないという点です。
テストの抜け漏れがある領域では、本当は成り立たない嘘のお約束も「一度も破られなかったので、きっと正しいでしょう」という顔で残ってしまいます。
具体例を出しましょう。円を描くように配列を使うキュー、というデータ構造があります。先頭を取り出すたびに、先頭の位置を示す印が一つずつ進んでいく。配列の端まで来たら0に戻る、という作りです。
この実装だと、「中身は空っぽなのに、先頭の印だけが途中まで進んでいる」という状態がふつうに発生します。ところが機械は「サイズと先頭の印が等しいなら、先頭の印は1未満のはず」という仮説を、自信満々で報告してきます。テストでたまたまその状態を踏んでいなかっただけなのに、です。
こういう嘘のお約束が、少ないときで数十個、多いときで数百個出てきます。人間が一つずつ眺めて「これは本物、これは偽物」と振り分けるのは、地味にしんどい作業です。自動化したはずなのに、結局は人の目が必要になってしまう。ここが、この分野の長年の困りごとでした。
LLMに「検査員」を頼む
LLMで生成した反例を用いた動的仕様推論の改善
Improving Dynamic Specification Inference with LLM-Generated Counterexamples
| 著者 | Agustín Balestra, Agustín Nolasco, Facundo Molina |
|---|---|
| URL | https://arxiv.org/abs/2604.10761 |
ここからは、その振り分けをLLMに手伝わせる具体的な手順を、最初から最後まで順を追って見ていきます。
1. 既存のツールで候補を出しきる
最初に、従来通りの仕様推論ツールを走らせて、候補の仮説をひと通り出しておきます。この段階で数十から数百の仮説が手元に並びます。嘘も混じっていますが、それは後で拾うので気にしません。
2. 候補を一つずつ取り出してLLMに渡す
候補を一つ選び、次の3点をまとめてLLMに送ります。
- 対象クラスのソースコード全部
- 対象メソッドの実装
- いま検証したい候補の仮説
メソッド単体だけでなくクラス全体を渡すのがポイントです。候補の正しさを崩す反例は、対象メソッドの外、たとえばフィールドを書き換える別メソッド(先ほどのキューの話で言うdequeueのような存在)によって作られることがよくあります。LLMに全体を見せておかないと、こういう反例を思いつけません。
3. 依頼文を、フォーマットを縛って書く
依頼は、次の4点を明示的に書き込むとLLMが動きやすくなります。
- 役割を先に与える(「プログラム検証とテストの専門家として」)
- 判定を二択に絞る(OKかFAILEDか)
- FAILEDなら、反例のテストコードをJUnitなどの決まった形式で出させる
- 出力の区切りを特殊タグで明示する(「[[VERDICT]]」「[[TEST]]」のような)
「正しいか考えて」と素で聞くより、出力形式を縛った方が、後でテスト部分だけを機械的に抽出しやすくなります。
4. 返ってきたテストをコンパイルにかける
LLMが書いてきたテストコードを、まずコンパイルに通します。通れば次のステップへ。通らなければ、エラーメッセージと元のテストをLLMに戻して直してもらいます。修正依頼は最大3回まで。それでも通らなければ、そのテストは諦めて破棄します。
コンパイルだけで実行判定はしない理由は、実行して仮説を破るかどうかは後続のステップでまとめて機械に任せるためです。ここでは「形式的にテストとして動かせる状態」だけを担保します。
5. 生き残ったテストをテストスイートに合流させる
コンパイルが通った反例テストを、元のテスト集に足し込みます。これでテストスイートが一回り賢くなります。
6. 仕様推論ツールをもう一度走らせる
増強したテストスイートで、ステップ1と同じ仕様推論ツールをもう一度走らせます。追加したテストによって実際に破られた候補は、そこで初めて外されます。
この二度回しが、仕組みのなかで一番効いている部分です。LLMが「嘘だ」と言っただけでは候補を捨てず、機械に最終ジャッジを任せる。こうしておけば、LLMが勘違いして本物のお約束に「嘘だ」と言ってしまっても事故が起きません。LLMが書いたテストは実際には何も壊さないので、本物の仮説はちゃんと残ります。
3つのLLMで実際に試してみた
実験には43個のJavaメソッドが使われました。スタックやキュー、Apache Commons Math、Google Guavaなど、この分野では定番の題材です。試したLLMはGPT-5.1、Llama 3.3 70B、DeepSeek-R1の3つ。
数字を表にまとめると、こんな感じになります。
| モデル | 生成したテストの数 | 嘘と見抜いて落とせた仮説の数 | 削減率 | 精度 | 再現率 | F1 |
|---|---|---|---|---|---|---|
| 補助なし | – | – | – | 67.83% | 54.57% | 51.39% |
| GPT-5.1 | 982 | 1,877 | 10.09% | 74.17% | 54.57% | 53.94% |
| Llama 3.3 70B | 430 | 1,048 | 5.63% | 71.13% | 54.57% | 50.31% |
| DeepSeek-R1 | 3,684 | 2,173 | 11.68% | 75.62% | 54.57% | 52.04% |
精度というのは「残った仮説のうち、本当に正しかったものの割合」です。GPT-5.1の補助で約7ポイント上がり、DeepSeek-R1はもう少し上を行きます。生成したテスト1本あたりの効率で見るとGPT-5.1が一番よく、コスパの観点ではGPT-5.1が有利と評価されています。
再現率が3つとも54.57%で揃っているのは、仕組み上そうなるから、というだけの話です。LLMはテストを足すだけで、新しい仮説を生み出すわけではありません。もともと候補に上がっていなかった本物のお約束を新たに拾うことはできない代わりに、本物を誤って捨てるリスクもない。そういう安全な改善になっています。
正解側の間違いまで暴いた話
論文のなかで一番面白かったのは、整数の絶対値を返すメソッドの話でした。
「結果は常に0以上のはず」という、誰がどう見ても正しそうな仮説が機械から出てきます。ところが、コンピュータが扱える最小の整数を入れると、計算があふれて負の値が返ってきてしまう。
GPT-5.1にこの実装と仮説を見せたところ、まさにこの一点だけが崩れる条件だと見抜いて、対応するテストを書いてきました。
さらに面白いのは、研究チームが用意していた「正解のお約束集」のほうが間違っていた、ということまで判明した点です。LLMが検査員の役割を超えて、正解側の修正にまで貢献したかたちになります。
ついでに、LLM単独に判定させてみたら
おまけの実験として、機械側のテスト数をぐっと減らして、LLMの判断だけで仮説を捨てるシンプルな形も試しています。
GPT-5.1での結果は、精度64.21%、再現率83.08%、F1 72.44%。補助なしでこの数字が出るのは、なかなか意外な水準です。
ただし、LLMが「嘘だ」と判定したもののうち、本当に嘘だったのは55%程度。半分近くは「嘘だ」と言われて巻き込まれた善良な仮説でした。見逃しは少ないものの、無罪のものを有罪と言いがち、という傾向が出ています。だからこそ、反例テストを書かせて機械でダブルチェックする、という二段構えの設計が活きてくる、ということになります。
注意点
論文のなかで正直に語られている限界もあります。
仕組み上、新しい本物のお約束を発見する力は元のツールに依存します。候補として出てこなかったお約束は、LLMで磨いても出てきません。再現率の天井を上げたいなら、候補を作る側の表現力を広げる別の研究が必要になります。
LLM単独の判定で精度が55%という数字は、半分が空振りということを意味します。空振り分はテストを作る手間として消費されるので、判定の精度を上げることが次の宿題として挙げられています。
加えて、今回の実験では反例テストを追加した後の再解析を一度しかやっていません。何度も繰り返したらどうなるか、という話は今後に残されています。
まとめ
仕様を書く文化は、なかなか根付きません。とはいえ「テストは書く」習慣がある現場なら、その先にある「テストからお約束を引き出して、LLMで磨く」という流れは、思ったより手の届くところまで来ています。
この研究をもとに作成したスキルファイルを共有します。
本記事の関連研究