🤖

AI-Augmented形式手法：Claude Codeへの指示精度を劇的に向上させる

2026/01/28に公開

 はじめに：2つの出会いから生まれた発見2025年12月、私は2つの学びに同時に没頭していました。
1つは放送大学大学院「要求工学」での形式手法の学習。もう1つはClaude DesktopとClaude Codeによる開発体験です。当初、この2つは別々のものだと思っていました。しかし試験直前に本格的にテキストと向き合い始めた時、ある確信が生まれました。
「ゴール志向分析（KAOS）と形式的記述法（Alloy）は、Claude Codeへの指示精度を飛躍的に向上させる」
そして、この手法にはすでに名前がついていることを知りました。その名も**「AI-Augmented形式手法」**です。

 なぜ形式手法なのか？
 自然言語の限界Claude Codeに指示を出す時、こんな経験はないでしょうか？
「ログイン機能を作ってください」
→ セッション管理が入っていない...

「データは必須です」
→ どのデータ？全部？一部？

「できるだけ早く処理してください」
→ 「早く」とは何秒？
自然言語には固有の曖昧性があります。エンジニア間の「暗黙の了解」に頼った記述では、AIは意図を正確に理解できません。

事実、このKAOSと形式的記述法Alloyを使ったClaude Codeへの指示出しについて、Claudeに理解してもらうまで3時間ほどの会話が必要ででした。

 形式手法という解決策形式的記述法（Formal Specification） とは、数理論理学や集合論を用いてシステムの仕様を厳密に定義する技術です（Wikipedia より）。
簿記が「借方・貸方」という複式で記録するように、要件も自然言語と形式記法の両方で表現することで、曖昧性を排除できます。
私が選んだのは：

KAOS：ゴール志向分析（グラフ構造で表現）

Alloy：軽量形式手法（論理検証が可能）

 KAOSの魅力：グラフで「なぜ」を可視化
 KAOSとはWikipedia によると：
KAOS（Keep All Objectives Satisfied）は、システムが「何（What）」をするかではなく、「なぜ（Why）」それを構築するのかという背景（ゴール）を重視し、グラフ構造を用いて体系化します。

 なぜグラフ構造が優れているのかNetworkXで可視化できる
Pythonで図を自動生成
AIにそのまま提示可能
階層的に整理できる
   ルートゴール: 農作業の生産性向上
     ├─ G1: 正確な指示ができる
     │   ├─ G11: 要件を形式化
     │   └─ G12: プロンプトに変換
     └─ G2: データが蓄積される
         ├─ G21: 入力を最適化
         └─ G22: リマインダー機能

AND/ORの論理が明確
ANDゲート：すべて必須
ORゲート：いずれか達成でOK


 Alloyの魅力：論理的整合性の自動検証
 Alloyとは形式的記述法の一種で、制約を数理論理で表現し、Alloy Analyzerで自動検証できるツールです。

 例：必須フィールドの制約自然言語（曖昧）：
作業日、作業種別、圃場は必須です
Alloy（厳密）：
fact MandatoryFields {
  all record: WorkRecord |
    some record.date and
    some record.workType and
    some record.field
}
検証：
Execute → check MandatoryFields
✅ No counterexample found
→ 論理的に矛盾がないことを数学的に証明

 AI-Augmented形式手法とは何か
 従来の形式手法の問題点習得期間：半年〜数年
記述者：人間（専門家）
適用範囲：限定的（安全性重視の分野のみ）
→ 習得コストが高すぎて実務で使われない

 AI-Augmented形式手法の革新習得期間：数時間〜数日
記述者：AI（人間は検証）
適用範囲：あらゆるプロジェクト

 私のワークフロー1. 人間：要件を自然言語で説明
   「農作業記録システムを作りたい」
   
2. AI（Claude）：KAOS図を生成
   NetworkXコードを出力
   
3. 人間：KAOS図を確認・修正指示
   「G21とG22は両方必須」
   
4. AI：Alloyモデルを生成
   制約をfactとして記述
   
5. 人間：Alloy Analyzerで検証
   check / run を実行
   
