Один пример показан, много концепций известно! Рассуждения на основе контрпримеров в математических LLMs.

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

February 12, 2025

Авторы: 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

Аннотация

Использование математических моделей больших языков (LLM) для генерации доказательств является фундаментальной темой в исследованиях LLM. Мы утверждаем, что способность текущих LLM доказывать утверждения в значительной степени зависит от того, сталкивались ли они с соответствующим процессом доказательства во время обучения. Эта зависимость ограничивает их глубокое понимание математических теорем и связанных концепций. Вдохновленные педагогическим методом "доказательства контрпримерами", широко используемым в образовании по математике, наша работа направлена на улучшение способности LLM к математическому мышлению и доказательствам через контрпримеры. В частности, мы вручную создаем высококачественный университетский математический бенчмарк, CounterMATH, который требует от LLM доказать математические утверждения, предоставляя контрпримеры, тем самым оценивая их понимание математических концепций. Кроме того, мы разрабатываем фреймворк инженерии данных для автоматического получения обучающих данных для дальнейшего улучшения модели. Обширные эксперименты и детальные анализы показывают, что CounterMATH является сложным, что указывает на недостаточные возможности LLM, таких как OpenAI o1, в доказательствах на основе контрпримеров. Более того, наше исследование в области обучения моделей показывает, что укрепление способностей LLM к концептуальному мышлению на основе контрпримеров критически важно для улучшения их общих математических возможностей. Мы считаем, что наша работа предлагает новые перспективы для сообщества математических LLM.

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.