DeepTheorem: Advancing LLM Reasoning for Theorem Proving Through Natural Language and Reinforcement Learning
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
2025-05-30
Summary
This paper talks about DeepTheorem, a new approach that helps AI models get much better at solving math problems and proving theorems by training them with lots of natural language explanations and a special learning technique.
What's the problem?
The problem is that while AI models have gotten good at understanding and generating text, they still struggle with the step-by-step reasoning needed to prove math theorems, especially when the explanations are written in everyday language instead of strict math symbols.
What's the solution?
The researchers built a huge dataset full of natural language explanations for different theorems and used reinforcement learning, which rewards the AI for making good progress, to teach the model how to reason through math problems more effectively. This combination helped the AI achieve the best results so far in informal theorem proving.
Why it matters?
This is important because it means AI could become a much more helpful tool for learning and exploring math, making it easier for students, teachers, and researchers to understand complex ideas and discover new solutions.
Abstract
DeepTheorem enhances LLM theorem-proving through a large-scale natural language dataset and a tailored reinforcement learning strategy, achieving state-of-the-art results in informal theorem proving.