A Proof Can Pass and Still Mean the Wrong Thing: What AxQM Changes About Formal AI Evaluation

TL;DR for operators

When an AI system produces a formal proof, an evaluation team can make one part of the verdict unusually objective: either the proof is accepted under the allowed rules, or it is not. That removes much of the grader variance found in rubric scoring or LLM judging.

AxQM provides 1,019 Lean 4 proof-synthesis tasks over 479 finite-dimensional quantum-mechanics textbook items. It keeps a private reference solution for every task and grades submissions through successful compilation, absence of sorry in the proof or its dependencies, and absence of newly introduced axioms.¹

The boundary is semantic. A kernel-accepted theorem can still formalize the wrong physical claim. For operators, the clean division is: use the kernel to judge deduction, private solutions to establish solvability without publishing answers, dependency metadata to diagnose library-navigation demands, and expert review to decide whether the formal statement still means what the original requirement was supposed to mean.

The objective signal is narrower than it first appears

A model returns a technical derivation. The evaluator needs a pass/fail decision that survives reruns, model changes, and regression testing. Natural-language grading is weak here because the grader can vary.

A formal proof assistant changes that. Once a claim has been encoded into definitions, hypotheses, and a theorem statement, a small trusted checker—the Lean kernel—can determine whether the submitted proof follows from those inputs.

AxQM scales this idea beyond isolated exercises. The authors extracted 687 explicitly numbered items from Nielsen and Chuang, formalized 505, and used 479 of them to produce 1,019 benchmark tasks. The released library adds 3,519 Lean declarations on top of its Mathlib fork; the complete private library, including solutions, contains 10,560.

For evaluation teams, the direct gain is reproducibility. Proof acceptance no longer depends on whether another model finds the reasoning persuasive.

Private solutions make solvability auditable without publishing the answers

Every AxQM task has a private reference proof. This guarantees that each released task is solvable while avoiding the most direct contamination route: placing the benchmark statement and its reference proof together in public training corpora.

Those private proofs also produce structural metadata. AxQM groups tasks into five proof-length bands according to the number of additional declarations required by the reference proof: 158 very small, 324 small, 280 moderate, 190 large, and 67 very large.

The label is easy to overread. It measures reference-proof size, not validated difficulty for a human or model. A product team can still use the bands to stratify regression results, but a drop on “very large” tasks does not by itself identify why the model struggled.

Lean can certify the proof and miss the wrong specification

The paper’s main warning is that deterministic proof checking does not make the whole evaluation deterministic.

Lean verifies whether a theorem follows from the formal objects supplied to it. It cannot determine whether those objects faithfully preserve the intended physical statement. The authors identify several kernel-invisible failure modes: a definition can make a theorem vacuous, quantifiers can be weakened, or assumptions can be written so that they effectively contain the intended conclusion.

This is the difference between deductive correctness and semantic faithfulness. The first asks whether the proof follows from the encoding. The second asks whether the encoding still represents the physics.

For high-assurance workflows, that distinction determines authority. Kernel acceptance can govern the proof layer. It should not have final authority over the specification layer when the costly failure is proving a weakened or incorrectly modeled requirement. Domain review remains necessary there.

The benchmark measures library use as well as theorem proving

AxQM is also structurally interconnected. For the median textbook item, 84% of the declarations in its dependency closure—the full set of earlier declarations it ultimately relies on—are also used by at least one other item.

Reference proofs for 387 of the 1,019 tasks invoke at least one other benchmark task. A prover may therefore need to navigate shared definitions, retrieve reusable lemmas, and compose earlier results rather than solve a self-contained theorem from scratch.

That supports two distinct evaluation regimes: independent tasks and dependency-ordered tasks. Cognaptus inference: teams should keep those results separate when they answer different product questions. Independent evaluation emphasizes proof synthesis against a fixed library; dependency-ordered evaluation better resembles a system that accumulates verified results over time. One aggregate score can hide that difference.

Match each control to the failure it can detect

This layered design is more useful than treating “formal verification” as a single guarantee. Each control removes a different class of uncertainty.

What remains unresolved

AxQM’s evidence is strong on benchmark composition, deterministic grading, guaranteed solvability, and dependency structure. The paper does not report a broad model leaderboard, so it does not establish which theorem-proving systems perform best on AxQM or which structural features most strongly predict model failure.

Its scope is also bounded to finite-dimensional quantum mechanics and quantum information. Infinite-dimensional systems, unbounded operators, and non-mathematical textbook tasks are outside scope. The benchmark also uses a Mathlib fork required to represent multi-semilinear structure for multi-register quantum systems.

These limits define the use case rather than nullify it. AxQM is a strong test bed for proof synthesis inside a coherent specialized library. It does not turn the modeling step that connects physics to mathematics into something the kernel can certify.

Give formal verification authority over deduction, not meaning

For operators, the most defensible use of AxQM is to narrow the authority of formal verification rather than inflate it. Let the kernel decide whether a submitted proof follows. Let hidden reference proofs establish solvability. Let dependency metadata expose shared-library demands. Keep expert review focused on the layer the kernel cannot inspect: whether the formal statement is the right statement.

That division makes the evaluation stronger because each control is responsible for the failure mode it can actually detect.

Cognaptus: Automate the Present, Incubate the Future.