Learning to Disprove: Formal Counterexample Generation with Large Language Models
summary
The gist
The gist The paper addresses the gap in mathematical reasoning AI by fine-tuning large language models to generate formal counterexamples, which requires both proposing candidate instances and
In short
The research fine-tunes large language models to generate formal counterexamples for mathematical statements, moving beyond simple proof construction. The method uses a symbolic mutation strategy to create training data and a multi-reward framework to guide the model. This approach significantly improves the model's ability to find disproofs, enhancing its self-corrective reasoning capabilities.
Key concepts
- Formal Counterexample Generation
- This is the core task where an AI must not only suggest a potential answer that disproves a theorem but also write a complete, formal proof using tools like Lean 4 to verify that the proposed counterexample actually works against the original statement.
- Symbolic Mutation Strategy
- This technique automatically creates new training problems by taking existing theorems and systematically removing one of their hypotheses. This process generates a large, varied dataset of 'before and after' scenarios, helping the LLM learn how to break logical structures.
- Multi-Reward Guided Training
- Instead of a single reward signal, this system uses two rewards: one for finding an actual counterexample that contradicts the removed hypothesis, and another for proving the target theorem. This dual reward system ensures the model learns both finding disproofs and maintaining formal correctness.
- Lean 4 Theorem Prover
- Lean 4 is a specific, powerful software tool used to automatically check if a mathematical statement or a proposed counterexample is logically sound. It acts as the automated 'judge' that verifies the formal proofs generated by the AI model.
Terminology used across episodes
This episode discusses
- Learning to Disprove: Formal Counterexample Generation with Large Language Models · Paper Radio
- Large Language Models for Mathematical Reasoning: Progresses and Challenges
- Thinking Machines: Mathematical Reasoning in the Age of LLMs
- MathConstruct: Challenging LLM Reasoning with Constructive Proofs
- Reviving DSP for Advanced Theorem Proving in the Era of Reasoning Models
- PatternBoost: Constructions in Mathematics with a Little Help from AI
- Seed-Prover: Deep and Broad Reasoning for Automated Theorem Proving
- Towards Reasoning Era: A Survey of Long Chain-of-Thought for Reasoning Large Language Models
- Gemini 2.5: Pushing the Frontier with Advanced Reasoning, Multimodality, Long Context, and Next Generation Agentic Capabilities
- STP: Self-play LLM Theorem Provers with Iterative Conjecturing and Proving
- Reinforcement learning for graph theory, I. Reimplementation of Wagner's approach
- Reinforcement learning for graph theory, II. Small Ramsey numbers
- DeepSeek-R1: Incentivizing Reasoning Capability in LLMs via Reinforcement Learning
- Dealing with Sparse Rewards in Reinforcement Learning
- MUSTARD: Mastering Uniform Synthesis of Theorem and Proof Data
- Leanabell-Prover-V2: Verifier-integrated Reasoning for Formal Theorem Proving via Reinforcement Learning
- Draft, Sketch, and Prove: Guiding Formal Theorem Provers with Informal Proofs
- LeanReasoner: Boosting Complex Logical Reasoning with Lean
- Adam: A Method for Stochastic Optimization
- A Survey on Deep Learning for Theorem Proving
- Goedel-Prover: A Frontier Model for Open-Source Automated Theorem Proving
The paper
Learning to Disprove: Formal Counterexample Generation with Large Language Models · Read on arXiv
Zenan Li, Zhaoyu Li, Kaiyu Yang, Xiaoxing Ma, Zhendong Su
ETH Zurich · University of Toronto · MiroMind · Nanjing University
Mathematical reasoning demands two critical, complementary skills: constructing rigorous proofs for true statements and discovering counterexamples that disprove false ones. However, current AI efforts in mathematics focus almost exclusively on proof construction, often neglecting the equally important task of finding counterexamples. In this paper, we address this gap by fine-tuning large language models (LLMs) to reason about and generate counterexamples. We formalize this task as formal counterexample generation, which requires LLMs not only to propose candidate counterexamples but also to produce formal proofs that can be automatically verified in the Lean 4 theorem prover. To enable effective learning, we introduce a symbolic mutation strategy that constructs candidate counterexample-generation tasks by systematically extracting theorems and removing selected hypotheses. Together with curated datasets, this strategy enables a multi-reward expert iteration framework that substantially enhances both the effectiveness and efficiency of training LLMs for counterexample generation and theorem proving. Experiments on three newly collected benchmarks validate the advantages of our approach, showing that the mutation strategy and training framework yield substantial performance gains.
Transcript
Introduction to the show: ident: AI Radio. Generated commentary on the latest Artificial Intelligence papers.
Tom: I'm Tom.
Jane: And I'm Jane, here with Lu, Meng and our in-house large language model, Lalam.
Tom: Today's paper: "Learning to Disprove".
Jane: The gist The paper addresses the gap in mathematical reasoning AI by fine-tuning large language models to generate formal counterexamples,
Tom: First, who's behind it and why it matters.
Title and authors: Tom: The paper's title itself, "Learning to Disprove: Formal Counterexample Generation with Large Language Models," sets the stage for what they are doing. It’s not just about generating random math problems; it’s specifically about learning to disprove statements formally.
Jane: And the authors are Zhaoyu Li, Kaiyu Yang, Xiaoxing Ma, and Zhendong Su from ETH Zurich and University of Toronto >
Tom: They are focusing on formal counterexample generation as a task for large language models, which means the AI has to do two things: propose a counterexample and then produce a formal proof that can be verified by the Lean four theorem prover <ref:2603.19514#pg1,the Lean 4 theorem prover>.
Lu: The implication here is that they move beyond just proof construction, which is what most current AI efforts in math focus on >
Meng: It’s about creating an AI that can actually check its own work by finding things that contradict its initial assumptions >
Jane: So, the summary of this paper explains how they do this by using a symbolic mutation strategy to synthesize training data and then employing a multi-reward guided training scheme >
The paper's summary: Tom: Let’s unpack that a bit more. They use symbolic mutation to create diverse training data by systematically extracting theorems and discarding selected hypotheses, which they call theorem mutated version: ∃ x: X, H2 x → C x:= by sorry theorem original version (x: X): H1 x → H2 x → C x:= by proof (correct) >
Jane: So they take a theorem and drop one of the hypotheses, like discarding H1, to create a new problem that needs to be solved >
Lu: And then for the expert stage, they introduce two rewards. One reward is based on whether the generated counterexample can prove the mutated version with dropped hypothesis >
Meng: The other reward checks if it proves both the necessary condition ¬H1(x*) and the target theorem H2(x*) → C(x*) >
Jane: So they combine those two rewards as a final sample weight for supervised fine-tuning, which is how they guide the model to find these counterexamples effectively >
Tom: It’s a structured way to train the LLM to not just guess, but to actively search for instances that disprove the original theorem's claim >
The paper's improvements: Tom: Now let's look at what they suggest are the improvements over existing methods. They tackle two big problems right away: a severe scarcity of training data and exceptionally sparse reward signals during training >
Jane: To handle the data scarcity, they use that symbolic mutation strategy to synthesize a large-sized unlabeled dataset, even beyond what is already available in datasets like CounterMath >
Lu: And to fix the sparse reward problem, they use a multi-reward strategy where the reward remains valid even when LLMs solve hard problems >
Meng: They also mention techniques like reducing the sample weight of the first formal proof and using group relative policy optimization to encourage longer formal proofs instead of just short ones >
Jane: So they’re addressing both sides: making sure they have enough data and making sure the learning signal is strong enough when things get difficult >
Conclusion: Tom: So to wrap up, this paper shows that combining symbolic mutation with a multi-reward scheme successfully addresses data scarcity and sparse reward signals >
Jane: The results show a relative improvement of forty-seven percent to seventy-four percent in the pass@one success rate compared to the strongest baseline on three newly collected benchmarks >
Lu: It confirms that this integrated approach yields significant performance gains across counterexample search, verification of autoformalized results, and reasoning steps >
Meng: For deployment, it suggests that this framework provides a practical copilot for validating mathematical conjectures, which is useful when you need to check a conjecture before committing resources >
Lalam: I’m pretty sure the core implication here is moving towards enhancing self-reflective reasoning capabilities in LLMs, giving them the ability to self-verify their logical processes >
Tom: It gives them a way to engage in a guess-and-check paradigm for mathematical discovery, which is really interesting for how we think about AI reliability >
Jane: So, the paper "Learning to Disprove: Formal Counterexample Generation with Large Language Models" provides a promising direction for making LLMs more self-corrective and reliable when dealing with formal logic.
More episodes
- 2606.11245-Position: Hippocampal Explicit Memory Is the Cornerstone for AGI
- 2311.04902-Beyond Size: How Gradients Shape Pruning Decisions in Large Language Models
- 2505.20085-Explanation User Interfaces: A Systematic Literature Review
- 2507.12145-PRISM: Distributed Inference for Foundation Models at Edge
- 2507.14843-The Invisible Leash: Why RLVR May or May Not Escape Its Origin
- 2509.18369-Align Where the Words Look: Cross-Attention-Guided Patch Alignment with Contrastive and Transport Regularization for Bengali Captioning
- 2509.21193-Eigen-Agent: Adaptive Multi-Agent Scientific Reasoning with Monitor-Based RAG
- 2509.23209-Context Value Informed In-Context Reinforcement Learning
- 2510.13928-LLMs Can Get "Brain Rot": A Pilot Study on Twitter/X
- 2511.08860-When is a System Discoverable from Data? Discovery Requires Chaos