6. AI：Claude Codeプロンプト生成
   検証済み仕様から実装指示
   
7. Claude Code：実装
   論理的矛盾のないコード生成

 重要な発見：AIがKAOSもAlloyも書く当初、私は「KAOSとAlloyを自分で書けるようになる」ことを目指していました。しかし実際は：
❌ 不要なこと：
Alloyを完璧に書けるようになる
複雑な論理式を自分で組み立てる
✅ 必要なこと：
AIが生成したモデルが正しいか判断できる
Alloy Analyzerの検証結果を解釈できる
エラー時に修正指示を出せる
つまり必要なのは**「読解力」と「検証力」**であって、「記述力」ではありません。

 人間の役割の変化：論理の建築家へ
 論文から学んだことAI-Augmented形式手法に関する論文を読んで、特に印象的だった一節：
自然言語には固有の曖昧さや「エンジニア間の暗黙の了解」が含まれており、AIによる自動翻訳だけでは論理的な整合性を完全に担保できません。人間が関与するメカニズムの必要性があります。
（Req2LTL論文より要約）

 新しい役割：レビューアとしての人間従来：
人間 = コードを書く作業員
AI時代：
人間 = 論理の建築家（レビューア）

役割：
1. ビジネスの意図を言語化
2. AIの出力を検証
3. 論理的整合性を判断
4. 数学的な正しさとビジネス意図をすり合わせる

 フィードバックループの重要性人間「未来日付は不可」
  ↓
AI「Alloyモデル生成」
  ↓
検証「❌ 反例発見：2026-12-31が許可されている」
  ↓
人間「date <= today の制約を追加して」
  ↓
AI「修正完了」
  ↓
検証「✅ No counterexample」
  ↓
実装へ
AIに丸投げするのではなく、対話を通じて精度を上げるのが本質です。

 具体例：農作業記録システム
 要件（自然言語）毎日の農作業を記録したい。
作業日、作業種別、圃場は必須。
未来日付は入力できないようにしたい。

 KAOS図（AI生成）G2: データが継続的に蓄積される
├─ G21: 入力項目を最適化（必須項目に絞る）
├─ G22: 入力リマインダーが機能
└─ G23: Neo4j MCPで保存

 Alloy制約（AI生成）// 必須フィールド制約
fact MandatoryFields {
  all record: WorkRecord |
    some record.date and
    some record.workType and
    some record.field
}

// 未来日付禁止
fact NoFutureDate {
  all record: WorkRecord |
    record.date <= today
}

 検証（人間が実行）$ alloy constraints.als

Execute → check MandatoryFields
✅ No counterexample found

Execute → check NoFutureDate  
✅ No counterexample found

 Claude Codeプロンプト（AI生成）# 農作業記録入力フォーム

## 制約（Alloyで検証済み）
1. 必須フィールド：date, workType, field
2. 日付は未来不可（date <= today）

## バリデーション
- 必須項目未入力 → エラー表示
- 未来日付入力 → 「今日以前の日付を選択」エラー

## 実装
React + TypeScript + Zod

 結果論理的に矛盾のない、テスト観点が明確な実装が生成されます。

 学習コストの比較

アプローチ
習得時間
必要スキル


従来の形式手法
半年〜数年
述語論理、集合論、Alloy記法

AI-Augmented
5-10時間
Alloy Analyzer操作、検証結果の読解

削減率：95%以上

 私が学ぶことAlloy Analyzer の使い方（2-3時間）
モデルファイルを開く
check / run 実行
結果の見方
検証結果の解釈（2-3時間）
✅ No counterexample → OK
❌ Counterexample found → 問題の特定
修正指示の出し方（1-2時間）
AIに「どこが違うか」伝える
段階的に精度を上げる
合計：5-7時間

 実践への道筋
 Phase 1: 基礎（1-2週間）□ Alloy Analyzer インストール
□ 今回生成したモデルで動作確認
□ check / run を実行してみる
□ Claude Codeの基本ワークフロー習得

 Phase 2: 統合（2-3週間）□ 要件をClaude Desktopに説明
