Learning to Disprove: Formal Counterexample Generation with Large Language Models

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 producing formal proofs verifiable by theorem provers.

How it works

The proposed framework integrates a symbolic mutation strategy for generating vast amounts of training data with a multi-reward guided training scheme to enhance model performance and efficiency. The core idea is to move beyond focusing solely on proof construction by equipping models with the ability to find counterexamples, which is vital for self-verification of logical processes.

The training process involves two main stages:

1. Counterexample problem synthesis. This stage focuses on creating a large-sized unlabeled dataset by applying a mutation strategy to formally provable theorems. The mutation involves discarding one of the hypotheses of a theorem, such as transforming theorem original version into theorem mutated version: ∃ x: X, H2 x → C x. This process is rigorously guided by using the Lean 4 theorem prover to analyze the formal proof and identify redundant hypotheses.

2. Multi-reward guided training. This stage employs an expert iteration pipeline where the LLM repeatedly generates counterexamples and formal proofs. The reward signal is multi-reward based, where a valid counterexample should contradict the removed hypothesis, leading to two distinct rewards: one based on whether x∗ proves the necessary condition ¬H1(x∗), and another based on whether it proves the target theorem H2(x∗) → C(x∗). These two rewards are combined as the final sample weight for supervised fine-tuning.

Key Components and Challenges

The paper identifies two significant challenges in this task: a severe scarcity of training data and exceptionally sparse reward signals during training. The existing dataset, CounterMath (Li et al., 2025), is too limited for practical LLM training.

To address the sparse reward problem, the multi-reward strategy ensures that the reward remains valid even when LLMs solve hard problems. Furthermore, to mitigate issues where formal reasoning models might fall into a low-difficulty trap by generating shorter proofs, the sample weight of the first formal proof is reduced, and techniques like group relative policy optimization (GRPO) can be employed to encourage longer formal proofs.

Experimental Results

Experiments on three newly collected benchmarks validate the advantages of the proposed approach. Leveraging the mutation strategy, 575K counterexample data points were synthesized for fine-tuning. The results show that the fine-tuned model achieves a relative improvement of 47% to 74% in pass@1 success rate compared to the strongest baseline.

The performance comparison across different models is summarized in Table 2, where the fine-tuned model substantially outperforms existing state-of-the-art LLMs by a large margin. For instance, for pass@1 on the FOR-COUNTER benchmark, our model solves 222 problems compared to 63 for the strongest baseline.

Conclusion

The proposed framework successfully addresses data scarcity and sparse reward signals by combining symbolic mutation with a multi-reward scheme. Experiments demonstrate that this integrated approach yields significant performance gains in counterexample generation, verification of autoformalized results, and reasoning steps. The work establishes a promising direction for enhancing the self-reflective and self-corrective reasoning capabilities of LLMs. The framework provides a practical copilot for validating mathematical conjectures.

Limitations

Several limitations remain, including the data quality of synthetic data, as generated data often lacks careful selection which downgrades training efficiency. Additionally, the limited capability of the LLMs significantly compromises performance when using smaller models like 7B. These limitations are noted for future work and further investigation.

References

The paper cites numerous works related to mathematical reasoning LLMs, formal theorem proving tools like Lean 4, and reinforcement learning techniques such as GRPO. It also references foundational concepts in computer science and mathematics relevant to the task. The paper's methodology draws connections to existing work on neural theorem proving and formal data synthesis methods. The authors acknowledge the need for sequential informal-to-formal reasoning in this paradigm. The paper's experimental setup details the use of specific LLMs and verification tools like lean-repl. The authors also reference related concepts such as autoformalization and various benchmarks in the field. The paper's ethical statement confirms no human subjects or sensitive data were involved. The reproducibility statement provides a link to the source code. The references section lists foundational texts and recent papers in the domain. The paper explicitly discusses the difference between informal-to-formal reasoning and other methods. The authors also reference specific LLM models used in the experiments. The paper's evaluation relies on established metrics like pass@k rates. The authors also reference the work of various researchers in the field of mathematical reasoning LLMs.

1. Bold header: Symbolic mutation strategy for data synthesis

This strategy systematically extracts theorems and discarding selected hypotheses, thereby producing diverse counterexample instances, which significantly enriches the dataset beyond existing curated collections. This allows LLMs to be trained on a much larger and more diverse set of problem instances.

2. Bold header: Multi-reward guided training framework

The introduction of a multi-reward function based on the proven success rate of both the extracted problem and discarded hypothesis ensures that the reward remains valid even when LLMs solve hard problems, overcoming the issue where the training reward vanishes. This leads to a model that is more robust and learns from difficult examples.

3. Bold header: Two-stage informal-to-formal reasoning pipeline

The system implements a sequential pattern of informal-to-formal reasoning, where the LLM first proposes a counterexample and then generates formal proofs for both the mutated and dropped hypothesis theorems. This structure is crucial for establishing a two-stage, informal-to-formal process that differs from methods where informal and formal reasoning are congruent.

4. Bold header: Improved performance on specialized tasks

The fine-tuned model achieves significant improvements across three applicable tasks: counterexample search, verification of autoformalized results, and verification of reasoning steps. This demonstrates the system's ability to not only find counterexamples but also to verify complex logical processes automatically.

5. Bold header: Enhanced self-reflective reasoning capabilities

By training LLMs on counterexample generation, the framework aims to equip models with the ability to self-verify their logical processes, thereby strengthening both their reasoning reliability and explanatory power. This enables LLMs to engage in a guess-and-check paradigm for mathematical discovery.

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.