第 10 章 — LLM で契約を生成する

10.1 発展課題（任意・★★★）：生成と検査のループ

概要。第 4〜9 章では契約を自分の手で書きました。この発展課題では、「応答は 5 秒以内」「低バッテリ機には割り当てない」といった自然言語の運行要件から LLM に CADL 契約を生成させ、cadl check を通るまで診断メッセージを返して自動修正させるループを構築し、評価します。LLM が提案し、型検査が門番をする——LLM の出力は検査を通るまで有効化しない、という構成が本質です。ただし、cadl check の合格は構文と型のレベルの検査であり、安全性の保証ではありません。合格が示すのはドラフトが CADL として整っていることだけで、期限や規則の内容が正しいことまでは示しません。

ポイント。

• 検査を通った契約が意図どおりとは限りません。合格したドラフトの deadline の値や監視ルールを、自分が第 5 章で手書きした契約と突き合わせてください（「合格 ≠ 意図一致」に気づくことがこの課題の最大の学びです）。
• 失敗時の診断メッセージは加工せずそのまま LLM に返すのが基本です。何を直せたか・直せなかったかを記録しましょう。
• 評価は回数の統計で行います：初回通過率（first_pass_rate）、K 回以内の通過率（pass@K）、通過までの平均ラウンド数。

ヒント。

• system prompt に CADL の文法制約（SoS type は 4 種のみ、識別子は ASCII、deadline: 5s の形式など）を明示すると、初回通過率の向上が期待できます。制約の有無で実際に測って比較するのも良い実験です。
• cadl check はサブプロセスとして呼び出せます（終了コードと出力を見る）。
• 現時点で公開されている参考実装はありません（著者らの実装である cadl-ai-governance リポジトリの step_a_design.py と measure_step_a.py は非公開です）。ループ本体と小さな計測スクリプトを書くことも、この課題の一部です。まず LLM の代わりに決定的なモック（決まった順にドラフトを返す関数）でループの動きを観察し、それから実 LLM に切り替えるのが安全です。