haynes26a_ja

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

---

Abstract

機械学習においては、モデルの正しさを事後的に保証するという前提が一般的です。本稿では、AI モデルが数値的に安定しているか、計算上正確であるか、物理的領域と整合しているかといった性質は、必ずしも事後に適用する必要はなく、設計段階で検証できることが分かります。その検証は訓練を開始する前に行われ、計算コストは僅少です。

このアプローチの設計により、現在の実務よりも有利なトレーニング・ランタイム特性が得られます。特に、高信頼性が要求される意思決定支援や科学的に制約された設定に適用したモデルで効果を発揮します。

本稿では、以下の望ましい性質は共通の代数構造を持つことを示します：

• それらは有限生成可換群 ${\mathbb{Z}}^n$ 上の制約として表現でき、推論は多項式時間で決定可能であり、主型（principal type）が一意に定まります。

この観点に基づくフレームワークは、以下の三つの先行研究を組み合わせています【Haynes, 2026b,c,a】：

1. 次元型システム – 物理単位など任意の注釈を保持し、モデルの展開過程で永続的なコードータとして扱える。
2. プログラムハイパーグラフ – 型シグネチャだけで Clifford 代数の次数（grade）を推定し、幾何積の疎性を導出する。
3. 適応型ドメインモデルアーキテクチャ – 前方モードの coeffect 分析と正確なポジティブ累積により、トレーニング中に次元情報と次数情報を保持し続ける。

この組み合わせは新たな情報理論的結果をもたらすと考えられます。具体的には、可換群上の Hindley–Milner 統合が Solomonoff の汎用事前確率の計算可能な制限下で最大事後確率仮説を算出し、フレームワークの型推論をユニバーサル帰納と同等の形式的基盤に位置付けます。

さらに、四つの代表的な AI 信頼性手法を比較し、各手法がもたらすオーバーヘッドが展開・層・推論リクエストごとに累積することを示しました。本フレームワークはそのような余分なコストを設計段階で除去します。

正しさは、単に brute‑force 計算や事後介入を行うのではなく、原理的に設計された型システムによって保証されます。

---

1. Current State of the Art

現代の AI 信頼性インフラストラクチャは、モデルがまず存在し、その後で修正機構を適用するという構造的仮定を共有しています。以下の各手法は実際の失敗モードに対処します。

• Moreau 投影【Boyd and Vandenberghe, 2004】
  GPU 加速された内部点法により、モデル出力を凸妥当集合へ射影します。

• Physics‑informed Neural Networks (PINNs)【Raissi et al., 2019】
  訓練ロスに物理残差項を追加し、物理的制約を組み込みます。

• DeepSeek の Engram【Cheng et al., 2026】
  経験的に選択した Transformer 層に $O(1)$ の検索モジュールを挿入します。

• Transversal ARC Solver【DH, 2026】
  Plücker 座標を用いて、学習なしでパターン認識タスクを解きます。

いずれの手法も、展開数や層数、推論リクエスト数に比例した繰り返しコストがかかります。共通する構造的要因は、従来パイプラインが「意味情報」を失うことで、修正介入が不要になることです。

Fidelity フレームワークの現在の研究方向では、AI モデルの正しさに関わる次元整合性、Clifford の次数保持、エスケープ分類、数値表現適切性といった性質はすべて型システムの一部として捉えることができ、決定可能（decidable）かつ多項式時間で計算でき、主型が一意に定まるという特性を持ちます。

フレームワークは、モデルが生成するハイパーグラフを展開しながら設計時にこれらの性質を検証します。検証のコストはごく僅かで、下流での効果は大きく見積もられます。トレーニングにおいては、従来のように動的ディスパッチやランタイム形状チェックに依存せず、設計段階で型が確認されたトレーニングループは一度だけ検証すればよく、迅速かつ正確です。

対照的に、事後的な計算や介入はすべての展開・層・推論ごとに繰り返し適用される可能性があります。

---

2. Decidability Thesis

定理 2.1（正しさに関する性質の決定可能性）
集合 $\mathcal{P}$ を AI モデルの正しさを規定する構造的性質とします。すなわち、次元整合性、Clifford の次数保持、エスケープ分類、数値表現適切性です。

これらは有限生成可換群 ${\mathbb{Z}}^n$ 上の制約として表すことができ、
[ \mathcal{P} \subseteq {,\text{constraints over } \mathbb{Z}^{n},} ]
と書くことができます。その結果、$\mathcal{P}$ に含まれるすべての性質は

• 決定可能（decidable）であり、
• 多項式時間で計算可能（polynomial‑time computable）であり、
• 主型が一意に定まる（principal type is unique）

という特性を有します。

