Learning to Disprove: Formal Counterexample Generation with Large Language Models

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

problem and core workflow

Li et al. train language models to find counterexamples to false universal mathematical statements and prove those counterexamples in Lean 4. The task is sequential: propose a concrete witness informally, then produce a formal existential proof that Lean checks. The paper states, “Formal counterexample generation aims to establish a two-stage, informal-to-formal process.” (Section 2, p. 2)

For a conjecture ∀x, P(x), a witness x* proves ∃x, ¬P(x). The paper’s Figure 2 example asks for A,V : Fin 2 → ℝ satisfying two equations. The model proposes A(0)=1, A(1)=0, V(0)=0, V(1)=1; Lean then checks use A; use V; dsimp [A,V]; simp. A successful proof is the acceptance criterion, not the model’s natural-language explanation.

The framework has two stages: symbolic mutation creates a large unlabeled counterexample dataset, and multi-reward expert iteration fine-tunes one model to propose witnesses and another to prove them. The authors report 575,039 mutated problems from 321,929 seed theorems (Table 1, p. 6), reserving 3,000 for validation and training for one epoch of 56 iterations with batch size 10,000 (Section 4.2, p. 7).

technique 1: proof-aware theorem mutation

What it is. Start from a formally proved universal theorem with hypotheses, remove one hypothesis, and ask for a witness showing the weakened theorem fails. The mutation is proof-aware: Lean analyzes the original proof to remove redundant hypotheses before generating a problem.

How to apply it.

1. Collect seed theorems that are formally provable and universally quantified. Sources are Mathlib, Leanworkbook, and intermediate lemmas/subgoals from MiniF2F and PutnamBench proofs generated by Goedel prover v2 and DSP+ (Section 3.1, pp. 3–4).
2. Decompose a proof into steps. A declarative have or suffices step is transformed directly into a theorem; a procedural simp or rw step is compared before and after the tactic to establish a theorem (Section 3.1, p. 3).
3. Normalize a seed as theorem original_version (x : X) : H1 x → H2 x → C x.
4. Use Lean to identify redundant hypotheses, then drop an essential H1, producing H2 x → C x.
5. Encode the counterexample problem as theorem mutated_version : ∃ x : X, H2 x → C x and invoke Lean again to ensure grammatical correctness.

Verus form. Inference: represent H1, H2, and C as spec fns over a Rust mathematical type, and express the original theorem as a proof fn with requires H1(x) && H2(x) and ensures C(x). A mutation generator can remove one conjunct and ask for a concrete witness; a Verus proof fn then proves the existential by constructing the witness and showing the implication. Verus does not automatically inspect a proof body to identify redundant hypotheses, so that analysis remains an external transformation.

Evidence and limits. Table 1 lists 43,990 Mathlib seeds yielding 88,217 mutations, 17,061 Leanworkbook yielding 42,480, 48,415 MiniF2F yielding 94,215, and 212,463 PutnamBench yielding 350,127; total seeds are 321,929 and mutations 575,039. Mutation ratios range from 1.64 to 2.48 and average execution time from 0.10 to 0.71 seconds per seed in Figure 3 (p. 6). The paper’s abstract rounds this to “575K counterexample data points”; the exact table total is 575,039. Mutation correctness is checked syntactically and by theorem-prover analysis, but the paper does not manually audit every generated witness problem.

technique 2: two-stage witness-and-proof generation

What it is. Separate informal search from formal checking. Model qϕ samples a witness xi from the mutated problem; proof model qψ generates a Lean proof conditioned on both problem and witness. A witness is accepted only if Lean verifies its proof.

How to apply it.

1. Prompt qϕ with a mutated existential problem and generate xi.
2. Prompt qψ with (Mi,xi) to generate πiM proving the mutated statement.
3. Run Lean on πiM; record I(Verify(πiM)).
4. Keep the pair for training only with its verification-derived weight.

The approach is deliberately guess-and-check. The paper says, “the LLM first proposes a potential counterexample and then verifies its validity.” (Section 2, p. 2)

Verus form. Inference: have an ordinary Rust/LLM generator propose concrete values, then call a Verus proof fn that takes those values and ensures the negated property. Verus’s solver proves the final witness; it does not prove that the LLM’s informal reasoning found all relevant edge cases. A finite witness proof refutes one statement instance and cannot establish a broader bug class.

technique 3: multi-reward training from necessary and target proofs

What it is. A valid witness for H2(x) → C(x) should also violate the dropped hypothesis, ¬H1(x). The system therefore asks for two Lean proofs and gives separate rewards: rM = α I(Verify(πM)) for the mutated theorem and rH = (1−α) I(Verify(πH)) for ∃x, ¬H1(x). The combined sample weight is r = rM + rH; the paper uses α=0.8 for multi-reward training and α=1.0 for the single-reward baseline (Section 3.2 and 4.2, pp. 4, 7).

