cs.LOSep 16, 2026

The Refutation Gap: Certifying Both Halves of an Optimality Claim

Authors: Rohan Pandey

Read PDF
Ask AI
Cite

Copy citation

DOINot available for this paper

Abstract

Synthesis pipelines increasingly claim not just that a program is correct, but that it is optimal. Such a claim has two halves with radically different verification stories. The upper bound, "a program of size m exists", is witnessed by an artifact that can be re-executed, proved equivalent to its specification, and shipped with a machine-checked certificate. The lower bound, "no program of size m-1 exists", has no witness and is discharged by running a solver until it reports UNSAT. Combinatorial optimization has known this asymmetry for decades and has largely addressed it: certifying algorithms make it explicit (McConnell et al., 2011), and pseudo-Boolean proof logging can certify optimality end to end with a formally verified checker (Bogaerts et al., 2023; Koops et al., 2025). That discipline has not reached circuit minimization. We call this the refutation gap: published gate counts for minimal XOR circuits provide no certificate for either half of the claim, and neither did 121 optimality results we ourselves produced. We close the gap with a pipeline that synthesizes minimal linear straight-line programs over GF(2), where every decisive UNSAT answer emits a DRAT proof checked by an independent third-party checker. We certify all 121 optimality results established by the project, across n = 6 to 9: 111 carry independently verified refutations, 10 are closed by a free counting bound, and none disagrees with the uncertified value. The median proof is 1.1 MB and checking costs 1.9x solving. We give five case studies where verification caught defects that code review did not, report two interface obstacles that push practitioners toward the uncertified path, and describe an adversarial audit that revealed a failure tail we were about to attribute to the problem was actually caused by our own budget.

Figures & tables