この結果により、設計時にモデルの性質を検証するプロセスは、有限生成可換群に対する制約解法として明確に定義され、効率的に実行できることが保証されます。

Decidable

フレームワークは、すべての well‑formed（適切に構成された）モデル仕様に対して、有限時間内に確定的な「はい」または「いいえ」の答えを生成します。

Polynomial

解の計算コストは、整数上でガウス消去法を行うことで

[ O(n^{3}) ]

となります。

3. Principal

最も一般的な解（自由変数が最も少なく、満たす制約が多い）は存在し、かつ一意である。

---

Practical implications

In practical terms, this means the framework can determine, before any computation executes, whether a model’s dimensional units are consistent, whether its geometric algebra operations preserve the correct grades, whether its memory allocation is deterministic, and whether its numeric representations are adequate for the target hardware. There is no ambiguity in the answer, no heuristic involved, and the computation completes in time proportional to the cube of the number of constraint variables. Standard type systems check syntax; this one checks physics.

“by construction” precision

The qualifier “by construction” is precise. The framework’s specification language admits only constraints expressible within the ${\mathbb{Z}}^n$ fragment. A model specification that type‑checks is, by that fact, within the decidable fragment. Properties requiring stronger reasoning (quantifier alternation, fixpoint computation) cannot be expressed in Tier 1 type system and are deferred to the graduated verification tiers described in Section 5.3. Decidability is not a property the framework discovers; it is a property the framework enforces through the structure of its type language.

---

2.1 Closure Under Differentiation

The abelian group fragment is closed under the chain rule. If $f:{\mathbb{R}}^{<d_1>}\to {\mathbb{R}}^{<d_2>}$, then

[ \frac{\partial f}{\partial x}: \mathbb{R}^{\langle d_{2}, d_{1}\rangle} ]

(1)

This is subtraction in the exponent algebra $(d_2-d_1)$ in ${\mathbb{Z}}^n$. Each gradient node inherits a dimension verified by the same Gaussian elimination that verifies the forward pass. The closure extends to Clifford grade: the gradient of a grade‑$k$ computation carries a grade determined by the dimensional arithmetic of the chain rule.

Corollary 2.1 (Training decidability).
Forward‑mode automatic differentiation [Baydin et al., 2022] computes directional derivatives with $O(1)$ auxiliary memory per layer. All intermediates are stack scoped; no values escape their creating scope. The derivative of a computation in the abelian group fragment remains in the fragment. Training is as decidable as inference.

---

2.2 The Combined Constraint Space

DTS with grade inference operates over a product of abelian groups:

[ \mathbf{Z}^{7}\times\mathbf{Z}= \mathbf{Z}^{8} ]

(2)

The unification algorithm solves systems of linear equations over ${\mathbb{Z}}^8$. The procedure is Gaussian elimination, extended by one axis; it is decidable, polynomial, and principal. The prior over the combined space favors assignments with fewest free dimension variables, maximum grade sparsity, and most constraints satisfied. In concrete terms, the framework reasons about physical units and geometric algebra grades simultaneously, in a single pass, using the same well‑understood linear algebra that underpins every modern numerical library. Adding grade inference to dimensional inference costs one additional integer per constraint variable.

---

3 Composition

The framework presented here composes three prior papers, each of which establishes its results independently. The first [Haynes, 2026b] introduces dimensional type systems and deterministic memory management. The second [Haynes, 2026c] introduces the program hypergraph with grade inference over Clifford algebras. The third [Haynes, 2026a] introduces an adaptive domain model architecture for verified training and deployment. The interested reader will find the full formal development in those papers; what follows is the composition argument that none of them can make alone.

The composition is not a concatenation. Each paper’s results become preconditions for results that no individual paper can state. DTS provides dimensional constraints; PHG provides grade constraints; ADM provides the training substrate that preserves both through weight updates. The dependency is cyclic: grade inference strengthens dimensional inference (by constraining the Cayley table), and dimensional inference strengthens grade inference (by determining which algebra signature applies to a given computation). The Program Semantic Graph (PSG) is the structure in which this mutual reinforcement is resolved to a fixed point during elaboration.

The formal structure presented in the following sections is established with sufficient precision to guide and constrain implementation. The implementation itself, across the full range of hardware targets and deployment topologies described, is in active development. Where the text uses present‑tense language to describe system behavior, it should be read as describing design intent whose formal properties are verified by the arguments given here.

---

3.1 DTS/DMM: Dimensional Persistence and Memory Determinism

The Dimensional Type System [Haynes, 2026b] extends Hindley–Milner with constraints drawn from ${\mathbb{Z}}^n$, yielding inference that is decidable, complete, and principal. Dimensional annotations persist through multi‑stage refinement [Lattner et al., 2021] as PSG codata, available at every stage. The coupling to Deterministic Memory Management is a formal dependency chain:

