本論文は、現実のソフトウェアの大半において、事前条件・事後条件、ループ不変条件、アサーションといった形式仕様が文書化されていないという問題を扱っており、その原因をこうした仕様を手作業で書くことの難しさに求めている。Houdini や Daikon などの既存の自動化ツールは、人間の専門家が定義したテンプレートから候補となる仕様を生成するが、著者らは、これでは単純すぎる仕様しか得られず、複雑なプログラムの振る舞いを捉えられないと論じる。これに対して SpecGen は、大規模言語モデルのコード理解能力を利用して Java Modeling Language（JML）で仕様を生成し、OpenJML 検証器でチェックする。
SpecGen は 2 つのフェーズで動作する。対話駆動の仕様生成フェーズでは、システムロール、few-shot の例、対象のプログラムから構築したプロンプトによって LLM に JML 仕様を求める。各出力は検証され、失敗した場合は、検証器のエラーメッセージに加えて、よくある失敗の種類に対する自然言語のガイダンスを含むフィードバックプロンプトが生成され、最大ラウンド数に達するまで次のラウンドに渡される。失敗した LLM の出力がすでに正しい仕様に近いことが多いという観察から、著者らは対話が失敗したプログラムに対してミューテーションベースのフェーズを追加している。このフェーズでは、述語、論理、比較、算術の 4 種類のミューテーション演算子が失敗した仕様中の演算子を置き換えて候補となるバリアントを生成し、ヒューリスティックな選択戦略がミューテーションの種類に重みを割り当て、どのバリアントを検証するかを選ぶ際にミューテーションの少ない候補を優先する。
要点
- SpecGen は、SV-COMP の Java ベンチマーク（265 個のプログラム）と著者らの SpecGenBench（120 個のプログラム）を合わせた 385 個のプログラムのうち 279 個について検証可能な仕様を生成した。これに対し、AutoSpec は 247 個、対話的アプローチ単独では 218 個、Houdini は 98 個、Daikon は 72 個であった。
- プログラムごとに 10 回試行した場合の平均成功確率は 59.97% で、AutoSpec の 46.13%、対話的生成の 35.95% を上回った。
- アブレーションでは、すべてのミューテーションの種類が寄与しており、中でも比較ミューテーションの寄与が最も大きかった（これを無効にすると対応できたプログラムは 223 個に減少した）。著者らはこれを、数値変数やループ変数の範囲を制限する必要が繰り返し生じるためだとしている。
- ヒューリスティックな選択戦略により、SpecGenBench における検証器の平均呼び出し回数は、ランダム選択と比べて 36.20 回から 28.51 回に減少した（21.23% の改善）。SV-COMP での改善はわずかであった。
- 15 人の博士課程の学生が 15 個のプログラムを評価したユーザー調査では、SpecGen の仕様の平均評価は 5 点満点中 4.54 で、正解仕様の 4.83 に近く、Houdini と Daikon の 2.32 を大きく上回った。
- 9 つの Defects4J リポジトリから取り出した 50 個の Java ファイルでは、SpecGen は 38 個に対応でき、対話的アプローチは 28 個、Daikon は 15 個であった。
補足
実験には gpt-3.5-turbo-1106 が使用された。著者らは、SpecGen がネストしたループを含むプログラムでは比較的性能が低いこと、OpenJML の実装上の欠陥によって一部の正しい仕様が検証に失敗する可能性があること、そしてデータの一部（既存のデータセットと SV-COMP に由来する 20 個のプログラム）にはデータ漏洩のリスクがあることを指摘している。ただし、残りの 100 個のプログラムのうち 87 個には SpecGen が対応できている。また、使用した SV-COMP のプログラムの 88.7% がループを含まないことも判明しており、これが SpecGenBench を構築する動機となった。