Um Exemplo Mostrado, Muitos Conceitos Conhecidos! Raciocínio Conceitual Orientado por Contraexemplos em LLMs Matemáticos

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

February 12, 2025

Autores: Yinghui Li, Jiayi Kuang, Haojing Huang, Zhikun Xu, Xinnian Liang, Yi Yu, Wenlian Lu, Yangning Li, Xiaoyu Tan, Chao Qu, Ying Shen, Hai-Tao Zheng, Philip S. Yu

cs.AI

Resumo

Aproveitar modelos de linguagem de grande escala (LLMs) matemáticos para a geração de provas é um tópico fundamental na pesquisa de LLMs. Argumentamos que a capacidade dos LLMs atuais de provar afirmações depende em grande parte de terem encontrado o processo de prova relevante durante o treinamento. Essa dependência limita sua compreensão mais profunda de teoremas matemáticos e conceitos relacionados. Inspirados pelo método pedagógico de "prova por contraexemplos", comumente usado na educação matemática humana, nosso trabalho visa aprimorar a capacidade dos LLMs de realizar raciocínio e prova matemática por meio de contraexemplos. Especificamente, criamos manualmente um benchmark matemático de alta qualidade em nível universitário, o CounterMATH, que exige que os LLMs provem afirmações matemáticas fornecendo contraexemplos, avaliando assim sua compreensão de conceitos matemáticos. Além disso, desenvolvemos uma estrutura de engenharia de dados para obter automaticamente dados de treinamento para melhorias adicionais do modelo. Experimentos extensivos e análises detalhadas demonstram que o CounterMATH é desafiador, indicando que LLMs, como o OpenAI o1, têm capacidades insuficientes de prova baseada em contraexemplos. Além disso, nossa exploração sobre o treinamento de modelos revela que fortalecer as habilidades de raciocínio conceitual baseado em contraexemplos dos LLMs é crucial para melhorar suas capacidades matemáticas gerais. Acreditamos que nosso trabalho oferece novas perspectivas para a comunidade de LLMs matemáticos.

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.