展示一个例子，了解许多概念！在数学LLM中驱动反例的概念推理

摘要

利用数学大型语言模型（LLMs）进行证明生成是LLMs研究中的一个基本主题。我们认为当前LLMs证明陈述的能力很大程度上取决于它们在训练过程中是否遇到了相关的证明过程。这种依赖限制了它们对数学定理和相关概念的深入理解。受人类数学教育中常用的“反例证明”教学方法启发，我们的工作旨在通过反例来增强LLMs进行数学推理和证明的能力。具体而言，我们手动创建了一个高质量的大学级数学基准CounterMATH，要求LLMs通过提供反例来证明数学陈述，从而评估它们对数学概念的掌握。此外，我们开发了一个数据工程框架，自动获取训练数据以进一步改进模型。大量实验和详细分析表明CounterMATH具有挑战性，表明像OpenAI o1这样的LLMs在反例驱动的证明能力方面不足。此外，我们对模型训练的探索显示，加强LLMs的反例驱动概念推理能力对提高它们的整体数学能力至关重要。我们相信我们的工作为数学LLMs社区提供了新的视角。

English

Leveraging mathematical Large Language Models (LLMs) for proof generation is a fundamental topic in LLMs research. We argue that the ability of current LLMs to prove statements largely depends on whether they have encountered the relevant proof process during training. This reliance limits their deeper understanding of mathematical theorems and related concepts. Inspired by the pedagogical method of "proof by counterexamples" commonly used in human mathematics education, our work aims to enhance LLMs' ability to conduct mathematical reasoning and proof through counterexamples. Specifically, we manually create a high-quality, university-level mathematical benchmark, CounterMATH, which requires LLMs to prove mathematical statements by providing counterexamples, thereby assessing their grasp of mathematical concepts. Additionally, we develop a data engineering framework to automatically obtain training data for further model improvement. Extensive experiments and detailed analyses demonstrate that CounterMATH is challenging, indicating that LLMs, such as OpenAI o1, have insufficient counterexample-driven proof capabilities. Moreover, our exploration into model training reveals that strengthening LLMs' counterexample-driven conceptual reasoning abilities is crucial for improving their overall mathematical capabilities. We believe that our work offers new perspectives on the community of mathematical LLMs.

展示一个例子，了解许多概念！在数学LLM中驱动反例的概念推理

One Example Shown, Many Concepts Known! Counterexample-Driven Conceptual Reasoning in Mathematical LLMs

摘要

Summary

Support