Large language models improved at finding false math conjectures
Counterexample Generation via Per-Theorem Symbolic Verifiers: When Imitation Hurts and Reinforcement Repairs
Computation and LanguageArtificial Intelligence
Summary
Large language models often prove true math statements but struggle to find counterexamples that disprove false but similar ones. The authors create a dataset of false math conjectures paired with exact Python verifiers that check the answers. They train models using a mix of imitation and reinforcement learning to better find counterexamples, fixing an issue where imitation learning alone made the models worse. Their improved models outperform bigger open-source math models and match commercial APIs on various math problems.
What this means in practice
- •For software engineers: Use precise symbolic verifiers with language models to detect and fix false claims in mathematical software or automated reasoning tools.
- •For automated theorem proving developers: Improve counterexample generation in theorem provers by combining symbolic verification with reinforcement learning techniques trained on verified false conjectures.
Authors
Omar Farouk Zouak, Houssam Eddine Boukhalfa, Soumaya Lakehal, Shiv Katiyar, Samia Nefti-Meziani
Abstract
Large language models often solve a theorem forward yet fail to disprove a closely related false one: a falsification gap that supervised fine-tuning does not close and can actively worsen. We frame counterexample generation as constrained witness emission against a deterministic per-theorem Python verifier, and release SymCE, a corpus of 4,707 false undergraduate-algebra and real-analysis conjectures, each paired with executable verifiers. The verifier also serves as the reward function, making SymCE a training environment. Training Qwen3-4B with SFT followed by GRPO under this oracle reveals an imitation trap: counterexample-only SFT collapses true-theorem recognition from 0.27 to 0.00, while RLVR with a sparse outcome-only reward repairs this and exceeds the base, to 0.66. The collapse replicates across four seeds and on Gemma-3-4B. Sparse and dense rewards yield statistically indistinguishable in-domain success yet diverge by 33 points on a held-out calibration probe, a dissociation we trace to the partial-credit term. Our 4B model outperforms every evaluated 7B open-weights math specialist, remains competitive with six frontier commercial APIs, and transfers under unchanged prompting to GSM8K, MATH-500 and MMLU-college-math. A human audit of 177 verifier decisions finds 97.7% accuracy. Code, data, verifier modules and annotations: https://github.com/ce-rlvr/SymCE.