[ \text{Dimension} \xrightarrow{\text{range}} \text{Representation} \xrightarrow{\text{width}} \text{Footprint} \xrightarrow{\text{escape}} \text{Allocation} ]

(3)

Each step consumes the output of the preceding inference. Dimensional range determines representation selection (posit, IEEE 754, fixed‑point per target). Representation width determines memory footprint. Footprint, combined with escape classification into the four‑way lattice (stack scoped, closure captured, return escaping, by‑reference escaping), determines allocation strategy. The chain is verified during elaboration and surfaced as design‑time feedback.

Kennedy’s Units of Measure [Kennedy, 2009] verifies dimensions during type checking and then discards them before code generation. Downstream stages never see them. DTS takes a different approach: dimensional annotations persist as PSG codata through every refinement stage, available at the point where representation selection occurs (posit vs. IEEE 754 vs. fixed‑point, determined by value range), at the point where memory placement occurs (determined by footprint and escape classification), and at the point where cross‑target transfer fidelity is verified (dimensional metadata accompanies serialized data through BAREWire). The annotations guide these decisions and are then consumed. The consequence is that representation, memory, and fidelity decisions are informed by the same dimensional structure that the type checker verified.

---

3.2 PHG: Grade Inference and Geometric Sparsity

The Program Hypergraph [Haynes, 2026c] generalizes binary PSG edges to k‑ary hyperedges. Grade in Clifford algebra Cl(p,q) is a DTS dimension axis. The inference machinery derives the non‑zero entries of the geometric product Cayley table from type signatures:

[ \mathrm{grade} - k \wedge \mathrm{grade} - j \rightarrow \mathrm{grade} - (k + j) ]

(4)

[ \mathrm{grade} - k \cdot \mathrm{grade} - j \rightarrow \bigoplus_{i=0}^{\min(k,j)} \mathrm{grade} - \left(\left|k-j\right| + 2i\right) ]

(5)

For Cl(3,0,1) (projective geometric algebra), bivector × bivector products are constrained to grades 0, 2, and 4. Grades 1 and 3 are structurally zero by the axioms of the algebra. These components are absent from the computation entirely.

The sparsity compounds across layers. In an $L$‑layer network over $\mathrm{Cl}(p,q)$, each layer’s output grade constrains the next layer’s input grade. A computation that appears to involve $2^{2(p+q)}$ Cayley table entries reduces to the non‑zero subset, which for practical algebras is 5–50 % of the full table. For $\mathrm{Cl}(3,0,1)$, the full Cayley table has 256 entries; grade inference reduces a bivector‑bivector product to 48 non‑zero entries, a factor of $5.3\times$. Across an $L$‑layer network, the reduction compounds: each layer’s output grade constrains the next input, and the framework propagates these constraints forward to determine the appropriate computations for each layer. The reduction is verified during elaboration. No runtime check is required; the structurally zero components were never instantiated.

---

3.3 ADM: Verified Training Architecture

The Adaptive Domain Model [Haynes, 2026a] composes the preceding results into a training substrate. To appreciate why this matters, consider the standard separation in contemporary AI systems: training happens in one environment, with one set of tools and assumptions, and the resulting model is then exported and deployed in a completely different environment. The two phases share almost nothing. The training pipeline does not know what hardware the model will run on. The deployment pipeline does not know what constraints the training process was supposed to satisfy. The gap between them is where most reliability failures occur.

The ADM architecture closes this gap. Training and inference operate over the same typed infrastructure, governed by the same dimensional and grade constraints, verified by the same elaboration process. The framework does not treat training as a black box that produces a

---

1 Current State of the Art

Bayesian distillation. Standard fine‑tuning adjusts a pre‑trained model’s parameters within a fixed architecture under a fixed loss. It explores only the local neighborhood of the pre‑trained point estimate. Bayesian distillation takes a different approach: it extracts a domain posterior from a general model’s latent prior via variational inference, constrained to the dimensionally consistent, grade‑preserving subspace. The result is not a locally adjusted copy of the original; it is a geometrically structured extraction that recovers the posterior distribution over the subspace satisfying the domain’s physical constraints. The resulting domain model is smaller, more precise, and provably consistent with the physical structure of its domain.

---

2 Decidability Thesis

The decidability thesis states that the combination of dimensional and grade constraints yields a unified constraint space where all inference problems are decidable. This is achieved by representing both dimensions and grades as integer vectors in ${\mathbb{Z}}^n$, allowing joint Gaussian elimination to solve for free variables across both axes simultaneously.

---

2.1 Closure Under Differentiation

