Daily Papers

haynes26a_ja

67 min read

Decidable By Construction: Design-Time Verification for Trustworthy AI

原題: Decidable By Construction: Design-Time Verification for Trustworthy AI 著者: H. Haynes | 会議: 2026 | 引用: 0 PDF: haynes26a.pdf

Decidable By Construction: Design-Time Verification for Trustworthy AI Houston Haynes SpeakEZ Technologies, Asheville, NC hhaynes2@alumni.unca.edu March 2026

要約 要約 機械学習における一般的な前提は、モデルの正しさを事後に強制しなければならないというものである。我々は、AI モデルが数値的に安定しているか、計算上正しいか、物理ドメインと整合性があるかを決定する性質は、必ずしも事後の強制を必要としないことを観察した。これらは、トレーニングの最初のステップが始まる前に設計時に検証可能であり、その際のコストは僅かな計算コストで済む。このアプローチの設計は、現在の慣行よりも有利なトレーニングおよびランタイム特性を示唆しており、特に高レバレッジ意思決定支援や科学的制約のある設定で展開されるモデルにとって重要である。本論文では、これらの望ましい性質が特定の代数的構造を共有することを示す：それらは有限生成アーベル群 Zn 上の制約として表現可能であり、推論は多項式時間で決定可能であり、主型（principal type）は一意である。この観察に基づいて構築されたフレームワークは、3 つの先行する結果 [Haynes, 2026b,c,a] を構成する：物理単位など任意のアノテーションをモデル展開を通じて永続的な codata として保持できる次元型システム；型シグネチャのみからクリフォード代数の grade（階数）を推論し、幾何積のスパース性を導出するプログラムハイパーグラフ；および順伝播モードのコエフェクト解析と正確な posit 蓄積を通じてトレーニング中に次元および grade の不変量を保持する適応ドメインモデルアーキテクチャである。我々は、この構成が新しい情報理論的結果をもたらすと考えられる：アーベル群上の Hindley–Milner 統一は、ソロモノフの普遍事前分布（Solomonoff’s universal prior）の計算可能な制限の下での事後最尤仮説を計算し、フレームワークの型推論を普遍誘導と同じ形式的基盤に置く。我々は AI の信頼性に関する4つの現代的アプローチを比較し、それぞれが展開、層、および推論リクエスト全体で増幅される可能性のあるオーバーヘッドを課すことを示す。このフレームワークは構成によってそのオーバーヘッドを排除する。正しさは、暴力的な計算や事後の介入ではなく、原理に基づいた設計から生じる。

  1. 現状 現代の AI 信頼性インフラは構造的に共通の前提を共有している：モデルが先に存在し、修正メカニズムが事後に適用される。以下の各アプローチは、真の故障モードに対処するものである。4 つの展開例がこのパターンを示す。 Moreau プロジェクション [Boyd and Vandenberghe, 2004] は、GPU アクセラレーションされた内点法を用いてモデル出力を凸実行可能集合に射影する。物理情報ニューラルネットワーク [PINNs; Raissi et al., 2019] は、トレーニング損失に物理残差項を追加する。DeepSeek の Engram [Cheng et al., 2026] は、経験的に選択された Transformer レイヤーに O(1) ルックアップモジュールを挿入する。横断的 ARC ソルバー [DH, 2026] は Plücker 座標を用いてゼロ学習でパターン認識タスクを解決する。 各展開アプローチは、展開数、層数、または処理される推論リクエストの数に比例した継続的なコストを支払う可能性がある。共通の構造的理由は、従来のパイプラインが修正介入を不要にするはずだった意味情報を消去していることである。 我々の Fidelity フレームワークに関する現在の研究トラックは、新たな立場を確立する。AI モデルの正しさ、次元的一貫性、grade 保存、エスケープ分類、および数値表現の適切性を支配する性質は、型システムの性質である。それらは決定可能であり、多項式時間であり、主型である。このフレームワークは、出現するハイパーグラフの展開中に設計時にこれらを検証する。この検証の边际コストは無視できるほど小さく、下流の便益に関する我々の見積もりは実質的である。トレーニングに対する結果は、有利なコストおよびエネルギー効率であり、特に解釈オーバーヘッドと標準的なトレーニングパイプラインの特徴である大幅なリソース管理負荷と比較して測定された場合である。標準的なパイプラインは、すべての操作で動的ディスパッチおよびランタイム形状チェックに対して支払う必要がある。設計時に型をチェックするネイティブ検証済みトレーニングループは、モデル仕様時（検証が高速、精密、かつ安価である時点）に一度だけ支払えばよい。対案は、各展開、各層、または各推論パスで繰り返される可能性のある暴力的な計算と事後の介入である。

  2. 決定性仮説 定理 2.1（正しさの性質の決定性）。AI モデルの正しさを支配する構造的性質 P を次元的一貫性、クリフォード grade 保存、エスケープ分類、および数値表現の適切性と定義する。これらが有限生成アーベル群 Zn 上の制約として表現されたとき、P のすべての性質は以下の通りである。

  3. 決定可能。フレームワークは、有限時間内にすべての整形式モデル仕様に対して明確な yes/no 回答を生成する。

  4. 多項式。解決コストは Z 上のガウス消去法により O(n^3) である。

  5. 主型。最も一般的な解（自由変数が最少で、満たされる制約が最多）が存在し、一意である。 実用的には、これはフレームワークが計算を実行する前に、モデルの次元単位が整合しているか、幾何代数演算が正しい grade を保存しているか、メモリ割り当てが決定論的であるか、数値表現が対象ハードウェアにとって適切であるかを判断できることを意味する。回答に曖昧さはなく、ヒューリスティックは関与せず、計算は制約変数の数の立方に比例した時間で完了する。標準的な型システムは構文をチェックするが、これは物理法則をチェックする。 「構成による（by construction）」という修飾語は精密である。フレームワークの仕様言語は Zn 断片内で表現可能な制約のみを許容する。型チェックに通るモデル仕様は、その事実により決定可能断片内にある。より強い推論（量化子の交互、不動点計算）を必要とする性質は Tier 1 型システムでは表現できず、セクション 5.3 で記述される段階的検証ティアに委ねられる。決定性はフレームワークが発見する性質ではなく、フレームワークがその型言語の構造を通じて強制する性質である。 代数的基盤は、モデル構築に必要な演算に対する Zn の閉包性である。物理次元は乗法に対してアーベル群を形成する（Zn における指数ベクトルの加法）。クリフォード grade は幾何積によって合成され、出力 grade は入力 grade と代数のシグネチャによって決定される。エスケープ分類は有限格子を形成し、決定可能な順序関係を持つ。各構造は Hindley–Milner 統一 [Hindley, 1969, Milner, 1978, Kennedy, 2009] の拡張を通じた多項式時間推論を許容する。

