Learning to Disprove: Formal Counterexample Generation with Large Language Models
AI math systems can prove theorems. This one learns to disprove them.
subtitle: A team at ETH Zurich and MiroMind shows that teaching models to find formal counterexamples requires a completely different approach—and almost no training data existed to do it.
The field of AI mathematics has a blind spot. Every major system—AlphaProof, Goedel-Prover, Kimina Prover—is built to prove theorems. None of them are designed to disprove them. But disproving false conjectures is half of mathematical work, and a new preprint posted to arXiv argues that this asymmetry isn't just an oversight. It's a tractable problem that the field has been ignoring.
The paper, submitted March 19, comes from a team spanning ETH Zurich, the University of Toronto, MiroMind's Verifiable AI Lab, and Nanjing University. The lead author is Zenan Li, a PhD student at ETH Zurich working under Zhendong Su, a computer science professor known for compiler testing and software verification research. Li's own background is in deep learning quality assurance—a fact that turns out to matter quite a bit for how they approached the problem.
The core task is this: given a mathematical statement that's false, generate a formal counterexample that proves it false—and have that counterexample verified by Lean 4, the formal proof assistant. Not an argument in natural language. Not a plausibility sketch. A machine-checkable proof.
The hardest part isn't the model. It's that training data essentially doesn't exist.
The data problem
CounterMath, a benchmark published in 2025 by some of the same researchers, contains 1,216 counterexample problems hand-curated from Chinese university mathematics textbooks, translated by professionals, and validated by mathematicians. That's the full extent of what was available for training. For comparison, Mathlib—the standard library of formally proven Lean 4 theorems—contains hundreds of thousands of theorems. The imbalance is severe.
Li and his colleagues solve this with what they call a symbolic mutation strategy. The insight comes directly from software testing methodology: mutation testing works by taking known-good code, introducing small faults (mutations), and checking whether a test suite catches them. Apply the same logic to mathematics: take a formally provable theorem with hypotheses H1, H2 that together imply a conclusion C. Drop one hypothesis—say H1. Now you have a weaker statement that may not hold. If H1 was genuinely essential (i.e., not redundant), then a counterexample must exist. Lean 4 confirms whether the dropped hypothesis was essential or redundant before the problem is included in the training set. Every problem in the resulting dataset is guaranteed to be solvable.
Seeds come from Lean 4 Mathlib and from intermediate subgoals generated during the proofs of other theorems. The result: 575,000 synthesized training data points, built almost from scratch.
The training challenge
Synthesizing training data solves one problem and reveals another. On hard counterexample problems, models fail completely at first—they can't find a counterexample, so there's nothing successful to learn from. Standard expert iteration (generate, filter for successes, fine-tune, repeat) stalls when the success rate approaches zero.
The team addresses this with a multi-reward approach. Even when the model fails to find the complete counterexample, it gets a training signal from partial success: whether it managed to prove the mutated statement and whether it correctly proved the dropped hypothesis. These auxiliary rewards keep the gradient alive on difficult problems. The combined approach—mutation-synthesized data, informal-to-formal generation pipeline, multi-reward expert iteration—is what they're calling their full system.
The results, on their own new benchmarks, show 47 to 74 percent relative improvement in pass@1 success rate over the strongest baseline. The paper does not specify what the absolute pass@1 numbers were at baseline—a notable gap that Giskard should check. Relative improvement is meaningful, but if the baseline was 5 percent, a 74 percent relative gain brings you to around 8.7 percent. Still a real result, but the framing matters.
Who built this
Kaiyu Yang, a co-author from MiroMind's Verifiable AI Lab, is the institutional anchor here. Yang created LeanDojo, the standard dataset and toolkit for LLM theorem proving in Lean, and Lean Copilot, which integrates LLMs into the Lean proof assistant. His stated goal is producing AI whose correctness can be verified without labor-intensive human checking. This paper fits directly into that agenda: before you try to prove a conjecture, you'd want to know whether it's even true. Counterexample generation is the complement to proof search.
Zhendong Su, the senior author, brings a different angle. Su's reputation is built on compiler testing—specifically differential testing and fuzzing, techniques for finding bugs by generating inputs that expose inconsistencies between implementations. The mutation strategy in this paper has his fingerprints on it. The logic is identical: take something known to be correct, introduce a controlled perturbation, verify that the perturbation matters, use that as a test case. The methodology crossed from software verification into mathematics through his students.
What it claims to do beyond math
The paper's most interesting claim—and the one that will need the most scrutiny—is that counterexample generation capability helps models self-verify their own reasoning. If a model can identify when one of its intermediate conclusions is wrong by generating a counterexample to it, it becomes more robust against hallucination in multi-step reasoning. The paper demonstrates this as one of three application tasks, alongside counterexample search and verification of autoformalized results.
That's a broader claim than "we got better at math benchmarks." But the paper is a preprint posted to arXiv; it hasn't been peer reviewed. No model or code appears to have been released alongside the paper. The three new benchmarks the team introduced—and on which they measure their 47 to 74 percent improvement—were also created by this group, which is worth noting even if it's not unusual in ML research.
CounterMath, the benchmark they beat, was also created by some of the same authors.
The gap in the field
The asymmetry between proof construction and counterexample generation in AI math is real. It's partly a consequence of where competition benchmarks have pointed the field—IMO problems, miniF2F, MiniF2F-Test are all about proving true statements. It's partly because evaluation is cleaner when you're checking proofs. And it's partly because the training data problem for counterexamples was, until this paper, genuinely unsolved.
The mutation strategy is a clean answer to the data problem. Whether the resulting capability is as general as the paper claims—and whether it transfers to the kind of reasoning verification that would make it useful beyond formal mathematics—is what the next round of work will need to establish.
This article is based on a preprint posted to arXiv on March 19, 2026. The paper has not been peer reviewed.