Decidable By Construction: Design-Time Verification for Trustworthy AI

Houston Haynes

arxiv: 2603.25414 · v4 · pith:RVMQBTV6new · submitted 2026-03-26 · 💻 cs.PL · cs.AI· cs.LG· cs.LO

Decidable By Construction: Design-Time Verification for Trustworthy AI

Houston Haynes This is my paper

Pith reviewed 2026-05-15 00:40 UTC · model grok-4.3

classification 💻 cs.PL cs.AIcs.LGcs.LO

keywords design-time verificationtrustworthy AItype inferenceabelian groupsHindley-Milner unificationSolomonoff priordecidable verificationAI reliability

0 comments

The pith

AI model properties for stability and correctness reduce to decidable constraints over abelian groups, allowing verification before training.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper argues that numerical stability, computational correctness, and physical consistency in AI models need not be enforced after training. Instead these properties fit an algebraic structure of constraints over finitely generated abelian groups Z^n, where Hindley-Milner unification decides them in polynomial time with a unique principal type. A framework assembles a dimensional type system that carries annotations through elaboration, a hypergraph that infers Clifford grades from signatures, and an adaptive architecture that preserves invariants via coeffect analysis and posit accumulation. The resulting type inference is claimed to compute the maximum a posteriori hypothesis under a computable restriction of Solomonoff's universal prior. This removes repeated post-training checks and their compounding costs in deployed systems.

Core claim

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. The composition of the dimensional type system, program hypergraph, and coeffect-preserving architecture therefore verifies the relevant model properties at design time.

What carries the argument

Hindley-Milner unification over constraints in finitely generated abelian groups Z^n, which carries persistent annotations through model elaboration and decides verification questions in polynomial time.

If this is right

Verification of stability, correctness, and domain consistency occurs before any training data is seen.
Post-training enforcement overhead is removed by construction across layers and inference requests.
Geometric product sparsity follows directly from type signatures without separate analysis.
The same inference procedure supplies both verification and a link to universal induction.
High-leverage decision-support models gain design-time guarantees at marginal cost.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

The same algebraic encoding could be applied to other verification tasks such as fairness constraints or robustness bounds if they admit group representations.
Integration with existing ML compilers might allow automatic insertion of the required type annotations during model construction.
The polynomial bound on unification suggests the approach remains practical even for large models whose dimension vectors stay modest.

Load-bearing premise

Properties that determine numerical stability, computational correctness, and physical consistency in AI models can be expressed as constraints over finitely generated abelian groups where inference is polynomial-time decidable and the principal type is unique.

What would settle it

An AI model property for stability or physical consistency that cannot be encoded as a constraint in Z^n, or for which the unification procedure either exceeds polynomial time or yields non-unique principal types.

Figures

Figures reproduced from arXiv: 2603.25414 by Houston Haynes.

**Figure 1.** Figure 1: RRM conceptual design (proposed; not implemented). Left: Transformer inference stack showing the intended placement of the RRM module. Right: typed consultation workflow for the porous RRM. The figure specifies design intent; no running system is depicted. Independent evidence supports this approach. Roy et al.’s λ-RLM framework [27] demonstrates that typed structural control of inference converts expone… view at source ↗

read the original 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.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Desk Editor's Note private letter to a colleague

The paper stitches three prior preprints into a design-time type system for AI properties and asserts this yields MAP inference under a restricted Solomonoff prior, but supplies no derivation for the link.

read the letter

The central claim is that properties like numerical stability and physical consistency in AI models can be expressed as constraints over finitely generated abelian groups, allowing Hindley-Milner unification to verify them before training at low cost. The authors reach this by combining a dimensional type system that carries annotations, a hypergraph for inferring Clifford grades, and a coeffect model that preserves invariants during training. They contrast this with four other reliability approaches that add overhead across layers and calls. That comparison is a clear practical point for high-stakes deployments. The algebraic framing itself is coherent on its own terms and draws on established type theory in a way that could reduce post-training checks if the encoding works. The soft spot is the information-theoretic step. The abstract states that the composition produces unification over Z^n that computes the MAP hypothesis under a computable restriction of Solomonoff's prior, yet it gives no definition of that restriction, no measure showing how unification selects the hypothesis, and no reduction connecting type constraints to program complexity. The assumption that all relevant properties fit uniquely into Z^n constraints is stated but not shown to bridge to universal induction without extra structure. This leaves the novelty resting on composition rather than an independent derivation. The work is aimed at people already working on formal methods for machine learning who know the three cited preprints. A reader looking for concrete proofs or empirical checks will find the abstract thin. If the full manuscript contains the missing mappings and any checks, it is worth sending out for review so referees can test whether the equivalence holds. Otherwise the paper stays at the level of a promising framing without demonstrated grounding.

Referee Report

2 major / 1 minor

Summary. The paper claims that properties ensuring numerical stability, computational correctness, and physical consistency in AI models can be expressed as constraints over finitely generated abelian groups Z^n (with polynomial-time decidable, unique-principal-type inference) and verified at design time. It composes three prior results—a dimensional type system with persistent codata annotations, a Clifford hypergraph deriving geometric sparsity from types, and a coeffect-based domain model preserving invariants—to assert a novel information-theoretic result: Hindley-Milner unification over these groups computes the MAP hypothesis under a computable restriction of Solomonoff's universal prior, thereby eliminating post-hoc enforcement overhead.

Significance. If the claimed equivalence between HM unification and restricted Solomonoff induction were rigorously derived, the framework would supply a formal, design-time foundation for trustworthy AI that aligns type inference with universal induction, potentially reducing compounded overhead in layered, high-stakes deployments. The algebraic restriction to Z^n constraints and the emphasis on decidability are strengths that could be impactful if substantiated.