2.1 微分に対する閉包性 アーベル群断片は連鎖律に対して閉じている。f : R⟨d1⟩→R⟨d2⟩の場合、 ∂f/∂x : R⟨d2·d−1_1⟩ (1) これは指数代数における減算（Zn における d2 − d1）である。各勾配ノードは、順伝播を検証するのと同じガウス消去法によって検証される次元を受け継ぐ。この閉包性はクリフォード grade に拡張される：grade-k の計算の勾配は、連鎖律の次元算術によって決定される grade を持つ。 補題 2.1（トレーニングの決定性）。順伝播モード自動微分 [Baydin et al., 2022] は、層ごとの O(1) 補助メモリで方向微分を計算する。すべての中間変数はスタックスコープであり、値は生成されたスコープから漏れない。アーベル群断片内の計算の導関数は、その断片内に留まる。トレーニングは推論と同じく決定可能である。 これは、設計時に検証された保証がモデルがトレーニングに入っても消失しないことを意味する。勾配計算は順伝播と同じ次元および grade 制約を受け継ぎ、層ごとの定数補助メモリを使用し活性化テープを持たず、全体を通じて決定可能な断片内に留まる。標準的なトレーニングパイプラインがトレーニングの発散または物理的に意味のない出力の生成後にのみ制約違反を発見するのに対し、このフレームワークはそれらの違反が発生すること自体を防ぐ。

2.2 結合制約空間 grade 推論を備えた DTS は、アーベル群の積上で動作する： Z^7_{SI base dimensions} × Z_{Clifford grade} = Z^8 (2) 統一アルゴリズムは Z^8 上の連立一次方程式系を解く。手順はガウス消去法であり、1 つの軸で拡張されたものであり、決定可能であり、多項式時間であり、主型である。結合空間における事前分布は、自由次元変数が最少で、grade スパース性が最大で、満たされる制約が最多の割り当てを好む。具体的には、フレームワークは物理単位と幾何代数 grade の両方を、すべての現代的数値ライブラリを支える同じよく知られた線形代数を用いて単一のパスで推論する。grade 推論を次元推論に追加することは、制約変数ごとに整数 1 つを追加コストとする。

  1. 構成 ここで提示されるフレームワークは、それぞれが独立して結果を確立した 3 つの先行論文を構成するものである。最初の論文 [Haynes, 2026b] は次元型システムと決定論的メモリ管理を導入する。2 番目の論文 [Haynes, 2026c] はクリフォード代数上の grade 推論を備えたプログラムハイパーグラフを導入する。3 番目の論文 [Haynes, 2026a] は検証済みトレーニングおよび展開のための適応ドメインモデルアーキテクチャを導入する。関心のある読者は、それらの論文に完全な形式的開発を見つけるであろう；以下は、どれか一つでは主張できない構成論である。 構成は連結ではない。各論文の結果は、個別の論文が主張できない結果に対する前提条件となる。DTS は次元制約を提供し、PHG は grade 制約を提供し、ADM は両方を重み更新を通じて保持するトレーニング基盤を提供する。依存関係は循環的である：grade 推論は次元推論を強化し（Cayley 表を制約することにより）、次元推論は grade 推論を強化する（特定の計算に適用される代数シグネチャを決定することによって）。Program Semantic Graph (PSG) は、この相互強化が展開中に不動点に収束する構造である。 以下のセクションで提示される形式的構造は、実装をガイドし制約するのに十分な精度で確立されている。実装自体は、説明されたハードウェアターゲットおよび展開トポロジーの全範囲にわたって活発に開発中である。テキストが現在形でシステム動作を記述している箇所では、ここで与えられた論証によって形式的性質が検証される設計意図を記述していると読むべきである。

3.1 DTS/DMM：次元の永続性とメモリの決定性 Dimensional Type System [Haynes, 2026b] は、Zn から導出された制約を用いて Hindley–Milner を拡張し、推論を決定可能で完全かつ主型とする。次元アノテーションは PSG codata として多段階精緻化 [Lattner et al., 2021] を通じて永続し、すべての段階で利用可能である。Deterministic Memory Management との結合は形式的な依存チェーンである： Dimension range → Representation width → Footprint escape → Allocation (3) 各ステップは先行する推論の出力を消費する。Dimensional range は表現選択（posit, IEEE 754, 対象ごとの固定小数点）を決定する。Representation width はメモリフットプリントを決定する。 Footprint は、エスケープ分類（スタックスコープ、クロージャキャプチャ、リターンエスケープ、参照によるエスケープの 4 つの格子）と組み合わされ、割り当て戦略を決定する。このチェーンは展開中に検証され、設計時のフィードバックとして提示される。 Kennedy の Units of Measure [Kennedy, 2009] は型チェック中に次元を検証し、コード生成前にそれらを破棄する。下流のステージではそれらを見ない。DTS は異なるアプローチを採用する：次元アノテーションは PSG codata としてすべての精緻化段階を通じて永続し、表現選択が行われる時点（posit vs. IEEE 754 vs. 固定小数点、値範囲によって決定）、メモリ配置が行われる時点（フットプリントとエスケープ分類によって決定）、およびクロスターゲット転送忠実度が検証される時点（次元メタデータは BAREWire を通じてシリアライズされたデータに付随する）で利用可能である。アノテーションはこれらの決定をガイドし、その後消費される。その結果、表現、メモリ、および忠実度の決定は、型チェッカーが検証したのと同じ次元構造によって情報提供される。