The algebraic foundation is the closure of ${\mathbb{Z}}^n$ under the operations that model construction requires. Physical dimensions form an abelian group under multiplication (addition of exponent vectors in ${\mathbb{Z}}^n$). Clifford grades compose under the geometric product with output grades determined by input grades and the algebra’s signature. Escape classifications form a finite lattice with a decidable ordering. Each structure admits polynomial‑time inference via extensions of Hindley–Milner unification [Hindley, 1969; Milner, 1978; Kennedy, 2009].

---

2.2 The Combined Constraint Space

The combined constraint space is the product of an abelian group for dimensions and a grade lattice. Formally, it can be represented as ${\mathbb{Z}}^n\times \mathbb{Z}$, where each dimension axis corresponds to a physical unit and the grade axis captures the Clifford grade information.

---

3 Composition

The framework composes three prior papers: the dimensional type system [Haynes, 2026b], the program hypergraph with grade inference [Haynes, 2026c], and the adaptive domain model architecture [Haynes, 2026a]. Together they provide a unified theory of physical units and geometric algebra grades.

---

3.1 DTS/DMM: Dimensional Persistence and Memory Determinism

The dimensional type system extends Hindley–Milner with constraints from ${\mathbb{Z}}^n$, yielding decidable, complete, and principal inference for dimensions. The program hypergraph introduces k‑ary edges that encode grade information, enabling joint reasoning about dimensions and grades.

---

3.2 PHG: Grade Inference and Geometric Sparsity

The program hypergraph generalizes binary edges to k‑ary hyperedges, allowing grade inference to capture the full structure of Clifford algebra products. This yields a sparse representation of geometric operations, reducing computational overhead.

---

3.3 ADM: Verified Training Architecture

The adaptive domain model architecture integrates dimensional and grade constraints into the training pipeline, ensuring that learned parameters respect both physical units and geometric algebra properties.

---

4 Consequences of the Composition

The three prior papers together yield several formal results that hold only when their contributions are combined. In particular,

4.1 Verified Training

A physics‑informed loss term computing $F-ma$ is verified during elaboration:

[ \langle \mathrm{N} \rangle - \langle \mathrm{kg} \rangle \cdot \langle \mathrm{m},\mathrm{s}^{-2} \rangle = \langle \mathrm{N} \rangle - \langle \mathrm{N} \rangle \quad \checkmark ]

(6)

The substitution $F-mv$ is rejected:

[ \langle \mathrm{N} \rangle - \langle \mathrm{kg} \rangle \cdot \langle \mathrm{m},\mathrm{s}^{-1} \rangle = \langle \mathrm{N} \rangle - \langle \mathrm{kg},\mathrm{m},\mathrm{s}^{-1} \rangle \quad \text{type error} ]

(7)

Gradient accumulation across parameters with different dimensions is similarly constrained. A gradient with dimension $⟨N/m⟩$ cannot be accumulated with $⟨J/s⟩$. This is a design‑time error, caught during model specification. No existing ML framework detects this because dimensional information is discarded before training begins.

The same principle applies outside physics. Consider a financial model that computes risk‑adjusted return as “return × volatility” when the correct formulation requires “return / volatility” (a Sharpe‑like ratio). The two expressions have different dimensional signatures: the first carries dimensions [currency · currency · time${}^{-1}$], the second [dimensionless]. DTS rejects the first during elaboration. No standard ML framework detects this error at any stage; the model trains, converges, and produces outputs that are numerically plausible but dimensionally incoherent.

3. Principal

最も一般的な解（自由変数が最も少なく、満たす制約が多い）は存在し、かつ一意である。

現在の実践における対処法

現在の慣例では、この種の潜在的なエラーに対しては 過剰パラメータ化 が標準的な手段です。モデルの容量を増やして損失曲面を十分に滑らかにし、最適化アルゴリズムが内部の一貫性の欠如にも関わらず収束できるようにします。

• 効果：訓練ロスは減少し続けますが、実際にはパラメータ量を増やすことでエラーを埋め込み、訓練分布上では統計的に無視できるほど小さくなります。
• 残存する問題点：不一致は依然として存在し、モデルが訓練データ以外の入力に直面したときに、次元ミスマッチが原因で出力が物理的に不可能になることがあります。

計算上の利点

過剰パラメータ化されたモデルは、構造的なエラーを事前に型システムで除去できなかった分だけ、追加の計算コスト（訓練時間・メモリ・エネルギー）を要します。次元が検証されたモデルでは、探索空間がコンパクトになり、

• 探索体積が小さくなる
• 各ステップでの演算回数も削減される

ことが期待できます。

結論：ターゲットドメインの知識を検証済みで活用すれば、同等またはそれ以上の成果を、はるかに短い壁時計時間と計算量で達成できると考えられます。

