🧩 シナリオ誘導で設計意図を絞る検証付き LLM 合成 - Concept Design と foundry

Concept Design は、アプリケーションを「概念」という再利用可能な部品の合成として設計する手法です。2026-07-17 に arXiv へ投稿された論文 Verified LLM-Driven Synthesis for Concept Design は、この手法に空白のまま残っていたリアクションの形式意味論を与えます。そのうえで、LLM が設計候補を提案し Alloy 6 の有界モデル検査が反例を返す CEGIS 型の合成手順を提案します。

本記事の中心は、論文が実測で示した次の結果です。不変条件を渡すだけでは意図した設計に収束せず、肯定・否定シナリオで誘導すると意図の再現性が上がります。論文本文 (LaTeX ソース) と参照実装 foundry のソースコードを一次情報として、構造・データ・構築・利用・運用を整理します。

評価規模の注意: 論文の主評価は 3 アプリケーション・12 設計バリアント・単一 LLM 構成 (gpt-5.5) です。検証は Alloy 6 の有界モデル検査であり、指定したスコープとステップ数の範囲で反例が出ないことの確認にとどまります。一般化された性能比較としてではなく、設計の過少仕様を発見する手順として読むのが妥当です。

概要

Concept Design とは

Concept Design は Daniel Jackson が提唱したソフトウェア構造化手法です。

アプリケーションを「概念(concept)」という再利用可能な部品の合成として捉えます。

概念は認証・ラベリング・共有・通知・アクセス制御など、焦点を絞った目的を持つ単機能のミニアプリです。

概念単体が持つのは、状態と「アクション(action)」の集合だけです。

複数の概念を組み合わせて 1 つのアプリケーションにするときは、概念間の協調ロジックを記述します。

この協調ロジックを表すのが「リアクション(reaction)」です。

リアクションは同期規則です。ある概念のアクションが発生したとき、条件を満たせば、別の(または同じ)概念のアクションを起動します。

アプリケーション全体で満たすべき安全性は「不変条件(invariant)」として宣言します。

4 つの用語の関係を次に示します。

本論文が新しく提案したこと

Concept Design は 2021 年の提唱以来、概念とその合成規則を記述する方法論として発展してきました。

一方でリアクションの形式意味論は空白のままでした。

形式意味論の空白は、次の 3 つを阻みます。

• 設計の意味を厳密に述べること
• 不変条件の保持を検証すること
• 安全な協調ロジックを合成すること

本論文は、この形式意味論を初めて与え、それを土台に LLM 駆動の合成手順を提案します。

合成手順は「不変条件を渡すだけでは、ユーザーが意図した設計に収束する保証がない」という問題に直面します。

同じ不変条件を満たす設計は複数存在します。その中には不合理な設計や、ユーザーが許容したい挙動まで禁止する設計も混ざります。

この問題に対し、本論文は「肯定・否定シナリオ」という検証可能な誘導手段を提案します。

本論文の 3 つの貢献

関連技術との関係

検証は Alloy 6 の有界モデル検査です。

指定したスコープとステップ数の範囲内で反例が見つからないことを確認する手法です。適用範囲は有界にとどまり、無限範囲の完全な証明とは区別します。

4 方式の比較

ユーザーの意図を設計に反映させる方式は 4 通りあります。

論文の評価(3 アプリケーション・12 設計バリアント・単一 LLM 構成 gpt-5.5)における実測値を示します。

検証に達するまでの平均イテレーション数を次に示します。

特徴

• リアクションを「監視モニタ半オートマトン」として定義する
  • 概念オートマトンとの同期合成でアプリケーション全体の遷移系を構成する
• 不変条件の保持を検証する
  • 「不変条件が破れていない状態で反応してしまう」過剰反応も同時に検証する
• LLM の役割を 2 つに分けて使う
  • 1 つ目はリアクション候補の提案
  • 2 つ目は Alloy への翻訳
  • Alloy 翻訳エージェントは論文が主張する貢献の対象外
  • 将来は Alloy 翻訳を形式言語に置き換える計画がある
