在形式化数学推理领域，反例生成长期处于被忽视的角落。

Valeron83enved

[AI]《Learning to Disprove: Formal Counterexample Generation with Large Language Models》Z Li, Z Li, K Yang, X Ma… [ETH Zurich & University of Toronto & MiroMind] (2026)


在形式化数学推理领域，反例生成长期处于被忽视的角落。现有AI系统几乎专注于定理证明，而反例——那个能在一秒内摧毁一个普遍猜想的具体实例——既缺乏专门的训练数据，又面临稀疏奖励陷阱：模型在难题上失败时，梯度信号彻底消失，训练陷入低成功率的死循环。

本文的核心洞见是：把"寻找反例"重新看作"删除定理的一个假设"。一个可证定理去掉必要前提，立刻生成一个有效的反例问题——这一符号变异操作从32万条种子定理中批量合成了57万条训练样本。同时，被删除的假设本身构成一个更简单的子目标，为难题提供了"部分奖励"的缓冲层，使训练信号在模型尚无法攻克完整问题时仍能保持激活。

这项工作真正留下的遗产是：将反例生成从自然语言猜测提升为可被定理证明器自动核验的形式化任务，并为此建立了完整的数据合成与训练范式。它为后来者打开的新门是：LLM的自我验证与自我纠错能力可以通过"证伪"而非"证明"来系统性培养。但尚未跨过的门槛是：57万条合成数据中存在大量冗余，模型在不足半个epoch时便已收敛；7B规模的模型在简单计算上仍频繁出错，数据质量筛选与更大规模模型的验证均悬而未决。

arxiv.org/abs/2603.19514

##