Learning to Disprove: Formal Counterexample Generation with Large Language Models

Each language version is independently generated for its own context, not a direct translation.

这篇论文讲述了一个关于如何让 AI 学会“找茬”（即寻找反例）的故事。

在数学世界里，AI 通常被训练成“证明者”：给它一个题目，它努力证明这个题目是对的。但这就像只教学生做“填空题”，却从不教他们如何发现题目本身可能是错的。这篇论文的核心就是：教 AI 学会说“不”，并找出那个让题目失效的具体例子（反例）。

为了让你更容易理解，我们可以用几个生动的比喻来拆解这项研究：

1. 核心问题：AI 只会“顺从”，不会“质疑”

想象一下，你有一个非常聪明的学生（AI），老师（数学家）给他一个命题：“所有的天鹅都是白色的”。

以前的 AI：会拼命找证据，试图证明“是的，所有天鹅都是白的”，哪怕它心里隐约觉得不对劲。它只会做“证明题”。
现在的挑战：如果命题其实是错的（比如存在黑天鹅），AI 需要能立刻跳出来大喊：“不对！看，这里有一只黑天鹅！”这就是反例。
痛点：以前的 AI 很难做到这一点，因为：
1. 没教材：市面上几乎没有专门教 AI 怎么找反例的练习题（数据太少）。
2. 没反馈：如果 AI 找错了，它不知道错在哪，就像在黑暗中摸索，很难进步。

2. 解决方案：给 AI 造一个“反例工厂”

为了解决“没教材”的问题，作者发明了一种**“符号突变”策略**。这就像是一个**“拆墙游戏”**：

原来的定理：就像一堵坚固的墙，由几块砖（假设条件）支撑着，墙顶是结论。
- 例子：如果“下雨”且“没带伞”，那么“你会淋湿”。
突变操作：AI 把其中一块关键的砖（比如“没带伞”）偷偷抽走。
- 新命题：如果“下雨”，那么“你会淋湿”。
结果：这堵墙塌了！因为如果下雨但你带了伞，你就不会淋湿。这个“带了伞”的情况，就是反例。

通过这种“抽走一块砖”的方法，作者从现有的数学库中“变异”出了57.5 万个新的反例题目。这相当于给 AI 建了一个巨大的、自动生成的“找茬训练场”。

3. 训练方法：双重奖励机制（“双保险”）

为了解决“没反馈”的问题，作者设计了一套**“双奖励”**系统，让 AI 在找反例时更有动力。

想象 AI 在做一个侦探游戏：

任务 A（找反例）：AI 提出一个具体的例子（比如“带了伞的人”）。
任务 B（双重验证）：
- 奖励 1：AI 必须证明这个例子确实推翻了原来的结论（证明“带了伞不会淋湿”）。
- 奖励 2：AI 必须证明这个例子同时也推翻了被抽走的那块砖（证明“带了伞”是存在的，即原命题中“没带伞”这个条件是多余的或错误的）。

为什么这样设计？
如果 AI 只盯着最难的任务（推翻结论），它很容易失败，导致没有奖励，训练就卡住了。但通过引入第二个任务（证明被抽走的条件），即使 AI 没能完美解决最难的数学题，只要它能证明“那个被抽走的条件确实不成立”，它也能得到一部分奖励。这就像**“只要你能指出老师哪里讲错了，哪怕你没完全解出难题，老师也给你加分”**。这让 AI 在困难面前也能持续学习，不会轻易放弃。

4. 工作流程：从“猜”到“证”

整个训练过程分为两步走，就像**“先拍脑袋，再写论文”**：

直觉猜测（非形式化推理）：AI 先用自然语言（像人说话一样）想出一个具体的反例。比如：“我想到了一个带伞的人。”
严谨证明（形式化证明）：AI 把这个想法写成严格的数学代码（Lean 4 语言），让计算机严格检查这个反例是否真的成立。

只有当计算机（定理证明器）说“通过”时，这个反例才算数，AI 才能获得奖励并升级。

5. 成果：AI 变得更聪明了

实验结果显示，经过这种“找茬训练”的 AI，表现远超其他模型：

找错能力：在三个新的测试集上，它找对反例的成功率比最强的竞争对手提高了 47% 到 74%。
自我纠错：它不仅学会了找错，还能帮助检查其他 AI 生成的数学证明是否有漏洞。

总结

这篇论文就像给 AI 装上了一副**“批判性思维眼镜”。
以前，AI 像个只会点头的“乖学生”，只会顺着题目做证明；
现在，通过“拆墙游戏”（数据合成）和“双保险奖励”（多奖励训练），AI 变成了一个“敏锐的侦探”**，不仅能证明真理，更能敏锐地发现谬误，指出哪里出了问题。

这对于数学研究和 AI 的安全可靠性来说，是一个巨大的进步——因为发现错误，往往比证明正确更重要。

Each language version is independently generated for its own context, not a direct translation.

这是一篇关于利用大型语言模型（LLM）进行**形式化反例生成（Formal Counterexample Generation）**的预印本论文。论文针对当前数学推理 AI 研究过度侧重于“证明真命题”而忽视“证伪假命题”的痛点，提出了一套完整的训练框架。

以下是该论文的详细技术总结：

1. 研究背景与问题 (Problem)

核心痛点：数学推理包含两个互补技能：构建严谨证明（针对真命题）和发现反例（针对假命题）。现有的 AI 数学研究几乎完全集中在证明构建上，忽视了反例发现。
现有挑战：
1. 数据稀缺：专门用于反例生成的训练数据极少（目前仅有 CounterMath 数据集，仅包含约 1,200 个自然语言问题），不足以支撑 LLM 的微调。
2. 奖励信号稀疏：在强化学习或专家迭代中，如果模型无法解决复杂问题，奖励信号会消失（Sparse Reward），导致模型训练陷入低成功率的平台期。
3. 验证困难：反例生成需要模型不仅提出候选反例，还要提供可在定理证明器（如 Lean 4）中自动验证的形式化证明。