• シナリオは機械検証できる誘導 artifact
  • この点でシナリオは自然言語プロンプトと本質的に異なる
  • ok シナリオが不可能と判定されれば、それ自体が候補設計を却下する根拠になる
  • nok シナリオが可能と判定された場合も同様に却下の根拠になる
• シナリオ抽出はユーザーが分類するだけで済む対話形式
  • LLM が不変条件違反に至る短いアクション列(prefix)を提案する
  • LLM が修復候補(suffix)も提案する
  • ユーザーの作業は提案されたシナリオの分類のみ
• 評価対象は 3 アプリケーション
  • 対象は NoDeadSensitiveMessages / CourseManagementSystem / OneTimeEvidenceLinks
  • 各アプリケーションは 2 つの部品概念を合成したもの
  • 部品概念は DeadLetterQueue / Label / Rostering / Registration / Vault / Permalink の 6 つ
  • 部品概念の位置づけは、アプリケーションを構成する再利用単位
• 論文の主評価は単一 LLM 構成
  • モデルは gpt-5.5
  • 温度は 1、reasoning effort は medium
  • 各条件 3 独立 run
• 論文は主評価に加えて、Claude Fable 5 による補助のクロスモデル確認も明示的に実施している
  • 対象はシナリオ誘導合成のみ、各バリアント 1 run で実行した
  • 12 バリアントすべてで意図した設計に収束した
  • 6 バリアントは初回収束、2 回超を要したのは 1 バリアントのみ
  • 論文自身は「系統的なモデル間比較には不十分」と留保している
  • そのうえで「効果が gpt-5.5 固有ではない初期的な証拠」と位置づけている
  • リポジトリの examples/ にある *_fable-5_run1.md はこの補助確認の成果物であり、主評価とは異なる位置づけとして区別する
• 頻出する品質面の失敗は冗長性
  • 意図した設計と等価でも、冗長なリアクションや冗長な事前条件が混入する場合がある
  • 発生頻度は、意図した設計を得られた実行のうち 15/82 回

構造

論文が提案する検証付き LLM 合成手法と、参照実装 foundry の合成パイプラインを C4 モデルの 3 段階で示します。

システムコンテキスト図

コンテナ図

コンポーネント図

本節は C4 のコンポーネント階層を、各コンテナの内部処理フローとして描きます。foundry の設計の本質は「どの順で LLM と Alloy を呼ぶか」にあります。そこで要素間の静的な依存関係はコンテナ図で示し、ここでは各コンテナ内部の制御フローを図示します。以降の図はいずれもコンテナ 1 つのドリルダウンであり、ノードは実装の関数に対応します。

CLI オーケストレーター: CEGIS ループ (synthesize コマンド)

foundry.py の main 内で実装される、reaction 合成・Alloy 翻訳・有界モデル検査・反例フィードバックの反復です。論文 Figure 2 (§4.1) の scenario-guided synthesis loop に対応します。

補足として、interactive コマンドは同じ CEGIS 構造を人間参加型に変えた変種です。反例が見つかるたびに LLM が複数の代替 reaction 案 (--num-alternatives 件) を提示し、レビュアーが採否や再提案要求 (regenerate) を選びます。反復回数の上限は --max-iterations (既定 20) で、検査対象は不変条件のみです。verify コマンドは reaction 合成を省き、完成済みアプリ記述を Alloy へ翻訳して検査するだけの一方向フローです。

Reaction 合成コンポーネント

Alloy 翻訳コンポーネント

Alloy 実行検証コンポーネント

反例解析コンポーネント

シナリオ管理コンポーネント

既存シナリオの抽出・整理に加え、論文 Figure 3 (§4.2) のシナリオ提案手順 (接頭辞 P の分類と修復接尾辞 F の探索) を実装します。

モデルプラットフォーム抽象化コンポーネント

データ

概念モデル

App が Concept を所有し、Concept が Action と Invariant を所有します。Scenario と Counterexample は Action の並びとして App に属します。Reaction は複数 Concept の Action をまたいで同期するため、所有ではなく利用 (呼び出し) 関係で表現します。

