arXiv:2603.25414cs.PLcs.AI2026-03被引 2

在设计阶段就验证AI模型的可靠性,无需训练后补救。

Decidable By Construction: Design-Time Verification for Trustworthy AI

  • 用代数结构在设计时验证模型稳定性与物理一致性
  • 提前发现错误,计算开销极低,适合高可靠场景
  • 适用于科学约束和关键决策系统,无需事后验证

机器学习中普遍认为模型正确性需在训练后强制。我们观察到,决定模型数值稳定、计算正确或符合物理规律的性质,并不必然需要事后验证,而可在设计阶段完成,且计算成本极低,尤其适用于高影响力决策支持与科学约束场景。这些性质具有特定的代数结构:可表达为有限生成阿贝尔群 $\mathbb{Z}^n$ 上的约束,其推理可在多项式时间内判定,主类型唯一。该框架整合三项已有成果:携带任意注解的维度类型系统;通过类型签名推断克利福德代数阶并导出几何乘积稀疏性的程序超图;以及通过前向模式共效应分析和精确正数累加,保持不变量的自适应域模型架构。我们认为此组合带来新的信息论结果:阿贝尔群上的霍尔迪-米尔纳统一算法,在可计算的索洛蒙诺夫全先验限制下,计算最大后验假设,使该框架的类型推断与通用归纳处于同一形式基础。对比四种当代AI可靠性方法,均引入可累积的开销,而本框架通过构造消除该开销。

原文摘要 · Abstract (English)

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.

可信AI形式验证设计时检查代数结构

Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品;中文卡片由大模型生成,请以原文为准。