TL;DR
- AI エージェントによる開発の問題は、形式手法で仕様を厳密に書くことで軽減できる。
- 形式仕様は、代数的データ型と関数型ドメインモデリングで実装に落とし込み、プロパティベーステストで確かめる。
内容
AI エージェントによる開発の問題
AI エージェントを使った開発には、次の問題がある。
- 物量が多い: ガードレールがないと、必要ないものもどんどん追加する
- コンテキストの理解に限界がある: 複雑な依存関係や暗黙的な要件を完全に把握するのは難しい
- 品質保証に新しい課題がある: うまくやってくれるが、開発や改修が数年単位で積み重なった先にどうなるかは分からない
なぜ形式手法か
これらの問題は形式手法で軽減できる。形式手法を開発プロセスに組み込むのは、導入面でも運用面でもコストが高かった。しかし AI エージェントが台頭したことで、このコストを下げられる可能性が出てきた。形式手法を使うと、自然言語の曖昧さを排除して AI が進む道筋をはっきりさせられる。数学的な記法なので自動で検証でき、すべての状態とケースを網羅して書ける。人間と AI がやり取りする手段にもなる。形式手法の例には Alloy や TLA+ がある。
AI エージェントに力を発揮させるには、数学的に厳密な仕様を書く形式手法と、型システムで制約を実装する関数型プログラミングを組み合わせる。AI 駆動開発では、Alloy と TLA+ は互いに補い合う。
自然言語から形式仕様へ
自然言語から形式仕様へは、次のステップで変換する。
- 曖昧さを含んだまま、最初の形式化をする
- 形式検証で問題を見つける
- 構造的な制約（Alloy で検証）、動的な制約（TLA+ で検証）、両方にまたがる制約（Alloy と TLA+ で検証）を明らかにする
- もう一度自然言語に落とし込む
形式仕様から実装へ
形式仕様を実装に落とし込むには、代数的データ型（ADT）と関数型ドメインモデリングを使う。ADT を使うと制約を型システムに直接埋め込め、組み合わせれば複雑な制約も表現できる。関数型ドメインモデリングでは、無効な状態を型で表現できないようにし、状態遷移の制約を型のレベルで表す。プリミティブ型を避けてドメインを型で表す。無効な状態を作れなければ、人間だけでなく AI がコードを生成するときの助けにもなる。
制約をテストするにはプロパティベーステストがよい。高度なテストのパターンとして、ラウンドトリップテスト、メタモルフィックテスト、不変条件の維持の確認がある。
AI 駆動開発の可能性
AI の力で、究極的なシフトレフトを加速できる。人間が律速になっている問題はこれからさらに深刻になるので、シフトレフトでその問題を軽減できる。
キーワード
- AI エージェント
- 形式手法
- Alloy
- TLA+
- 時相論理
- 関数型プログラミング
- 代数的データ型
- プロパティベーステスト
- メタモルフィックテスト
- 不変条件
- シフトレフト
自分の理解
Alloy 6 から時相論理（線形時相論理）が入ったが、TLA+ ほどの表現力はないので、そこは TLA+ に任せるということなのかな？ そもそも TLA+ は時相論理がベースである（Alloy 6 の可変フィールドについての記事）。