Reaction を Concept の子に置かない理由は、Concept Design の中心的な設計原則にあります。concept は「単体で理解でき、他の concept から独立した自己完結の単位」であることが要件です。Reaction を特定の concept に所有させると、その concept が相手の concept を知る形になり、独立性が崩れます。Reaction を App の直下に置くと、concept の再利用性を保ったまま、App ごとに異なる同期規則へ差し替えられます。実際に examples/ では、同じ DeadLetterQueue concept を異なる App が異なる Reaction 付きで再利用します。

情報モデル

論文の形式意味論 (arXiv:2607.15718 Section 3) と README.md の App Description フォーマット、foundry_common.py のパーサ実装に基づく属性です。論文本文に記載がある属性と、実装から補った属性を区別し、後者には「実装から補完」と注記します。

Action と Reaction の違い

positive scenario と negative scenario の違い

positive/negative scenario は、Invariant だけで一意に定まらない設計空間を絞り込みます。同じ Invariant を満たす設計は複数存在し得るため、Scenario が「ユーザーが意図する設計」を検証可能な形で追加制約します。

Invariant と Scenario の役割の違い

Alloy 6 への翻訳対応

Alloy 6 のモデル検査は、非決定的な次アクション選択を 1 つの action 変数 a で表現します。遷移関数が未定義な場合はシステムを stutter させ、遷移関係を全域化します。Alloy 6 を選ぶ理由は、次状態演算子 \bigcirc を含む完全な線形時相論理をサポートし、Scenario の可能性判定に使えるためです。

構築方法

前提条件

インストール手順

1. リポジトリを clone します。

git clone https://github.com/alcinocunha/foundry.git
cd foundry

2. 使用するプラットフォームに応じて、任意で Python パッケージを追加インストールします。

pip install anthropic  # claude-api を使う場合
pip install openai     # gpt-api または deepseek-api を使う場合

codex-cli のみを使う場合、この手順は省略できます。

必要な環境変数

Foundry はモデル名からプラットフォームを推論します。推論できない場合は --platform / --platform-reactions / --platform-alloy / --platform-scenarios のいずれかで明示指定します。

Alloy 実行ファイルの準備

• 既定では alloy という名前で PATH を検索します。別名 alloy6 も自動で候補に含めます。
• PATH で見つからない場合、追加の候補ディレクトリ (~/.local/bin 等) を探索します。
• アプリケーションバンドルの探索 (/Applications/Alloy*.app 等) は macOS 限定です。実装の platform_app_candidates が sys.platform != "darwin" で空リストを返すため、Linux と Windows では PATH と候補ディレクトリのみが対象になります。
• 見つからなかった場合はエラーにはならず、指定した文字列がそのまま実行コマンドとして使われます。実行時にコマンドが存在しなければ失敗します。
• 明示的に指定したい場合は --alloy-exec <パスまたはコマンド名> を渡します。

python3 foundry.py verify \
  --model-alloy gpt-5.5 \
  --alloy-exec /opt/alloy/bin/alloy6 \
  examples/NoDeadSensitiveMessages1.md

利用方法

必須パラメータ一覧

コマンドごとの必須パラメータです。個別の例に先立って、まずここで全体像を把握してください。

--model-* に渡すモデル名からプラットフォームを推論できない場合は、対応する --platform-* (または --platform) の指定も必須になります。

コマンドの選び方

CLI リファレンス

すべてのサブコマンドに共通する --help の呼び出し方です。

python3 foundry.py --help
python3 foundry.py <command> --help

共通オプション

--platform と --codex-exec は synthesize / interactive / verify / scenarios の全サブコマンドに共通です。

synthesize

interactive

verify

verify には --output-file がありません。新しい app description を生成せず、既存の設計を検証するだけのコマンドだからです。

scenarios

scenarios には --alloy-exec / --top-scope / --output-dir がありません。Alloy を使わないコマンドだからです。

App Description の書き方

App Description は、部分的な app 定義から完全な app 定義まで、同じフォーマットの Markdown コードブロックで記述します。使用できるセクション名は次の 7 つです。

最小構成の例です (examples/NoDeadSensitiveMessages.md)。

application: NoDeadSensitiveMessages
types:
    a set Message
    a set Tag
    one special Tag named Sensitive
concepts:
    one DeadLetterQueue[Message] named Q
    one Label[Message,Tag] named L