□ KAOS図生成を依頼
□ Alloyモデル生成を依頼
□ 検証実行・確認
□ Claude Codeで実装

 Phase 3: 実務適用（継続的）□ 農作業記録システム（実プロジェクト）
□ フィードバックループの確立
□ ワークフローの改善

 メリットとデメリット
 メリット✅ AIへの指示精度が飛躍的に向上
曖昧性の排除
論理的整合性の保証
✅ 手戻りの削減
実装前に制約を検証
テスト観点が明確
✅ ドキュメントの自動生成
KAOS図が要件書に
Alloyモデルが仕様書に
✅ 学習コストの劇的削減
従来の1/20の時間で実用可能

 デメリット・限界⚠️ AIの誤りのリスク
生成されたモデルが間違っている可能性
人間による検証が必須
⚠️ 複雑な制約の限界
高度な数学的制約は困難な場合も
万能ではない
⚠️ ツール依存
Alloy Analyzerのスケーラビリティ制限
大規模システムでは工夫が必要

 この手法が向いているプロジェクト
 適している✅ 制約が明確なシステム
入力バリデーション
ワークフロー
アクセス制御
✅ 正しさが重要なシステム
業務システム
データ管理
自動化ツール
✅ 個人開発・小規模チーム
要件定義に時間をかけられない
でも品質は担保したい

 適していない❌ UI/UXデザイン中心

❌ 数値計算・科学技術計算

❌ 超大規模システム（要工夫）

 おわりに：新しい開発スタイルへAI-Augmented形式手法は、形式手法の民主化です。
従来は専門家の領域だった厳密な検証が、AIの支援により誰でも活用できるようになりました。
人間の役割は変わります：
コードを書く作業員 → 論理の建築家
実装者 → レビューア・検証者
これからの時代、エンジニアに求められるのは：
要件を明確に言語化する力
AIの出力を検証する力
ドメイン知識
論理的思考力
私はこれから、KAOSとAlloyを使いこなし、Claude Codeへの指示精度を上げていきます。
そして、この新しいワークフローを実践し、農作業という実業務に適用し、その知見をコミュニティに還元していきたいと思います。

 参考文献放送大学大学院「要求工学」テキスト
KAOS - Wikipedia
Alloy Documentation
Req2LTL論文（AI-Augmented形式手法に関する研究）

 関連リンク-[私のGitHub]（今回紹介したKAOS図・Alloyモデル）
[Claude Code公式ドキュメント]
次回予告：実際にこの手法でサンプルアプリを構築する過程を記事にします。お楽しみに！
#Claude #形式手法 #KAOS #Alloy #AI #要求工学 #ソフトウェア開発

アプローチ	習得時間	必要スキル
従来の形式手法	半年〜数年	述語論理、集合論、Alloy記法
AI-Augmented	5-10時間	Alloy Analyzer操作、検証結果の読解

はじめに：2つの出会いから生まれた発見

なぜ形式手法なのか？

自然言語の限界

形式手法という解決策

KAOSの魅力：グラフで「なぜ」を可視化

KAOSとは

なぜグラフ構造が優れているのか

Alloyの魅力：論理的整合性の自動検証

Alloyとは

例：必須フィールドの制約

AI-Augmented形式手法とは何か

従来の形式手法の問題点

AI-Augmented形式手法の革新

私のワークフロー

重要な発見：AIがKAOSもAlloyも書く

人間の役割の変化：論理の建築家へ

論文から学んだこと

新しい役割：レビューアとしての人間

フィードバックループの重要性

具体例：農作業記録システム

要件（自然言語）

KAOS図（AI生成）

Alloy制約（AI生成）

検証（人間が実行）

Claude Codeプロンプト（AI生成）

結果

学習コストの比較

私が学ぶこと

実践への道筋

Phase 1: 基礎（1-2週間）

Phase 2: 統合（2-3週間）

Phase 3: 実務適用（継続的）

メリットとデメリット

メリット

デメリット・限界

この手法が向いているプロジェクト

適している

適していない

おわりに：新しい開発スタイルへ

参考文献

関連リンク

Discussion