DeepTheorem: Улучшение способности языковых моделей к рассуждению в доказательстве теорем с использованием естественного языка и обучения с подкреплением

DeepTheorem: Advancing LLM Reasoning for Theorem Proving Through Natural Language and Reinforcement Learning

May 29, 2025

Авторы: Ziyin Zhang, Jiahao Xu, Zhiwei He, Tian Liang, Qiuzhi Liu, Yansi Li, Linfeng Song, Zhengwen Liang, Zhuosheng Zhang, Rui Wang, Zhaopeng Tu, Haitao Mi, Dong Yu

cs.AI

Аннотация

Теоретическое доказательство служит важной площадкой для оценки сложных способностей к рассуждению в больших языковых моделях (LLM). Однако традиционные подходы к автоматизированному доказательству теорем (ATP) в значительной степени опираются на формальные системы доказательств, которые плохо согласуются с сильными сторонами LLM, основанными на неформальных знаниях, полученных в ходе предварительного обучения на естественном языке. В данной работе мы предлагаем DeepTheorem — всеобъемлющую неформальную систему доказательства теорем, использующую естественный язык для улучшения математического рассуждения в LLM. DeepTheorem включает в себя масштабный эталонный набор данных, состоящий из 121 тыс. высококачественных неформальных теорем и доказательств уровня Международной математической олимпиады (IMO), охватывающих различные математические области, тщательно аннотированных на предмет корректности, сложности и тематических категорий, а также сопровождаемых систематически сконструированными проверяемыми вариантами теорем. Мы разрабатываем новую стратегию обучения с подкреплением (RL-Zero), специально адаптированную для неформального доказательства теорем, которая использует проверенные варианты теорем для стимулирования устойчивого математического вывода. Кроме того, мы предлагаем всеобъемлющие метрики оценки результатов и процесса, анализирующие корректность доказательств и качество шагов рассуждения. Обширные экспериментальные анализы демонстрируют, что DeepTheorem значительно улучшает производительность LLM в доказательстве теорем по сравнению с существующими наборами данных и протоколами контролируемого тонкого настройки, достигая передовой точности и качества рассуждений. Наши результаты подчеркивают потенциал DeepTheorem для фундаментального продвижения автоматизированного неформального доказательства теорем и математических исследований.

English

Theorem proving serves as a major testbed for evaluating complex reasoning abilities in large language models (LLMs). However, traditional automated theorem proving (ATP) approaches rely heavily on formal proof systems that poorly align with LLMs' strength derived from informal, natural language knowledge acquired during pre-training. In this work, we propose DeepTheorem, a comprehensive informal theorem-proving framework exploiting natural language to enhance LLM mathematical reasoning. DeepTheorem includes a large-scale benchmark dataset consisting of 121K high-quality IMO-level informal theorems and proofs spanning diverse mathematical domains, rigorously annotated for correctness, difficulty, and topic categories, accompanied by systematically constructed verifiable theorem variants. We devise a novel reinforcement learning strategy (RL-Zero) explicitly tailored to informal theorem proving, leveraging the verified theorem variants to incentivize robust mathematical inference. Additionally, we propose comprehensive outcome and process evaluation metrics examining proof correctness and the quality of reasoning steps. Extensive experimental analyses demonstrate DeepTheorem significantly improves LLM theorem-proving performance compared to existing datasets and supervised fine-tuning protocols, achieving state-of-the-art accuracy and reasoning quality. Our findings highlight DeepTheorem's potential to fundamentally advance automated informal theorem proving and mathematical exploration.