Quokka: 不変条件合成による LLM を活用したプログラム検証の加速

本論文「Quokka: Accelerating Program Verification with LLMs via Invariant Synthesis」は、大規模言語モデル（LLM）を用いてループ不変条件（Loop Invariants）を生成し、プログラム検証の速度向上と成功率の向上を目指す新しいフレームワーク「Quokka」を提案するものです。

以下に、問題定義、手法、主要な貢献、実験結果、および意義について詳細にまとめます。

1. 背景と問題定義

プログラム検証において、ループ不変条件の自動発見は長年の課題です。不変条件は、ループの各反復前後で成り立つ条件であり、帰納的検証の核心です。

• 課題: 単に「正しい」不変条件を見つけることは比較的容易ですが、検証を加速し、最終的なアサーション（主張）を証明するために十分な「強さ（strength）」を持つ不変条件を見つけることは困難です。
• 既存手法の限界: 従来の LLM 活用研究（例：Pei et al., 2023）は、不変条件の「正しさ」のみを動的解析ツール（Daikon など）で評価しており、形式的検証の観点からは健全性（Soundness）が保証されていません。また、LaM4Inv や LEMUR などの先行研究は、LLM の出力を「ノイズの多い記号材料」とみなし、複雑なフィルタリング、再構成、修復アルゴリズム（Houdini 法やバックトラッキングなど）を適用して使用可能な形に直すアプローチをとっています。これらは実装が複雑で、モデルの能力向上に伴い過剰な処理が必要になる可能性があります。

2. 手法：Quokka

Quokka は、LLM の出力を複雑に加工するのではなく、**「検証器（Verifier）による直接評価」**に焦点を当てたシンプルで健全なフレームワークです。

2.1 検証器ベースの評価アプローチ

Quokka は、LLM が提案した不変条件 $q$ が、ターゲットのアサーション $p^*$ を証明する際に有効かどうかを、以下の 2 つの並列な検証クエリで直接判定します。

1. 不変条件の正当性確認 ($d_a$): $q$ が実際にループ不変条件として正しいか検証する（V(P, ∅, q)）。
2. ターゲット証明の確認 ($d_b$): $q$ を仮定（assume）として追加した状態で、ターゲット $p^*$ が証明されるか検証する（V(P, {q}, p*}）。

この 2 つの結果に基づき、以下の判断を下します：

• 成功 (T): 不変条件が正しく、かつそれを用いてターゲットが証明された場合。
• 失敗 (F): 仮定 $q$ の下でもターゲットが反証された場合（または $q$ 自体が誤り）。
• 未決定 (U): タイムアウトや検証器の不完全性により結論が出ない場合。

このアプローチにより、LLM の出力を「証明候補」として直接扱い、複雑な記号処理や修復ロジックを排除しています。

2.2 実装と最適化

• 並列クエリ: 上記の 2 つの検証クエリを並列に実行し、レイテンシを削減します。
• 構文検証: 生成された述語が変数を更新する式（+= など）を含んでいないかなど、構文レベルのチェックを事前に行います。
• 学習とサンプリング:
  • 教師あり微調整 (SFT): 検証器（UAutomizer）が生成した正解の不変条件データセット（3,589 件）を用いてモデルを微調整します。
  • Best-of-N サンプリング: 複数の候補を生成し、検証器による検証時間が最も短い（最も効果的な）ものを選択します。

3. 主要な貢献

1. Quokka フレームワークの提案: LLM 生成の不変条件を、複雑な後処理なしに検証器で直接評価する、健全かつ高性能な評価フレームワーク。
2. 大規模ベンチマークの構築: SV-COMP（ソフトウェア検証コンペティション）から派生した866 件のインスタンスからなる評価データセット。これは既存の LLM ベース検証器の評価データセットの中で最大規模であり、複数のループ、関数、配列、ポインタを含む複雑なプログラムを含みます。
3. 包括的な評価: 9 つの最先端 LLM（Llama, Qwen, Claude, GPT 系列など）を対象とした評価。
4. 性能向上手法の検証: 教師あり微調整と Best-of-N サンプリングが、検証の加速において有意な改善をもたらすことを実証。

4. 実験結果

• モデル性能の差異: 最新かつ大規模なモデル（例：gpt-5.2, claude-opus-4.5）ほど、正しい不変条件の生成数と解決インスタンス数において優位でした。
  • 60 秒のタイムアウト条件下では、ベースライン（UAutomizer 単体）に対して最大 21 件追加のインスタンスを解決しました。
  • 500 秒のタイムアウトでは追加解決数は減少しましたが、依然として有効な加速が確認されました。
• 微調整と Best-of-N:
  • Qwen2.5-7B の微調整により、正しい不変条件数と解決インスタンス数がわずかに向上しました。
  • Best-of-N サンプリングは非常に効果的でした。特に $N=8$ の場合に最適化され、解決インスタンス数が最大化されました。
• 先行研究との比較:
  • Quokka（gpt-5.2 + Best-of-8）は、LaM4Inv、Clause2Inv、LEMUR、Loopy などの先行する LLM ベース検証器をすべてのタイムアウト閾値において凌駕しました。
  • 特に、LEMUR ベンチマーク（UAutomizer が 10 分以内に解決できない難問）においても、Quokka はより多くのインスタンスを短時間で解決しました。

5. 意義と結論

Quokka は、LLM を活用したプログラム検証において、「複雑なアルゴリズムによる修復」から「検証器による直接評価」へとパラダイムシフトをもたらしました。

• 単純さの優位性: 先行研究が抱えていた複雑な「クエリ・フィルタ・再構成」や「再帰的修復」の必要性を排除し、LLM の能力を最大限に引き出すシンプルな設計が、むしろ最高性能を実現しました。
• 健全性と実用性: 形式的検証器（UAutomizer）に基づく評価により、不変条件の正しさと実用的な加速効果を同時に保証しています。
• 将来展望: モデルの能力向上に伴い、LLM ベースの検証システムは、複雑なハブ（harness）を必要とせず、より直接的な評価と利用が可能になることを示唆しています。

本論文は、LLM を用いたプログラム検証における新しい SOTA（State-of-the-Art）を確立し、今後の研究の原理的な基盤を提供するものです。