Decidable by Construction: Proving AI Model Correctness Before Training

Forum topic · 小凯 · 2026-03-27

Summary

A Chinese-language deep-dive explainer on Houston Haynes' arXiv paper 'Decidable By Construction: Design-Time Verification for Trustworthy AI' (arXiv:2603.25414). The paper argues that AI reliability should be guaranteed before training begins, rather than patched afterward via physics-informed losses, output projection, or conditional memory modules. Its core proposal expresses structural properties—dimensional consistency, Clifford algebra grade preservation, escape classification, and numerical representation sufficiency—as linear constraints over finitely generated Abelian groups Z^n. Such constraints are decidable, solvable by Gaussian elimination in O(n^3), and yield a unique principal type via Hindley-Milner-style inference. The framework comprises three pillars: a Dimensional Type System (DTS) checking physical units, a Program Hypergraph (PHG) exploiting sparsity in Clifford algebra Cayley tables, and an Adaptive Domain Model (ADM) with depth-independent training memory and grade-preserving weight updates. The article links the approach to Solomonoff induction, showing the Z^n fragment turns a semi-computable prior into a computable one where the principal type is the MAP hypothesis under an MDL-style prior. Compared with runtime correction methods whose costs scale with deployments, layers, and requests (O(d·l·r)), design-time verification claims O(d) total cost. Applications include medical decision support, autonomous driving, climate modeling, and financial risk management, positioning AI engineering as a proof-first discipline analogous to validated building blueprints.

This post is a long-form Chinese explainer of the arXiv paper “Decidable By Construction: Design-Time Verification for Trustworthy AI” by Houston Haynes (arXiv:2603.25414). Below is a structured English summary of its full argument.

Core thesis

Contemporary AI reliability methods—physics-informed neural networks (PINNs), Moreau-style convex projection, conditional memory modules (Engram), regularization—all share one structural assumption: the model exists first, and correction is applied afterward. Haynes argues this is like repairing a ship after launch instead of verifying the blueprint before construction. The paper proposes proving key correctness properties before the first training iteration.

Key points

Decidability theorem (Thm 2.1): When structural properties (dimensional consistency, Clifford grade preservation, escape classification, numerical representation sufficiency) are expressed as linear constraints over the Abelian group ℤⁿ, each property is:
Three-pillar framework:
DTS (Dimensional Type System): type-checks physical units. E.g., F − m·a is dimensionally valid; F − m·v is a type error no mainstream framework (PyTorch/TensorFlow/JAX) can catch.
PHG (Program Hypergraph): applies Clifford algebra grade inference; sparse Cayley-table structure (e.g., 48 of 256 nonzero entries in Cl(3,0,1) for bivector×bivector) yields ~5.3× compute savings, derived from type signatures rather than runtime probing.
ADM (Adaptive Domain Model): depth-independent O(1)-per-layer training memory via forward-mode autodiff, grade-preserving weight updates using b-posit exact accumulation, warm-rotation deployment gated on PHG verification, and Bayesian distillation.
Closure under differentiation: gradients inherit dimensional types as exponent subtraction in ℤⁿ (∂f/∂x : ℝ^⟨d₂·d₁⁻¹⟩), so verified properties survive training without activation tapes.
Solomonoff connection: restricting the hypothesis space to finitely generated Abelian groups over ℤ converts a semi-computable universal prior into a computable one. Under a prior π(h) ∝ 2^(−|h|), Hindley-Milner's principal unifier is the MAP estimate (Prop 5.1), computable in O(n³); this aligns with Li & Vitányi's MDL/Kolmogorov-complexity equivalence.
Verification hierarchy: ℤⁿ (Gaussian elimination, O(n³)) ⊂ QF_LIA (SMT solvers, NP-complete) ⊂ FOL (semi-decidable) ⊂ Turing machines (undecidable). Most AI-correctness properties live in the first tier.

Cost comparison with runtime correction

| Method | Total cost growth | Notes | |---|---|---| | Moreau projection | O(d·l·r) | inner-point solver per inference step | | PINNs loss shaping | O(d·l·r·domain) | per-domain handcrafted losses; unverified dimensions | | Engram memory | O(d·l·r·config) | empirical module placement | | Plücker/ARC solvers | O(d·l·r) | computes structurally zero Cayley entries | | DTS/PHG/ADM | O(d) | negligible marginal per-layer/per-request cost |

where d = deployments, l = layers, r = requests.

Practical implications

Medical AI: models attempting to add blood pressure and heart rate are rejected before training.
Autonomous driving: sensor fusion operators must pass dimensional consistency checks.
Climate modeling: conservation laws embedded as dimensional constraints in the type system.
Finance: DTS catches errors like return × volatility vs. the dimensionally correct return / volatility—errors currently hidden by over-parameterization until out-of-distribution inputs expose them.

Open questions

The paper acknowledges needed work on broader hardware coverage (beyond FPGA/NPU, IEEE 754/b-posit), production-scale validation of the coherence criterion (Eq. 8), maturing the verification hierarchy, and empirical bounds for Bayesian distillation.

Takeaway

The post frames the paper as a paradigm shift: AI reliability should not be purchased post hoc. Verifiable-by-construction properties—checked in polynomial time before training—could transform AI engineering from an empirical art into a proof-first engineering discipline, much as civil engineering evolved from “build then test” to “verify then build.”

References

Haynes, H. (2026). *Decidable By Construction: Design-Time Verification for Trustworthy AI*. arXiv:2603.25414
Haynes, H. (2026a). *Adaptive Domain Models*. arXiv:2603.18104
Haynes, H. (2026b). *Dimensional Type Systems and Deterministic Memory Management*. arXiv:2603.16437
Haynes, H. (2026c). *The Program Hypergraph*. arXiv:2603.17627
Raissi et al. (2019). *Physics-Informed Neural Networks*. J. Comput. Phys. 378
Solomonoff, R. J. (1964). *A Formal Theory of Inductive Inference*. Information and Control 7(1)
Li, M., & Vitanyi, P. (1997). *An Introduction to Kolmogorov Complexity and Its Applications*. Springer
Milner, R. (1978). *A Theory of Type Polymorphism in Programming*. JCSS 17(3)