Decidable By Construction: Design-Time Verification for Trustworthy AI

• URL: http://arxiv.org/abs/2603.25414v1
• Date: Thu, 26 Mar 2026 13:09:36 GMT
• Title: Decidable By Construction: Design-Time Verification for Trustworthy AI
• Abstract summary: A prevailing assumption in machine learning is that model correctness must be enforced after the fact.<n>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.
• Score: 0.0
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: 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.

Related papers

• TERRA: Task-Embedded Reasoning and Representation Architecture for Cross-Domain Applications [0.0]
  A single action-conditioned latent predictive architecture can be trained on the structured state of a driving scene, a robot workspace, or a financial order book.<n>What is not established, and what TERRA addresses, is the transfer question: when does a representation or predictor learned in one structured-state domain carry over to a structurally analogous but otherwise unrelated domain, and by how much.<n>We model each domain as a controlled Markov process on a graded latent grid, factor any instantiation into thin domain adapters and a shared domain-invariant core, and identify a cross-domain correspondence with an approximate Markov decision process homomorphism
  arXiv  Detail & Related papers  (2026-06-01T00:50:59Z)
• I-SAFE: Wasserstein Coherence Metrics for Structural Auditing of Scientific AI Models [5.562984399879219]
  We introduce the textscI-SAFE (Interventional Secure, Accurate, Fair and Explainable) framework for scientific AI models.<n>textscI-SAFE evaluates raw model outputs under structurally guided perturbations of the input.<n>We instantiate textscI-SAFE on drug--target interaction (DTI) prediction using the Davis kinase benchmark.
  arXiv  Detail & Related papers  (2026-05-20T20:44:30Z)
• Probing Structural Mathematical Reasoning in Language Models with Algebraic Trapdoors [0.0]
  We introduce a benchmark suite for evaluating structural mathematical reasoning in language models.<n>Each instance presents a finitely generated subgroup as a list of integer matrices.<n>We report empirical results across five representative reasoning traces from two state-of-the-art models.
  arXiv  Detail & Related papers  (2026-05-05T23:16:30Z)
• Adaptive Domain Models: Bayesian Evolution, Warm Rotation, and Principled Training for Geometric and Neuromorphic AI [0.0]
  This paper develops an alternative training architecture grounded in three prior results.<n>We introduce Bayesian distillation, a mechanism by which the latent prior structure of a general-purpose model is extracted through the ADM training regime.<n>For deployment, we introduce warm rotation, an operational pattern in which an updated model transitions into an active inference pathway without service interruption.
  arXiv  Detail & Related papers  (2026-03-18T12:36:19Z)
• Hypothesis Class Determines Explanation: Why Accurate Models Disagree on Feature Attribution [0.0]
  We find that models with identical predictive behavior can produce substantially different feature attributions.<n>We identify hypothesis class as the structural driver of this phenomenon, which we term the Explanation Lottery.<n>Our results demonstrate that model selection is not explanation-neutral: the hypothesis class chosen for deployment can determine which features are attributed responsibility for a decision.
  arXiv  Detail & Related papers  (2026-03-16T18:55:50Z)
• Making Foundation Models Probabilistic via Singular Value Ensembles [56.4174499669573]
  Foundation models have become a dominant paradigm in machine learning, achieving remarkable performance across diverse tasks through large-scale pretraining.<n>Standard approach to quantifying uncertainty, training an ensemble of independent models, incurs prohibitive computational costs that scale linearly with ensemble size.<n>We propose Singular Value Ensemble (SVE), a parameter-efficient implicit ensemble method that builds on a simple, but powerful core assumption.<n>We show that SVE uncertainty quantification achieves comparable to explicit deep ensembles while increasing the parameter count of the base model by less than 1%.
  arXiv  Detail & Related papers  (2026-01-29T18:07:18Z)
• Unifying Tree Search Algorithm and Reward Design for LLM Reasoning: A Survey [92.71325249013535]
  Deliberative tree search is a cornerstone of Large Language Model (LLM) research.<n>This paper introduces a unified framework that deconstructs search algorithms into three core components.
  arXiv  Detail & Related papers  (2025-10-11T03:29:18Z)
• Approximate learning of parsimonious Bayesian context trees [0.0]
  The proposed framework is tested on synthetic and real-world data examples. It outperforms existing sequence models when fitted to real protein sequences and honeypot computer terminal sessions.
  arXiv  Detail & Related papers  (2024-07-27T11:50:40Z)
• LoRA-Ensemble: Efficient Uncertainty Modelling for Self-Attention Networks [52.46420522934253]
  We introduce LoRA-Ensemble, a parameter-efficient ensembling method for self-attention networks.<n>The method not only outperforms state-of-the-art implicit techniques like BatchEnsemble, but even matches or exceeds the accuracy of an Explicit Ensemble.
  arXiv  Detail & Related papers  (2024-05-23T11:10:32Z)
• Prototype-based Aleatoric Uncertainty Quantification for Cross-modal Retrieval [139.21955930418815]
  Cross-modal Retrieval methods build similarity relations between vision and language modalities by jointly learning a common representation space. However, the predictions are often unreliable due to the Aleatoric uncertainty, which is induced by low-quality data, e.g., corrupt images, fast-paced videos, and non-detailed texts. We propose a novel Prototype-based Aleatoric Uncertainty Quantification (PAU) framework to provide trustworthy predictions by quantifying the uncertainty arisen from the inherent data ambiguity.
  arXiv  Detail & Related papers  (2023-09-29T09:41:19Z)
• Towards Characterizing Domain Counterfactuals For Invertible Latent Causal Models [15.817239008727789]
  In this work, we analyze a specific type of causal query called domain counterfactuals, which hypothesizes what a sample would have looked like if it had been generated in a different domain. We show that recovering the latent Structural Causal Model (SCM) is unnecessary for estimating domain counterfactuals. We also develop a theoretically grounded practical algorithm that simplifies the modeling process to generative model estimation.
  arXiv  Detail & Related papers  (2023-06-20T04:19:06Z)
• Disentanglement via Latent Quantization [60.37109712033694]
  In this work, we construct an inductive bias towards encoding to and decoding from an organized latent space. We demonstrate the broad applicability of this approach by adding it to both basic data-re (vanilla autoencoder) and latent-reconstructing (InfoGAN) generative models.
  arXiv  Detail & Related papers  (2023-05-28T06:30:29Z)
• Representation Disentaglement via Regularization by Causal Identification [3.9160947065896803]
  We propose the use of a causal collider structured model to describe the underlying data generative process assumptions in disentangled representation learning. For this, we propose regularization by identification (ReI), a modular regularization engine designed to align the behavior of large scale generative models with the disentanglement constraints imposed by causal identification.
  arXiv  Detail & Related papers  (2023-02-28T23:18:54Z)
• Structural Causal Models Are (Solvable by) Credal Networks [70.45873402967297]
  Causal inferences can be obtained by standard algorithms for the updating of credal nets. This contribution should be regarded as a systematic approach to represent structural causal models by credal networks. Experiments show that approximate algorithms for credal networks can immediately be used to do causal inference in real-size problems.
  arXiv  Detail & Related papers  (2020-08-02T11:19:36Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.