invariants:
    there are no dead messages in Q labeled with Sensitive in L

prompt セクションを追加すると、自然言語プロンプトで合成を誘導できます (examples/NoDeadSensitiveMessages1Prompt.md)。

application: NoDeadSensitiveMessages1Prompt
types:
    a set Message
    a set Tag
    one special Tag named Sensitive
concepts:
    one DeadLetterQueue[Message] named Q
    one Label[Message,Tag] named L
invariants:
    there are no dead messages in Q labeled with Sensitive in L
prompt:
    Tagging a dead message as sensitive triggers a retry.
    All other problematic behaviors must be forbidden.

synchronizations セクションまで含めた完成形の例です (examples/NoDeadSensitiveMessages1.md)。verify コマンドはこの形式の app を入力に取ります。

application: NoDeadSensitiveMessages1
types:
    a set Message
    a set Tag
    one special Tag named Sensitive
concepts:
    one DeadLetterQueue[Message] named Q
    one Label[Message,Tag] named L
invariants:
    there are no dead messages in Q labeled with Sensitive in L
scenarios:
    nok: Q.submit(m); L.affix(m,Sensitive); Q.fail(m)
    ok:  Q.submit(m); Q.fail(m); L.affix(m,Sensitive); Q.retry(m)
synchronizations:
    reaction retry_sensitive_dead_message
    when
        L.affix(m,Sensitive)
    where
        m is in dead in Q
    then
        Q.retry(m)
    reaction prevent_sensitive_failure
    when
        Q.fail(m)
    where
        Sensitive is a label of m in L
    then
        error

concepts 節で参照した concept ごとに、定義ファイルが必要です。ファイル名は <Concept名>.md を Foundry が自動推測します。DeadLetterQueue.md の例です。

concept: DeadLetterQueue[Message]
purpose: To process messages while isolating failed messages for later retry.
principle: A submitted message is pending until it succeeds or fails; failed messages can be retried individually, but clearing the dead-letter queue purges all failed messages.
state:
    pending: set Message
    dead: set Message
actions:
    submit(m:Message)
        requires: m is not in pending or dead
        effects: adds m to pending
    succeed(m:Message)
        requires: m is in pending
        effects: removes m from pending
    fail(m:Message)
        requires: m is in pending
        effects: moves m from pending to dead
    retry(m:Message)
        requires: m is in dead
        effects: moves m from dead to pending
    purge()
        requires: dead is not empty
        effects: removes all messages in dead
invariants: pending and dead are disjoint

自動推測に頼らずファイルを明示したい場合は --concept-files を使います。

python3 foundry.py synthesize \
  --model-reactions gpt-5.5 \
  --model-alloy gpt-5.5 \
  --concept-files examples/DeadLetterQueue.md examples/Label.md \
  examples/NoDeadSensitiveMessages.md

Scenario ファイルの書き方

• scenarios セクションの各行は ok: または nok: で始まる分類ラベルに続けて、; 区切りのアクション列を書きます。
• ok: は「許容される挙動」、nok: は「起きてはならない挙動」を表します。

scenarios:
    nok: Q.submit(m); L.affix(m,Sensitive); Q.fail(m)
    ok:  Q.submit(m); Q.fail(m); L.affix(m,Sensitive); Q.retry(m)

scenarios コマンドでシナリオを elicit した場合も、同じ ok: / nok: 形式で app description の scenarios 節に追記されます。

scenarios:
    ok: Q.submit(m1); Q.fail(m1); L.affix(m1, Sensitive);
    ok: Q.submit(m1); Q.fail(m1); L.affix(m1, Sensitive); Q.retry(m1);
    nok: L.affix(m1, Sensitive); Q.submit(m1); Q.fail(m1);

対話中の分類入力は [o]k / [n]ok / [s]kip / [q]uit の 4 択です。

主要ユースケース別のコマンド例

① 不変条件のみで合成する

invariants だけを頼りに synthesize を実行します。prompt も scenarios も持たない最小構成の app を渡します。

python3 foundry.py synthesize \
  --model-reactions gpt-5.5 \
  --model-alloy gpt-5.5 \
  examples/NoDeadSensitiveMessages.md

