形式的手法の基礎と応用
English
  1. ホーム
  2. Appendices
  3. 付録f：ai支援で形式仕様/検証を回す実践ガイド

付録F：AI支援で形式仕様/検証を回す実践ガイド

この付録は、AI支援で仕様作成・検証を回すための実践テンプレートをまとめたものです。AIの出力は「提案」として扱い、最終判定は検証器（TLC/Alloy/Rocq（旧称：Coq）/Dafny等）に寄せる前提で運用してください。

F.1 AI時代の前提

  • 生成は速いが、誤りも速い。
  • 仕様・不変条件・証明スケッチの生成はAIが得意。
  • 合否判定は検証器とCIで行う。

F.2 信頼境界（Trust Boundary）

  • LLM/エージェント: 提案者（untrusted）
  • 検証器（TLC/Alloy/Rocq（旧称：Coq）/Dafny）: 判定者（trusted）
  • CI: 執行者（再現性の担保）

この境界を崩すと、AIの誤りが品質保証の誤りに直結します。

F.3 ワークフロー（テンプレ）

  1. 要求（目的/禁止事項）を短文で明確化
  2. 用語定義（名詞の境界・同義語）を整理
  3. 不変条件（常に成り立つ性質）を列挙
  4. モデル化（小スコープ/浅い探索）
  5. 反例の確認 → 原因分析
  6. 修正 → 再検証（再現性確保）

CIでは「PR/夜間/リリース前」で深度を段階化し、検証コストを制御します。

F.4 プロンプトテンプレ（コピペ用）

1) 仕様抽出

あなたは仕様担当です。以下の要求から、用語定義、状態、イベント、不変条件、許容しない振る舞いを抽出してください。
要求: <要求テキスト>
出力形式: 用語/状態/イベント/不変/禁止事項

2) Alloy雛形生成

以下の用語定義と不変条件をAlloyのsig/fact/assertに変換してください。小スコープで検証可能な雛形にしてください。
用語: <用語定義>
不変: <不変条件>

3) TLA+雛形生成

以下の状態とイベントから、TLA+のInit/Next/Specを作成してください。必要な変数と不変条件も含めてください。
状態: <状態>
イベント: <イベント>
不変: <不変>

4) 反例トレースの要約

以下の反例トレースを要約し、原因の候補と修正案を3つ提示してください。
反例: <トレース>

5) PR向け検証チェックリスト

以下の変更に対して、必要な検証チェック項目と実行コマンドを列挙してください。
変更内容: <PR差分要約>

F.5 エージェント運用ガイド

Issue作成時

  • 受け入れ条件（検証で合否判定可能な形）
  • 非目標（やらないこと）
  • 実行コマンド（検証器/テスト）

PRレビュー時

  • 仕様差分と検証差分が一致しているか
  • 検証ログ（seed/深さ/スコープ）を添付しているか
  • 反例が出た場合の修正手順が残っているか

F.6 反例→修正→再検証の例（最小）

  • 反例: FIFOを満たさないトレースが出力
  • 原因: Dequeue操作の前提条件が弱い
  • 修正: 空キュー時のDequeueを禁止する不変を追加
  • 再検証: seed/深さ/スコープを固定して再実行

F.7 PRに添付すべき成果物

  • 検証ログ（コマンド/seed/深さ/スコープ）
  • 反例トレース（ファイル名・再現手順）
  • 変更の意図（仕様差分の要約）
  • 実行環境（OS/ツールバージョン）

本付録のテンプレートは、チーム内の標準運用ルールとして流用できます。

F.8 反例トリアージテンプレ（事実/仮説を分離）

反例の処理では、「ログに書かれている事実」と「原因の推測」を混ぜないことが重要です。
AIは要約や観点列挙に有用ですが、事実欄はログ/トレースから転記し、仮説欄は別枠に分離してください。

テンプレファイル（リポジトリ内）：templates/counterexample-triage.md（以下にも同内容を掲載）

テンプレ（コピペ用）

## 検証対象
- 対象（仕様/実装/設定）:
- 期待する性質（安全/活性/不変/契約）:
- 変更差分の要約:
- 関連Issue/PR:

## 実行環境（事実）
- OS/CPU:
- 実行場所（ローカル/CI）:
- ツール/バージョン:
  - Alloy:
  - TLC:
  - Apalache:
  - Dafny:

## 再現手順（事実）
- command:
- seed:
- scope/depth/length:
- time-limit:
- artifact（ログ/反例）:

## 観測された事実（ログ/トレース抜粋）
- どの性質が破れたか:
- 反例の最短トレース（要約）:

## 仮説（原因候補）
- H1:
- H2:
- H3:

## 修正案（候補）
- Fix案1:
- Fix案2:

## 再検証
- 再実行コマンド:
- 結果（OK/NG）:
- 学び（再発防止策）:

F.9 AI生成物の品質保証チェックリスト（仕様/証明/CI）

AI生成物を含む変更は、次の観点で「検証可能な成果物」へ落とし込む。

仕様（自然言語/Alloy/TLA+）

  • 用語定義が明確（同義語、境界、単位、例外条件）
  • 前提条件（環境仮定、公正性、障害モデル）が明示されている
  • 不変条件（安全性）が列挙され、破れたときの意味が説明できる
  • 活性（必要な場合）が定義され、過剰な仮定で「見かけ上成立」していない
  • 数値（%/倍/件数）は出典付き、または例示であることを明記

証明/模型検査（再現性）

  • 何をチェックしたか（性質名、範囲、スコープ/深さ/長さ）が明確
  • 実行条件（seed、上限時間、探索上限）が記録されている
  • 反例が出た場合、反例の再現手順と最小トレースが残っている
  • 「直した結果」を再検証し、回帰（同系統の性質）も確認している

CI（ゲート設計）

  • PR/夜間/リリース前で検証深度が段階化されている
  • 失敗時にログ/反例がartifactとして保存され、再現可能
  • 例外（検証スキップ）の条件と承認フローが定義されている
  • ツールのバージョンが固定され、キャッシュ/再現性が担保されている
GitHub で原稿を編集