Each language version is independently generated for its own context, not a direct translation.

この論文「VeriStruct」は、**「AI が書いたコードの安全性を、AI 自身が徹底的にチェックして証明する」**という新しい仕組みを紹介しています。

専門用語を抜きにして、わかりやすい例え話で説明しましょう。

🏗️ 物語：AI 建築家と「完璧な設計図」

想像してください。AI が「リングバッファ（データを循環して蓄える箱）」のような複雑なデータ構造を設計しようとしています。
AI は非常に優秀で、コードを素早く書けます。しかし、AI には**「致命的な欠陥」**があります。

数学的な抽象化が苦手: 「この箱は、実際には円形に配置されているけど、中身は『並んだ列』として考えよう」というような、人間なら直感的にわかる「概念の整理」ができません。
特殊な言語のルールを知らない: 検証用の言語（Verus）には、「ここには計算してはいけない」「ここには『古い状態』を参照しなさい」といった厳格なルールがあります。AI はこれを無視して、普通のコードと同じように書いてしまい、エラーになります。

このままでは、AI が作ったコードは「バグだらけの危険な建物」になってしまいます。

🛠️ VeriStruct の登場：AI の「監督官」と「修理工」

そこで登場するのがVeriStructです。これは、AI にただコードを書かせるのではなく、**「AI 監督官」と「AI 修理工」**を配置して、完璧な設計図（検証コード）を作るシステムです。

1. 計画を立てる「監督官（プランナー）」

まず、AI 監督官が「この建物を安全にするには、何が必要か？」を考えます。

「この箱は『円形』だから、数学的な『列（シーケンス）』という概念に変換する必要がある（View モジュール）」
「箱の容量と位置関係にルールがあるから、『型不変量（Type Invariant）』というルールブックを作る必要がある」
「これらを証明するための『証明ブロック』も必要だ」

監督官は、必要な作業だけを順序立てて指示します。無駄な作業を省き、効率的に進めます。

2. 概念を整理する「抽象化の魔法」

AI は往々にして、コードの「中身（変数）」をそのまま羅列してしまいます。

AI の失敗例: 「箱の中身、頭の位置、尻尾の位置……全部そのまま書いちゃおう」
VeriStruct の修正: 「待て！重要なのは『中身がどう並んでいるか』だけだ。頭の位置や尻尾の位置は隠して、『並んだ列』という概念でまとめ直せ！」

このように、AI に「実装の細部」ではなく「本質的な概念」を捉えさせることで、複雑な証明を簡単化します。

3. 間違いを直す「修理工（リペア）」

AI が書いた設計図（アノテーション）は、完璧ではありません。

エラー: 「ここは『計算してはいけない場所』なのに、計算している！」
VeriStruct の対応: 検証ツールが「エラー！」と叫ぶと、**「修理工 AI」**が即座に駆けつけます。
- 「あ、これは『実行可能な関数』と『仕様関数』の使い分けミスだ」
- 「ルールブック（型不変量）を証明の文脈に追加すれば直る」
- 「テストが失敗しているから、関数の『約束事（仕様）』を強化しよう」

この「書く→チェック→直す」を何回も繰り返すことで、最終的に**「数学的に間違いがないこと」が証明されたコード**が完成します。

📊 結果：驚異的な成功率

このシステムを使って、11 種類の複雑なデータ構造（リングバッファ、木構造、並行処理のロックなど）をテストしました。

対象: 129 個の関数
成功: 128 個（99.2%）が自動で検証成功！
比較: 従来の「AI にただ書かせて直す」方法では、成功したのは半分以下でした。

💡 なぜこれが重要なのか？

これまでは、AI が書いたコードの安全性を証明するには、熟練した人間が何時間もかけて「証明の魔法（アノテーション）」を書き足す必要がありました。それは非常に大変で、専門知識が要る仕事でした。

