DeepTheorem: Avanzare il Ragionamento dei Modelli Linguistici per la Dimostrazione di Teoremi Attraverso il Linguaggio Naturale e l'Apprendimento per Rinforzo

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

May 29, 2025

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

Abstract

La dimostrazione di teoremi rappresenta un banco di prova fondamentale per valutare le capacità di ragionamento complesso nei grandi modelli linguistici (LLM). Tuttavia, gli approcci tradizionali alla dimostrazione automatica di teoremi (ATP) si basano fortemente su sistemi di prova formali che si allineano male con i punti di forza degli LLM, derivati dalla conoscenza informale e in linguaggio naturale acquisita durante il pre-addestramento. In questo lavoro, proponiamo DeepTheorem, un framework completo per la dimostrazione informale di teoremi che sfrutta il linguaggio naturale per potenziare il ragionamento matematico degli LLM. DeepTheorem include un dataset di riferimento su larga scala composto da 121K teoremi e dimostrazioni informali di livello IMO, che coprono diversi domini matematici, rigorosamente annotati per correttezza, difficoltà e categorie tematiche, accompagnati da varianti di teoremi verificabili costruite sistematicamente. Progettiamo una nuova strategia di apprendimento per rinforzo (RL-Zero) specificamente adattata alla dimostrazione informale di teoremi, sfruttando le varianti verificate dei teoremi per incentivare un'inferenza matematica robusta. Inoltre, proponiamo metriche di valutazione complete sia per i risultati che per il processo, esaminando la correttezza delle dimostrazioni e la qualità dei passaggi di ragionamento. Analisi sperimentali estensive dimostrano che DeepTheorem migliora significativamente le prestazioni degli LLM nella dimostrazione di teoremi rispetto ai dataset esistenti e ai protocolli di fine-tuning supervisionato, raggiungendo un'accuratezza e una qualità del ragionamento all'avanguardia. I nostri risultati evidenziano il potenziale di DeepTheorem di avanzare fondamentalmente la dimostrazione automatica informale di teoremi e l'esplorazione matematica.

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.