4.2 Grade‑Preserving Geometric Networks

Cayley 表のスパース性が層ごとに蓄積されます。Cl(3,0,1) の場合、フルテーブルは 256 個（16 × 16）の要素を持ちます。

• 双ベクトル × 双ベクトル の積は grades 0, 2, 4 のみを使用します。
• ベクトル × ベクトル の積は grades 0 と 2 のみを使用します。

これらの制約は展開時に解決され、非ゼロ成分だけが計算に参加します。

IEEE 754 の丸め誤差により、構造的にゼロである要素が数値的には非ゼロになることがありますが、b‑posit quire による正確な累積で、内部積算が支配的な勾配計算において構造的ゼロは常に保持されます。

4.3 Typed Inference Control

最新のドメイン指向推論技術は急速に進化しており、検索拡張生成から構造化ツール使用、学習型ルーティングまで多様な手法が登場しています。最も一般的な出発点は コンテキストウィンドウ増幅 で、取得したテキストをプロンプトに付加して追加入力として扱います。

• 取得された情報は型付けされていないため、次元や grade の構造が明示的に示されていません。

本フレームワークは再帰的アーキテクチャの進化を通じてこの課題に対処します。

• Hierarchical Reasoning Model (HRM) [Nguyen et al., 2025] は、複数時間スケールで相互作用する再帰モジュールが深い計算を実現し、最小データでもほぼ完璧な性能を示します。
• Resonant Recurrent Model (RRM) は動的結合により時間レベル間の情報交換を拡張し、外部状態への依存は残りますが、porous RRM では指定されたコンサルテーションステップで再帰ループを開き、モデルが型付けられたクエリを発行し、ドメイン固有の Adaptive Domain Model から構造化された応答を受け取ります。

「porous」 という用語は、モジュール境界が選択的に透過的であることを示しています。各コンサルテーションポイントで、クエリ投影により次元型付けされた要求を生成し、ドメインモデルは BARE プロトコル（BAREWire 実装）を通じて構造化事実を返します。

• value：b‑posit かつ正確な累積
• dimension：${\mathbb{Z}}^n$ の指数ベクトル、ガウス消去で検証
• confidence：事後区間、範囲解析で検証
• certificate：PHG 超辺ハッシュ、Z3 で検証

受信した応答は型付けされたインジェクションにより再帰に組み込まれ、次元と grade の構造が保持されます。型チェックに失敗した応答は統合前に除外されます。

このコンサルテーションは テキストインターフェース ではなく 型付きプロトコル です。モデルは「X について何を知っていますか？」と尋ねるのではなく、次元型付けされたクエリを投げ、次元型付けされた応答を受け取ります。その整合性が統合前に検証されます。

コンサルテーションは 一貫性基準 を満たす必要があります。具体的には、外部知識の統合によって生じる状態変化が、モデルの現在の期待とドメイン事後分布との差異よりも小さくなることが保証されます。形式的には

[ D_{\mathrm{KL}} \bigl(p_{\mathrm{RRM}}(\mathbf{h}{t_c+1}) ,|, p{\mathrm{RRM}}(\mathbf{h}{t_c}) \bigr) < D{\mathrm{KL}} \bigl(p_{\mathrm{RRM}}(\mathbf{h}{t_c}) ,|, p{D}(\mathbf{r}_{t_c}) \bigr) ]

(式 8)

が成り立ちます。これにより過剰なコンサルテーションを防ぎ、各コンサルテーションごとに状態変化の上限が測定・適用されます。

独立した検証結果として、Roy らの λ‑RLM フレームワーク [Roy et al., 2026] は、型付けされた構造制御により指数的な精度低下を多項式的低下へと変換し、最大 +21.9 の精度向上と 4.1 倍のレイテンシ削減を実現しました。これにより、推論時の型付けが信頼性特性を質的に改善することが確認されています。

4.4 Continuous Learning

推論と継続学習における coeffet（補助メモリ）サインは次の二点で異なります：

Property	Inference	Continuous Learning
Auxiliary memory	$O(1)$ per layer	$O(1)$ per layer
Escape classification	All stack‑scoped	All stack‑scoped
Accumulation	Not required	Quire (exact)
Weight update	None	Local, scoped

両方ともスタック可能であり、推論／学習フェーズの境界は coeffet 設定です。AMD XDNA 2 の空間ハードウェア上では、タイル割り当て比がこの設定を反映し、coeffet システムがリソース検証を行います。

5 Tractable Prior: The Solomonoff Connection

決定可能性の議論はアルゴリズム情報理論と結びつき、以下の結果が文献に明示的に記載されていないことに気付きました。

