Learning to Disprove: Formal Counterexample Generation with Large Language Models

Abstract

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 synthesizes diverse training data by systematically extracting theorems and discarding selected hypotheses, thereby producing diverse counterexample instances. 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 significant performance gains.

Figures (5)

• Figure 1: Framework of counterexample training. In the data synthesis stage, the symbolic mutation drops the hypothesis of a provable theorem, creating new counterexample problems. In the subsequent expert stage, two rewards are introduced based on whether the generated counterexample can prove the mutated version and dropped hypothesis, boosting training effectiveness and efficiency.
• Figure 2: Task of formal counterexample generation. This task requires the LLM first to perform informal reasoning to identify a valid counterexample for the given problem, and then generate the corresponding formal proof, which is automatically verified by theorem provers (e.g., Lean 4).
• Figure 3: Pass@k ($k=1,4,9$) rate curves on the validation set. Compared with the single-reward baseline, multi-reward training converges faster and yields superior final performance.
• Figure 4: An instantiation of our counterexample training framework. The original theorem shown is an intermediate subgoal extracted from DSP+’s proof of AIME-II 2001 Problem 3 in miniF2F.
• Figure 5: Pass@k curves of five neural theorem provers. The results are derived from the evaluation of For-Counter and show that the performance nearly converges when $k=10$.