Learning to Disprove: Formal Counterexample Generation with Large Language Models

• URL: http://arxiv.org/abs/2603.19514v1
• Date: Thu, 19 Mar 2026 22:42:49 GMT
• Title: Learning to Disprove: Formal Counterexample Generation with Large Language Models
• Abstract summary: Current AI efforts in mathematics focus almost exclusively on proof construction.<n>We formalize this task as formal counterexample generation.<n>We introduce a symbolic mutation strategy that synthesizes diverse training data.
• Score: 26.262810717227108
• License: http://creativecommons.org/licenses/by/4.0/
• 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.

Related papers

• INSPIRE: An Internalize-Then-Improve Approach for Example-Driven Mathematical Reasoning [61.60016491769943]
  In human mathematics education, example-based reasoning such as constructing counterexamples to test theorem boundaries reflects deep conceptual understanding.<n>We propose INSPIRE, an Internalize-Then-Improve approach combining Reference-Guided Student Internalization (RGSI) with a stage-wise preference training strategy.<n>Experiments across multiple model scales and families demonstrate consistent improvements, even surpassing larger open-source models.
  arXiv  Detail & Related papers  (2026-08-27T03:24:03Z)
• Counterexample Guided Learning in the Large using Reasoning Agents [15.424030391880677]
  We show that verifier feedback substantially improves sample efficiency on challenging-induction tasks, reducing the number of labeled examples required and enabling learning of complex target expressions where standard prompting fails.<n>These results suggest that LLMs can benefit from rich feedback beyond treating it as additional data, opening the door for robust verifier-guided methods for LLM-based program synthesis and formal reasoning.
  arXiv  Detail & Related papers  (2026-06-09T23:46:46Z)
• Learning to Reason with Insight for Informal Theorem Proving [50.054221663394195]
  In this work, we identify a primary bottleneck in informal theorem proving as a lack of insight.<n>We propose a novel framework designed to cultivate this essential reasoning skill and enable LLMs to perform insightful reasoning.<n>Our experiments on challenging mathematical benchmarks demonstrate that this insight-aware generation strategy significantly outperforms baselines.
  arXiv  Detail & Related papers  (2026-04-17T17:36:21Z)
• Learning from Equivalence Queries, Revisited [62.46207559138802]
  We study learning from equivalence queries under both full-information and bandit feedback.<n>Our analysis combines a game-theoretic view of symmetric adversaries with adaptive weighting methods and minimax arguments.
  arXiv  Detail & Related papers  (2026-04-06T08:55:41Z)
• ExVerus: Verus Proof Repair via Counterexample Reasoning [8.819482630789217]
  We present EXVERUS, a counterexample-guided framework for large language models (LLMs)<n>When a proof fails, EXVERUS automatically generates and validates counterexamples, and then guides the LLM to generalize them into inductive invariants to block these failures.<n>Our evaluation shows that EXVERUS significantly improves proof accuracy, robustness, and token efficiency over the state-of-the-art prompting-based Verus proof generator.
  arXiv  Detail & Related papers  (2026-03-26T18:14:34Z)
• LeanConjecturer: Automatic Generation of Mathematical Conjectures for Theorem Proving [6.220998637943786]
  We introduce LeanConjecturer, a pipeline for automatically generating university-level mathematical conjectures in Lean 4 using Large Language Models (LLMs)<n>Through iterative generation and evaluation, LeanConjecturer produced 12,289 conjectures from 40 Mathlib seed files, with 3,776 identified as syntactically valid and non-trivial.
  arXiv  Detail & Related papers  (2025-06-27T08:17:18Z)
• DeepTheorem: Advancing LLM Reasoning for Theorem Proving Through Natural Language and Reinforcement Learning [67.93945726549289]
  DeepTheorem is a comprehensive informal theorem-proving framework exploiting natural language to enhance mathematical reasoning.<n>DeepTheorem includes a large-scale benchmark dataset consisting of 121K high-quality IMO-level informal theorems and proofs.<n>We devise a novel reinforcement learning strategy (RL-Zero) explicitly tailored to informal theorem proving, leveraging the verified theorem variants to incentivize robust mathematical inference.
  arXiv  Detail & Related papers  (2025-05-29T17:59:39Z)
• Steering LLMs for Formal Theorem Proving [1.083373217040891]
  We develop an inference-time intervention that identifies linear directions in residual activations associated with informal reasoning traces.<n>This mechanism also yields interpretable information about how reasoning is internally encoded in the activation space of Large Language Models.<n>Our contributions are twofold: (1) a novel activation-based intervention for guiding proof synthesis in LLMs; and (2) demonstration that this intervention improves performance under two decoding strategies.
  arXiv  Detail & Related papers  (2025-02-21T15:04:48Z)
• One Example Shown, Many Concepts Known! Counterexample-Driven Conceptual Reasoning in Mathematical LLMs [75.95179490687018]
  Leveraging mathematical Large Language Models for proof generation is a fundamental topic in LLMs research.<n>We argue that the ability of current LLMs to prove statements largely depends on whether they have encountered the relevant proof process during training.<n>Inspired by the pedagogical method of "proof by counterexamples" commonly used in human mathematics education, our work aims to enhance LLMs' ability to conduct mathematical reasoning and proof through counterexamples.
  arXiv  Detail & Related papers  (2025-02-12T02:01:10Z)
• Lean-STaR: Learning to Interleave Thinking and Proving [53.923617816215774]
  We present Lean-STaR, a framework for training language models to produce informal thoughts prior to each step of a proof.<n>Lean-STaR achieves state-of-the-art results on the miniF2F-test benchmark within the Lean theorem proving environment.
  arXiv  Detail & Related papers  (2024-07-14T01:43:07Z)
• A Critical Analysis of the Theoretical Framework of the Extreme Learning Machine [1.9503475832401784]
  We refute the proofs of two main statements and a dataset that provides a counterexample to the ELM learning algorithm. We provide alternative statements of the foundations, which justify the efficiency of ELM in some theoretical cases.
  arXiv  Detail & Related papers  (2024-06-25T10:06:07Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.