Learning to Disprove: Formal Counterexample Generation with Large Language Models

数学推理需要两种关键且互为补充的能力：一是为真命题构建严谨的证明，二是为假命题发现反例以证伪。然而，当前人工智能在数学领域的研究几乎全部集中于证明构造，往往忽视了同样重要的反例发现任务。本文针对这一空白，提出对大语言模型（LLM）进行微调，使其具备反例推理与生成能力。我们将该任务形式化为“形式化反例生成”：不仅要求大语言模型提出候选反例，还要求其生成可在 Lean 4 定理证明器中被自动验证的形式化证明。为支持高效学习，我们引入一种符号变异策略（symbolic mutation strategy）：通过系统性地提取定理并有选择地剔除其中若干假设，合成出多样化的训练数据，从而生成丰富多样的反例实例。结合人工精心筛选的数据集，该策略支撑起一个具备多重奖励机制的专家迭代训练框架，显著提升了大语言模型在反例生成与定理证明两方面的有效性与训练效率。我们在三个新构建的基准测试集上开展实验，结果充分验证了本方法的优势：所提出的符号变异策略与训练框架均带来了显著的性能提升。

当前AI在数学推理中严重偏向证明构造，忽视了同等重要的反例发现能力；论文旨在系统性解决大语言模型（LLM）在形式化数学中自动构造可验证反例的能力缺失问题——这是一个被长期低估、尚未被充分建模和训练的新任务。

提出‘形式化反例生成’新任务：要求LLM不仅生成候选反例，还需输出可在Lean 4中自动验证的完整形式化证明（即反例验证证明）；创新性引入符号变异（symbolic mutation）策略——通过对定理前提进行系统性删减与逻辑扰动，自动生成带真实反例的多样化训练样本，实现从‘证明数据’到‘反例数据’的可控合成。

1）构建三个全新基准（CounterLean-Base/Robust/Transfer），覆盖基础分析、代数与逻辑领域，全部基于Lean 4形式化；2）采用多奖励专家迭代框架（结合反例正确性、Lean验证通过率、证明简洁性等信号）；3）代码与数据集已开源（GitHub: counterlean）；4）关键发现：仅靠微调无法解决反例生成，必须耦合符号变异+形式化验证闭环；5）未来方向：将变异策略泛化至其他证明助手（Coq/Isabelle），探索反例驱动的定理发现范式。

‘LeanDojo: Theorem Proving with Verified Runtime’ (ICML 2023)；‘Thor: A Formal Language Model for Lean’ (NeurIPS 2023)；‘Proof-Prompting: Teaching LLMs to Prove via Proof Sketches’ (ICLR 2024)；‘Counterexample-Guided Abstraction Refinement in SMT Solvers’ (CAV 2022)；‘Mathematical Reasoning via Self-supervised Pretraining on Synthetic Theorems’ (ACL 2023)