2. 方法论 (Methodology)

论文提出了一个集成框架，包含两个主要阶段：符号突变数据合成和多奖励引导训练。

2.1 符号突变策略 (Symbolic Mutation Strategy) - 数据合成

为了解决数据稀缺问题，作者设计了一种从可证明定理中自动生成反例问题的方法：

输入：收集大量形式化定理（来自 Mathlib, Leanworkbook 等），这些定理通常具有全称量词形式（ $\forall x, H_1(x) \land H_2(x) \to C(x)$ ）。
突变过程：
1. 利用 Lean 4 定理证明器分析原定理的证明过程，识别并剔除一个必要假设（例如 $H_1$ ）。
2. 生成突变版本（Mutated Version）：移除 $H_1$ 后，原定理变为假命题（ $\exists x, H_2(x) \to C(x)$ 不再成立，或者更准确地说是寻找 $x$ 使得 $H_2(x) \to C(x)$ 为假，即寻找反例）。
3. 生成被丢弃假设版本（Dropped Hypothesis）：构造一个新定理证明被丢弃的假设 $H_1$ 对于该反例是不成立的（ $\exists x, \neg H_1(x)$ ）。
产出：通过此策略，从约 32 万个种子定理中生成了 57.5 万 个反例问题实例，极大地丰富了训练数据。

2.2 多奖励引导训练 (Multi-Reward Guided Training) - 专家迭代

为了解决奖励稀疏问题，作者设计了一种双奖励机制，结合专家迭代（Expert Iteration）框架：

双模型架构：
- $q_\phi$ ：负责非形式化推理，提出具体的反例候选（如具体的数值或函数）。
- $q_\psi$ ：负责形式化推理，基于候选反例生成 Lean 4 形式化证明。
多奖励机制：
对于生成的反例 $x^*$ $x^{*}$ ，计算两个独立的奖励信号：
1. 目标奖励 ( $r_M$ )：验证 $x^*$ 是否成功证明了突变后的定理（即证明原命题为假）。
2. 必要条件奖励 ( $r_H$ )：验证 $x^*$ 是否证明了被丢弃的假设不成立（即 $\neg H_1(x^*)$ ）。
- 优势：即使模型未能完全证明复杂的突变定理，只要它能证明被丢弃的假设不成立（这通常更容易），也能获得部分奖励。这有效缓解了稀疏奖励问题，引导模型逐步学习。
训练流程：
1. 大规模推理：模型生成反例和证明。
2. 验证与评分：Lean 4 验证器验证证明，根据双奖励计算样本权重。
3. 监督微调（SFT）：使用加权数据集更新模型。

3. 关键贡献 (Key Contributions)

任务定义：首次将“形式化反例生成”定义为需要同时提供非形式化推理和可自动验证的形式化证明的任务。
数据合成方法：提出了一种基于符号突变的自动化数据合成策略，成功构建了大规模（57.5K+）的高质量反例训练数据集。
训练框架：设计了多奖励专家迭代框架，通过双奖励机制解决了反例生成任务中奖励稀疏的难题，显著提升了训练效率和模型性能。
基准测试：建立了三个新的基准测试（FOR-COUNTER, VERI-REASON, VERI-FORMALIZE），涵盖了反例搜索、自动形式化结果验证和推理步骤验证。

4. 实验结果 (Results)

数据合成效率：突变策略在多个数据源上实现了 1.65 到 2.48 的突变率，且平均执行时间极短（0.3-0.71 秒/定理）。
训练效果：
- 与单奖励训练相比，多奖励训练收敛更快，最终 Pass@1 成功率提升了约 6%（从 43% 提升至 49%）。
基准测试表现：
- 在三个基准测试上，微调后的模型（Ours）显著优于现有的 SOTA 模型（包括专有模型如 GPT-4.1, DeepSeek-R1 和开源证明器如 Leanabell, Goedel-prover）。
- 具体提升：在 Pass@1 指标上，相比最强基线，模型在三个基准上分别多解决了 95、69、63 个问题，相对提升幅度达到 47% 到 74%。
- 开源神经证明器表现优于专有通用推理模型，而本文微调模型进一步刷新了 SOTA。

5. 意义与影响 (Significance)

提升推理可靠性：赋予模型“自我验证”和“自我纠错”的能力。通过寻找反例，模型可以反思其逻辑过程，增强推理的鲁棒性。
辅助数学研究：为数学猜想验证提供了实用的 Copilot 工具，帮助数学家快速发现潜在的错误猜想。
方法论创新：证明了通过符号突变生成合成数据结合多奖励机制，可以有效解决形式化推理中数据稀缺和奖励稀疏的共性难题，为未来的数学 AI 研究提供了新的范式。

6. 局限性 (Limitations)

合成数据质量：虽然数据量大，但部分生成数据可能存在冗余或质量不高，导致训练效率在后期下降（约半个 epoch 后收敛）。
模型规模限制：受限于计算资源，实验主要使用 7B-8B 参数量的模型。较小的模型在复杂计算和遵循指令方面存在不足，限制了框架的上限。

总结：该论文通过“符号突变”解决数据问题，通过“多奖励机制”解决训练信号问题，成功训练出了在形式化反例生成任务上表现卓越的 LLM，填补了 AI 数学推理中“证伪”能力的空白。