VeriStruct は、**「AI が AI のコードを、AI 自身が厳格なルールでチェックし、自動修正する」**というサイクルを確立しました。これにより、AI が生成したコードが「バグなく、セキュリティ上も安全」であることを、人間が手作業で追わなくても保証できるようになります。

🌟 まとめ

VeriStruct は、AI の「速さ」と、形式検証（数学的な証明）の「厳密さ」を、「監督官」と「修理工」という役割分担によって融合させた画期的なシステムです。

これにより、AI が生み出す「山のようなコード」が、単なる「バグの山」ではなく、「安全で信頼できるインフラ」へと変わる未来が、一気に近づいたのです。

Each language version is independently generated for its own context, not a direct translation.

VeriStruct: Verus におけるデータ構造モジュールの AI 支援型自動検証に関する技術的サマリー

本論文は、Rust 言語の形式検証ツール「Verus」において、単一関数からより複雑なデータ構造モジュールへと AI 支援型自動検証の範囲を拡大する新しいフレームワーク「VeriStruct」を提案したものです。

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

1. 背景と問題定義

生成 AI はコード解析能力に優れていますが、AI 生成コードや AI 支援開発によるバグやセキュリティ脆弱性のリスクも増大しています。プログラム検証（形式検証）はこれらのリスクを数学的に証明することで軽減できますが、従来の検証には高度な専門知識と膨大な手作業によるアノテーション（事前条件、事後条件、不変条件など）の作成が必要でした。

近年、大規模言語モデル（LLM）を用いた自動検証の研究が進んでいますが、既存の手法は主に単一関数や教科書的なアルゴリズムに限定されていました。データ構造モジュールの検証には、以下の点で追加の難易度があり、既存の手法では対応が困難でした。

数学的抽象化（View）の必要性: データ構造の内部状態を、検証器が論理的に扱える抽象的な数学的表現（例：シーケンス、集合）へ変換する必要がある。
型不変条件（Type Invariants）の維持: データ構造の操作が、オブジェクトが満たすべき論理的な制約（例：インデックスの範囲、容量の正しさ）を破らないことを保証する必要がある。
複数メソッドの共同検証: 単一の関数ではなく、共有された不変条件の下で複数のメソッドを統合的に検証する必要がある。
Verus 特有の構文とセマンティクス: LLM は Verus の特殊な構文（仕様関数のみ呼び出し可能など）や検証固有のセマンティクスを理解しておらず、構文エラーや意味論的な誤りが頻発する。

2. 提案手法：VeriStruct

VeriStruct は、LLM を活用しつつ、データ構造モジュールの検証を成功させるための体系的なワークフローと修復メカニズムを提供します。

2.1 全体アーキテクチャ

入力として、検証対象の Rust ソースコードと、その意図された動作を示す単体テストスイートを受け取ります。出力は、Verus 検証器をパスする完全なアノテーション付きコードです。
プロセスは以下の 2 つのステージで構成されます（アルゴリズム 1）。

ステージ 1: アノテーション生成 (GenAnnos)
- プランナーモジュール: 検証タスクを分析し、必要な生成モジュール（View, 型不変条件, 仕様, 証明ブロック）の組み合わせを決定します。すべてのモジュールを常に実行するのではなく、タスクに応じて選択的に実行することで、LLM の不安定性や計算コストを削減します。
- 専用生成モジュール:
  - View モジュール: データ構造の数学的抽象化（例：リングバッファをシーケンスと容量のペアとして表現）を生成します。
  - Type Invariant モジュール: 型不変条件（フィールド間の関係性や範囲制約）を生成します。
  - Specification モジュール: 事前条件（requires）、事後条件（ensures）、仕様関数を生成します。
  - Proof Block モジュール: 証明のヒントやループ不変条件を生成します。
