Tractability tests are often computed from input syntax: support-graph treewidth, local coefficient patterns, backdoor tests, or action-count bounds. Before such a test can be lower-bounded or made algorithmic, it must define a predicate on the exact-certification problem itself. Equivalent presentations must receive the same verdict. The semantic object is the correctness quotient, whose classes are states with the same correct outputs. Correctness-preserving presentation moves generate closure orbits. A target that changes inside one closure orbit has an orbit gap and fails descent. Exact closure-invariant classification is possible exactly when the positive and negative orbit hulls are disjoint; the positive hull is then the least exact classifier, and computable orbit representatives make the classifier algorithmic. The results separate three layers. The descent layer gives orbit-gap obstructions for raw local syntax, raw action and coordinate counts, and raw support-graph predicates. The post-descent complexity layer applies ordinary reductions to descended objects: graph-predicate lower bounds transfer through action-gap graph extraction, and Action-Gap-Treewidth is NP-complete when the width bound is part of the input. The certification layer asks whether a proxy descends: for split proxies b∧φ(z), SAT reduces to non-descent and UNSAT reduces to descent. Positive regimes use quotient-preserving normalizations or catalogues before model checking; bounded quotient size, bounded full Gaifman treewidth of the constructed quotient, sparse unary-gap certificates, and strict-margin perturbation balls give explicit cost bounds after quotient construction.
As state-of-the-art neural networks are deployed on reasoning and algorithmic tasks, exactness guarantees become increasingly important. However, high average-case accuracy can still mask inconsistent behaviors. This motivates exact certification, which asks for the smallest set of labeled examples needed to certify that a learned hypothesis equals the target. We show that while some hypotheses are easy to certify, even minimal overparametrization can make certification exponentially hard across several hypothesis classes. For threshold circuits of depth ≥2, adding a single extra gate can force certificate sizes exponential in the input dimension. We show an analogous hardness result for log-precision Transformers with only constant architectural overhead. We also characterize approximate certification, showing that allowing only polynomially many mistakes still requires exponentially large certificates, whereas constant relative-error guarantees can hide exponentially many mistakes. Empirically, we study certification for constructed circuits and trained Transformers for recognizing binary addition. While the constructed circuits instantiate the exponential barrier for certification, the trained Transformer analysis shows that imperfect models can evade detection by large uniformly sampled certificate candidates.
Grounding, the translation of high-level theories into equivalent quantifier-free formulas, is a crucial step in declarative solving, yet it has so far escaped the proof-logging revolution. When this grounding step is not certifying, there is no way of knowing that the obtained solutions actually correspond to the original problem specification, resulting in a trust gap. In this paper, we close the trust gap between the user's high-level specification and the solver's low-level input by introducing a novel certifying grounding framework for first-order logic model expansion (FOX) over finite domains. We present CertiFOX, a framework consisting of: (1) a proof format for grounding derivations, (2) GroundFOX, a certifying grounder operating on theories in Grounding Normal Form (GNF)--a new normal form designed for compact, domain-aware grounding--and (3) CheckFOX, an independent proof checker. Our approach guarantees that the grounder's output is equivalent to the input specification, setting the stage for trustworthy end-to-end certified solving pipelines for declarative languages. Experimental evaluation confirms that CertiFOX is a feasible approach. The GroundFOX grounder is broadly comparable with other grounders, and proof checking with CheckFOX adds overhead within a small constant factor of grounding time.
Daimy Van Caudenberg, Alexander Ek, Carlos Cantero +1
We develop an exact linear programming (LP) formulation for bounded-depth classification trees with binary features, using a junction-tree representation. The formulation is integral and supports recursive subtree optimization. Exact reductions make the model smaller while preserving the optimal value and recovery of an optimal tree. The reduced model supports two solution methods: column generation and message passing. Column generation solves integral restricted LPs and uses bounds over the full feasible domain to certify optimality. Message passing recursively combines optimal subtree costs. Both methods solve common subtree problems that, once the preceding tree decisions are fixed, can be evaluated independently and in parallel. Computational experiments show that the exact reductions substantially reduce the size of the junction-tree formulation. The resulting linear programming formulation certifies instances for which the tested mixed-integer formulation does not establish optimality within the same computational budget, while the column-generation and message-passing methods certify more instances and achieve an order-of-magnitude reduction in geometric-mean runtime relative to an existing state-of-the-art exact method for optimal classification trees.