3.2 PHG：grade 推論と幾何スパース性 Program Hypergraph [Haynes, 2026c] は、バイナリ PSG エッジを k-ary ハイパーエッジに一般化する。クリフォード代数 Cl(p, q) における grade は DTS の次元軸である。推論機構は型シグネチャから幾何積 Cayley 表の非ゼロエントリを導出する： grade-k ∧ grade-j → grade-(k + j) (4) grade-k · grade-j → ⋁_{i=0}^{min(k,j)} grade-(|k −j| + 2i) (5) Cl(3, 0, 1)（射影幾何代数）の場合、双ベクトル×双ベクトル積は grade 0, 2, および 4 に制約される。grade 1 と 3 は代数の公理により構造的にゼロである。 これらのコンポーネントは計算から完全に欠落している。 スパース性は層全体で増幅する。Cl(p, q) 上の L レイヤーネットワークにおいて、各レイヤーの出力 grade は次レイヤーの入力 grade を制約する。2^{2(p+q)} の Cayley 表エントリを関与するように見える計算は、非ゼロ部分に還元されるが、実用的な代数ではこれは完全な表の 5–50% である。Cl(3, 0, 1) の場合、完全な Cayley 表には 256 エントリがあり、grade 推論は双ベクトル-双ベクトル積を 48 の非ゼロエントリに還元し、5.3 倍の削減となる。L レイヤーネットワーク全体で、この削減が増幅する：各レイヤーの出力 grade が次レイヤーの入力を制約し、フレームワークはこれらの制約を前方伝播して各レイヤーに適した計算を決定する。この削減は展開中に検証される。ランタイムチェックは不要であり、構造的にゼロなコンポーネントは決してインスタンス化されなかった。

3.3 ADM：検証済みトレーニングアーキテクチャ Adaptive Domain Model [Haynes, 2026a] は、先行する結果をトレーニング基盤として構成する。これがなぜ重要かを理解するために、現代の AI システムにおける標準的な分離を考えること：トレーニングは一つの環境で、一つの一連のツールと仮定の下で行われ、得られたモデルはその後完全に異なる環境にエクスポートされて展開される。2 つのフェーズはほとんど共通点を持たない。トレーニングパイプラインはモデルが実行されるハードウェアを知らない。展開パイプラインはトレーニングプロセスが満たすべき制約を知らない。その間のギャップこそが、信頼性故障の多くが発生する場所である。 ADM アーキテクチャはこのギャップを埋める。トレーニングと推論は同じ型付きインフラ上で動作し、同じ次元および grade 制約によって支配され、同じ展開プロセスによって検証される。フレームワークはトレーニングをモデルを生成するブラックボックスとして扱うのではなく、実行前および実行中に性質が検証可能な型付き計算として扱う。これは現在の慣行とは根本的に異なる運用モデルである。 これを可能にする 3 つの性質がある： 深さ非依存トレーニングメモリ。標準的な逆伝播モード自動微分は、すべてのレイヤーの中間活性化を保存し、ネットワーク深さに比例して増加するメモリを必要とする。順伝播モードのコエフェクト解析 [Baydin et al., 2022] はこれを排除する：層ごとの O(1) 補助メモリ、すべての中間変数はスタックスコープ、活性化テープなし。実用的な結果は、トレーニングメモリが深さに関わらず推論フットプリントの約 2 倍に制限されることである。 grade 保存重み更新。b-posit quire [Gustafson and Yonemoto, 2017, Jonnalagadda et al., 2025] は、勾配内積のための正確な蓄積を提供する。丸めは最終変換時に一度だけ発生する。これは重要である。なぜなら IEEE 754 の丸めはトレーニングステップ全体で構造的ゼロを破損し、代数的にゼロな grade に数値的に非ゼロなコンポーネントを生じさせる可能性があるからである。一度破損すると、後続の演算はこれらの幻影コンポーネントを実在として扱い、破損が伝播する。quire はこのドリフトを完全に防止する。 ウォームローテーションによる検証済み展開。標準的な展開はコールドスワップである：アクティブなモデルがアンロードされ、代替品がロードされ、移行中に推論が利用不能となる。ウォームローテーション [Haynes, 2026a] は、更新された重み構成を交換しながら推論を継続し、どのリクエストも部分的状態を観測しないという運用パターンである。着信構成は PHG 展開を通過し、次元的一貫性、grade の正しさ、および表現の適切性のすべての証明義務を果たした後でローテーションの対象となる。移行は推論リクエストに対して原子操作である：飛行中のリクエストは現在のモデルに対して完了し、新しいリクエストは検証済みの代替品によって処理される。展開に失敗した構成は、アクティブなパスに入る前に拒絶される。順伝播トレーニングメモリが推論フットプリントの約 2 倍に制限されているため、代替品のトレーニング計算は、専用トレーニングウィンドウを必要とせずに、利用可能な計算容量（同一場所または別ノード）で並行して実行可能である。 ベイズ蒸留。標準的なファインチューニングは、固定アーキテクチャおよび固定損失の下で事前学習済みモデルのパラメータを調整する。事前学習済み点推定の局所近傍のみを探査する。ベイズ蒸留は異なるアプローチを採用する：変分推論を用いて一般モデルの潜在事前分布からドメイン事後分布を抽出し、次元的一貫性および grade 保存部分空間に制約される。結果は元のものの局所的に調整されたコピーではなく、ドメインの物理的制約を満たす部分空間上の事後分布を回復する幾何構造化された抽出である。得られたドメインモデルはより小さく、より精密であり、そのドメインの物理的構造と証明可能に整合している。 これはまた、ドメイン固有 AI に悩まされるブートストラップ問題を解決する。ドメインモデルには通常、専門分野では収集が困難または不可能な大量のドメイン固有トレーニングデータが必要である。ベイズ蒸留はこの問題を回避する：一般モデルの潜在構造が事前分布を提供し、ドメイン制約が尤度を提供し、蒸留手順が事後分布を計算する。事前分布がすでに情報提供されているため、ドメインデータの要件は劇的に低下する。

  1. 構成の結果 3 つの論文はそれぞれ独立して存在する。以下の結果は構成の形式的結果であり、いずれかの単独の論文には成立しない。

