Mathematical reasoning in large language models : bridging natural language and formal mathematics

Abstract

Large Language Models (LLMs) increasingly confront the challenge of processing and reasoning about mathematical content in both natural language and formal systems. This complexity arises from the dual nature of mathematical reasoning: understanding informal mathematical text and producing verifiable formal proofs. The challenge is further amplified by the need to bridge these two domains effectively while maintaining mathematical rigor.

In this thesis, we investigate mathematical reasoning in LLMs with a focus on three interconnected areas: natural language mathematical reasoning, autoformalization, and automated theorem proving. In the natural language reasoning domain, we introduce SELF, a novel framework enabling autonomous improvement of LLMs through language-based feedback, and AutoPSV, an automated verification system that evaluates reasoning steps without manual annotation. For autoformalization, we develop Process-Driven Autoformalization (PDA), which leverages compiler feedback to enhance translation quality, and FormalAlign, an automated framework for evaluating semantic alignment between informal and formal mathematics. In automated theorem proving, we propose POETRY, a recursive theorem-proving approach that significantly extends proof length capabilities through level-based search strategies.

Our research establishes a comprehensive framework for enhancing mathematical reasoning capabilities in LLMs through three interconnected domains. Experimental results demonstrate substantial improvements across multiple stages: in natural language reasoning, SELF achieves continuous performance improvement without human intervention, while AutoPSV improves verification accuracy by 15\% through automated process supervision. In bridging natural and formal mathematics, PDA increases compiler success rates by 25\% with process-driven training, and FormalAlign outperforms GPT-4 by 11.58\% in semantic alignment evaluation. Finally, in formal mathematics, POETRY extends the maximum provable theorem length from 10 to 26 steps while improving the average proving success rate by 5.1\%. These quantitative advances demonstrate the effectiveness of our systematic approach in leveraging both natural language and formal mathematical capabilities to enhance LLMs' mathematical reasoning.