📄 中文摘要
数学推理需要两项关键的互补技能：为真命题构建严格的证明和发现反例以驳斥假命题。然而，目前的人工智能在数学领域的努力几乎完全专注于证明构建，往往忽视了寻找反例这一同样重要的任务。为填补这一空白，研究通过微调大型语言模型（LLMs）来进行反例推理和生成。该任务被形式化为形式反例生成，要求LLMs不仅提出候选反例，还需生成可以在Lean 4定理证明器中自动验证的正式证明。为实现有效学习，研究引入了一种符号变异策略，旨在提升反例生成的质量和效率。
学习反驳：利用大型语言模型生成形式化反例
📄 English Summary
Learning to Disprove: Formal Counterexample Generation with Large Language Models
Mathematical reasoning requires two critical, complementary skills: constructing rigorous proofs for true statements and discovering counterexamples that disprove false ones. Current AI efforts in mathematics predominantly focus on proof construction, often neglecting the equally important task of finding counterexamples. This research addresses this gap by fine-tuning large language models (LLMs) to reason about and generate counterexamples. The task is formalized as formal counterexample generation, which requires LLMs to propose candidate counterexamples and produce formal proofs that can be automatically verified in the Lean 4 theorem prover. To enable effective learning, a symbolic mutation strategy is introduced to enhance the quality and efficiency of counterexample generation.