DeepTheorem: Verbesserung des logischen Denkens von LLMs für den Beweis von Theoremen durch natürliche Sprache und bestärkendes Lernen

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

May 29, 2025

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

Zusammenfassung

Theorem Proving dient als wichtiger Testfall zur Bewertung komplexer Schlussfolgerungsfähigkeiten in großen Sprachmodellen (LLMs). Traditionelle Ansätze des automatisierten Theorem Beweisens (ATP) stützen sich jedoch stark auf formale Beweissysteme, die sich nur schlecht mit den Stärken von LLMs deckt, die aus informellem, natürlichem Sprachwissen während des Vortrainings gewonnen werden. In dieser Arbeit schlagen wir DeepTheorem vor, ein umfassendes Framework für informelles Theorem Beweisen, das natürliche Sprache nutzt, um das mathematische Denken von LLMs zu verbessern. DeepTheorem umfasst einen groß angelegten Benchmark-Datensatz, bestehend aus 121.000 hochwertigen, IMO-Level informellen Theoremen und Beweisen aus verschiedenen mathematischen Bereichen, die sorgfältig auf Korrektheit, Schwierigkeitsgrad und Themenkategorien annotiert sind, begleitet von systematisch konstruierten, überprüfbaren Theorem-Varianten. Wir entwickeln eine neuartige Verstärkungslernstrategie (RL-Zero), die speziell auf informelles Theorem Beweisen zugeschnitten ist und die verifizierten Theorem-Varianten nutzt, um robuste mathematische Inferenz zu fördern. Zusätzlich schlagen wir umfassende Bewertungsmetriken für Ergebnisse und Prozesse vor, die die Korrektheit der Beweise und die Qualität der Schlussfolgerungsschritte untersuchen. Umfangreiche experimentelle Analysen zeigen, dass DeepTheorem die Theorem-Beweis-Leistung von LLMs im Vergleich zu bestehenden Datensätzen und überwachten Feinabstimmungsprotokollen deutlich verbessert und dabei höchste Genauigkeit und Schlussfolgerungsqualität erreicht. Unsere Ergebnisse unterstreichen das Potenzial von DeepTheorem, das automatisierte informelle Theorem Beweisen und die mathematische Exploration grundlegend voranzutreiben.

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.