major comments (2)

[Abstract] Abstract: the assertion that 'Hindley-Milner unification over abelian groups computes the maximum a posteriori hypothesis under a computable restriction of Solomonoff's universal prior' is presented as following directly from the composition, yet supplies neither the definition of the prior restriction, the probability measure under which unification selects the MAP hypothesis, nor a reduction showing how Z^n type constraints correspond to program complexity in the universal prior.
[Composition section] Composition of prior results (arXiv:2603.16437, arXiv:2603.17627, arXiv:2603.18104): the manuscript describes the three components at a high level but contains no explicit theorem, derivation, or mapping demonstrating that their integration produces HM unification over Z^n that exactly realizes the claimed information-theoretic equivalence.

minor comments (1)

[Abstract] The comparison of four contemporary approaches to AI reliability is mentioned but lacks concrete overhead metrics or references; if present in the full text, ensure they are tabulated with specific numbers.

Simulated Author's Rebuttal

2 responses · 0 unresolved

We thank the referee for the careful review and constructive focus on the rigor of the information-theoretic claim. We address each major comment below.

read point-by-point responses

Referee: [Abstract] Abstract: the assertion that 'Hindley-Milner unification over abelian groups computes the maximum a posteriori hypothesis under a computable restriction of Solomonoff's universal prior' is presented as following directly from the composition, yet supplies neither the definition of the prior restriction, the probability measure under which unification selects the MAP hypothesis, nor a reduction showing how Z^n type constraints correspond to program complexity in the universal prior.

Authors: The abstract qualifies the claim with 'We believe this composition yields', signaling an observed consequence of the three prior results rather than a fully derived theorem. The manuscript's core contribution is the design-time Z^n verification framework; the Solomonoff link is noted as emerging from the unique principal types and polynomial-time decidability, which align with minimal-description-length selection under an algebraically restricted prior. We will revise the abstract to label the equivalence explicitly as conjectural and add a one-sentence motivation tying Z^n constraints to program complexity. revision: partial
Referee: [Composition section] Composition of prior results (arXiv:2603.16437, arXiv:2603.17627, arXiv:2603.18104): the manuscript describes the three components at a high level but contains no explicit theorem, derivation, or mapping demonstrating that their integration produces HM unification over Z^n that exactly realizes the claimed information-theoretic equivalence.

Authors: We agree that the composition section remains high-level and lacks an explicit theorem or detailed mapping. The integration is intended to show that the dimensional type system, Clifford hypergraph, and coeffect domain model jointly support decidable HM inference over Z^n. We will add a short paragraph in the composition section providing a high-level correspondence (codata annotations preserve invariants, hypergraph derives sparsity, coeffects maintain domain constraints) and will state the HM-MAP equivalence as a conjecture supported by the algebraic properties, with the full reduction deferred to future work. revision: partial

Circularity Check

1 steps flagged

Central claim that HM unification over Z^n computes MAP under restricted Solomonoff prior reduces to composition of three self-cited prior works with no derivation shown

specific steps

self citation load bearing [Abstract]
"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 unifying"

The novel result (HM unification over abelian groups computes the MAP hypothesis under a computable restriction of Solomonoff's universal prior) is asserted to follow from the composition of the three self-cited prior works, yet the paper provides neither the explicit mapping nor the additional structure needed to bridge type constraints in Z^n to Solomonoff complexity; the equivalence is not derived but taken as following from the priors.

full rationale

The paper's strongest claim is presented as following directly from composing three prior results (arXiv:2603.16437, arXiv:2603.17627, arXiv:2603.18104). The abstract asserts the equivalence as a 'novel information-theoretic result' but supplies no definition of the prior restriction, no measure under which unification selects the MAP hypothesis, and no reduction showing how type constraints in finitely generated abelian groups correspond to program complexity in the universal prior. This matches self-citation load-bearing: the load-bearing argument reduces to the cited priors without independent derivation or external grounding exhibited in the manuscript.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 1 invented entities

The paper rests on the domain assumption that AI model properties fit the algebraic structure of finitely generated abelian groups with decidable inference, plus the composition of three prior works whose details are not re-derived here.

axioms (1)

domain assumption Properties determining numerical stability, computational correctness, and physical consistency are expressible as constraints over finitely generated abelian groups Z^n with polynomial-time decidable inference and unique principal type.
Invoked in the abstract as the shared algebraic structure enabling design-time verification.

invented entities (1)

program hypergraph no independent evidence
purpose: infers Clifford algebra grade and derives geometric product sparsity from type signatures
Introduced as one of the three composed components of the framework.

pith-pipeline@v0.9.0 · 5575 in / 1489 out tokens · 62904 ms · 2026-05-15T00:40:52.634725+00:00 · methodology

discussion (0)

Forward citations

Cited by 2 Pith papers

Reviewed papers in the Pith corpus that reference this work. Sorted by Pith novelty score.

Fixed-Point Scaffolding in the Clef Programming Language
cs.PL 2026-06 unverdicted novelty 5.0

Clef compiler applies fixed-point scaffolding and a functor from compilation poset to target category to preserve dimensional, grade, escape and numeric structure through MLIR lowering while adding compact-closed nega...
Negative and Fractional Types in the Fidelity Framework
cs.PL 2026-06 unverdicted novelty 2.0

Applies established negative and fractional type dualities to the authors' existing NTU framework to enable new resolution forms in specialized compute modalities.