A prevailing assumption in machine learning is that model correctness must be enforced after the fact. We observe that the properties determining whether an AI model is numerically stable, computationally correct, or consistent with a physical domain do not necessarily demand post hoc enforcement. They can be verified at design time, before training begins, at marginal computational cost, with particular relevance to models deployed in high-leverage decision support and scientifically constrained settings. These properties share a specific algebraic structure: they are expressible as constraints over finitely generated abelian groups $\mathbb{Z}^n$, where inference is decidable in polynomial time and the principal type is unique. A framework built on this observation composes three prior results (arXiv:2603.16437, arXiv:2603.17627, arXiv:2603.18104): a dimensional type system carrying arbitrary annotations as persistent codata through model elaboration; a program hypergraph that infers Clifford algebra grade and derives geometric product sparsity from type signatures alone; and an adaptive domain model architecture preserving both invariants through training via forward-mode coeffect analysis and exact posit accumulation. We believe this composition yields a novel information-theoretic result: Hindley-Milner unification over abelian groups computes the maximum a posteriori hypothesis under a computable restriction of Solomonoff's universal prior, placing the framework's type inference on the same formal ground as universal induction. We compare four contemporary approaches to AI reliability and show that each imposes overhead that can compound across deployments, layers, and inference requests. This framework eliminates that overhead by construction.
翻译:机器学习领域普遍假设模型正确性必须在事后强制保证。我们观察到,决定人工智能模型是否数值稳定、计算正确或与物理领域一致的属性,未必需要事后强制执行。这些属性可以在设计时(即训练开始前)以极小的计算成本进行验证,对于部署在高风险决策支持和科学约束环境中的模型尤为重要。此类属性具有特定的代数结构:它们可表达为有限生成阿贝尔群 $\mathbb{Z}^n$ 上的约束条件,其中推理在多项式时间内可判定且主类型唯一。基于这一观察构建的框架整合了三项前期成果(arXiv:2603.16437、arXiv:2603.17627、arXiv:2603.18104):一种维度类型系统,可在模型精化过程中将任意注释作为持久共数据传递;一种程序超图,可从类型签名单独推断克利福德代数阶数并推导几何乘积稀疏性;以及一种自适应领域模型架构,通过前向模式共效应分析与精确正数累积,在训练过程中保持两个不变量。我们认为这一组合产生了新颖的信息论结果:阿贝尔群上的 Hindley-Milner 统一化可在所罗门诺夫通用先验的可计算限制下计算最大后验假设,从而使框架的类型推理与通用归纳具有相同的形式基础。我们比较了四种当代人工智能可靠性方法,表明每种方法都会产生在部署、层级与推理请求间复合增长的额外开销。而该框架通过构造消除了这一开销。