Ein Beispiel gezeigt, viele Konzepte bekannt! Gegenbeispiel-getriebene konzeptuelle Schlussfolgerung in mathematischen LLMs.

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

February 12, 2025

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

Zusammenfassung

Die Nutzung mathematischer Großer Sprachmodelle (LLMs) zur Beweisgenerierung ist ein grundlegendes Thema in der LLMs-Forschung. Wir argumentieren, dass die Fähigkeit aktueller LLMs, Aussagen zu beweisen, weitgehend davon abhängt, ob sie den relevanten Beweisprozess während des Trainings durchlaufen haben. Diese Abhängigkeit begrenzt ihr tieferes Verständnis mathematischer Theoreme und verwandter Konzepte. Inspiriert von der pädagogischen Methode des "Beweises durch Gegenbeispiele", die in der menschlichen Mathematikausbildung häufig verwendet wird, zielt unsere Arbeit darauf ab, die Fähigkeit von LLMs zur mathematischen Argumentation und Beweisführung durch Gegenbeispiele zu verbessern. Konkret erstellen wir manuell einen qualitativ hochwertigen, universitätsniveau Mathematik-Benchmark, CounterMATH, der von LLMs verlangt, mathematische Aussagen zu beweisen, indem sie Gegenbeispiele liefern und damit ihr Verständnis mathematischer Konzepte bewerten. Darüber hinaus entwickeln wir einen Datenverarbeitungsrahmen, um automatisch Trainingsdaten für eine weitere Modellverbesserung zu erhalten. Umfangreiche Experimente und detaillierte Analysen zeigen, dass CounterMATH anspruchsvoll ist und darauf hindeutet, dass LLMs wie OpenAI o1 über unzureichende Fähigkeiten zur Beweisführung durch Gegenbeispiele verfügen. Darüber hinaus zeigt unsere Untersuchung des Modelltrainings, dass die Stärkung der konzeptuellen Argumentationsfähigkeiten von LLMs durch Gegenbeispiele entscheidend ist, um ihre allgemeinen mathematischen Fähigkeiten zu verbessern. Wir sind der Ansicht, dass unsere Arbeit neue Perspektiven für die Gemeinschaft mathematischer LLMs bietet.

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.