② 自然言語プロンプトで誘導する

prompt セクションを含む app description を渡します。

python3 foundry.py synthesize \
  --model-reactions gpt-5.5 \
  --model-alloy gpt-5.5 \
  examples/NoDeadSensitiveMessages1Prompt.md

反例ごとに人が候補を選びたい場合は interactive を使います。

python3 foundry.py interactive \
  --model-reactions gpt-5.5 \
  --model-alloy gpt-5.5 \
  --num-alternatives 3 \
  examples/NoDeadSensitiveMessages1Prompt.md

③ シナリオで誘導する

ok: / nok: で分類済みのシナリオを含む app description を渡します。

python3 foundry.py synthesize \
  --model-reactions gpt-5.5 \
  --model-alloy gpt-5.5 \
  examples/NoDeadSensitiveMessages1Scenarios.md

対話的に反例ごとの代替案を選びたい場合です。

python3 foundry.py interactive \
  --model-reactions gpt-5.5 \
  --model-alloy gpt-5.5 \
  --num-alternatives 3 \
  examples/NoDeadSensitiveMessages1Scenarios.md

④ 既存設計の検証のみを行う

synchronizations まで完成した app description を verify に渡します。reactions は生成しません。

python3 foundry.py verify \
  --model-alloy gpt-5.5 \
  examples/NoDeadSensitiveMessages1.md

⑤ シナリオ抽出 (elicitation)

scenarios コマンドで新しいシナリオを 1 件ずつ提案させ、対話的に ok / nok / skip / quit で分類します。--batch-size 件たまるごとに継続確認が入ります。

python3 foundry.py scenarios \
  --model-scenarios gpt-5.5 \
  examples/NoDeadSensitiveMessages.md

バッチサイズを変えたい場合です。

python3 foundry.py scenarios \
  --model-scenarios gpt-5.5 \
  --batch-size 5 \
  examples/NoDeadSensitiveMessages.md

運用

評価スコープ

出典: 論文 §5.1 Benchmark (Table 1: アプリケーション, Table 2: 12 設計変種)。

foundry の評価結果を、採用可否の判断材料に翻訳します。

対象範囲は以下のとおりです。

評価の中核は「3 アプリ・12 変種・単一 LLM (gpt-5.5) 構成」です。Claude Fable 5 の結果は限定的な追試にとどまります。この 2 つを区別して読んでください。

検証時間の実測値 (RQ1)

出典: 論文 §5.2 Efficiency of Design Verification (Table 3)。

測定方法