4.1 検証済みトレーニング F − ma を計算する物理情報損失項は展開中に検証される： ⟨N⟩−⟨kg⟩· ⟨m · s^−2⟩= ⟨N⟩−⟨N⟩ ✓ (6) 置換 F − mv は拒絶される： ⟨N⟩−⟨kg⟩· ⟨m · s^−1⟩= ⟨N⟩−⟨kg · m · s^−1⟩ type error (7) 異なる次元を持つパラメータ間の勾配蓄積も同様に制約される。次元が ⟨N/m⟩の勾配は ⟨J/s⟩と蓄積できない。これはモデル仕様時に検出される設計時のエラーである。次元情報がトレーニング開始前に破棄されるため、既存の ML フレームワークはこのエラーを検知しない。 同じ原則が物理学以外でも適用される。リスク調整リターンを return × volatility として計算する金融モデルを考えるが、正しい定式化は return/volatility（Sharpe 類似比）が必要である場合がある。2 つの式は異なる次元シグネチャを持つ：最初のものは [currency · currency · time^−1] の次元を持ち、2 番目は [dimensionless] である。DTS は展開中に最初のものを拒絶する。標準的な ML フレームワークはいかなる段階でもこのエラーを検知しない；モデルはトレーニングし、収束し、数値的には妥当だが次元的には不整合な出力を生成する。 現在の慣行では、この種の潜在的エラーに対する標準的な救済策は過剰パラメータ化である：損失曲面が十分に滑らかになり、最適化子が根本的な不整合にもかかわらず収束するようにモデル容量を追加すること。これはトレーニング損失が減少するという意味で機能するが、その効果はトレーニング分布への影響を統計的に無視できるほど小さくするために十分なパラメータ体積にエラーを埋め込むことによる。不整合は残っており、次元の不一致が出力を生じさせる分布外入力にモデルが遭遇するまで露出されない。より深い結果は計算に関するものである。過剰パラメータ化されたモデルは、型システムがトレーニング開始前に排除した構造的エラーを補償しているため、収束に至るために比例して多くのトレーニング時間、メモリ、およびエネルギーを必要とする。次元検証済みモデルは、制約され整合した部分空間上でトレーニングする。探索体積は小さい。セクション 4.2 で記述される grade 推論と Cayley 表の除去はこの利点を増幅する：構造的にゼロなコンポーネントはすべての操作から削除されるため、モデルはより小さな空間を検索しているだけでなく、その空間内でステップごとの演算数も減少させる。探索体積およびステップごとのコストの両方の削減により、ターゲットを絞った検証済みドメイントレーニングが、大幅に短いウォークロック時間と計算で同等またはそれ以上の結果を達成できることが示唆される。

4.2 grade 保存幾何ネットワーク Cayley 表スパース性は層全体で増幅する。Cl(3, 0, 1) の場合、完全な表には 256 エントリ（16 × 16 ベーシス要素）がある。双ベクトル×双ベクトル積は grade 0, 2, および 4 のみを使用し、ベクトル×ベクトル積は grade 0 と 2 のみを使用する。これらの制約は展開中に解決され、非ゼロコンポーネントのみが計算に参加する。 IEEE 754 の丸めはトレーニングステップ全体で構造的ゼロを破損する可能性がある。grade 1 で代数的にゼロなコンポーネントが累積丸め誤差を通じて数値的に非ゼロの値を獲得し、後続の演算はそれを非ゼロ grade-1 コンポーネントとして扱う。b-posit quire は勾配計算を支配する内積のための正確な蓄積を提供する。構造的ゼロはトレーニングを通じて構造的にゼロのままとなる。

4.3 型付き推論制御 ドメイン認識推論における最先端技術は急速に進化しており、検索拡張生成から構造化ツール使用、学習済みルーティングに至るまで、各手法がパラメトリック知識と展開要件の間のギャップを縮めている。最も一般的な出発点は依然としてコンテキストウィンドウ拡張であり、取得されたテキストがプロンプトに付加され追加入力として条件付けられることである。これは効果的であることが証明されているが、検索自体は型付きではない：取得されたコンテンツには次元アノテーションも grade 構造も、消費する計算との形式的関係もない。 このフレームワークは再帰アーキテクチャにおける進展を通じてこれに対処する。Hierarchical Reasoning Model (HRM) [Nguyen et al., 2025] は、複数の時間スケールで動作する相互依存再帰モジュールがトレーニング安定性をもって大幅な計算深さを達成し、最小限のデータで複雑な推論タスクにおいてほぼ完璧な性能を達成できることを示す。Resonant Recurrent Model (RRM) はこの原則を時間レベル間の動的結合によって拡張するが、外部状態に対して閉じている。porous RRM は指定された相談ステップで再帰ループを開き、モデルが型付きクエリを発信し、ドメイン固有の Adaptive Domain Models から構造化応答を統合することを可能にする。 「porous（多孔質）」という用語は意図的なものである：モジュール境界は選択的に透過性であり、型付き制約を満たす相談のみを受け入れる。各相談ポイントで、クエリ投影が次元型付き要求を生成する。応答ドメインモデルは BARE プロトコル（BAREWire によって実装）を通じて構造化事実を返す。ここで各フィールドには検証可能な型情報が含まれる：値（b-posit, 正確な蓄積）、次元（Zn 指数ベクトル、ガウス消去法で検証）、信頼度（事後区間、範囲分析で検証）、および証明書（PHG ハイパーエッジハッシュ、Z3 充足可能性で検証）。応答は標準的なトークン化-埋め込み-アテンションパイプラインを再エンコードすることなく次元および grade 構造を保持する型付き注入を通じて再帰に入る。型チェックのいずれかに失敗した応答は、モデルの状態に影響を与える前に拒絶される。 これは従来の検索との決定的な相違である。相談境界はテキストインターフェースではなく、型付きプロトコルである。モデルは「X について何を知っていますか？」と尋ねて段落を受け取るのではなく、次元型付きクエリを問いかけ、統合前に進行中の計算との整合性が検証された次元型付き応答を受け取る。

