学会反驳：用大语言模型进行形式化反例生成

数学推理需要两项关键且互补的能力：为真命题构造严谨的证明，以及发现能驳倒假命题的反例。然而，当前AI在数学方面的努力几乎完全聚焦于证明构造，往往忽视了同样重要的寻找反例任务。本文通过微调大语言模型（LLM）来推理并生成反例，以填补这一空白。我们将该任务形式化为形式化反例生成，要求LLM不仅提出候选反例，还要产出可在Lean 4定理证明器中自动验证的形式化证明。为实现有效学习，我们引入一种符号变异策略，通过系统地抽取定理并舍弃选定的假设来合成多样的训练数据，从而产生多样的反例实例。该策略与精选数据集相结合，支撑起一个多奖励专家迭代框架，显著提升了训练LLM进行反例生成与定理证明的效果与效率。在三个新收集的基准上的实验验证了本方法的优势，表明变异策略与训练框架带来了显著的性能提升。