Figure 1: The refutation gap. The two halves of one optimality claim get opposite treatment. The upper bound is an object, so every verification technique applies to it and the reader ends up holding a machine-checked certificate; the costs shown are the ones we measure in § 3 . The lower bound is the absence of an object, so the same three slots are empty and what reaches the reader is a solver’s verdict. This paper is about giving the right-hand column a certificate too.
Figure 2: The construction-side stack. (a) Each layer establishes more than the one below and trusts a different thing, so a defect must survive three unrelated checks to reach a recorded result. (b) Measured cost per circuit: Layer 1 on re-verifying the 108108 -gate AES MixColumns circuit, Layer 2 on the five cipher matrices, Layer 3 on the thirteen emitted certificates. The fraction at each Layer 2 bar is how many of the five the encoding actually settles: the fast encoding is 100×100\times quicker and returns unknown on one matrix, which is the cheapest illustration we have of why a default matters.
DefectCaught byMissed by
(i) Paar rewrite rescanned signals created in the same pass: inflated gate counts, occasional self-XORLayer 1, immediatelycode review
(ii) CLEFIA diffusion matrices built as circulant; they are Hadamardan external anchor: published baseline, 134→121134\to 121 on correctionall three layers: the circuits were valid, for the wrong matrix
(iii) Lean emitter line-wrapped inside (a, b) tuples, producing invalid Leanround-trip parse testvisual inspection of the output
(iv) A source review argued one cipher applies its matrix by right-multiplication, so we transposednumerical cross-validation: failed transposed, passed originala clear, confident natural-language argument
(v) The Lean emitter put the instance name into the namespace unescaped, so a density made namespace CertRandn8m8d0.3s11 : two identifiers, not onecompiling the file, the first time a certificate for a random instance was ever producedevery test we had, and the shadow evaluator: the file was right about the mathematics and malformed as a file
Table 1: Five real defects and what caught each. None was found by reading. Item (ii) is the failure mode internal verification structurally cannot reach, and argues that reproducing published numbers is a verification layer in its own right. In (iv), and in a second instance where a size trend we had written up as a headline finding turned out to be an artifact of a counting bug, a natural-language argument was confidently wrong and a mechanical check was right. Where an LLM supplies the reasoning, the reasoning is worth having and it is not evidence. Item (v) is the sharpest version of the paper’s whole argument, and it arrived late enough to be embarrassing: Lean elaborated the broken file anyway and #print axioms still reported [propext] , so every semantic check we owned passed a file that does not parse. It is also defect (iii) returning in a case (iii)’s own regression test cannot see, because that test reads the gate list back and never looks at the scaffolding around it.
Figure 3: Twenty-five years of upper bounds, and no certificates. Published g-XOR counts for the AES MixColumns matrix: 108108 [ 20 ] , as collated by Kranz et al. [15] ; 103103 [ 13 ] ; 9797 [ 15 ] ; 9595 [ 3 ] ; 9292 [ 17 ] ; 9494 [ 24 ] ; 9191 [ 16 ] , obtained independently and under the stricter s-XOR metric by Yuan et al. [28] ; 8989 [ 22 ] ; 8888 [ 12 ] . Filled markers held the record when published; 9494 is hollow because Maximov ’s 9292 preceded it on ePrint by three days. Within-year points are offset horizontally for legibility. The hatched region is everything no published result excludes for this matrix; its floor is the free counting bound of 3232 , the only lower bound obtainable without work. Progress is entirely one-sided, and no entry ships a certificate for either half.
Figure 4: One certified optimality result, in full. Left: the witness, an 88 -gate program, re-executed, proved equivalent to MM over the whole input space, and shipped as a Lean 4 certificate whose printed axiom list is [propext] (compiled under Lean 4.34.0; the thirteen cipher certificates of § 3 were compiled under 4.33.1). Right: the refutation at k=7k=7 , a 0.910.91 MB DRAT proof an independent checker confirms in 0.240.24 s. Together they instantiate ( 5 ) for a single matrix: both halves of SLP(M)=8\mathrm{SLP}(M)=8 are objects a reader can re-check, rather than verdicts. Two things are still taken on trust, and we name them in § 7 : drat-trim itself, and the argument that φk(M)\varphi_{k}(M) faithfully encodes ( 3 ).
Figure 5: Certification is affordable at this scale. (a) Every one of the 121121 results is certified: 111111 by a refutation an independent checker verified, 1010 by a counting bound that makes a refutation unnecessary. (b) DRAT proof size against formula size: small in absolute terms, but spanning five orders of magnitude. (c) Independent check time against solve time, with the y=xy=x reference. The points far above the diagonal at the left are the checker’s fixed startup cost on instances that solve in milliseconds, not a scaling problem. The ratio falls to about 1.2×1.2\times in mid-range and then rises again in the tail, reaching 2.7×2.7\times on the largest proof, so the median of 1.9×1.9\times understates what a practitioner pays on the instances that matter.
Optimality results the project had established121
certified by an independently checked refutation111
closed by a free counting bound, no refutation needed10
uncertified0
Refutations the checker rejected0
Disagreements with the uncertified value0
Instances by size ( n=6/7/8/9n=6/7/8/9 )51 / 50 / 18 / 2
Table 2: Proof-carrying optimality over every optimality result the project had established. Checking costs 1.9×1.9\times solving at the median, 2.7×2.7\times on the largest proof. The 121121 is itself the closable subset of 148148 instances the search attacked; over all 148148 , 82%82\% end in a certified optimality result.
More in this topic

Formal Verification

Formal verification uses mathematical models and machine-checked proofs to establish whether software and systems satisfy precise specifications.

See all 341 papers

Explore similar work

CardsList
Jul 18, 2026

Falsification-Based Verification of LLM-Generated Optimization Models: Sound Test Batteries and Their Detection Limits

Large language models now translate natural-language descriptions of decision problems into solver-ready optimization models, but they fail silently. A generated model often runs and still formulates the wrong problem. This paper develops a theory of falsification-based verification for this setting. Every numeric quantity in the description is a typed slot, and a candidate model is tested only through solver calls on slot-transformed instances; no reference model or label is consulted. From duality, comparative statics, and polyhedral limit arguments we derive a battery of test classes covering directions, curvature, crush probes, prohibitive limits, annihilation, and exchange. Every test is sound, so a violation certifies unfaithfulness and the false-positive rate is zero by design. We characterize what such verification can never see, give conditions under which the canonical error classes are detected with certainty, and prove that no fixed-threshold perturbation tester is simultaneously sound and nontrivial. Experiments on 326 ground-truth models from NL4OPT and four benchmark families confirm the theory. The battery attains a 0.0% false-positive rate against 54.9% for a threshold tester, detects 70.0% of certified conditional-class mutants, convicts 40.4% of the mutants invisible to execution-accuracy scoring, and reproduces the predicted detectability pattern including its zeros.