How to apply it.

1. Generate xi, πiM, and πiH for each mutation.
2. Verify both proofs in Lean and compute the two indicator rewards.
3. Weight witness fine-tuning examples (Mi,xi) by rM+rH.
4. Weight proof fine-tuning examples separately by rM and rH.
5. Use Dr.GRPO, a normalized GRPO variant, to regulate proof length so the model does not exploit easy short proofs (Section 4.2, p. 7).
6. Repeat inference, verification, and supervised updates for each training iteration.

Verus form. Inference: define two proof fns, one proving the target negation and one proving the omitted-hypothesis violation, and combine their Boolean verification results in an external trainer. Keep the target ensures fixed; never grant reward for a vacuous requires or an ensures true. Verus itself supplies binary proof evidence, while reward weighting and length control remain training code.

Evidence. On the 3,000-instance validation set, multi-reward training converges to approximately 49%, 52%, and 54% pass@1/4/9, versus 43%, 46%, and 47% for single-reward training (Figure 4, p. 7). The denominators are the 3,000 held-out validation instances; the paper reports approximate rates from curves, not exact counts. The easier ¬H1 proof can create a low-difficulty trap, so its weight is intentionally reduced through 1−α.

technique 4: benchmarked counterexample and error detection

The fine-tuned model is tested on three tasks. FOR-COUNTER contains 1,058 formalized problems from CounterMath. VERI-REASON contains 3,000 unprovable problems made by formalizing FormalMath reasoning steps. VERI-FORMALIZE contains another 3,000 unprovable problems generated by formalizing FormalMath theorems (Section 4.3, p. 7). Table 2 reports absolute correctly solved counts at pass@1, pass@4, and pass@9 because the established benchmark contains inaccuracies.

For the authors’ model, Table 2 gives FOR-COUNTER 222/274/302, VERI-REASON 213/260/295, and VERI-FORMALIZE 174/255/313 at k=1/4/9. The strongest-baseline differences at pass@1 are +95, +69, and +63 respectively, as stated in the paper. Inference: pass@k values are counts, not percentages; denominators are 1,058 for FOR-COUNTER and 3,000 for each 3K verification benchmark, but the paper does not convert the table to rates. The paper itself warns that benchmark inaccuracies motivated count reporting.

Verus form. Inference: use a corpus of Rust/Verus functions with deliberately weakened contracts, generate concrete violating inputs, and require a proof fn witness for each violation. Count only witnesses that Verus accepts, and report denominator and contract version. This tests specification bugs as well as implementation bugs; it does not prove that no other violating input exists.

what remains trusted and product risk

Lean verifies the formal proof terms for each supplied witness. The seed theorem statements, proof decomposition, mutation tactic, LLM-generated informal reasoning, model training data, and external benchmark formalization remain trusted inputs or search components. The authors report that 7B models often fail arithmetic, ignore supplied witnesses, or produce inaccurate rewards (Section 6, p. 9). Synthetic-data quality is also limited: training curves converge in roughly half an epoch, suggesting redundancy. These are explicit limitations, not evidence that larger models solve the problem.

Inference: counterexample generation is valuable for VeruLaw because it can challenge overly strong or vacuous Rust/Verus contracts before accepting generated code. It threatens a product that treats one passing proof as evidence that a specification is correct. VL should not redo generic Lean mutation or the idea of a verifier-gated witness; a useful adaptation is mutation of Verus requires/ensures, with independent contract review and regression tests. A Verus pass for a generated counterexample proves that the particular witness violates the written contract; it does not establish that the intended product behavior is wrong unless the contract is the right one.

techniques for the catalog

• proof-aware hypothesis mutation — remove an essential hypothesis from a proved universal theorem and generate an existential counterexample problem
• two-stage formal counterexample generation — propose a witness informally, then prove the instantiated existential statement in Lean
• multi-reward witness training — reward both violation of the dropped hypothesis and proof of the mutated target
• proof-length reward shaping — downweight easy auxiliary proofs and regulate generated proof length with normalized policy optimization
• verifier-gated benchmark checking — count only counterexamples whose formal proofs pass the theorem prover
• counterexample-based specification audit — use witnesses to test autoformalized theorem statements and intermediate reasoning steps

Checked 2026-10-15 against the paper by a Codex agent for learning_to_disprove_20261014.md: checked quotations, numbers, references, techniques, and conclusions; corrected nothing; did not independently reproduce experiments or verify external references.

Last edited: 2026-10-15