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

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

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

F.1 AI 時代の前提

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

F.2 信頼境界（Trust Boundary）

  • LLM/エージェント: 提案者（untrusted）
  • 検証器（TLC/Alloy/Lean/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として保存され、再現可能
  • 例外（検証スキップ）の条件と承認フローが定義されている
  • ツールのバージョンが固定され、キャッシュ/再現性が担保されている

F.10 Lean/Rocq/LLM 支援証明の運用チェックリスト

LLM 支援で Lean、Rocq、Isabelle などの証明を扱う場合は、次の順序を標準にします。

  1. LLM が定理文、不変条件、補題、証明スクリプトの候補を生成する。
  2. 人間が、要求との対応、境界条件、例外、捨象した前提をレビューする。
  3. 証明器、型検査器、SMT ソルバー、模型検査器が候補を検査する。
  4. CI が同じバージョン、同じ依存、同じ設定で再実行し、ログと artifact を保存する。
  5. 人間レビューで、未検証範囲、例外承認、実務上のリスクを記録する。

必須チェックリスト：

  • LLM が生成した定理文、不変条件、補題、前提条件を、人間が要求仕様と照合した。
  • sorry、admit、未検証 axiom、未検証 assume、検証スキップを CI で検出する。
  • Lean/Rocq/Isabelle などのバージョン、依存ライブラリ、lock file、タイムアウト、乱択 seed を PR に記録する。
  • LLM に反例説明をさせた場合でも、元の反例ログ、proof state、ゴール、trace を artifact として保存する。
  • ベンチマーク成功率、コンペティション成績、論文の pass ratio を、そのまま実務性能や仕様妥当性として扱っていない。
  • 自然言語要求から形式仕様へ変換したときに、捨象した前提、対象外ケース、手作業で補った形式化を明記した。
  • 「LLM → 検証器 → CI → 人間レビュー」の順序を崩さず、LLM 出力を直接マージ条件にしていない。

CI では、未完了マーカーを単純な文字列検索だけに頼らず、対象言語の構文と運用例外を確認します。 たとえば Lean では sorry や追加 axiom、Rocq では Admitted. や不要な公理、仕様系では assume や検証スキップを棚卸しします。 例外として残す場合は、Issue、期限、承認者、影響範囲を例外台帳に書きます。

F.11 生成 AI 出力検査と証明支援の切り分け

LLM 支援証明と、Amazon Bedrock Guardrails Automated Reasoning checks のような生成 AI 出力検査は、どちらも AI 時代の形式手法に見えるが、検査対象が異なる。

観点 LLM 支援証明 生成 AI 出力検査
LLM の役割 定理文、補題、証明スクリプト、反例説明の候補生成 業務応答や説明文の生成元
仕様 形式仕様、定理、補題、不変条件 業務ルール、ポリシー、ドメイン知識から抽出した論理
判定者 Lean/Rocq/SMT/模型検査器/CI 形式化されたポリシーに対する検査器/ガードレール
未検証範囲 sorry、admit、公理、変換、証明器外の要求妥当性 ポリシー外の事実、自然言語から論理への変換、プロンプトインジェクション、オフトピック
PR 証跡 toolchain、lockfile、proof state、ログ、例外台帳 ポリシー版、入力/出力、検査結果、除外範囲、サービス仕様

いずれの場合も、「AI が正しい」とは扱わない。 LLM 出力を未信頼入力として受け取り、検証器・検査器・CI・人間レビューの順に証跡を閉じる。

F.12 テスト戦略との責務分界と PR 証跡

AI 支援で仕様、テスト、証明スケッチを同時に生成すると、どの活動が何を保証したのかが曖昧になりやすくなります。PR では次のように責務と証跡を分けてください。

観点 確認すること 残す証跡
仕様差分 要求、用語、状態、イベント、不変条件のどれを変えたか 変更前後の仕様、関連 Issue、非目標
テスト差分 仕様差分から追加・変更したテスト/eval/benchmarkがあるか 実行コマンド、入力データ、期待結果、失敗ログ
検証差分 Alloy/TLA+/Dafny 等で確認した性質が仕様差分と対応しているか 性質名、スコープ、深さ、seed、ツールバージョン
レビュー差分 未検証範囲、抽象化、例外承認、運用影響を確認したか review thread、残リスク、採用しなかった手法の理由

形式仕様で見つかった反例はテストケース化し、テストで見つかった欠陥は仕様や不変条件の不足として見直します。どちらか一方だけを「品質保証の最終根拠」にしないでください。

GitHub で原稿を編集