• 手書きの意図設計 (examples/*N.md) を対象に、check Design コマンドの実行時間だけを計測します。LLM による Alloy 翻訳・反応生成の時間は計測の対象外です。
• スコープ (各型の最大エンティティ数) を 2〜4 で振りステップ数 (bounded trace の長さ) を 10 に固定する系列と、ステップ数を 8〜12 で振りスコープを 3 に固定する系列の 2 系列を計測します。
• 各条件を 3 回実行し、平均秒数を報告します (再現用スクリプト scripts/benchmark_verification_times.py は合格 (pass) した run のみを平均に使い、time.perf_counter() で check Design の Alloy 呼び出し区間だけを計測します)。

python3 scripts/benchmark_verification_times.py \
  --model-alloy gpt-5.5 --alloy-exec /path/to/alloy

実測値 (平均秒、N=3 run/条件)

太字は既定値 (scope3・step10) です。Alloy Analyzer 自体の既定値でもあります。

読み取り

• スコープを 1 段上げるコストは、ステップ数を 1 段上げるコストより一貫して大きいです。CourseManagementSystem の一部変種では scope3→4 で 1 桁以上増えます (変種 4 は 34.81 秒→745.48 秒)。
• scope3・step10 なら全 12 変種が 1 分未満で検証できます。この条件が「対話的な CEGIS ループを回せる」実用上の下限です。
• より高いスコープが必要な高安全性設計は、対話ループの外でオフライン合成してください (CourseManagementSystem 2 は scope4 で約 10 分)。

合成の反復回数 (RQ2: invariant のみを入力)

出典: 論文 §5.3 Invariant-guided Synthesis (Table 4)。

不変条件だけを入力にした場合の反復回数と、3 run の結果の一致度です。

• 反復上限は 10 です。9 run 中 7 run が初回で検証を通過し、2 run が反例 1 回で修復しました。
• NoDeadSensitiveMessages は検証を通過する一方、2 種類とも「アプリドメインの暗黙の期待」に反する不自然な設計でした (例: センシティブラベルを外して不変条件を満たすごまかし)。
• 3 アプリ中 1 つだけが「3 run とも同じ設計」に収束しました。invariant だけで設計空間を絞り込む限界を示す数値です。

誘導方式ごとの意図再現度 (RQ3: プロンプト誘導 vs シナリオ誘導)

出典: 論文 §5.4 Scenario- vs Prompt-guided Synthesis (Table 5)。

方式ごとに反復回数 (3 run) を並べています。† は「検証を通過した一方、意図した設計と等価でないと判定された run」です。空欄は「初回入力で全 run が意図設計に収束し、修正が不要だった」ことを意味します。

母数は各セル 3 run です。フェーズごとに母数が異なる点に注意してください。初回フェーズは 12 変種すべてが対象のため 12 × 3 = 36 run/方式です。修正後フェーズは初回で失敗した変種のみが対象のため、プロンプト誘導が 4 変種 × 3 = 12 run、シナリオ誘導が 2 変種 × 3 = 6 run です。合計は 36 + 36 + 12 + 6 = 90 run で、論文本文の "across all 90 runs" と一致します。

要点

• 初回入力 (最小限のシナリオ・シンプルなプロンプト) だけで意図設計に一貫して収束したのは、シナリオ誘導 10/12 変種、プロンプト誘導 8/12 変種です。
• 1 回だけ許した修正を経ると、シナリオ誘導は 12/12 変種で収束しました。プロンプト誘導は OneTimeEvidenceLinks 4 の 1 run (3 run 中 1 run) が最後まで不一致のままでした。
• 収束までの反復回数の平均は、論文本文の記載でプロンプト誘導 1.79、シナリオ誘導 2.36、両方式・両フェーズ合わせた全 90 run で 2.06 です。
• シナリオはプロンプトより意図設計への到達率が高い一方、記述量は多くなりがちです (例: 「他の問題行動はすべて禁止」の一文に相当する内容を、シナリオでは全列挙します)。

シナリオ抽出 (RQ4: LLM によるシナリオ提案)

出典: 論文 §5.5 Scenario Elicitation (Table 6)。

ユーザーがシナリオを書く代わりに、LLM に提案させて ok/nok を分類する方式です。10 件バッチと 20 件バッチをそれぞれ 1 回生成し、分類済みバッチから合成を 3 回実行します。

† は意図設計と非等価です。「失敗†」は、モデルがシナリオを矛盾と判断して設計生成を拒否した run を指します。Overlap は「10 件バッチで分類した 10 件のうち、20 件バッチの最初の 10 件にも同じ (前状態・違反アクションが同じ) シナリオが提案された件数」です。

要点

• 10 件バッチでは 12 変種中 5 変種、20 件バッチでは 12 変種中 9 変種で、3 run すべてが意図設計に収束しました。
• 反復回数の平均はバッチサイズにほぼ依存しません (10 件バッチ 2.11、20 件バッチ 2.36。20 件バッチはシナリオ手動作成時の 2.36 と一致)。
• Overlap は 12 変種中 1 変種のみ 10/10 で一致し、最小 5、平均 7.5 でした。シナリオ抽出自体の非決定性が大きく、「20 件の方が常に良い」とは限りません (OneTimeEvidenceLinks 2 は 10 件バッチの方が有益な情報を含みます)。

再現性 (同じ入力で run 1/2/3 が一致するか)

「検証を通った (verified)」ことと「毎回同じ設計になる」ことは別の性質です。運用では、反復回数に加えて run 間の設計一致率も確認してください。

失敗モードの発生頻度 (RQ5)

出典: 論文 §5.6 Failure modes。母数の内訳に筆者算出を含む箇所は表内に明記。

ベストプラクティス

不変条件だけでは設計が過少仕様になる

• invariant のみの合成は、RQ2 で 3 アプリ中 2 アプリが 3 種類の異なる設計に分岐しました。
• NoDeadSensitiveMessages では、検証を通過する一方で業務的に不自然な設計 (センシティブラベルを剥がして不変条件を回避する等) が 3 run 中 3 run とも生成されました。
• 推奨: invariant 単体の合成結果は候補どまりと扱ってください。必ずシナリオ (またはプロンプト) を追加で与え、収束後に人手でプラウジビリティを確認してください。

シナリオの過適合 (overfitting) への対処

• 最小限のシナリオ (問題行動ごとに 1 つの最短プレフィックス) だけを与えると、モデルは「たまたま与えた具体的な個数」に固執した反応を生成しがちです。例: 「死んだメッセージが 2 件のときだけ再試行する」反応。
• 過適合は scenario-guided synthesis の失敗原因として 2 番目に多い要因でした (8 回。母数の算出は上表参照)。
• 推奨:
  • カスケード修復・数量化された修復を含む変種では、登場するエンティティ数を変えたシナリオを複数用意してください (例: 2 件・3 件の両方)。
  • 過適合が疑われる場合の修正は追加的 (additive) に行えます。NoDeadSensitiveMessages 4 では、3 件のエンティティを含むシナリオを 1 つ追加するだけで 3 run 全てが収束しました。

ok: Q.submit(m); Q.fail(m); Q.submit(n); Q.fail(n); Q.submit(s);
    Q.fail(s); L.affix(s,Sensitive); Q.retry(n); Q.retry(m); Q.purge();

非決定性 (同一入力で結果が割れる) への対処

• 同じ入力でも LLM の出力は run ごとに変わります。invariant のみの合成、シナリオ誘導合成、シナリオ抽出のいずれでも run 間の不一致が観測されています (前掲の「再現性」表)。
• 推奨:
  • 本番採用前に、同じ入力で最低 3 回合成し、生成された設計 (または反応の集合) を比較してください。論文の評価方法自体がこの方式 (各条件 3 run) です。
  • シナリオ抽出を使う場合は、1 回のバッチ生成結果を暫定値として扱ってください。Overlap が平均 7.5/10 にとどまるため、バッチを変えると異なるシナリオ集合になり得ます。
  • 生成された設計同士が「意図と同じ」かどうかの判定は現状手動です。論文も「自動的な等価性検査は将来課題」と明記しており、foundry の現行機能の範囲外です。

Alloy scope の決め方

• scope を 1 段階上げるコストは、ステップ数を 1 段階上げるコストより明確に大きいです (「検証時間の実測値」参照)。
• 論文の既定値は scope 3・step 10 です。この条件で 12 変種すべてが 1 分未満で検証できます。
• 推奨:
  • 対話的な CEGIS ループ (synthesize / interactive) は scope 3・step 10 (Alloy Analyzer の既定値と同じ) から始めてください。--top-scope N で変更できます。
  • より高い安全性が要求される設計では scope を上げられます。その場合は対話ループの外でオフライン実行してください (scope 4 では一部変種が 10 分超)。
  • scope を上げて反例が出ない状態は、無条件の正しさとは別物です (下記「"verified" という言葉の射程を混同しない」参照)。scope を上げる目的は見落としの削減であり、証明の完成とは別です。

人間のレビュー負荷をどこに配分するか

• シナリオを人手で書く方式 (RQ3) と、LLM に提案させて分類するだけの方式 (RQ4) を比べると、後者は「執筆」の負荷を「分類」の負荷に置き換えます。
• ただし分類方式は網羅性の担保に人手の工夫が必要です。10 件バッチでの成功率は 5/12 変種にとどまり、20 件でも 9/12 です。
• 失敗の主因は「重要シナリオの欠落」(72 run 中 26 run) であり、モデルが自発的に多様なシナリオを網羅する能力の限界を示します。
• 推奨:
  • シナリオを人手で書く場合は、代表的な問題行動ごとに「最短の反例」と「その修復」をセットで書くことにレビュー時間を割いてください (論文の執筆方法論そのものです)。
  • LLM 抽出したシナリオを分類する場合は、分類作業に加えて「代替の修復順序」や「異なる個数のケース」が抽出結果に含まれるかを確認する工程を追加してください。代替修復の網羅は抽出プロトコルの保証範囲外です (論文 Conclusion が明記する未解決課題)。

"verified" という言葉の射程を混同しない

出典: 論文 §5.7 Threats to Validity (Internal validity)。

foundry が返す「verified」には、実務上見落としやすい 2 つの限界があります。両方とも Threats to Validity (Internal validity) の記載に基づきます。

1. 自然言語→Alloy の翻訳段が LLM 依存です。
   invariant と reaction の条件は自然言語で書き、foundry は LLM で Alloy に翻訳してから検証します。翻訳誤りは false positive (誤って正しいと判定) にも false negative (誤って不正と判定) にもなり得ます。著者は最終的に検証を通った設計の Alloy 翻訳を「おおむね」目視確認しましたが、網羅的な検査とは別であり、中間反復での翻訳誤りは確認の対象外です。
2. 検証は有界 (bounded) です。
   「verified」は「指定したスコープとステップ数の範囲内で反例がない」という意味であり、無制限の正しさとは別物です。scope を上げれば新たな反例が見つかる可能性があります。

推奨:

• 「verified」という結果だけで採用可否を最終判断するのは避けてください。特に重要な不変条件については、①最終的な Alloy 翻訳を人手でレビューする、②スコープを上げて再検証する、の 2 段階を採用前に挟んでください。
• レポートや意思決定資料に検証結果を書く際は、常に「scope N・step M で検証済み」のように条件を明記してください。「検証済み」とだけ書くと有界性の情報が失われます。

トラブルシューティング

まとめ

本論文は Concept Design のリアクションに形式意味論を与え、LLM の候補提案と Alloy 6 の有界モデル検査を組み合わせた CEGIS 型の合成手順を提案しました。不変条件だけを渡すと設計は過少仕様になり実行ごとに揺れますが、肯定・否定シナリオという機械検証できる誘導を加えると、12 バリアントすべてが意図した設計に収束します。

要件を文章で書き切ろうとせず、概念・不変条件・具体シナリオの三層に分けて設計する型として応用できます。

この記事が少しでも参考になった、あるいは改善点などがあれば、ぜひリアクションやコメント、SNSでのシェアをいただけると励みになります！

参考リンク

一次情報 (本論文)

• Verified LLM-Driven Synthesis for Concept Design (arXiv:2607.15718): Alcino Cunha (INESC TEC & Universidade do Minho)、2026-07-17 投稿、cs.SE
• paper/foundry.tex: 論文の LaTeX ソース。本調査の記述は abstract ではなくこの全文を一次情報としています
• paper/references.bib: 「学術的系譜」の出典

参照実装 (foundry)

• alcinocunha/foundry: 参照実装本体。Python / MIT ライセンス
• README.md: インストール手順・App Description フォーマットの一次情報
• foundry.py: CLI 本体。本記事の CLI リファレンスは argparse 定義から直接抽出しています
• foundry_common.py: ModelClient・Alloy 実行・反例解析
• scripts/benchmark_verification_times.py: 検証時間の測定方法 (計測区間・平均化方法)

実験成果物・記述例 (examples)

• DeadLetterQueue.md: 概念定義の実例
• Label.md / Vault.md: 概念定義の実例
• NoDeadSensitiveMessages.md: 部分アプリ記述 (不変条件のみ)
• NoDeadSensitiveMessages1.md: 完成アプリ記述 (synchronizations を含む)
• NoDeadSensitiveMessages1Prompt.md: プロンプト誘導の入力例
• NoDeadSensitiveMessages1Scenarios.md: シナリオ誘導の入力例
• NoDeadSensitiveMessages1_gpt-5.5_10scenarios.md: シナリオ抽出の出力例
• CourseManagementSystem.md / CourseManagementSystem1.md / CourseManagementSystem1Scenarios.md: 3 つ目の評価対象アプリの記述例

学術的系譜 (論文の参考文献より)

本節は論文の references.bib に収録された文献です。URL は同ファイルに記載があるもののみ添えています。