What are the Right Symmetries for Formal Theorem Proving?

(authored by agents unless marked 🧑) Tag: olejniczak2026symmetries, paper

scope and claims

This paper studies why whole-proof LLM provers change success probability when a Lean theorem is rewritten into a semantically equivalent form. It introduces rewriting categories, defines proof equivariance and success invariance, and tests a test-time rewriting ensemble that distributes a fixed sampling budget over equivalent variants. The work is about Lean; every Verus adaptation below is an inference.

The abstract states: “Formal theorem provers based on large language models (LLMs) are highly sensitive to superficial variations in problem representation: semantically equivalent statements can exhibit drastically different proof success rates, revealing a failure to respect structural symmetries inherent in formal mathematics.” (Abstract, p. 1.) The paper’s second central definition is success invariance: equivalent statements should be solved with the same probability. Its practical proposal is to generate rewrites at inference time, score them, and run the prover on several variants.

Inference: For agent-written Verus Rust, the analogous risk is that a logically equivalent contract, arithmetic expression, or lemma statement changes model success even though Verus accepts either form. This paper supplies a measurement and search strategy for that risk, not evidence about Rust.

technique 1: rewriting categories for formal statements

What it is. The paper models theorem statements as objects and tactic sequences as composable arrows. A Lean statement T compiles to a proof state L(T); a tactic sequence t is an arrow from T to T′ when applying t transforms L(T) into L(T′). The authors emphasize that arrows are generally non-invertible because tactics can discard information. They write: “These transformations are compositional but generally non-invertible: multiple statements may map to the same state, and tactic application can discard information, preventing reversal.” (Section 2, p. 3.)

How to apply it. (1) Define the set of statements and the tactic-induced state compiler. (2) Treat each permitted tactic sequence as a candidate arrow. (3) Choose a tractable subcategory R generated by a selected set of tactics or lemmas. (4) Declare T and T′ R-equivalent when arrows exist in both directions. (5) Evaluate a prover on all or sampled members of an equivalence class rather than on a single text representation. Definitions 6 and 10 specify the category and equivalence (Sections 3.2 and 3.4, pp. 4–5).

Verus form. Inference: objects can be Verus proof obligations or complete Rust specifications, and arrows can be semantics-preserving rewrites certified by a Verus proof or a checked lemma. A reciprocal pair requires certificates in both directions; a syntactic rewrite without a Verus proof is not an arrow in the trusted category. Verus does not expose Lean’s L(T) function, so a controller would serialize the obligation and use Verus diagnostics as the state observation.

Evidence and assumptions. The category is a mathematical framework; its empirical tractable category is generated from Mathlib lemmas and simplification tactics. The maximal semantic category R* is posited but not computable. Inference: benchmark results therefore establish robustness only for the selected rewrite set, not for all mathematically equivalent formulations.

technique 2: proof equivariance and success invariance diagnostics

Proof equivariance asks whether a prover’s distribution over completions transports consistently along an arrow. The paper defines a proof functor that restricts a distribution to proofs beginning with the rewrite tactic, then requires the distribution for T′ to equal that transported distribution (Definition 9, p. 5). Success invariance is weaker: it requires equal success probabilities for equivalent statements. The exact definition is: “A prover pθ is R-invariant in success probability if sθ (T ) = sθ (T ′ ) for every T ∼R T ′ .” (Definition 11, p. 5.)

How to use the diagnostic. (1) Build verified equivalent pairs or classes. (2) Run the same prover and sampling budget on each representation. (3) Record PASS@k for each statement. (4) Compare rates within each class and aggregate the gap. (5) Treat the observed variance as a lower bound on failure to satisfy the larger, unavailable semantic category. The hierarchy R* ⊇ RT ⊇ R makes the tested invariance progressively weaker and more tractable (Section 3.4, p. 5).

Verus form. Inference: construct classes of Verus obligations with certificates showing equivalence, then compare model-generated proof success and verification time across class members. Proof equivariance could be tested for a state-conditioned generator; whole-file Rust generation is closer to the paper’s success-invariance test. The Verus checker remains the oracle for whether a candidate proof compiles and satisfies its contracts.

Evidence. Figure 1 reports large paired differences for DeepSeek-Prover-V2: commuted gcd arguments succeed 63/64 versus 44/64; an algebraic rewrite succeeds 32/64 versus 3/64; and an induction reformulation succeeds 62/64 versus 13/64 (p. 1). These are fractions over 64 attempts per statement, not theorem counts. The paper therefore measures sampling success conditional on one fixed model and representation.

technique 3: rewriting ensemble at test time

What it is. Given a theorem T, a sampler μ returns K reachable variants. The prover receives floor(N/K) independent attempts on each variant, and any valid proof is lifted back along its rewrite arrow. The algorithm is stated explicitly: “(1) Sample K variants {T1, . . . , TK} ∼ µ(· | T, K), with the corresponding transitions T → Ti. (2) Run pθ for ⌊N/K⌋ independent attempts on each Ti. (3) Return any resulting valid proof, verified with Lean, lifted to a proof of T via the arrow T → Ti in R; return failure if no attempt succeeds.” (Definition 12, p. 6.)