要約（続き） 相談は整合性の基準も満たす：ドメイン応答を統合することによって引き起こされる状態変化は、モデルの現在の期待とドメイン事後分布との間の発散よりも小さくなければならない。形式的には： DKL(pRRM(htc+1) ∥pRRM(htc)) < DKL(pRRM(htc) ∥pD(rtc)) (8) これは過剰相談を防ぐ：モジュールは、統合がモデルの状態を、最初の相談を引き起こした不一致よりも大きく乱す応答を受容しない。この基準は測定可能であり、すべての相談イベントで強制され、外部知識の統合の累積効果に対する形式的な上限を提供する。 独立した検証がこのアプローチをサポートしている。Roy 他 [Roy et al., 2026] のλ-RLM フレームワークは、推論の型付き構造化制御が指数関数的な精度の低下を多項式的な低下に変換し、最大 +21.9 精度ポイントと 4.1 倍のレイテンシ削減をもたらすことを示している。彼らの結果は核心的洞察を確認する：推論時の推論が型付き構造によって支配される場合、信頼性特性は質的に変化する。

4.4 継続的学習 推論と継続的学習のコエフェクト・シグネチャは、2 つのアノテーションにおいて異なる： 表 1：コエフェクト比較：推論 vs 継続的学習。 プロパティ 推論 継続的学習 補助メモリ 層ごとの O(1) 層ごとの O(1) エスケープ分類 すべてスタックスコープ すべてスタックスコープ 蓄積 不要 クワイア（正確） 重み更新 なし ローカル、スコープ付き 両方ともスタック適格である。推論/トレーニングフェーズの境界はコエフェクト設定である。空間ハードウェア（AMD XDNA 2）上では、この区別はタイル割り当て比率にマッピングされ、コエフェクトシステムは両方の構成がリソース有効であることを検証する。

  1. 処理可能な事前分布：ソロモノフとの接続 決定性仮説は、私たちが知る限り文献で明示的に述べられていない結果を通じてアルゴリズム情報理論につながる。 5.1 普遍事前分布から計算可能断片へ ソロモノフ [Solomonoff, 1964] は、二進文字列上の普遍事前分布を定義した： P(x) = Σ_{p : U(p)=x*} 2^{-|p|} (9) ここで U はユニバーサルチューリングマシンであり、x*は x で始まる出力を持つプログラムを表し、|p|はビット単位のプログラム長である。この事前分布は半計算可能である：上から計算列挙可能だが、有限計算不可能である [Kolmogorov, 1965, Hutter, 2000]。 仮説空間はすべてのプログラムである。和は無限の非計算集合上で取られる；P(x) は上から計算列挙可能だが有限計算不可能である。実用的適用性を支配する問いは：仮説空間のどの制限が対応する事前分布を計算可能にし、それらの制限のうちどれが重要な性質を捉えるのに十分表現力があるか？ 5.2 処理可能性メカニズムとしてのアーベル群 仮説空間を Z 上の有限生成アーベル群に制限することは、半計算可能な事前分布を計算可能なものに変換する。この制限は 2 つの性質を保持する：十分な表現力（制限されたクラスにはモデル正しさを支配する仮説が含まれる）と処理可能な推論（決定手続きが多項式である）。 Zn 上の HM 統一は主型を計算する：自由変数が最少で満たされる制約が最多の割り当て。この主型は、短い記述を好む事前分布の下での事後最尤仮説である。

