💻 computer science

VeriScale: Adversarial Test-Suite Scaling for Verifiable Code Generation

本論文は、既存のベンチマークでは検出できない最先端のLLMのコード生成および仕様能力における重大な弱点を明らかにするVerinaPlusやVerinaLiteのようなより厳格なベンチマークを創出するために、テストスイートを拡張し蒸留する敵対的フレームワークであるVeriScaleを導入する。

原著者： Yifan Bai, Xiaoyang Liu, Zihao Mou, Guihong Wang, Jian Yu, Shuhan Xie, Yantao Li, Yangyu Zhang, Jingwei Liang, Tao Luo

公開日 2026-05-22

📖 1 分で読めます☕ さくっと読める

CC BY 4.0

原著者： Yifan Bai, Xiaoyang Liu, Zihao Mou, Guihong Wang, Jian Yu, Shuhan Xie, Yantao Li, Yangyu Zhang, Jingwei Liang, Tao Luo

原論文は CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/) でライセンスされています。 ✨ これは以下の論文のAI生成解説です。著者が執筆または承認したものではありません。技術的な正確性については原論文を参照してください。免責事項の全文を読む

ロボットシェフに複雑な料理を任せることを想像してください。あなたはロボットにレシピ（「仕様」）を与え、その料理を調理するよう依頼します（「コード」）。ロボットが優れているかどうかを確認するために、あなたは料理を味わいます。

問題：「簡単なクイズ」の罠
現在、これらのAIシェフをチェックするために使用されているテストは、非常に簡単なクイズのようなものです。私たちは「塩」や「水」のようなごく単純な材料を数種類だけ与え、「スープ」という単純な結果を求めます。ロボットがスープを作れば、私たちはそれにA+を与えます。

しかし、ここには落とし穴があります。ロボットは不正をしているかもしれません。「塩＋水＝スープ」という答えを暗記しているだけなのに、「歯磨き粉」といった奇妙な材料を与えられても、まだスープを作ろうとして、それが正しいと主張するかもしれません。あるいは、「塩を加える」というレシピを書くが、「毒を加えない」という記述を忘れるかもしれません。「歯磨き粉」や「毒」がテストに含まれていないため、ロボットは合格しますが、実際には危険だったり壊れていたりするのです。

この論文は、現在のテストが小さすぎたり簡単すぎたりするため、AIが実際よりも賢く見えていると主張しています。

解決策：VeriScale（「ストレステスト」フレームワーク）
著者らは、VeriScaleと呼ばれる新しいシステムを開発しました。これは、AIコードに対する「ストレステスト」や「レッドチーム演習」と考えてください。AIにスープを作らせるだけでなく、VeriScaleはAIを失敗に追い込むように仕向けます。

これは主に2つのステップで機能します：

ステップ1：「障害物競争」（拡張）

まず、VeriScaleは材料の巨大で混沌とした障害物競争を作成します。

シード（種）： 通常の材料から始まります。
変異： 「変異マシン」を使用して、これらの材料をねじ曲げたり回転させたりします。水1カップを氷のバケツに変えたり、塩ひとつまみを塩の山に変えたりします。AIがこれまで見たことのない奇妙なエッジケースのシナリオを作成します。
「いたずらっ子」シェフ（敵対的合成）： これが巧妙な部分です。VeriScaleは、別の非常に賢いAIに「いたずらっ子」として行動させるよう依頼します。このいたずらっ子は、ルールに従っているように見えるが、実際にはゴミを生み出す偽のレシピを書こうとします。
- 例：ルールが「スープは熱くなければならない」場合、いたずらっ子は「アイスクリーム」を出力するレシピを書くかもしれませんが、「まあ、技術的にはアイスクリームも食品なので、ルールに従いました！」と主張するかもしれません。
- VeriScaleは、これらのいたずらっ子のレシピをAIのルールに対して実行します。AIのルールがアイスクリームを「熱いスープ」として受け入れた場合、VeriScaleはその欠陥を捕捉します。これにより、「ひっかけ」の瞬間の膨大なリストが生成されます。

ステップ2：「必須チェックリスト」（削減）

さて、VeriScaleにはこれらの厄介なテストケースが数千件あります。これらすべてをすべてのAIで実行するには時間がかかりすぎ、費用も莫大になります。そのため、「削減」を実行します。

「この1,000のひっかけのうち、どれが最も重要か？」と問います。
最も多くのミスを捕捉する特定のひっかけを保持し、単なる繰り返しとなるものを捨てます。
その結果、迅速に実行できるほどコンパクトでありながら、巨大なリストが見つけたすべての欠陥を依然として捕捉するコンパクトで超難易度の高いテストが生まれます。

結果：「真実の血清」
著者らは、この新しいシステムを入手可能な最高のAIモデル（GPT-5.5 など）でテストしました。

