本記事は、Hashnodeに公開したSAGA's Cape of Good Hope: The One Cent That Cohomology Caughtの日本語版です
TL;DR
- この記事は SAGA 定理の記事 の続編です。前回は「局所は正しいのに大域で壊れる」現象に Lean 4 で証明された定理を与えるところまでを書きました。今回は、その定理を現実世界に持ち出した報告です。
- 実在のマイクロサービス(研究用ベンチマーク train-ticket)に、定理の前提を満たす構造がそのまま見つかりました。
- 各サービスは自分の金額規約に完全に従っている。それでも払い戻しの 1 セント未満が、システムのどこにも記帳されずに消える。計測はこの2つを同時に判定し、修理案を与えると CI ゲートが遮断から通過に変わりました。
- 発見物は拍子抜けするほど地味です。しかし価値は発見物ではなく、航路が実在すると確認できたことにあります。
0. これまでのあらすじ
シリーズ初見の方のために、登場するものを先にまとめておきます。このプロジェクトの目標は、ソフトウェアアーキテクチャを、図と経験則とレビュー上の好みで語る対象から、定義・定理・反例・証明書で研究できる数学的対象へ移すことです。
| 名前 | 何であるか |
|---|---|
| AAT (Algebraic Architecture Theory) | ソフトウェアアーキテクチャの代数幾何的理論。コードから読み取った型付きの最小の事実(Atom)の上に、守られるべき規約を方程式(law)として立て、アーキテクチャを「方程式の解のなす幾何」として扱う |
| SAGA 定理 | AAT の中心定理。「局所の修理たちは1つの大域修理に貼り合うか」という問いが、コホモロジー H^1 という量の零性として計算できることを確立した比較定理。Lean 4 で機械検証済み。名前は代数幾何の GAGA 定理へのオマージュで、分散トランザクションの Saga パターンとは無関係 |
| ArchSig | AAT に基づく Rust 製の計測ツール。観測データ(ArchMap)と law を入力に、貼り合わせの障害を有限計算で判定し、証明書付きの結論を返す。観測器であって採点器ではない |
| Lean | 定理証明支援系。AAT の定理はここで機械検証される |
前回の記事では、SAGA 定理の証明までを書きました。定理は真です。残った問いはひとつ。その前提を満たす構造は、現実のコードに実在するのか。今回はその報告です。シリーズを既にお読みの方は、この節は飛ばして構いません。
1. Lean の形式検証は通った。果たして現実のソフトウェアに適用できるのか?
SAGA 定理は Lean 4 で証明済みです。sorry(証明の未完成箇所を示すプレースホルダ)はなく、依存公理は Lean 標準のものだけ。定理が正しいかどうかは、もう問いではありません。
残っていた問いは、こちらです。その前提を満たす構造は、現実のソフトウェアに存在するのか。
どれほど正しく証明された定理も、前提を満たす対象が数学の中にしか存在しなければ、現実に対しては静かに空振りします。SAGA の前提の束は、かみ砕くとこうです。以後、各サービスを「チャート」、サービスが自分に課している規約を「法」と呼びます。各チャートは自分の法を守っている。チャートの間には値の受け渡しがある。それなのに、受け渡しを閉じたループに沿って一周すると、どこにも帳尻を合わせる場所のないズレが残る。この「一周して残るズレ」を数える量が、前回の記事の主役だったコホモロジー H^1 でした。
この前提の束は、悪くすると人工的な例でしか組み上がらない構造かもしれなかった。私たちが公開している one-cent デモ(1 セントの丸めズレがモジュール間で行方不明になる筋書きを、意図的に設計した小さな Rust 製サンプル)は、「この構造なら障害が立つ」の実演にはなります。しかし「この構造は現実に生じる」の証拠にはなりません。後者は実データでしか確かめられません。そこで、実ユーザーと同じ手順で外部の OSS を丸ごと計測してみることにしました。ドッグフーディングです。
大航海時代の喜望峰の発見が意味したのは「インドに着いた」ではなく、「この航路は実在する」でした。今回の実験が確かめようとしたのも同じことです。AAT という航路は、数学の中だけの海なのか。それとも現実のコードという海につながっているのか。だからこの報告を「SAGA の喜望峰」と名付けました。
2. 実験の設計 — 外部 OSS を正規フローで丸ごと計測する
対象は FudanSELab/train-ticket。産業システムの調査に基づいて作られた、マイクロサービス研究の標準ベンチマークです。40 以上の Java マイクロサービスからなり、注文・決済・払い戻し・託送などの業務フローを持ちます。リポジトリ全体はフロントエンド資産まで含めると約 50 万行、そのうち今回の計測対象は Java の実装本体、約 28.5 kLOC です。重要なのは、こちらの都合を一切知らないコードベースであることでした。
計測は2段階で行いました。
第1段(観測データのフルビルド): 42 サービス+共有モジュールの Java ソースから、ArchMap、すなわちコードから読み取った最小の観測事実(Atom)を集めた地図を正規フローで構築しました。2 系統の独立した読み取りパスで抽出し、差分を全件調停し、監査を通す。実ユーザー向けに定めた手順そのままです。結果は 2,118 個の Atom と 43 の観測単位(context)。読み取りはすべて軽量モデル(Claude Sonnet)のサブエージェントで行い、供給コストは実測で約 4.1 分/kLOC(壁時計、並列実行込み)でした。
この時点で、金額の持ち運び方を観測した 24 サービスには 8 つの流儀が共存していることが写っていました。double のフィールドで持つ、文字列のまま素通しする、使う場所で BigDecimal に直す、文字列連結で組み立てる。どれも単体では動くコードです。
第2段(SAGA): このフルビルドの成果物の上で、law(守られるべき規約を計測器が読める形で書いたもの)を SAGA 診断のフルスタックに拡張し、診断の階段を一周させました。この記事の主役はこちらです。
3. 発見 — 「1 セントが消える構造」は現実のコードに実在した
フルビルドの実呼び出しグラフを調べていて、次の構造が見つかりました。
cancel(払い戻し)、inside-payment(内部決済)、order(注文)の3サービスが、実際の呼び出し関係で三角形をなし、その3辺すべてで金額規約が食い違っている。
3サービスの規約は、実ソースでこう確認できます(commit 313886e9)。
まず order。注文の価格は文字列のまま保管されます。
// ts-order-service: Order.java
private String price;
次に inside-payment。決済残高の計算では、その文字列を BigDecimal に直して正確に演算します。
// ts-inside-payment-service: InsidePaymentServiceImpl.java
totalExpand = totalExpand.add(new BigDecimal(order.getPrice()));
そして cancel。払い戻し額の計算では、同じ文字列を double に直して 0.8 を掛け、小数第2位に丸めて文字列に戻します。
// ts-cancel-service: CancelServiceImpl.calculateRefund
double totalPrice = Double.parseDouble(order.getPrice());
double price = totalPrice * 0.8;
DecimalFormat priceFormat = new java.text.DecimalFormat("0.00");
String str = priceFormat.format(price);
つまり同じ「注文の価格」という値が、素通しの文字列 / 正確な十進演算 / 浮動小数点+丸め、という3つの別世界を一周します。0.8 × 価格が2桁で割り切れないとき(たとえば 91.33 × 0.8 = 73.064)、丸めで生じる 1 セント未満の剰余は、どのサービスの帳簿にも現れません。
そして決定的なのはここです。3サービスの金額を同時に突き合わせるコードが、計測対象の Java ソースのどこにも存在しない。 ペアごとの受け渡しはあります(cancel は order から価格を読む、cancel は inside-payment に払い戻しを渡す、inside-payment は order の価格を読む)。しかし三者を一度に照合する場所はない。
前回の記事の言葉で言えば: 3辺の食い違いが閉じたループをなし、それを埋める面(三角形の内側を塞ぐ膜、すなわち三者を同時に照合する場所)が欠けている。これは SAGA 定理の前提の束、そのものです。私たちが仕込んだのではありません。普通の開発者たちの、それぞれ合理的な実装判断の積み重ねが、この形をしていたのです。
4. 計測 — 診断階段が一周する
診断階段とは、単純な計測から順に積み上がる診断の系列です。最下段が生の食い違いの計測(Čech 計測)、その上に grounding(各チャートは自分の法を守っているか)、descent(ズレは一周して残るか)、comparison(修理前後の比較は数学的に正当か)、そして CI ゲートが載ります。この構造の上に law を組み、階段を流しました。結果を表で示します(等幅のトークンは計測器の出力そのままです)。
| 幕 | 結果 |
|---|---|
| 修理前(head)の計測 | MEASURED_NONGLUING_RESIDUAL_CLASS |
| ├ grounding(各チャートは法を守っているか) |
measured_zero — 守っている |
| ├ descent(ズレは一周して残るか) |
measured_nonzero — 残る |
| └ comparison(修理前後の比較の正当性) | established |
| ゲート判定 | BLOCKED_BY_GATE_POLICY |
| 修理案を与えた状態の計測 | REPAIR_GLUES_WITHIN_SELECTED_COMPLEX |
| 修理前後の比較 | MEASURED_OBSTRUCTION_NO_LONGER_RECORDED_AFTER_CHANGE |
| 修理後のゲート判定 | PASS_WITHIN_GATE_POLICY |
順に読みます。
grounding = measured_zero。 これが SAGA の罠の部分です。cancel も inside-payment も order も、自分が掲げる金額規約には完全に従っています。サービス単位のレビュー(人間でも AI でも)が、この食い違いを「そのサービスの違反」として弾く根拠はどこにもありません。局所はすべて合法です。
descent = measured_nonzero。 それでも、三角形を一周したときのズレは零ではない。しかもこのズレは、どのサービスが自分の規約をどう選び直しても消えない種類のものです。1つのチャートの規約を張り替えると、そのチャートに接する辺の食い違いが同時に動くだけで、ループ一周分のズレは残る。これが計算の返した内容です。消すには規約の張り替えではなく、剰余を記帳する場所を作るような、構造の変更が要ります。「どのファイルにもバグはないのに壊れている」の、計測としての姿です。
ゲート = BLOCKED。 CI に置いたとき、この PR は止まります。たとえ全モジュールのテストが緑でも、「システムは 1 セントずれ得る」状態を緑の海の中から止められる。前回の記事で「lint の先にある解析のクラス」と呼んだものの実走です。
修理 → 貼り合い回復 → PASS。 「3サービスの共有読みを scale-2 の BigDecimal に統一し、丸め剰余を明示的に記帳する」という修理案を仮説状態として与えると、選ばれた範囲の上でズレは零になり、比較は「障害はもう記録されない」を返し、ゲートは PASS に変わります。修理案の段階で、実装前に「この直し方なら貼り合う」を検証できるわけです。
one-cent デモで設計した物語(非零の障害 → BLOCKED → 修理 → PASS)が、合成例ではなく実在のコードベースで、同じ順序で再生されました。理論が予言する障害の最小実例が、ちゃんと最小の姿(1 セント未満)で見つかったことは、理論の解像度が現実に合っている証拠だと読んでいます。
5. 何が確かめられたのか
第一に、前提の実在証明です。SAGA 定理は「証明済みだが、実例は合成のみ」から「証明済みで、実例が現実のコードで再現した」へ移りました。空虚であるリスクは、この1例で消えました。
第二に、こちらが本命ですが、忠実性契約の耐久試験です。理論と計測器のあいだには「計測器は定理が語れる範囲だけを語る」という契約があります。今回、計測器は初めて敵対的な実データに触れましたが、含意の連鎖(局所合法 → 一周のズレが非零 → 修理で貼り合う)は Lean 側の定理の連鎖と同じ順序・同じ条件で発火し、契約は一度も破れませんでした。ツールの拒否もすべて正当でした。たとえばドリフトのある三角形に「三者を照合する面がある」と偽って申告すると、帳尻の計算との矛盾で正しく弾かれます。
6. 静的解析や LLM レビューとの違いは?
「コード全体を読める LLM に3ファイル見せれば、この不整合くらい指摘できるのでは?」
この個別事例を「見つける」こと自体は、LLM にもおそらくできます。それどころか、今回のパイプラインでも各サービスの金額規約を読み取ったのは LLM(Claude Sonnet)のサブエージェントでした。差は、見つけた後の出力の形式にあります。
- 非局所性の判定。 LLM は「この3つは不整合です」と言えます。計測が返すのは「どのサービスが規約を選び直しても消えない種類のズレだ」という計算結果です。語りには、この保証が付きません。
- 良性と構造的の選別。 フルビルドで実測された食い違いは、観測できた受け渡し 6 辺中 5 辺に及びましたが、判定は零、つまり局所の張り替えで貼り合う良性のドリフトでした。非零が立ったのは三角形だけです。すべてを「問題」として列挙する指摘の洪水と、構造的な一点の指摘。この差は、レビュー疲れの時代には実用価値そのものです。
- 零の言明と再現性。 LLM は「問題ありませんでした」を保証付きで言えず、走らせるたびに指摘は揺れます(私たち自身の独立2パス観測でも、生の機械一致は 9.4% でした。詳細は §8)。計測は同じ入力から常に同じ判定を返し、根拠はソースの典拠まで遡れます。
- 修理の事前検証。 提案はどちらもできますが、「この修理案なら貼り合う」を実装前に判定できるのは計測だけです。
コストの構造も違います。全読みレビューは、レビューのたびにコードベース全体をコンテキストに載せます。毎回 O(コードベース) を払う構造で、コードベースが大きくなるほどトークンコストと読み落としが増えていきます。
ArchMap の構築は一度きりで、軽量モデルで足りました。以後は変更差分だけを更新すればよく(この差分更新を支える再現性の工学が進行中です。§8)、貼り合わせ障害の計算自体は Rust 側で走るのでほぼ無料です。O(コードベース) を一度だけ払い、あとは O(差分)。コードベースが大きく長命であるほど、差は開いていきます。
つまり本当の関係は競合ではなく分業です。LLM が局所観測を担い(ファイル単位の事実の読み取り。LLM が得意な形)、数学が大域化を担う(観測を貼り合わせてループ上の障害を計算する。長大コンテキストの attention に頼ると崩れる形)。ArchSig は、LLM の観測に数学の背骨を通す装置だというのが正確な位置づけです。
grounding = measured_zero という計測結果は、この問いへの実証でもあります。サービス単位のレビューが見る範囲では、全部合法だった。障害はレビューの単位の外側、重なりの上にだけ存在したのです。
もう一つの当然の疑問にも答えておきます。「型システムや静的解析では捕まえられないのか?」
ここは性質の違いがいちばんはっきり出るところです。今回の三角形で、order が保管する価格も、cancel が返す払い戻し額も、型はどちらも String です。型システムと静的解析の目には、同じものに見えます。 食い違っていたのは型ではなく、「この文字列は未パースの金額表現である」「この文字列は丸め済みの払い戻し額である」という意味論の規約でした。障害は構文にも型にも写らない場所に住んでいたのです。
ArchSig の入力が AST や型情報ではなく Atom(コードや言語から抽象化された、型付きの最小の観測事実)であるのは、このためです。Atom は、依存や呼び出しのような構造的な事実と、規約・責務・状態・権限のような意味論的な事実を、同じ基礎単位で扱います。金額規約の観測は semantic atom の仕事で、静的解析の語彙の外にある分析です。
Atom という中間表現を挟むことには、もう一つの帰結があります。言語にもフレームワークにも依存しないことです。実際、one-cent デモは Rust、train-ticket は Java ですが、計測器も law の語彙も診断階段も、まったく同じものが走っています。マイクロサービスのように多言語が混在するシステムでも、地図は1枚で済みます。
7. この報告が主張しないこと
シリーズの慣例に従って、言えないことを言わないための節です。
- 計測器がひとりでに見つけたわけではありません。 食い違いそのものを写したのは階段の一番下の段で、「そのズレがどの受け渡しの上に現れるか」は、ソースを読んだ私たちが観測データとして計測器に与えたものです。SAGA 階段の手柄は発見ではなく、診断の進め方にあります。「各サービスは合法」とわざわざ確定させ、ズレが一周して残ることを認証し、修理案を先に検証し、CI を止める。この一続きを機械の判定でつないだことです。
- 修理はまだ実装されていません。 PASS が言っているのは「この直し方なら整合が戻る」という事前の検証結果で、直したコードが存在するわけではありません。
- 被害額は測っていません。 丸めの剰余がどこにも記帳されないことはコードから確実に言えますが、実際にいくら・どれくらいの頻度でずれるかは、動かして測らないと分かりません。測っていない数字は語らない、もこのプロジェクトの流儀です。
- train-ticket を批判する意図はありません。 これは研究用のベンチマークで、本番のシステムではありません。「よくある書き方の混在」がそのまま定理の前提になっていた、という観測として読んでください。よくある書き方で起きるということは、他の現実のコードでも珍しくないだろう、ということでもあります。
8. 岬の先の海 — 伸びしろの海図
ところで喜望峰は、発見者のディアスが最初「嵐の岬」と名付け、のちに航路への希望を採って「喜望峰」に改名された岬です。発見の現場が地味で荒れているのは、昔からそういうものらしい。そして喜望峰の到達からインド航路の開通までには、さらに 10 年かかりました。最難関は岬の先。インド洋の横断には、沿岸航法とは別の技術が必要だったからです。
この研究も同じ位置にいます。航路の実在は確認できた。ここから先は理論ではなく供給の工学で、伸びしろは3つあります。
第一に、観測の再現性。 ArchMap の生命線はここです。同じコードを2つの独立した LLM パスに読ませたとき、機械的に一致した観測は生の状態でわずか 9.4% でした。ただし内訳が重要で、誤りとして棄却されたのは全 2,819 件の調停(サブエージェントによる全件ソース再読)のうち 29 件だけ。観測の正しさは再現していて、ずれの主因(約9割)は同じ事実を指す名前の書き方、残りは粒度の選び方と、片方のパスだけが拾った観測でした。命名・粒度・記法の収束規約と正規化した照合鍵を入れた再抽出実験で、鍵の収束率は 0.32 → 0.74 まで上がっています。目標は 0.8。届くまでは独立2パス+全件調停という重い安全網で品質を担保し、届けば §6 の差分更新の経済性が本格的に立ち上がります。数字が動くたびに、この連載で報告していくつもりです。
第二に、供給の抽象化。 今回、SAGA の供給契約を満たすために、私たちは ArchSig の評価器のソースコードを読みました。実ユーザーに要求できる手順ではありません。ArchMap 供給には既にある「理論を知らなくても組める」抽象化を SAGA 供給にも作る。修理対象のループを指させば必要な観測一式が組み上がる形が、設計の目標です。
第三に、次の計測。 実害の規模を語るための runtime 実測(金額で重み付けした解析)と、2つ目・3つ目の外部 OSS です。
岬に旗は立ちました。「局所は正しいのに大域で壊れる」は、実在の OSS で、計測として、確かに観測される。前回の記事の最後に書いた「公理から生えた数学」は、現実の海につながっていました。
参考
- リポジトリ: AlgebraicArchitectureTheoryV2(MIT ライセンス)
- one-cent デモ(合成例・再現可能):
tools/archsig/examples/practical-rust-service/ - 対象コードベース: FudanSELab/train-ticket(commit
313886e9)