命題 5.1（MAP 仮説としての主型）。H をプログラムの型制約と整合するすべての次元割り当ての仮説空間とし、Zn 上の連立一次方程式系として表現する。π(h) ∝2^{-|h|} という事前分布の下で、|h|は自由次元変数の数を数える場合、HM によって計算される主統一子は MAP 推定である： h* = arg max_{h∈H} π(h) = arg min_{h∈H} |h| (10) この MAP 推定は Z 上のガウス消去法により O(n^3) で計算可能である。 ソロモノフとの接続は形式的であり、単なる類推ではない。Li と Vitanyi [Li and Vitanyi, 1997] は、Minimum Description Length [Rissanen, 1978] と Kolmogorov 複雑性の間の等価性を確立した。任意の計算可能クラス H に対して、MDL 仮説は H に制限された普遍事前分布の下での MAP 仮説と一致する。Zn 断片は計算可能クラスである；DTS 推論はその上での MDL 手続きである： • |M| = 自由次元変数の数（モデル複雑度） • |D|M| = 違反した制約の数（データ適合性） • 主統一子は |D|M| = 0 を条件として |M|を最小化する grade 推論はこれに第 2 の軸を追加する。「モデル複雑度」は非ゼロの Cayley 表エントリの数になる。grade 推論はすべての grade 制約が満たされるという条件下でこの量を最小化する。 5.3 段階的検証モデル 処理可能性の結果は、より強力な検証ティアへの自然な拡張を許容する： 表 2：仮説空間の段階的制限としての検証ティア。 断片 表現力 推論 事前分布 コスト Zn（Tier 1） 次元、grade、エスケープ 多項式 計算可能、正確 無視できる （積による精緻化；グラフ整合性は Z3 で処理される） QF LIA（Tier 2） 範囲、不変量 NP-完全 計算可能 中程度 （Tier 1 を超える追加の Z3 クエリ） FOL（Tier 3） 任意の一階性質 半決定性 半計算可能 高い （PSG の証明義務） ティアは包含鎖を形成する： Zn ⊂ QF LIA ⊂ FOL ⊂ TM (11) 各包含は仮説空間を広げ、表現力を高め、処理可能性を低下させる。重要な注記：Z3 は Tier 2 に限定されない。Tier 1 では、ガウス消去法が Zn 算術を解決するが、PSG 自身が精緻化を通じて構造的不変量を維持し、次元および grade 制約がハイパーエッジ変換全体で正しく伝播するという証明は、コンパイル時に Z3 を通じて処理される。これはコード証明ではない；グラフ整合性証明であり、ハイパーグラフがモデル仕様の各段階を通じて検証済み性質を保持していることを確認するものである。Tier 2 は、Zn 断片がカバーするものを超える追加の性質（範囲、不変量）に対して Z3 を呼び出す。実用的観察：AI モデル正しさを支配する最も有用な性質は Zn 断片（Tier 1）に存在する。フレームワークはこれらを自動的に、すべてのモデルについて多項式時間で導出する。 5.4 クワイアによる断片保存 クワイアは、順伝播モード勾配計算を支配する内積に対する正確な蓄積を提供する。処理可能な事前分布の観点から：正確な蓄積とは、数値誤差によって勾配計算がアーベル群断片から逸脱しないことを意味する。IEEE 754 の丸めは構造的にゼロのコンポーネントを数値的に非ゼロにし、計算を構造的不変性がもはや検証できない領域へドリフトさせる可能性がある。クワイアは、トレーニング全体を通じて計算が決定可能な断片内に留まるという不変量を維持する。 統合された図像は、普遍誘導の処理可能な制限を実装する検証フレームワークである。この制限は同時に 3 つの性質を購入する：計算可能性（事前分布は有限計算可能）、処理可能性（推論が多項式）、十分性（制限されたクラスが AI モデル正しさを支配する性質を捉える）。フレームワークは、正確な意味で、重要な断片上のソロモノフ誘導子である。

  1. 比較分析 以下の各アプローチは実際の故障モードに対処している。分析はそれぞれが抱える構造的限界と課すコスト構造を特定する。 6.1 凸射影（Moreau） Moreau プロジェクション [Boyd and Vandenberghe, 2004] は、微分可能な内点法を用いてモデル出力を凸実行可能集合に射影する。CVXPY はチームの先行作品であり、月間 300 万ダウンロードを超え、微分最適化のパラダイムを確立した。射影演算子はトレーニング動態に幾何学的病理を導入する。制約なし出力 y と実行可能集合 C に対して、射影 ΠC(y) = arg min_{c∈C} ||y − c|| は常に最寄りの境界に向かって指す。ヤコビアン ∇yΠC(y) はトレーニングステップ全体でこの方向を強化し、制約境界に沿ったアトラクター盆地を作成する。C 内部では勾配は変更なしで通過し、外部では最寄りの境界へ曲がる。非凸ネットワークと凸射影の合成は、目的関数に依存せず制約境界への体系的バイアスを持つ損失曲面を生成する。これは収束の問題ではない；最適化幾何の構造的歪みである。 制約集合の次元的一貫性は検証されていない。ソルバーは y ∈ C を強制するが、C が意図した物理を符号化しているかチェックしない。 コスト：各推論ステップごとの内点法解決、リクエスト量に比例、非アモタイズ。 DTS 代替案：設計時における制約仕様の次元検証；各推論コストゼロ。 6.2 損失整形（PINNs） 物理情報ニューラルネットワーク [PINNs; Raissi et al., 2019] はトレーニング損失に物理残差項を追加する。損失関数の次元的一貫性は検証されていない。F − mv（力マイナス運動量）を計算する項は検証を通り、トレーニングされ、トレーニング分布上では良好に機能する可能性がある。不整合はモデルが物理的に不可能な予測を生み出す分布外入力で表面化する。既存の ML フレームワークはこの検出を行わないのは、次元情報がトレーニング開始前に破棄されるからである。 コスト：ドメインごとのカスタム損失項、ドメイン専門家による導出が必要；ドメイン数に比例。 DTS 代替案：型推論中のすべての算術操作の次元的一貫性を検証；無視できる増分コストで。 6.3 条件付きメモリ（Engram） DeepSeek の Engram [Cheng et al., 2026] は、特定の Transformer レイヤーに静的パターン用の O(1) ルックアップを追加し、バックボーンが計算を通じて検索をシミュレートする負担を軽減する。等パラメータおよび等 FLOP バジェットにおいて、Engram-27B は MoE-27B を上回り、推論（BBH +5.0）とコード（HumanEval +3.0）で改善をもたらす。 モジュール配置（30 ブロックの Transformer のレイヤー 2 と 15）は経験的である。取得された埋め込みには次元アノテーション、grade 構造、または消費計算との形式的関係がない。過剰相談はパフォーマンスを低下させる；アーキテクチャには相談頻度を支配する形式的基準がない。 コスト：各アーキテクチャごとに最適な配置を再発見；展開構成に比例。 Fidelity 代替案：BARE プロトコル（BAREWire）による型付き相談、周波数を支配する整合性基準（式 (8)）、応答には次元アノテーションと PHG 証明書を含む。 6.4 幾何ソルバー（Plücker / ARC） 横断的 ARC ソルバー [DH, 2026] は Plücker 座標（Cl(3, 0, 1) の grade-2 ビベクター）を用いて、ゼロ学習で 316 の ARC-AGI タスクを解決する。 ソルバーは 2 つの PHG クレームを検証する：クリフォード代数は抽象パターン認識に十分な幾何構造を提供し、grade 非意識は測定可能な計算コストを伴う。 grade 構造はすべての操作に含まれるが実装には見えない。Plücker 線は double[6] アレイである。ソルバーは構造的にゼロの Cayley 表エントリを計算するタスクの 34% でタイムアウトし、設計外の転換タイプを捉えることができない固定埋め込みのために 3% で失敗する。 両方の故障モードは grade 推論（構造的にゼロのコンポーネント上の計算を除去）と型付き埋め込み導出（PHG ガイド型分析を通じて埋め込みセットを拡張）によって対処可能である。 6.5 コスト構造サマリー 表 3：AI 信頼性アプローチのコスト構造。 アプローチ フェーズ 边际コスト スケール Moreau ランタイム リクエストごとの定数 リクエスト量 PINNs トレーニング ドメインごとの線形 ドメイン数 Engram 設計 構成ごとの線形 アーキテクチャ変種 Fidelity 精緻化 無視できる アモタイズ 事後アプローチは線形または定数の边际コストを持つ。各新しい展開、層、または推論リクエストは最初のものと同じ価格を支払う。設計時アプローチはフレームワークが存在した後に無視できる边际コストを持つ。コスト構造は実装の詳細ではない；決定性仮説の結果である。精緻化時に決定可能な性質にはランタイム強制を必要としない。ランタイムで強制される性質は、強制サイトの数に比例する強制を必要とする。展開が普及し、アーキテクチャが深くなり、推論量が増大するにつれて、集約コストの差は複利する：各新しい展開は各追加層および各追加リクエストと相互作用する。事後コストは O(d · l · r) としてスケールし、d は展開数、l は層数、r は推論リクエスト数である；設計時コストは展開ごとの O(1) のまま。

  2. 関連研究 Kennedy の Units of Measure [Kennedy, 2009] は、次元制約が HM 推論と統合されることを示した。DTS はこれを拡張し、すべての精緻化段階を通じて次元を保持する（Kennedy のシステムはコード生成前に破棄する）こと、および次元推論を表現選択およびメモリ管理に結合することによって。 Petriˇcek, Orchard, および Mycroft [Petricek et al., 2014] はコエフェクトを文脈依存計算の微積分として形式化した。DMM はこの形式化をメモリ配置に適用し、ここで計算が要求する「文脈」は割り当て戦略と寿命バウンドである。 CDL 論文 [Gavranovic et al., 2024] はニューラルアーキテクチャ合成のための圏論的意味論を提供する。Fidelity フレームワークはこの意味論の特定の断片（順伝播/逆伝播モードを支配する随伴対応）を実装し、設計時の検証として 2-圏推論の一般性を処理可能なアーベル群推論と交換する。 Baydin, Pearlmutter, および Syme [Baydin et al., 2022] は順伝播勾配計算を示した。ADM 論文 [Haynes, 2026a] はこれを拡張し、順伝播トレーニングメモリを決定論的かつスタック適格にするコエフェクト解析を行う。 Gustafson [Gustafson and Yonemoto, 2017] は posit 算術を導入した；Jonnalagadda 他 [Jonnalagadda et al., 2025] は b-posit 有界レジームを通じてハードウェア競争力を付与した。DTS は posit 算術が前提とする形式的メカニズムを提供する：特定の計算に対してどの値範囲が重要かという知識。

  3. スコープと限界 決定性仮説は Zn 断片に適用される。Z3 はすべてのティアで役割を果たす：Tier 1 では、PSG が精緻化を通じて構造的不変量を維持していることを確認するグラフレベルの整合性証明を処理し；Tier 2 では QF LIA クエリを通じて追加の性質（範囲、不変量）を扱い；Tier 3 では証明義務は半決定性であるか外部定理証明を必要とする可能性がある。これらすべてのティア外の性質、終了、活性、任意のプログラム不変量を含むものは非決定可能である。 ソロモノフとの接続は制限されたものである。普遍事前分布はすべてのプログラム上にある；Zn 事前分布は次元および grade 割り当て上にある。制限は計算可能性を購入するが、普遍性を犠牲にする。特定の応用において、次元的一貫性、grade 保存、表現選択、構造的スパース性に対して、制限は重要な性質を捉える。断片外の性質に対して、段階的検証モデルはフォールバックを提供する。 フレームワークはすべてのモデル性質を決定可能にすると主張しない。AI モデル正しさを支配する特定の性質クラスを特定し、このクラスが多項式断片内に含まれることを示し、それ以外の性質に対する段階的メカニズム（Tier 2 および Tier 3）を提供する。境界はアーベル群構造である：Zn 上の線形制約として表現可能な性質は断片内にある；量化子の交互または不動点推論を必要とする性質はない。主張は、前者のクラスが AI モデルが物理的、数値的、構造的に正しいか決定する性質を網羅することである。

  4. 結論 本論文で調査したアプローチは AI 信頼性の真の故障モードに対処しており、それぞれが最先端を進化させた。構造的限界を共有している：修正メカニズムはモデルが存在した後に適用され、その修正のコストは各展開、各層、および各推論リクエストで再発する。AI システムが科学分野、医療機器、自律プラットフォーム、金融商品に普及するにつれて、事後強制の集約コストはモデル、ドメイン、ターゲットの積としてスケールする。 本論文は、AI モデル正しさを支配する性質、次元的一貫性、クリフォード grade 保存、数値表現適切性、エスケープ分類、およびメモリ決定性は、経験的に発見しなければならない出現的性質ではないことを示した。それらは Zn 上の制約として表現可能な代数的性質であり、推論は多項式時間で決定可能であり、主型は一意である。DTS、PHG、ADM の合成はループを閉じる：次元アノテーションはすべての精緻化段階を通じて永続し、grade 推論は構造的にゼロの計算がインスタンス化される前に除去し、トレーニング基盤は順伝播モードのコエフェクト解析と正確な posit 蓄積を通じて重み更新で両方の不変量を保持する。 ソロモノフとの接続はこの観察を情報理論的基盤上に置く。アーベル群上の Hindley–Milner 統一は、普遍事前分布の計算可能な制限の下での MAP 仮説を計算する。フレームワークは正確な意味で、AI モデルの構造的性質に適用された普遍誘導の処理可能な断片である。これは一般知能に関する主張ではない；モデル出力が物理的に意味があり、数値的に安定し、メモリセーフか決定する特定の性質クラスに関する主張である。 実用的帰結は異なるコスト構造である。事後アプローチが各展開、各層、各推論リクエストごとに支払うのに対し、設計時検証は精緻化時に一度だけ支払い、その時はコストが無視できる。この差はスケールとともに複利する。深いアーキテクチャで数百万のリクエストに応える数百の展開を管理する組織にとって、O(d · l · r) の再発コストと O(1) のアモタイズコストの違いは漸増的ではない；質的なものである。 残された重要な作業がある。フレームワークのリファレンス実装は現在特定のハードウェア基盤（FPGA および NPU）および特定の数値表現（IEEE 754 およびクワイア蓄積を持つ b-posit）を対象としている。より広いハードウェアターゲットへのカバレッジ拡張、生産規模での整合性基準（式 (8)）の検証、段階的検証ティアを Tier 1 から Tier 3 まで成熟させることは開発中のアクティブな領域である。 証明義務は PSG でネイティブに運ばれ、Clef 言語および Fidelity フレームワークの一部である Composer 検証エンジンによって処理される。このディープテックインフラストラクチャは SpeakEZ Technologies のアクティブな任務である。ベイズ蒸留手続きは形式的基盤を持つが、ドメインデータ削減の実用的上限を確立するために多様なドメインで経験的検証を必要とする。 本論文で詳述した我々の仮説は、AI 信頼性は事後に購入する必要はないというものである。性質は決定可能である。検証は多項式である。保証は構造的である。情報理論的基盤、アーベル群上の HM 統一がソロモノフの普遍事前分布の計算可能な制限の下での MAP 仮説を計算するという事実は、これらの保証が普遍誘導自体と同じ形式的基盤に支えられていることを確立する。残っているのは、これらの形式的結果を生産成熟に持ち込むためのエンジニアリング努力と、数値的に精密で安全性クリティカルかつ科学的制約のあるドメインにおける影響を検証するための経験的作業である。 先行研究 この作業の形式的基础を提供する 3 つの伴侶論文は arXiv で入手可能： • Dimensional Type Systems and Deterministic Memory Management [Haynes, 2026b]: https://arxiv.org/abs/2603.16437 • The Program Hypergraph [Haynes, 2026c]: https://arxiv.org/abs/2603.17627 • Adaptive Domain Models [Haynes, 2026a]: https://arxiv.org/abs/2603.18104

