摘要
arXiv:2502.10454v1 交叉类型:cross
摘要:利用数学大型语言模型(LLMs)进行证明生成是LLMs研究中的一个基本课题。我们认为,当前LLMs能否证明命题主要取决于它们在训练过程中是否遇到过相关的证明过程。这种依赖限制了它们对数学定理及相关概念的更深层次理解。受人类数学教育中常用的“反例证明法”启发,我们的工作旨在通过反例增强LLMs进行数学推理和证明的能力。具体来说,我们手动创建了一个高质量的大学水平数学基准数据集CounterMATH,要求LLMs通过提供反例来证明数学命题,从而评估它们对数学概念的掌握程度。此外,我们开发了一个数据工程框架,以自动获取进一步模型改进所需的训练数据。广泛的实验证明和详细分析表明,CounterMATH具有挑战性,表明诸如OpenAI的o1这样的LLMs缺乏足够的基于反例的证明能力。另外,我们在模型训练中的探索表明,加强LLMs的基于反例的概念推理能力对于提高它们整体的数学能力至关重要。我们认为,我们的工作为数学LLMs社区提供了新的视角。