5.1 From Universal Prior to Computable Fragment

Solomonoff [Solomonoff, 1964] は二進文字列 $x$ のユニバーサル事前確率を

[ P(x) = \sum_{{p : U(p)=x^{*}}} 2^{-|p|} ]

(式 9)

と定義しました。ここで $U$ は汎用チューリング機械、$x^{\ast }$ は出力が $x$ で始まるプログラムの集合、$|p|$ はプログラム長（ビット）です。この事前確率は 半計算可能：上から列挙可能ですが、有限的に計算できるわけではありません [Kolmogorov, 1965; Hutter, 2000]。

仮説空間はすべてのプログラムです。無限かつ非計算可能な集合に対して $P(x)$ を求めると、上から列挙可能ですが有限的に計算できません。実用性を問うと、次の二つの質問が重要です：

1. どの制約付き仮説空間が事前確率を 計算可能 にするか？
2. その制約はどれだけ表現力があるか？

5.2 Abelian Groups as Tractability Mechanism

仮説空間を $\mathbb{Z}$ 上の有限生成アーベル群に限定すると、半計算可能な事前確率が 計算可能 になります。この制約は次の二つの性質を保ちます：

• 十分な表現力（モデル正しさに関わる仮説をすべて含む）
• 推論が多項式時間で行える

HM（ヒルベルトマッピング）統合を ${\mathbb{Z}}^n$ 上で実施すると、主型 が得られます。これは自由変数が最も少なく、満たす制約が多い割り当てです。

命題 5.1（主型は MAP 推定）
$\mathcal{H}$ をプログラムの型制約から導かれる次元割り当て全体とし、線形方程式系として ${\mathbb{Z}}^n$ に表現します。事前確率 $\pi (h)\propto 2^{-|h|}$（$|h|$ は自由次元変数の個数）としたとき、HM が計算する主型 $h^{\ast }$ は
[ h^{*} = \arg\max_{h\in\mathcal{H}} \pi(h) = \arg\min_{h\in\mathcal{H}} |h| ]
（式 10）
であり、これはガウス消去により $O(n^3)$ 時間で求められます。

Solomonoff の事前確率と MDL（最小記述長）との関係は Li & Vitanyi [Li & Vitanyi, 1997] によって示されています。計算可能な仮説クラスに対して、MDL 推定はユニバーサル事前確率を制限したものの MAP 推定と一致します。${\mathbb{Z}}^n$ フラグメントは計算可能であり、DTS 推論はその MDL 手続きです。

• $|M|$：自由次元変数の個数（モデル複雑度）
• $|D|M$：満たす制約の数（データ適合度）

主型は $|M|$ を最小化しつつ、すべての制約を満たします。grade 推論はこの二軸に加えて、Cayley 表の非ゼロエントリ数 がモデル複雑度として扱われます。

5.3 The Graduated Verification Model

決定可能性結果は次の検証段階へ自然に拡張できます：

Fragment	Expressiveness	Inference	Prior	Cost
${\mathbb{Z}}^n$ (Tier 1)	次元、grade、escape	多項式時間	計算可能・正確	ほぼゼロ（展開の副産物；グラフ整合性は Z3 で検証）
QF_LIA (Tier 2)	範囲、不変条件	NP‑complete	計算可能	中程度（Tier 1 に加えて追加の Z3 クエリ）
FOL (Tier 3)	任意の一階性質	半決定的	半計算可能	高い（PSG の証明義務）

包含関係は

[ \mathbb{Z}^{n} \subset \mathrm{QF}_{\mathrm{LIA}} \subset \mathrm{FOL} \subset \mathrm{T M} ]

(式 11) で示されます。

5.4 The Qure as Fragment Preservation

Qure は前方モード勾配計算において内部積算を正確に行う機構です。事前確率の観点では、正確な累積により勾配計算が アーベル群フラグメント の外へ逸脱しないことが保証されます。IEEE 754 の丸め誤差で構造的にゼロである要素が数値的に非ゼロになることはありますが、Qure はそのような変化を許容しつつも、最終的な結果は依然として決定可能な次元・grade 情報を保持します。

このように、検証フレームワークは 計算可能 かつ 効率的 な仮説空間（アーベル群）に限定することで、ユニバーサルインダクションの本質を保ちつつ、実装上のコストを抑えることができます。

6 Comparative Analysis

以下では、各手法が実際に直面する失敗モードと、その構造的制限・コスト構造を整理します。

6.1 Convex Projection (Moreau)

• 手法：モデル出力を凸集合 $\mathcal{C}$ に射影し、内部点として返す。
• 利点：異なるドメイン間でも柔軟に制約を適用でき、実装が簡単。
• 構造的制限：射影は次元情報の検証を行わないため、集合 $\mathcal{C}$ が正しい物理単位や grade を持っているかは別途確認が必要。