References References Atilim Gunes Baydin, Barak A. Pearlmutter, Don Syme, Frank Wood, and Philip Torr. Gradients without backpropagation. arXiv preprint arXiv:2202.08587, 2022. Stephen Boyd and Lieven Vandenberghe. Convex Optimization. Cambridge University Press, 2004. Xingjian Cheng, Wenqi Zeng, Dai Dai, et al. Conditional memory via scalable lookup: A new axis of sparsity for large language models. arXiv preprint arXiv:2601.07372, 2026. Khalil DH. Transversal ARC solver: ARC-AGI solver via Pl¨ucker geometry. github.com/khalildh/transversal-arc-solver, 2026. Bruno Gavranovic, Paul Lessard, Andrew Dudzik, et al. Categorical deep learning is an algebraic theory of all architectures. arXiv preprint arXiv:2402.15332, 2024. John L. Gustafson and Isaac T. Yonemoto. Beating floating point at its own game: Posit arithmetic. Supercomputing Frontiers and Innovations, 4(2), 2017. Houston Haynes. Adaptive domain models: Bayesian evolution, warm rotation, and principled training for geometric and neuromorphic ai. arXiv preprint arXiv:2603.18104, 2026a. Houston Haynes. Dimensional type systems and deterministic memory management: Design- time semantic preservation in native compilation. arXiv preprint arXiv:2603.16437, 2026b. Houston Haynes. The program hypergraph: Multi-way relational structure for geometric algebra, spatial compute, and physics-aware compilation. arXiv preprint arXiv:2603.17627, 2026c. J. Roger Hindley. The principal type-scheme of an object in combinatory logic. Transactions of the American Mathematical Society, 146:29–60, 1969. Marcus Hutter. A theory of universal artificial intelligence based on algorithmic complexity. arXiv preprint arXiv:cs/0004001, 2000. Aditya Anirudh Jonnalagadda, Rishi Thotli, and John L. Gustafson. Closing the gap between float and posit hardware efficiency. arXiv preprint arXiv:2603.01615, 2025. Andrew Kennedy. Types for units-of-measure: Theory and practice. In Central European Functional Programming School, volume 6299 of LNCS. Springer, 2009. Andrey N. Kolmogorov. Three approaches to the quantitative definition of information. Problems of Information Transmission, 1(1):1–7, 1965. 17

