本記事は、Hashnodeに公開したThe Rising Sea of Software Engineering — Rebuilding the Discipline on Algebraic Geometryの日本語版です
AI がコードを書く速度は、人間がレビューできる速度を超えつつあります。これは予測ではなく、多くの開発現場の実感だと思います。
そしてもう一つの実感があります。テストと CI/CD をどれだけ整備しても、E2E の障害は起きるのです。ユニットテストは全部通っている。統合テストも通っている。CI は green だ。それでも本番で壊れる。
私はこの問題を、テストの量や CI の速度の問題ではなく、ソフトウェア工学そのものが追いついていない問題だと考えています。この記事は、その診断から始まる一つの登山の記録です。一つの山頂(SAGA 定理)には登れたこと。その山頂から彼方に見えた景色。そして、これから登る山。
初見の方のために、この記事に登場するものを先にまとめておきます。
| 名前 | 何であるか |
|---|---|
| AAT (Algebraic Architecture Theory) | ソフトウェアアーキテクチャの代数幾何的理論。Atom を公理とする純粋数学 |
| Atom | AAT の公理的な最小単位。コードや言語やライブラリから抽象化された、アーキテクチャの構成要素 |
| SAGA 定理 | AAT の中心定理 (SAGA Grounding Theorem)。アーキテクチャ意味論側の H^1 と、Atom が生成する site 上の本物の Čech H^1 が一致するという比較定理。Lean 4 で証明済み。名前は Serre の GAGA へのオマージュ |
| ArchSig | AAT に基づく Rust 製の計測ツール。アーキテクチャの観測データから貼り合わせの障害 (obstruction) を検出する |
| SFT (Software Field Theory) | ソフトウェアの時間発展を記述する動力学の理論。AAT が静力学なら SFT は動力学 |
| Lean | 定理証明支援系。AAT / SFT の定理はここで形式検証される |
SAGA定理についてはこちら
https://zenn.dev/iroha1203/articles/31b2683d4828fa
先に断っておくと、この記事には「証明済みのこと」「構想」「未証明のこと」の三種類が出てきます。三つを混ぜないで書きます。証明されていないことを証明済みのように語らないのが、このプロジェクトの流儀だからです。
麓 — E2E の障害には数学的な名前がある
まず診断からです。
テストと CI が保証しているのは局所的な正しさです。ユニットテストは一つのモジュールの断面を検証します。統合テストも、結局は選ばれた有限の経路を検証しています。
ところが E2E の障害は、各部分がすべて正しいのに全体が壊れるという形で起きます。局所的には整合している断片たちが、大域的には貼り合わないのです。
数学、特に層 (sheaf) の理論には、この状況を指す正確な言葉があります。局所切断がすべて存在するのに、大域切断が存在しない。そして、その「貼り合わせの障害」を数える道具がコホモロジー — まず第一に H^1 です。
「テストは全部通っているのに本番で壊れる」現象は、integration hell と呼ばれて経験則で殴られ続けてきましたが、実は正確な数学的名前を持っています。重要なのは、この障害が各部分の性質ではなく、部分と部分の重なりの上に住んでいることです。インターフェースの暗黙の前提、状態の共有、時間的な順序 — どれも単体のモジュールの中には存在しません。だからテストカバレッジを 100% にしても消えないのです。測っている対象が局所である限り、原理的に届きません。
既存のソフトウェア工学は「部品の品質を上げれば全体の品質が上がる」という暗黙の合成原理の上に建っています。しかし貼り合わせ問題は、まさにその合成が自明でないことを言っています。局所の総和は大域ではないのです。
AI 駆動開発がこの問題を悪化させる理由
AI 駆動開発でこの問題が急激に悪化しているのは、偶然ではありません。
AI は局所生成が異様に得意で、しかも各断片は個別には正しい。生成速度が上がるほど、重なりの上の不整合が蓄積していきます。
ここで気づくべきことがあります。人間のレビューが担っていたのは、実はコードの正しさの確認ではありませんでした。頭の中で貼り合わせを検算することだったのです。「この変更、あっちのモジュールの前提と噛み合ってるか?」— レビュアーが無意識にやっていたのはこれで、それが追いつかなくなった、というのが現場感の正体だと思います。
このギャップを埋める方法は、原理的に二つしかありません。
- レビューする側も AI にする
- レビューを判定可能な数学にする
前者には「誰が見張りを見張るのか」という無限後退がつきまといます。生成物が生成物を検査する世界では、どのエージェントの判断も、別のエージェントの判断以上の権威を持てません。私は後者を選びました。
Rising Sea — 水位を上げて殻を開ける
方法について話します。
Grothendieck は代数幾何で、難問を釘とハンマーでこじ開けるのではなく、抽象度の水位を上げて、あるとき気づけば殻が自然に開いている、という方法を取りました。彼自身の言葉で la mer qui monte — 上昇する海です。
ソフトウェア工学の歴史は、ハンマーの歴史でした。E2E が壊れるならテストを増やす。統合が壊れるなら CI を速くする。境界が壊れるなら契約テストを書く。個々の道具は正しいのに問題が消えないのは、道具が悪いからではなく、問題が定式化されている抽象度が低すぎるからです。局所と大域の関係という問題を、局所の道具で殴り続けてきたのです。
私の研究プログラム AAT がやっているのは、この水位上げです。コードやモジュールという水面下の岩を直接扱うのをやめ、Atom、層、被覆、貼り合わせという水準まで上がります。すると「テストが通るのに本番で壊れる」という工学の難問は、闘うべき敵ではなく、H^1 という座標を持った当たり前の対象になります。
この水位上げには、実務的な副産物もあります。Atom はコードから抽象化された単位なので、理論も計測も、特定の言語・フレームワーク・ライブラリに依存しません。Rust のマイクロサービスでも、レガシーな Java モノリスでも、観測データさえ与えれば同じ定理で同じ障害が語れます。lint やアーキテクチャテストのようにエコシステムごとに道具を作り直す必要がなく、技術スタックが移り変わっても理論は古びません。抽象化とは、この意味で可搬性のことでもあるのです。
問題は消えません。しかし謎ではなくなります。謎でなくなったものは、測れます。測れるものは、道具の仕事になります。
正しい一般性の水準に持ち上げると、難問は「解かれる」のではなく自明になる。これが rising sea の要点であり、このプロジェクトの方法です。
一つ、Grothendieck の海と違うところがあります。彼の海は EGA/SGA という数千ページの散文に堆積し、後の世代がその水位を維持するのに苦労しました。私の海は Lean が水位を保証しています。定理が形式検証されている限り、水は引きません。この海の中心にある定理を SAGA 定理と名付けたのは、Serre の GAGA — 代数幾何と解析幾何という二つの世界の対応を確立した記念碑的な仕事 — へのオマージュです。GAGA が二つの幾何を橋渡ししたように、SAGA 定理はアーキテクチャ意味論と代数幾何を橋渡しする比較定理です。そこに機械検証という一枚を足しています。
もう一つ、忘れてはならないことがあります。rising sea は逃避としての抽象化ではありませんでした。Grothendieck は常に具体的な問題(Weil 予想)を、水没させるべき対象として中心に持っていました。このプロジェクトも同じ形をしています。**E2E の破綻という現場の具体的な痛みが、水没させるべき殻として最初から中心にあります。**抽象化は現実から離れるためではなく、現実を自明化するために行うのです。
ここまでが方法の話です。方法は海 — 抽象度の水位を上げて、問題を沈める。しかし研究の行程そのものは、海よりも登山に似ています。どの峰に登れたのか。山頂から何が見えたのか。次はどの峰か。ここからは、その登攀の記録です。
登頂 — SAGA 定理という山頂(証明済み)
ここは境界を厳密に守って書きます。以下は既に成立しています。
- AAT 数学本文 — Atom を公理とする純粋数学理論としての AAT 本文です。ツールや形式化への弁明を一切持たず、数学が自分の言葉だけで語る体裁になっています。
- SAGA 定理 — アーキテクチャ意味論の側で育てた H^1 と、Atom から生成された site 上の本物の Čech H^1 が一致する、という比較定理です。Lean 4 で証明済み。この登攀は AI エージェントの自動研究ループで 352 サイクルかかり、うち 347 サイクルは「この語彙では登れない」という不可能性定理の壁を積む作業でした。最後の 5 サイクル、「law(アーキテクチャの法)は述語ではなく方程式である」という語彙の転換が、岩盤を破りました。
- Lean 形式化の塔 — 「語れる命題だけを形式化する」規律の下で、定義・定理・例を sorry なしで積んでいます。
- ArchSig — Rust 製の計測器です。アーキテクチャの観測データ (ArchMap)、守るべき法 (LawPolicy)、証拠の契約 (evidence contract) を入力に取り、H^1 障害検出が稼働しています。重要な設計原則が一つあります。**与えられた contract から語れることだけを語り、語れないことには沈黙する。**入力を補完も推測もしません。
- SFT — ソフトウェアの時間発展を記述する動力学の側です。AAT が静力学(ある時点の整合性)なら、SFT は変更がどう伝播するかの理論で、こちらも定理を生み始めています。
- 開発体制そのものが実証実験 — このリポジトリは、AI エージェントが高速に実装し、敵対レビューと Lean ゲートが整合性を判定し、人間は問いの設定と受け入れだけを握る、という体制で回っています。つまり AAT/ArchSig が守ろうとしている開発様式で、AAT/ArchSig 自身が開発されているのです。この自己適用性は、理論が実際の開発に耐えることの最初の証拠だと考えています。
山頂からの展望 1 — 静かな未来
ここからは構想です。SAGA の山頂から彼方に見えた景色を、二つ書き残します。
一つ目はこうです。
あるエンジニアが仕事を始める。できあがったコードを「ArchSig で分析して」と言う。いくつかの obstruction が検知される。彼はコードを修正する。E2E の障害は、未然に防がれた。
この光景で注目してほしいのは、その静けさです。そこには圏も層もコホモロジーも登場しません。エンジニアは「分析して」と言い、obstruction という言葉だけを受け取り、直し、先へ進みます。振る舞いとしては lint を掛けるのと区別がつきません。
エンジニアは代数幾何を習得しなくてよい — これはこのプロジェクトが最初から定めている抽象化原則であり、この光景の設計図です。理論が完成に近づくほど、理論は見えなくなります。水位が十分に上がった海は、水面しか見えないのです。
この光景には、もっと深い変化が隠れています。「E2E の障害は未然に防がれた」という文は、反実仮想です。起きなかった障害は観測できません。今日のソフトウェア工学には、防がれた障害について語る語彙が原理的にないのです。だからテストは事後にしか価値を証明できず、アーキテクチャの良し悪しは事故が起きるまで宙に浮いています。
obstruction が定理に接地したとき初めて、「この修正がなければ貼り合わせは失敗していた」が、経験則ではなく帰結として言えるようになります。あの静かな光景は、反実仮想が数学になった世界なのです。
山頂からの展望 2 — エージェント社会の不動点
もっと極端な未来もあります。
エンジニアは外から見ているだけ。複数の AI エージェントがダイナミックに連携してソフトウェアを爆速で作る。途中、ArchSig のアラートが鳴る — デプロイゲートに ArchSig が配されているのだ。エージェントは ArchSig の出力を読んで、コードを修正する。
この未来では、コードも、テストも、レビューも、修正も、すべてが AI の生成物になります。すべてが同じ地盤の上で揺れている世界で、唯一揺れないのが、定理に接地したゲートです。その判定は誰かの意見ではなく、形式検証された定理の、選ばれた contract 上での帰結だからです。猛烈な速度で回る生成の渦の中に、一点だけ動かない岩がある。デプロイゲートに置くべきなのは、そういう性質のものだけです。ArchSig は人間の道具から、エージェント社会の不動点になります。
この未来では、「語れないことに沈黙する」という設計原則が、贅沢品から安全装置に変わります。人間相手なら曖昧な警告でも行間を読んでもらえますが、エージェントは出力を字義通りに読んで字義通りに行動します。「なんとなく怪しい」を出力する検査器は、エージェントのループを発散させます。沈黙の規律は、マルチエージェント時代の interface 仕様なのです。
では人間はどこへ行くのでしょうか。「外から見ているだけ」というのは、正確には立法府に移るということだと思います。LawPolicy を書くのは誰か。どの語彙で語ることを許し、何を SAFE と呼ぶかを定めるのは誰か。エージェントは行政であり、検査器は司法であり、人間は法を書く。コードを書く手は手放しても、「何が守られるべきか」の決定は手放していません。むしろそこだけが、人間の仕事として純化されるのです。
エンジニアが外から見ているだけの未来は、人間が退場した未来ではありません。人間が信頼の根拠を作り終えた未来です。
経済的な追い風も一つあります。検証は生成より桁違いに安いのです。ArchSig は決定的な計算で、LLM の推論コストと比べれば実質タダに近い。Lean も一度証明が立てば再検証は軽い。計算資源が逼迫する世界ほど、「LLM が LLM をレビューする」贅沢な構成は割に合わなくなり、安い決定的ゲートで生成の無駄撃ちを早期に落とす構成が経済的に勝ちます。メモリが希少だった時代に型システムが割に合ったのと同じで、資源制約は常に「実行前に間違いを落とす」技術の価値を吊り上げます。爆速生成の時代に一番高価なのは、間違ったコードを生成してから気づくことなのです。
下降路 — 次の定理の名は descent(未証明)
登山では「山頂は半分でしかない。無事に下りて、初めて登山は完成する」と言われます。SAGA の登頂にも、まだ下降路が残っています。そして出来すぎた偶然ですが、その下降路の最初の定理は、文字通り descent(下降)定理と呼ばれるものです。
願望を成果のように語らないために、未証明のものを明記します。
- descent 定理(本丸) — 「どういう条件下でなら、局所的な正しさから大域的な正しさが従うか」。ソフトウェア工学が暗黙に信じ、一度も証明したことのない合成原理に、初めて成立条件を与える定理です。検出側(大域修復が存在するなら障害は消えている)は積み上がりつつありますが、本丸である逆向き(障害が消えていれば大域修復が実在する)はまだ open です。
- H^2 以上 — 高次の障害構造を語る言葉はまだありません。導来的な拡張は意図的に保留しています。
- 観測層の忠実性 — ArchSig の判定の信頼性は、ArchMap が現実のコードをどこまで忠実に写すかを超えられません。ここが理論ではなく工学の急所であり、観測の純化(判定の主観を排し、観測を生値で残す)を防御線として固めています。
- 実コードベースでの実証 — H^1 の障害検出が、実プロジェクトで「人間が見落としていた貼り合わせの失敗」を先に見つけること。理論の真偽とは別に、道具としての価値はここで決まります。
descent が証明されると何が変わるでしょうか。ArchSig はそれを検査項目にできます — 「このアーキテクチャは descent の仮定を満たしているので、局所テストの合格が大域整合を含意する」と。逆に仮定が破れている場所こそ E2E テストを集中させるべき場所だと、理論が指させるようになるのです。山頂からの展望は、この下降路を無事に下りて初めて、現実の谷に届きます。
語れることだけを語る
最後に、この道具が何を言わないかをはっきりさせておきます。
ArchSig が言えるのは「この変更は、与えられた語彙と法の内側で安全」ということまでです。「この変更は良い設計だ」とは言いません。言えないからです。安全性の判定と設計の良し悪しの間には、意図的に引かれた沈黙の境界があります。
これは弱点ではなく、信頼の条件だと考えています。判定できないものまで判定する道具は、どこかで必ず嘘をつきます。判定できるものだけを判定する道具は、その範囲では絶対に嘘をつきません。AI が何でも語りたがる時代に、語れることだけを語る道具は希少です。デプロイゲートに置いてよいのは、後者だけです。
この記事もその規律で書きました。証明済みの節、構想の節、未証明の節。三つを混ぜないこと。
結び
ソフトウェア工学が追いついていないのではありません。必要な数学が、まだ工学に輸入されていなかったのです。この研究プログラムはその輸入作業であり、しかも密輸ではなく、Lean で通関手続きをした正規輸入です。
課題はまだ多く残っています。descent、高次障害、観測層の忠実性、実コードベースでの実証 — どれも軽くありません。しかし、登れない山と登れる山の違いは標高ではなく、ルートを引けるかどうかだと思っています。
水位は上がり始めています。そして海は、上がり始めてからが速いのです。
やってやれなくはない。そして、登れない山ではない。
参考
- リポジトリ: AlgebraicArchitectureTheoryV2(MIT ライセンス)
- Website: AAT/SFT Research Notes