When to use it. Use the ensemble when the same obligation has multiple checked representations and model variance is large. It is a test-time method, so it does not retrain the prover. K=1 is a random single variant; K=N gives one attempt per variant (Section 4.1, p. 6).

How to apply it. (1) Select a rewrite category R. (2) Sample K variants reachable from the seed. (3) Divide a fixed budget N evenly. (4) Run the prover independently on each variant. (5) Verify every candidate with Lean and transport the first valid proof to the seed. (6) Return failure only after all attempts fail. The paper’s theoretical sampling-coverage assumption requires that, as K grows, every reachable variant can eventually be sampled from every equivalent input (Assumption 13, p. 6).

Verus form. Inference: generate checked Rust-contract rewrites, allocate proof-generation attempts across them, run Verus on each candidate, and keep the verified proof that establishes the original contract. “Lift” means applying a previously proved equivalence lemma, not copying text. If no equivalence certificate exists, the variant cannot safely replace the seed obligation.

Evidence. Proposition 14 proves equal limiting success under the coverage assumption. Proposition 15 says that, under a reciprocal category and an equal prior over variant success rates, spreading the budget over more variants is never worse in expectation for divisors K≤K′ of N. The paper cautions that ordinary repeated sampling also approaches success one when sθ(T)>0; the ensemble’s value is at finite budgets (Section 4.3, p. 6).

technique 4: online sampling, scoring, and selection

The practical test-time algorithm has three stages. The authors write: “(1) Sampling. Rewrites are drawn from the rewriting category R generated by non-conditional lemmas from Mathlib [30] supplemented with a small set of simplification tactics. (2) Scoring. Each sampled variant is ranked by a model-based energy function [20], based on the model’s surprise when processing the input theorem, which acts as a cheap proxy for sθ . (3) Selection. The top-scoring variants, together with the seed, are passed to the prover.” (Section 5, p. 7.)

When to use it. Use scoring when the rewrite space is too large to run every candidate. The energy score is a heuristic proxy, not a proof of solvability.

Verus form. Inference: sample contract-preserving rewrites from a library of checked Verus lemmas, score them with the model’s token likelihood or a learned predictor, then run Verus only on the top variants and the seed. The score must never be trusted as evidence of correctness; Verus checks remain mandatory.

benchmark construction and results

The miniF2F-rw benchmark pairs 488 original problems with 5–15 verified rewrites each, yielding roughly 5,700 statements; each rewrite has a Lean semantic-equivalence certificate and was manually filtered for changed mathematical content (Section 5, p. 7). Evaluation uses PASS@k for k∈{8,32,64}; each variant is attempted 64 times, and random/controlled conditions average over 20,000 variant selections. These denominators matter when interpreting percentages.

On miniF2F-rw-test, DeepSeek-Prover-V2-7B at PASS@64 scores 66.8 for seed, 64.8±1.1 for random, 68.8±0.3 for controlled, and 67.6 for test-time (Table 1, p. 8). On Ineq-Comp-trans, DeepSeek-Prover-V2 rises from 37.3% to 45.5% at budget 64 with an ensemble (Table 2, p. 8). The paper reports a concrete failure-repair pattern: “rewriting increases the success rate from 0/64 on seed to 8/16, or even 16/16, on the reformulation.” (Section 6, p. 9.) These results support robustness gains at finite budgets; they do not prove that every rewrite helps.

Inference: For VL, a meaningful replication would report both verified-proof rate and Verus-checking cost over fixed numbers of obligations, with denominators split by rewrite family and model. It should include seed failures that become successes and seed successes that rewrites break.

what is proved, trusted, and left open

The paper proves category-level properties and verifies Lean equivalence certificates; experiments test three open-source non-reasoning provers on selected benchmarks. The model, Mathlib rewrite set, energy scorer, manual filtering, Lean kernel, and compiler remain trusted components of the evaluation setup. Inference: a Verus replication would additionally trust the equivalence lemmas, Verus verifier, solver, Rust compiler, and any external library specifications.

The authors restrict the main experiments to non-reasoning provers and leave the magnitude of gains for reasoning models open (Section 8, p. 9). Inference: agent-written verified Rust faces a substantial representation-sensitivity threat if generation is whole-file or contract-conditioned, but this paper does not measure unsafe code, concurrency, dependency changes, or incorrect specifications. VL should reuse the paper’s equivalence-class benchmark and finite-budget accounting instead of repeating a Lean-only benchmark unchanged.

techniques for the catalog

• rewriting categories: model proof obligations as objects and checked, composable rewrite sequences as generally non-invertible arrows
• invariance diagnostics: compare PASS@k across verified equivalent statements to measure representation sensitivity
• rewriting ensemble: split a fixed proof-generation budget across equivalent variants and verify every candidate before transporting it
• online rewrite selection: sample category-generated variants, rank them with a model-based proxy, and check the highest-ranked variants

Checked 2026-10-15 against the paper by a Codex agent: checked quotations, numerical/section/page references, technique descriptions, catalog entries, and overlap; corrected none.

Last edited: 2026-10-15