古いテスト： AIは96%や98%のようなスコアを獲得しました。彼らは天才のように見えました。
VeriScale テスト： ストレステストにかけられたとき、スコアは劇的に低下しました。あるトップモデルのスコアは、コーディングにおいて96%から86%に、仕様（ルール）の作成においては68%から44%に落ち込みました。

大きな教訓
この論文は、古いテストが私たちに嘘をついていたことを示しています。それらは、AIが安全で正確なコードを書く能力を過大評価していました。新しい「VeriScale」テストは、AIが「正しいように見える」コードを書くのは得意だが、あらゆる可能性のあるミスを捕捉するルールを書くのは依然として非常に下手であることを明らかにします。

彼らはまた、この新しいテストの2つのバージョンを公開しました：

VERINAPLUS： 巨大なフルスケールのストレステスト（元の83倍の規模）。
VERINALITE： 「ライト」バージョン。元の14倍の規模ですが、「削減」のトリックを使用して迅速かつ安価に実行可能でありながら、同じミスを捕捉します。

要約すると：VeriScaleは、簡単なテストを合格するだけのAIにだまされないようにするためのツールです。それはAIに、奇妙で、散らかっており、厄介な現実世界を処理できることを証明させるのです。

技術的サマリー：VeriScale 検証可能コード生成のための敵対的テストスイート拡張

問題定義

大規模言語モデル（LLM）がソフトウェア工学においてますます展開されるにつれ、機能的なコードだけでなく、形式的に検証可能な仕様と証明を生成する能力を評価することが重要になっています。VERINA や CLEVER などの既存の検証可能コード生成ベンチマークは、仕様生成（SpecGen）とコード生成（CodeGen）を評価するために、テストスイート評価に大きく依存しています。しかし、これらのベンチマークは根本的な限界に直面しています。すなわち、特にネガティブテストケース（予期しない入力と予期しない出力）の質の高いテストケースが不足しているという制約です。

現在のベンチマークは、通常、限られた数のポジティブな入出力ペアのみを提供します。その結果、モデルはこれらの希薄なテストを満たすことで、プログラムの意図を真に捉えたり、生成された仕様の健全性や完全性を保証したりすることなく、過剰に評価されたパス率を達成する可能性があります。これは、モデルの能力を過大評価することにつながります。つまり、誤った実装や非健全な仕様であっても、テストスイートが論理的欠陥や境界違反を露呈できないため、評価を通過してしまうのです。

手法：VeriScale フレームワーク

これらの限界に対処するため、著者は敵対的実装に駆動された新しいフレームワークVeriScaleを提案します。これは、検証可能コード生成のためのテストスイートを体系的に拡張し、洗練させることを目的としています。このフレームワークは、テストスイート拡張とテストスイート削減の 2 つの主要な段階で動作します。

1. テストスイート拡張

この段階の目的は、期待される入出力ペア、予期しない入力、予期しない出力を含む、多様で困難なテストケースのプールを構築することです。

シード生成とタイプ意識的変異：EvalPlus から着想を得て、VeriScale は LLM を用いて初期シード入力を合成します。これらのシードは、反復的なタイプ意識的変異戦略によって拡張されます。フレームワークは、入力タイプを維持しつつ構造的な摂動を導入する 5 項プロセス（ $M = (T, D, O, p, q)$ ）として変異を形式化します。これには、「材料プール」からの文脈値の再利用や、複雑なエッジケースを生成するためのタイプ固有のヒューリスティックの適用が含まれます。
事前条件ガイド入力分類：候補入力は、Lean における 2 段階の検証パイプラインを用いて、真の事前条件に対して厳密に分類されます。
- 構文フィルター：候補が構文的に有効な Lean 式であることを保証します。
- 双方向検証：#guard decide と妥当な証明探索を用いて、入力を「期待されるもの」（事前条件を満たす）または「予期しないもの」（事前条件に違反する）に分類します。
予期しない出力の敵対的合成：これが中核的な革新です。LLM にランダムな誤った出力を幻覚させることに頼るのではなく、VeriScale は敵対的実装を合成します。
- 有能なモデルが「レッドチーム」として機能し、問題に対する形式的仕様を生成します。
- もう一つのモデル（または同じモデルの異なる役割）が、これらの仕様の弱点を突くように設計された敵対的実装の作成を試みます。
- これらの実装は期待される入力に対して実行されます。もし敵対的実装が真の出力とは異なる出力を生成し、かつ生成された事後条件によって誤って受け入れられた場合、その出力は高品質な「予期しない出力」として保持されます。このプロセスにより、テストケースが仕様の非健全性を露呈するために真に有益なものであることを保証します。

2. テストスイート削減

拡張されたスイートの計算コストを管理するため、VeriScale は大規模なプールをコンパクトかつ識別力のあるスイートに集約するための削減戦略を採用します。

