DeepTheorem: Avançando o Raciocínio de LLMs para Prova de Teoremas Através de Linguagem Natural e Aprendizado por Reforço

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

Resumo

A prova de teoremas serve como um importante campo de testes para avaliar habilidades de raciocínio complexo em modelos de linguagem de grande escala (LLMs). No entanto, as abordagens tradicionais de prova automática de teoremas (ATP) dependem fortemente de sistemas formais de prova que se alinham mal com as forças dos LLMs, derivadas do conhecimento informal em linguagem natural adquirido durante o pré-treinamento. Neste trabalho, propomos o DeepTheorem, um framework abrangente de prova informal de teoremas que explora a linguagem natural para aprimorar o raciocínio matemático dos LLMs. O DeepTheorem inclui um conjunto de dados de referência em larga escala, composto por 121 mil teoremas e provas informais de nível IMO, abrangendo diversos domínios matemáticos, rigorosamente anotados quanto à correção, dificuldade e categorias temáticas, acompanhados por variantes de teoremas verificáveis construídas sistematicamente. Desenvolvemos uma nova estratégia de aprendizado por reforço (RL-Zero) especificamente adaptada para a prova informal de teoremas, aproveitando as variantes verificadas para incentivar inferências matemáticas robustas. Além disso, propomos métricas abrangentes de avaliação de resultados e processos, examinando a correção das provas e a qualidade das etapas de raciocínio. Análises experimentais extensivas demonstram que o DeepTheorem melhora significativamente o desempenho dos LLMs na prova de teoremas em comparação com conjuntos de dados existentes e protocolos de ajuste fino supervisionado, alcançando precisão e qualidade de raciocínio de ponta. Nossos resultados destacam o potencial do DeepTheorem para avançar fundamentalmente a prova automática informal de teoremas e a exploração 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.