DeepTheorem: Verbetering van LLM-redenering voor stellingbewijzen via natuurlijke taal en reinforcement learning

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

May 29, 2025

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

Samenvatting

Theoriebewijzen dient als een belangrijke testomgeving voor het evalueren van complexe redeneervaardigheden in grote taalmodellen (LLM's). Traditionele benaderingen van automatisch theoriebewijzen (ATP) zijn echter sterk afhankelijk van formele bewijssystemen die slecht aansluiten bij de kracht van LLM's, die voortkomt uit informele, natuurlijke taal kennis die is opgedaan tijdens pre-training. In dit werk stellen we DeepTheorem voor, een uitgebreid informeel theoriebewijskader dat natuurlijke taal benut om het wiskundig redeneren van LLM's te verbeteren. DeepTheorem omvat een grootschalige benchmarkdataset bestaande uit 121K hoogwaardige informele theorema's en bewijzen op IMO-niveau, die diverse wiskundige domeinen bestrijken, rigoureus geannoteerd op correctheid, moeilijkheidsgraad en onderwerpcategorieën, en vergezeld gaan van systematisch geconstrueerde verifieerbare theorema-varianten. We ontwikkelen een nieuwe reinforcement learning strategie (RL-Zero) die expliciet is afgestemd op informeel theoriebewijzen, waarbij gebruik wordt gemaakt van de geverifieerde theorema-varianten om robuust wiskundig redeneren te stimuleren. Daarnaast stellen we uitgebreide evaluatiemetrics voor resultaten en processen voor, die de correctheid van bewijzen en de kwaliteit van redeneerstappen onderzoeken. Uitgebreide experimentele analyses tonen aan dat DeepTheorem de prestaties van LLM's op het gebied van theoriebewijzen aanzienlijk verbetert in vergelijking met bestaande datasets en supervised fine-tuning protocollen, waarbij state-of-the-art nauwkeurigheid en redeneerkwaliteit worden bereikt. Onze bevindingen benadrukken het potentieel van DeepTheorem om geautomatiseerd informeel theoriebewijzen en wiskundige exploratie fundamenteel vooruit te helpen.

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.