境界保存削減（予期しない入力用）：ランダムサンプリングの代わりに、この戦略は一般的な境界違反（空のコンテナ、ゼロ値、長さの不一致など）に対応する入力を優先します。典型的な事前条件違反の網羅性を確保するため、重要な境界バケットから代表的な例を保持します。
敵対者殺し削減（期待される入力用）：この戦略は、拡張段階で合成された敵対的実装を流用します。各期待される入出力ペアは、それがいくつの「変異体」（敵対的）実装を「殺す」（すなわち、異なる出力を生成する）ことができるかに基づいて評価されます。削減は集合被覆問題として定式化され、これまでに殺されていない変異体の最大数をカバーするペアを貪欲に選択します。これにより、削減されたスイートが欠陥のある仕様を区別する能力を保持することが保証されます。

主要な貢献

VeriScale フレームワーク：著者は、敵対的実装を活用して、検証可能コード生成のためのテストスイートの体系的な拡張と削減の両方を推進する一般フレームワークを提案します。
VERINAPLUS と VERINALITE：このフレームワークは VERINA ベンチマークに具体化され、2 つの新しいデータセットを作成します。
- VERINAPLUS：テストスイートが83 倍以上（具体的には期待される入力で 62.83 倍、予期しない出力で 87.79 倍、予期しない入力で 183.08 倍）拡張された拡張ベンチマークです。
- VERINALITE：削減戦略によって最適化され、低い評価コストで識別力を維持するよう調整された、14 倍に拡張された軽量バリアントです。
実証的検証：この論文は、元のベンチマークがモデルの能力を著しく過大評価していることを示しています。強化されたベンチマークは、以前は隠れていた最先端の LLM の重大な弱点を明らかにしました。

実験結果

著者は、VERINA、VERINAPLUS、VERINALITE において、8 つの最先端 LLM（GPT-5.5、Claude-Sonnet-4.6、DeepSeek-V4-Pro などを含む）を評価しました。

モデルの弱点の露呈：拡張されたベンチマークは、急激なパフォーマンス低下を引き起こしました。例えば、GPT-5.5の SpecGen スコアは、VERINA の**68.78%から VERINAPLUS の44.44%に急落し、CodeGen スコアも96.83%から86.24%**に低下しました。これは、元のベンチマークの希薄なテストケースが、モデルに真の理解なしに通過させることを許していたことを示しています。
評価不確実性の低減：拡張されたテストスイートは、SpecGen 評価における誤差範囲を著しく狭めました。元のベンチマークでは、未決定の検証結果により、上限と下限の間に広いギャップ（例：Claude-Opus-4.7 で 13.23%）が存在していました。VERINAPLUS では、この曖昧さが解消され、ギャップは**4.76%**に縮小し、より統計的に信頼性の高い評価を提供しました。
ロバストネスの格差：結果は、根本的な格差を浮き彫りにしています。モデルは SpecGen よりも CodeGen の方がはるかに得意です。CodeGen スコアは中程度の低下を示したのに対し、SpecGen スコアは急激な低下を遂げました。これは、健全かつ完全な形式的仕様の合成が、現在の LLM にとって依然として大きなボトルネックであることを示唆しています。
削減の効率性：VERINALITE は、VERINAPLUS とほぼ同一のパフォーマンス低下プロファイルを実現しながら、計算オーバーヘッドを大幅に削減しました。VERINALITE の評価時間は、SpecGen でベースラインの1.38 倍、CodeGen で1.05 倍であり、フル VERINAPLUS スイートの1.80 倍および1.50 倍と比較して優れています。

意義と主張

この論文は、VeriScale が、LLM ベースの検証可能コード生成を進展させるための重要かつ極めて信頼性の高い基準を提供すると主張しています。希薄なポジティブテストを超えて、敵対的に合成されたネガティブケースを含めることで、このフレームワークはモデルの能力の過大評価を防ぐ、より厳格な評価を提供します。

著者は、VeriScale を既存の取り組みに補完的なものとして位置づけています。新しいタスクを導入するのではなく、テスト信号の質と量を拡張することで既存のベンチマークを強化します。この研究は、現在のモデルの形式的推論タスクにおける脆弱性を露呈させるために、敵対的テストの拡張が不可欠であることを強調しています。

認められた限界：
著者は、VeriScale が真の事前条件と参照実装の入手可能性に依存していることを指摘しています。さらに、合成された予期しない出力の品質は、「レッドチーム」として機能する LLM の推論能力によって制限されます。最後に、構築段階は依然として計算集約的であり、大規模な LLM サンプリングと Lean 実行を必要とします。

将来の課題：
著者は、VeriScale を欠陥のある仕様を修正するモデルを導く閉ループ修復システムへと進化させることを提案しています。また、VeriScale を敵対的データエンジンとして活用し、専用の自動形式化モデルのためのトレーニングコーパスを合成すること、および Dafny などの他の検証バックエンドにフレームワークを一般化することも計画しています。