DeepTheorem: Avanzando en el razonamiento de LLM para la demostración de teoremas mediante lenguaje natural y aprendizaje por refuerzo

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

May 29, 2025

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

Resumen

La demostración de teoremas sirve como un banco de pruebas principal para evaluar las habilidades de razonamiento complejo en los modelos de lenguaje de gran escala (LLMs, por sus siglas en inglés). Sin embargo, los enfoques tradicionales de demostración automática de teoremas (ATP) dependen en gran medida de sistemas formales de demostración que no se alinean bien con las fortalezas de los LLMs, derivadas del conocimiento informal en lenguaje natural adquirido durante el preentrenamiento. En este trabajo, proponemos DeepTheorem, un marco integral de demostración informal de teoremas que aprovecha el lenguaje natural para mejorar el razonamiento matemático de los LLMs. DeepTheorem incluye un conjunto de datos de referencia a gran escala que consta de 121K teoremas y demostraciones informales de nivel IMO, abarcando diversos dominios matemáticos, rigurosamente anotados en cuanto a corrección, dificultad y categorías temáticas, junto con variantes de teoremas verificables construidas sistemáticamente. Diseñamos una novedosa estrategia de aprendizaje por refuerzo (RL-Zero) específicamente adaptada para la demostración informal de teoremas, aprovechando las variantes verificadas de teoremas para incentivar una inferencia matemática robusta. Además, proponemos métricas integrales de evaluación de resultados y procesos que examinan la corrección de las demostraciones y la calidad de los pasos de razonamiento. Análisis experimentales exhaustivos demuestran que DeepTheorem mejora significativamente el rendimiento de los LLMs en la demostración de teoremas en comparación con conjuntos de datos existentes y protocolos de ajuste fino supervisado, logrando una precisión y calidad de razonamiento de vanguardia. Nuestros hallazgos resaltan el potencial de DeepTheorem para avanzar fundamentalmente la demostración automática informal de teoremas y la exploración matemática.

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.