Chris Lattner, Mehdi Amini, Uday Bondhugula, Albert Cohen, Andy Davis, Jacques Pienaar, River Riddle, Tatiana Shpeisman, Nicolas Vasilache, and Oleksandr Zinenko. MLIR: Scaling compiler infrastructure for domain specific computation. In Proceedings of the IEEE/ACM International Symposium on Code Generation and Optimization (CGO), 2021. Ming Li and Paul Vitanyi. An Introduction to Kolmogorov Complexity and Its Applications. Springer, 1997. Robin Milner. A theory of type polymorphism in programming. Journal of Computer and System Sciences, 17(3):348–375, 1978. Tung Nguyen, Kyogo Kawaguchi, Jui-Nan Yen, Bin Hu, Izzeddin Gur, Michael Ryoo, and Hyung Won Chung. Hierarchical reasoning model. arXiv preprint arXiv:2506.21734, 2025. Tomas Petricek, Dominic Orchard, and Alan Mycroft. Coeffects: A calculus of context- dependent computation. In Proceedings of the 19th ACM SIGPLAN International Con- ference on Functional Programming (ICFP), 2014. Maziar Raissi, Paris Perdikaris, and George Em Karniadakis. Physics-informed neural networks: A deep learning framework for solving forward and inverse problems involving nonlinear partial differential equations. Journal of Computational Physics, 378:686–707, 2019. Jorma Rissanen. Modeling by shortest data description. Automatica, 14(5):465–471, 1978. Aurko Roy, Riad Tutunov, Xiao Ji, et al. The y-combinator for llms: Solving long-context rot with lambda-calculus. arXiv preprint arXiv:2603.20105, 2026. Ray J. Solomonoff. A formal theory of inductive inference. Information and Control, 7(1): 1–22, 1964. 18

グラフビュー

バックリンク