- プロンプト設計: 各モジュールには、Verus の構文ガイドライン、ステップバイステップの指示、および他の検証済みデータ構造の例（In-context learning）が含まれた専用プロンプトが使用されます。
ステージ 2: アノテーション修復 (RepairAnnos)
- 生成されたコードは Verus 検証器に渡され、エラーが発生した場合、修復ループに入ります。
- エラー分類と修復: 検証器からのエラーメッセージをパターンマッチングし、適切な修復モジュールを呼び出します。
  - 例：実行可能関数を仕様文脈で誤って呼び出した場合、対応する仕様関数版を作成して置換する。
  - 例：テストアサーションの失敗に対して、直前のメソッドの事後条件を強化する。
- 反復処理: 最大反復回数（ $m$ ）まで、エラーを特定・修正・再検証を繰り返します。各修復ステップでもサンプリング（ $n$ 回生成）を行い、最も検証成功数が多いものを選択します。

2.2 技術的工夫

構文ガイドラインの埋め込み: Verus のチュートリアルや標準ライブラリから構文ルールを抽出し、プロンプトに明示的に含めることで、構文エラーを低減。
View の洗練（Refinement）: LLM が初期に生成しがちな「すべてのフィールドを単純にマッピングする」ような非抽象的な View に対し、抽象化と最小性を促す追加のプロンプトステップを導入し、論理的な本質に焦点を当てた View を生成させます。
テストスイートの活用: 生成された仕様が開発者の意図と合致しているか、また自明な仕様（vacuous specifications）でないかをテストスイートで検証します。

3. 主要な貢献

データ構造モジュール向けの新しい LLM 支援ワークフローの提案: 単一関数検証を超え、View、型不変条件、複数メソッドの共同検証を含む複雑なタスクを自動化するパイプラインを設計。
VeriStruct ツールの実装: 上記ワークフローを具現化したツールの実装と公開。
大規模ベンチマークによる評価: 11 の Rust データ構造モジュール（リングバッファ、ツリー、並行データ構造など）を用いた評価により、その有効性を実証。

4. 評価結果

ベンチマークセット: Verus 公式リポジトリおよびオープンソースから選ばれた 11 のモジュール（計 129 関数）。
性能:
- VeriStruct: 11 のベンチマークのうち10を完全解決。合計**128/129 関数（99.2%）**の検証に成功。
- ベースライン（単純な LLM 反復）: 4/11 のベンチマーク、52/129 関数（40.3%）のみ。
- Claude Code（自律エージェント）: 8/11 のベンチマーク、102 関数（79.1%）。VeriStruct よりも劣る結果となりました。
効率性: VeriStruct は、より新しいモデル（Claude Sonnet 4.5）を使用するエージェントよりも少ないトークン数（平均 22k トークン vs 24k）で、より高い検証成功率を達成しました。
ケーススタディ（Bitmap）: 人間が作成した複雑な 2 次元配列の抽象化に対し、LLM はより単純な 1 次元配列の抽象化を見出し、同等の検証成功を収める異なる解決策を生成しました。

5. 意義と将来展望

実用性の向上: 形式検証の導入障壁を下げ、AI 生成コードを含む大規模な Rust コードベースの信頼性を高める可能性を示しました。
ライブラリ検証の基盤: データ構造ライブラリ自体を検証可能にすることで、それを依存する上位コードの検証負担を軽減します。
将来の方向性:
- 検証に必要な補題（Lemma）の検索を支援する RAG（Retrieval-Augmented Generation）の統合。
- 並行データ構造の検証に必要なリソース代数ライブラリの合成支援。
- 構文エラーを減らすための制約付きデコーディング技術の適用。
- 単体テストスイートの自動生成による、完全な検証パイプラインの構築。
- 検証成功を報酬信号とする強化学習（RL）による仕様推論の最適化。

本論文は、AI 支援による形式検証が「単一関数」の域を超え、「複雑なデータ構造モジュール」の検証へと飛躍した重要なステップであり、将来的に検証済みで再利用可能なコードライブラリの自動生成への道を開くものと言えます。

VeriStruct: AI-assisted Automated Verification of Data-Structure Modules in Verus