Learning to Disprove: Formal Counterexample Generation with Large Language Models

TL;DR

This paper introduces a method for training large language models to generate formal counterexamples in mathematics, complementing proof generation and improving AI reasoning capabilities.

Contribution

It presents a novel approach combining symbolic mutation and multi-reward training to enhance LLMs in formal counterexample generation and theorem proving.

Findings

Significant performance improvements on three benchmarks.

Effective data synthesis via symbolic mutation.

Enhanced training framework for counterexample generation.

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.