評価駆動開発の可能性メモ①
#AI時代のエンジニアリング , #アプリケーションアーキテクチャ , #ドメイン駆動設計(DDD) #テスト・検証 #設計原則
#共有する
inputはこの辺り
形式手法入門:生成 AI 時代の『設計』のあり方について | CyberAgent Developers Blog
Evaluation Driven Development for Agentic Systems.を読む
ニューレガシー徹底抗戦ガイド
NotebookLM: 形式手法と生成AI: NotebookLM
Geminiと: https://gemini.google.com/gem/89de0aaaf033/faad623002a18b34
思い付き
DSLをアプリケーション開発におけるSSOTにできないかと思考実験したいんだよ。
ついでに言うと、昨今の「仕様駆動開発」という流れにおいて、より仕様を厳密にしかし省力して記述するっことを目的に、kawashima-sanの簡易なDSLを出発点として形式手法的な堅牢さに昇華させることはできないか?AIの使いどころは?みたいなことを考えたい。
/icons/hr.icon
Geminiさんのターン
それは非常に刺激的な思考実験です。
kawasimaさんの簡易なDSL を出発点に、AIを活用して「形式手法(Formal Methods)の堅牢性」を「省力して(安価に)」手に入れる、というアプローチですね。
これは、私が重視する「SSOT(単一の真実の源)」 、「文脈知識の形式知化」 、そして「仕様駆動開発(SDD)」の思想が交差する、まさに中核的な課題です。
この思考実験を、私の視点から分析・発展させてみます。
課題:なぜ「DSL = 堅牢」にならないか
まず、kawasimaさんのDSLは「ドキュメント」として非常に優れています。しかし、それが即座に「堅牢な仕様」にはなりません。
従来の形式手法(TLA+やAlloyなど)が「高コスト」なのは、仕様を「記述する」コストよりも、その仕様が**「論理的に破綻していないか」を「検証する」コスト**が圧倒的に高いためです。
私たちの目的は、この「検証」のコストをAIによって劇的に下げ、「人間が記述しやすいDSL」を「機械が検証可能なSSOT」に昇華させることにあると考えます。
/icons/hr.icon
思考実験:AIブリッジによる「省力版・形式手法」
このSSOTを実現するプロセスを、3つのステップで構築します。AIは、ステップ1(記述)とステップ2(検証)、ステップ2(検証)とステップ3(実装)の間を繋ぐ「ブリッジ」として機能します。
ステップ1:人間(設計者)による「ドメインの形式知化」 (DSL記述)
まず、我々人間が、業務エキスパートとの対話(私の言う「概念構成図」での議論 )を通じて得たドメインの核となるルールを、簡易なDSLで記述します。
このDSLには、kawasimaさんの「データ構造」 に加え、私たちが議論した「振る舞い(状態遷移)」と「制約(不変条件)」 を含めます。
code:_
// 1. データ構造 (kawasima-san's DSL)
data OrderStatus = "受付済" | "出荷準備中" | "出荷済" | "キャンセル済"
// 2. 振る舞い(状態遷移)
transition "注文出荷" {
from "出荷準備中" to "出荷済"
}
// 3. 制約(不変条件)
invariant "出荷済の注文はキャンセルできない" {
reject "注文キャンセル" when OrderStatus is "出荷済"
}
ここが人間の「本質的な複雑性」 への集中点です。
ステップ2:AIによる「仕様の論理検証」 (形式手法へのブリッジ)
記述されたDSLを、AIに「形式手法のモデル」として解釈させ、論理的な矛盾や欠陥がないかを自動検証させます。これが「省力化」の核です。
AIの使いどころ(検証):
1. 矛盾の検出:
AIにDSLのtransitionとinvariantを読み込ませ、TLA+やZ言語のモデルチェッカーのように振る舞わせます。
AI: 「警告:あなたの定義したtransitionでは、『受付済』から『出荷済』への直接遷移が可能です。しかしinvariant『出荷済の注文はキャンセルできない』ルールと組み合わせると、この注文はキャンセル不可能な状態に意図せず陥る可能性がありますが、仕様通りですか?」
2. 網羅性の確認:
AI: 「分析:OrderStatusが『出荷準備中』の状態では、いかなるtransitionも定義されていません。この状態で固まる可能性がありますが、意図的ですか?」
ステップ3:AIによる「SSOTからの実装生成」 (コードへのブリッジ)
検証済みのDSLを「SSOT」として、AIに**「実装コード」と「テストコード」を自動生成**させます。
AIの使いどころ(生成):
1. ドメインモデル(実装)の生成:
AIはDSLのdata定義から、堅牢な値オブジェクト(VO)や集約(Aggregate) のコード(例: OrderStatus.ts)を生成します。
AIはDSLのtransition定義から、状態遷移メソッド(例: order.ship())を生成します。
AIはDSLのinvariant定義から、メソッド内のガード節や不変条件を保証するドメインロジック を生成します。
2. テストコードの生成:
これが非常に重要です。AIはDSLのinvariantとtransitionから、自動的にプロパティベースド・テストやシナリオテストを生成します。
これは私の関心事である「Evaluation Driven Development (EDD)」 の考え方にも通じます。DSLそのものが「評価基準(Evaluation Rules)」 となるのです。
/icons/hr.icon
このアプローチの課題と「人間の新たな役割」
もちろん、これは思考実験であり、課題もあります。
DSLの表現力とコストのトレードオフ:
ドメインのすべてのルールをDSLで記述しようとすると、DSL自体が複雑化し、「省力」のメリットが失われます。どこまでをDSL(形式的)で記述し、どこからを実装コード(手続き的)に委ねるかの**「境界設定」 ** が、アーキテクトの新たな腕の見せ所になります。
AI検証の「正しさ」問題:
AIによる論理検証(ステップ2)が間違っていたら元も子もありません。AIの検証結果を鵜呑みにせず、「なぜそれを矛盾と判断したのか?」とAIに**「問い質す」能力**が人間に求められます。
結論:エンジニアは「仕様設計者」から「AI対話型検証者」へ
この思考実験が導く未来において、エンジニアの役割は「コーダー」ではなくなります。
エンジニアの仕事は、業務エキスパートと対話して「SSOTとなるDSL」を設計し、AIによる検証結果を「レビュー」し、AIが生成したコードの「境界」を定義することへとシフトします。
AIは、高コストだった「形式手法の検証者」の役割を(部分的に)肩代わりし、人間は「何を検証させるべきか」を定義する、より上流の「アーキテKT」 としての役割を強めていくことになるでしょう。