Haifeng Li, Mo Hai

School of Information, Central University of Finance and Economics

Metamorphic TestingFormal VerificationLLM ReliabilityNatural Language to Optimization Modeling
AskPDF
Oct 21, 2026

ORSMT: Unleashing the Potential of Satisfiability Modulo Theories for Semantic Verification and Repair in LLM-Based Optimization

Large language models increasingly automate optimization modeling from natural language problems, producing written mathematics, solver code and a returned report. Verifying one optimization problem across these artifacts requires semantic comparison: unequal models can attain the same objective, equivalent models can use different auxiliary variables, and mutually consistent artifacts can omit the same source requirement. ORSMT provides a typed semantic interface and exact SMT relation queries. It aligns observable decisions, projects auxiliary variables, proves or refutes feasible region and objective relations, localizes refutations to implicated rows or domains and links source texts when available. It then reconstructs one artifact from another, and each adopted candidate passes the required relation checks. Across 3,034 problems and six generator sizes, ORSMT improves the model-code match rate in all 72 benchmark and generator combinations before selection. Protected selection raises the aggregate rate from 43.2% to 88.2% and the share that are both correct and matched from 25.2% to 40.2%. On the 1,905 refuted outputs, certified voting under the shared fallback makes 50.9% of outputs correct and matched, compared with 44.8% for ReLoop and 49.4% for Opt-Verifier. A separate one-round source revision followed by exact reconstruction restores a model-code match for 84.4% of the refuted pairs.

Rui Zhang, Chenyu Zhou, Jianghao Lin +3

Shandong University · Shanghai Jiao Tong University · Eindhoven University of Technology

Large Language Model-Guided OptimizationNatural Language to Optimization ModelingFormal Verification
AskPDF
Jun 29, 2026

A Machine-Verified Proof of a Quantum-Optimization Conjecture

We report a machine-verified resolution of a problem open for over a decade in quantum optimization: the Farhi, Goldstone and Gutmann (FGG) conjecture that depth-pp Quantum Approximate Optimization Algorithm (QAOA) on the ring of disagrees attains approximation ratio (2p+1)/(2p+2)(2p+1)/(2p+2) exactly. We found the proof using a large language model, Claude Fable 5, and verified its correctness end-to-end by the Lean 4 proof assistant. Our methodology includes several ingredients: building on a substantial Lean library of quantum information, we formalized the QAOA components and the known parts of the problem, and reduced the conjecture to a single open mathematical statement. The model was then handed the library and our agentic toolkit, and tasked with closing that gap by constructing a proof in Lean. The resulting process is a feedback loop between the model's natural-language reasoning and Lean's mechanical verification, which converged to a machine-verified proof. Human verification is required only for the structural scaffolding - that the formal statement faithfully encodes the intended claim - while the proof itself is supplied by the model and certified mechanically by Lean. The proof is nevertheless striking - the model uncovered a hidden dynamical symmetry of the problem and exploited it, borrowing tools and machinery from an adjacent field to turn a hard existence problem into an explicit construction. This work paves the way for resolving open conjectures in quantum information science and beyond.

Uri Kol, Maor Ben-Shahar, Kfir Sulimany +1

Center of Mathematical Sciences and Applications, Harvard University, Cambridge, Massachusetts 02138, USA · MIT Center for Theoretical Physics - a Leinweber Institute, Cambridge, MA 02139, USA · Research Laboratory of Electronics, Massachusetts Institute of Technology, Cambridge, Massachusetts 02139, USA

Large Language Model-Guided Theorem ProvingQuantum Approximate Optimization Algorithm
AskPDF