項目	内容
コスト	推論時に内部点計算（線形時間）を実行。非償却的で、リクエストごとに計算が発生。
代替案	DTS では型推論段階で次元情報を検証し、推論時は追加コストなしで正しい単位・grade を保証できる。

6.2 Loss Shaping (PINNs)

• 手法：物理法則を残差項として損失関数に組み込む（例：$F-mv$）。
• 構造的制限：各残差項の次元が正しく合わせられているかは、手動での型付けが必要。誤った単位や grade の残差は、訓練データでは検証できないことがある。

項目	内容
コスト	ドメインごとにカスタム残差項を実装し、物理法則に基づく型付けを行う必要がある（線形コスト）。
代替案	DTS ではすべての算術演算が型推論時に次元・grade を検証するため、追加コストはほぼゼロ。

---

以上が、提示された英語テキストを日本語に翻訳した結果です。Markdown の見出し構造と数式はそのまま残しています。

3. Principal

最も一般的な解（自由変数が最も少なく、満たす制約が多い）は存在し、かつ一意である。

6.3 Conditional Memory (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）を通じた型付き問い合わせを行い、Equation 8 が示す整合性基準で問い合わせ頻度を制御します。応答は次元情報を含み、PHG 証明書も付与されます。

6.4 Geometric Solver (Plücker / ARC)

Transversal ARC ソルバー [DH, 2026] は、Clifford 空間 (\mathrm{Cl}(3,0,1)) の grade‑2 バイベクトル（Plücker 座標）を用いて、ARC‑AGI タスク 316 問題を ゼロ学習で解きます。

PHG の主張は次の二点です。

1. Clifford 代数は抽象パターン認識に十分な幾何構造を提供する。
2. grade を意識しない処理は計算コストが増大することを示す。

grade 構造はすべての演算で暗黙的に存在しますが、実装上では可視化されていません。Plücker 線は二重配列として表現されます。ソルバーは 34 % のタスクで構造的にゼロとなる Cayley 表エントリの計算にタイムアウトし、残りの 3 % では固定された埋め込みが対応できない変換タイプにより失敗します。

• 失敗モードは次の二つに対処可能です。
  • grade 推論：構造的にゼロになる計算を事前に除外し、不要な演算を削減。
  • 型埋め込み導出：PHG の指針に従い、埋め込み集合を拡張して対応範囲を広げる。

6.5 Cost Structure Summary

Approach	Phase	Marginal Cost	Scales With
Moreau	Runtime	Constant per request	Request volume
PINNs	Training	Linear per domain	Domain count
Engram	Design	Linear per configuration	Architecture variants
Fidelity	Elaboration	Negligible	Amortized

• ポストホックアプローチは線形または定数の追加コストです。新しいデプロイ、層、推論リクエストごとに最初と同様の価格がかかります。
• 設計時アプローチはフレームワークが整っていれば追加コストはほぼ無視でき、実装上の詳細ではなく決定可能性定理の結果として現れます。

具体的には、ポストホックのコストは (O(d \cdot l \cdot r)) と表せます（(d) = デプロイ数、(l) = 層数、(r) = 推論リクエスト数）。設計時のコストはデプロイごとに (O(1)) のみです。

7. Related Work

• Kennedy の Units of Measure [Kennedy, 2009] では、次元制約が HM 推論に統合できることを示しました。DTS はこの概念を拡張し、すべてのリファイン段階で次元情報を保持します（Kennedy のシステムはコード生成前に次元情報を破棄します）。また、次元推論と表現選択・メモリ管理を結びつけました。

• Petricek, Orchard, and Mycroft [Petricek et al., 2014] はコンテキスト依存計算のコエフェクト（coeffects）を形式化しました。DMM はこの理論をメモリ配置に適用し、「コンテキスト」 を割り当て戦略とライフタイム制約として表現します。

• CDL 論文 [Gavranovic et al., 2024] はニューラルアーキテクチャのカテゴリ的意味論を提供します。Fidelity フレームワークはその中の特定のフラグメント（前方/後方モードを支配する adjoint 対応）を設計時に検証可能な形で実装しています。

• Baydin, Pearlmutter, and Syme [Baydin et al., 2022] は前方モード勾配計算を示しました。ADM 論文 [Haynes, 2026a] は係数解析を拡張し、前方モードトレーニングがメモリ決定的かつスタック可能であることを示しています。

• Gustafson [Gustafson and Yonemoto, 2017] は posit 数値表現を導入しました。Jonnalagadda et al. [Jonnalagadda et al., 2025] は b‑posit の bounded モードでハードウェア競争力を実証しました。DTS は posit を前提とした 「どの数値範囲が重要か」 を形式的に把握する機構を提供します。

8. Scope and Limitations

• 決定可能性定理は (\mathbb{Z}^{n}) のフラグメントに適用されます。

  • Tier 1: Z3 がグラフレベルの整合性証明を行い、PSG が構造的不変性をリファイン過程で保持することを確認します。
  • Tier 2: QF_LIA クエリにより追加の制約（範囲・不変条件）を処理します。
  • Tier 3: 証明義務は半決定的になるか、外部定理証明器に委ねられます。

• (\mathbb{Z}^{n}) の外側にある性質（例：終了性、活性化、任意のプログラム不変条件）は決定不可能です。

• Solomonoff 接続は限定的です。

  • 全てのプログラムを対象とした汎用事前分布に対し、(\mathbb{Z}^{n}) の事前分布は 次元 と grade の割り当てに焦点を当てます。制限により計算可能性が得られますが、普遍性は失われます。
  • 具体的な応用では、次元整合性、grade 持続性、表現選択、構造的スパース性が重要です。

• フレームワークはすべてのモデル属性を決定可能にするわけではありません。AI モデルの正確性を支える クラス の属性（次元整合性、Clifford grade 持続性、数値表現適切性、エスケープ分類、メモリ決定性）を特定し、これらは (\mathbb{Z}^{n}) 上の線形制約として表現でき、ポリノミアル時間で推論可能です。

• 境界は アーベル群構造 です。

  • 線形制約（(\mathbb{Z}^{n}) の要素）で表せる性質は Tier 2 に属し、
  • 量化や固定点推論が必要な性質は Tier 3 へと拡張されます。

9. Conclusion

本稿で取り上げた手法は AI の信頼性における実際的な失敗モードに対処し、各々が状態を向上させました。共通の構造的制限として、修正機構はモデルが生成された後に適用され、そのコストはデプロイ、層、推論リクエストごとに再び発生します。AI システムが科学、医療、自律走行、金融といった多様な領域に広がる中で、ポストホックのコストはモデル数・ドメイン数・ターゲット数の積だけ増大します。

本稿では、AI モデルの正確性を支える属性（次元整合性、Clifford grade 持続性、数値表現適切性、エスケープ分類、メモリ決定性）が (\mathbb{Z}^{n}) 上の制約 として表現でき、推論は多項式時間で可能であり、主型（principal type）は一意であることを示しました。

• DTS が次元情報を全リファイン段階に保持し、PHG が grade 推論で構造的にゼロな計算を事前に除去し、ADM が前方モード係数解析と正確な posit 累積で重み更新を保証します。

Solomonoff の観点からは、Hindley–Milner の型統一が アーベル群 上の HM 推論を行い、計算可能な事前分布の MAP 仮説を導出します。したがって、本フレームワークは汎用的な推論の一部として、構造的性質に対する 決定可能かつ唯一 の保証を提供します。

実務上のインパクトはコスト構造の変化です。

• ポストホック手法はデプロイ・層・リクエストごとに費用が発生し、(O(d \cdot l \cdot r)) に比例します。
• 設計時検証は一度だけ（実装段階で）費用がかかり、以後は (O(1)) の amortized コストです。

今後の課題として、以下の点が挙げられます。

1. ハードウェアの多様化に対応した実装を拡張し、FPGA・NPU だけでなく他のプラットフォームでも動作確認を行う。
2. Equation 8 の整合性基準を本番環境で検証し、スケールに耐えることを実証する。
3. Tier 1〜Tier 3 の検証階層を成熟させ、特に Tier 3 の半決定的証明や外部定理証明器との統合を強化する。

Proof obligations は PSG（Program Hypergraph）に組み込まれ、Composer 検証エンジンが自動的に処理します。これらは SpeakEZ Technologies が提供する Clef 言語と Fidelity フレームワークの一部です。

ベイズ的蒸留手順は形式的に裏付けられていますが、実際の多様なドメインでの検証により、データ削減効果や精度向上の具体的な境界を明らかにします。

結論として、AI の信頼性は事前に決定可能な属性に基づいて保証でき、設計時に一度だけ検証すれば、実運用では追加コストなしで次元・grade・数値表現・エスケープ・メモリの正確さが保たれます。情報理論的には、HM 統一がアーベル群上の事前分布から MAP 仮説を導くことにより、構造的性質は決定可能かつ唯一であることが示されました。

Prior Work

本研究の形式的基盤となる以下の三つの論文が 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

Atilim Gunes Baydin, Barak A. Pearlmutter, Don Syme, and Frank Wood. 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ücker 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 Thoti, 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.

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 Conference 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. Automata, 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.