Decidable By Construction: Design-Time Verification for Trustworthy AI — In-Depth Paper Explainer

*Translation and structured summary of a zhichai.net forum deep-dive into Houston Haynes' paper "Decidable By Construction: Design-Time Verification for Trustworthy AI" (arXiv:2603.25414).*

> "If a building can prove its structural safety before ground is broken, why wait until it leans to reinforce it?"

The Core Argument

Contemporary AI reliability infrastructure shares a structural assumption: the model exists first, and correction mechanisms are applied afterward. Current remedies include:

• PINNs — adding physics residual terms to the loss function
• Moreau projection — projecting model outputs onto feasible sets with GPU-accelerated optimization
• Conditional memory modules (Engram) — O(1) lookup modules inserted into Transformer layers
• Regularization techniques — dropout, weight decay, adversarial training

All work, but like patching a leaking ship after launch, each fix incurs per-inference compute, energy, and latency costs that scale with deployments × depth × request volume.

Haynes proposes the opposite: prove key properties—dimensional consistency, numerical stability, geometric structure preservation—before the first training iteration, via rigorous mathematical proof rather than heuristics or statistical testing.

Key points

• Abelian group Z^n: Physical dimensions ([M], [L], [T], etc.) form an abelian group under multiplication. If model properties can be expressed as linear constraints over Z^n, verification becomes solving linear systems—decidable, polynomial-time, principal-type.
• Decidability Theorem (Thm 2.1): Structural properties (dimensional consistency, Clifford grade preservation, escape classification, numerical representation sufficiency), when expressed over Z^n, are (1) decidable in finite time, (2) polynomial at O(n^3) via Gaussian elimination, (3) principal-typed with a unique most-general solution.
• Differentiation closure: Gradients inherit dimensional types (d₂·d₁⁻¹ exponent subtraction in Z^n), so training itself stays inside the decidable fragment with O(1) auxiliary memory per layer (forward-mode AD, no activation tape).

Three Framework Pillars

1. DTS (Dimensional Type System) — checks physical meaning, not just syntax. F − m·a passes; F − m·v (force minus momentum) is rejected at design time. PyTorch/TensorFlow/JAX cannot detect such errors; models train happily and emit physically impossible outputs on out-of-distribution inputs.

2. PHG (Program Hypergraph) — uses Clifford algebra with grade inference. In Cl(3,0,1), the full 16×16 Cayley table has 256 entries, but bivector×bivector products touch only grades 0, 2, 4 (48 nonzero entries) — a 5.3× computation reduction, derivable from type signatures with zero runtime cost.

3. ADM (Adaptive Domain Model) — depth-independent training memory (forward-mode AD), grade-preserving weight updates via b-posit exact accumulation, atomic hot-swap deployment where new configs must pass PHG verification, and Bayesian distillation of domain-constrained posteriors.

Connection to Solomonoff Induction

The most striking theoretical result: restricting the hypothesis space to finitely generated abelian groups converts Solomonoff's semi-computable universal prior into a computable one.

• Proposition 5.1: Under a prior π(h) ∝ 2^(−|h|) (|h| counting free dimensional variables), the Hindley-Milner principal unifier is the MAP estimate: h* = argmin |h|, computable by Gaussian elimination in O(n³).
• Via Li & Vitanyi's MDL/Kolmogorov equivalence, DTS inference is an MDL process on a computable class; grade inference extends "model complexity" to the count of nonzero Cayley table entries.

A layered verification hierarchy emerges: ℤⁿ ⊂ QF_LIA ⊂ FOL ⊂ TM, with complexities O(n³) / NP-complete / semi-decidable / undecidable. Most AI-correctness properties live in Level 1 (ℤⁿ).

Cost Structure vs. Contemporary Methods

| Method | Per-deployment | Per-layer | Per-request | Total growth | |--------|---------------|-----------|-------------|--------------| | Moreau projection | O(1) | O(1) | O(1) | O(d·l·r) | | PINNs | O(domain) | O(1) | O(1) | O(d·l·r·domain) | | Engram | O(config) | O(1) | O(1) | O(d·l·r·config) | | Plücker solver | O(1) | O(1) | O(1) | O(d·l·r) | | DTS/PHG/ADM | O(1) | O(0) | O(0) | O(d) |

Post-hoc methods pay per deployment, layer, and request; design-time verification has negligible marginal cost once the framework exists—presented as a consequence of the decidability theorem, not an implementation detail.

Practical Applications

• Medical decision support: models adding blood pressure (mmHg) to heart rate (bpm) are rejected before training.
• Autonomous driving: sensor fusion must pass dimensional consistency checks (no adding pixels to velocities).
• Climate modeling: conservation laws embedded as dimensional constraints in the type system.
• Financial risk: return × volatility is dimensionally rejected in favor of return / volatility; today such latent errors are hidden by over-parameterization, inflating training cost and failing on out-of-distribution inputs.

Open Problems and Outlook

The paper acknowledges remaining work: extending hardware coverage (FPGA/NPU, IEEE 754 / b-posit with quire), validating the coherence criterion (Eq. 8) at production scale, maturing the hierarchy through Level 3, and empirically bounding Bayesian distillation data reduction.

Philosophically, the deepest implication: Hindley-Milner unification over abelian groups computes the MAP hypothesis of a computably-restricted Solomonoff universal prior — a 'sweet spot' where universal induction becomes tractable. For AI governance, this suggests a paradigm shift from test-based trust to provable correctness, moving AI engineering from empirical craft toward a true engineering discipline — the way civil engineering evolved from "build and test" to "verify, then build."

References

1. Haynes, H. (2026). *Decidable By Construction: Design-Time Verification for Trustworthy AI*. arXiv:2603.25414. 2. Haynes, H. (2026a). *Adaptive Domain Models: Bayesian Evolution, Warm Rotation, and Principled Training for Geometric and Neuromorphic AI*. arXiv:2603.18104. 3. Haynes, H. (2026b). *Dimensional Type Systems and Deterministic Memory Management*. arXiv:2603.16437. 4. Haynes, H. (2026c). *The Program Hypergraph*. arXiv:2603.17627. 5. Baydin, A. G., Pearlmutter, B. A., & Syme, D. (2022). *Gradients without Backpropagation*. arXiv:2202.08587. 6. Boyd, S., & Vandenberghe, L. (2004). *Convex Optimization*. Cambridge University Press. 7. Cheng, X., et al. (2026). *Conditional Memory via Scalable Lookup*. arXiv:2601.07372. 8. Gustafson, J. L., & Yonemoto, I. T. (2017). *Beating Floating Point at Its Own Game: Posit Arithmetic*. Supercomputing Frontiers and Innovations, 4(2). 9. Kennedy, A. (2009). *Types for Units-of-Measure*. LNCS 6299. 10. Li, M., & Vitanyi, P. (1997). *An Introduction to Kolmogorov Complexity and Its Applications*. Springer. 11. Milner, R. (1978). *A Theory of Type Polymorphism in Programming*. JCSS, 17(3), 348-375. 12. Raissi, M., Perdikaris, P., & Karniadakis, G. E. (2019). *Physics-Informed Neural Networks*. Journal of Computational Physics, 378, 686-707. 13. Solomonoff, R. J. (1964). *A Formal Theory of Inductive Inference*. Information and Control, 7(1), 1-22.

*This post is a popular-science interpretation; any inaccuracies are the forum author's, not the original paper's.*