Un exemple montré, de nombreux concepts connus ! Raisonnement conceptuel basé sur les contre-exemples dans les LLM mathématiques

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

February 12, 2025

Auteurs: 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

Résumé

L'utilisation des grands modèles de langage mathématique (LLM) pour la génération de preuves est un sujet fondamental dans la recherche sur les LLM. Nous soutenons que la capacité des LLM actuels à prouver des énoncés dépend largement de s'ils ont rencontré le processus de preuve pertinent lors de l'entraînement. Cette dépendance limite leur compréhension approfondie des théorèmes mathématiques et des concepts associés. Inspirés par la méthode pédagogique de "preuve par contre-exemples" couramment utilisée dans l'enseignement des mathématiques humaines, notre travail vise à améliorer la capacité des LLM à mener un raisonnement mathématique et des preuves à travers des contre-exemples. Plus précisément, nous créons manuellement un banc d'essai mathématique de haute qualité de niveau universitaire, CounterMATH, qui demande aux LLM de prouver des énoncés mathématiques en fournissant des contre-exemples, évaluant ainsi leur compréhension des concepts mathématiques. De plus, nous développons un cadre d'ingénierie des données pour obtenir automatiquement des données d'entraînement en vue d'améliorer davantage le modèle. Des expériences approfondies et des analyses détaillées montrent que CounterMATH est un défi, indiquant que les LLM, tels que OpenAI o1, ont des capacités de preuve insuffisantes basées sur les contre-exemples. De plus, notre exploration de l'entraînement du modèle révèle que renforcer les capacités de raisonnement conceptuel des LLM basées sur les contre-exemples est crucial pour améliorer leurs capacités mathématiques globales. Nous pensons que notre travail offre de nouvelles perspectives à la communauté des LLM mathématiques.

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.