Mathesis: Towards Formal Theorem Proving from Natural Languages

This paper introduces Mathesis, the first end-to-end theorem-proving pipeline designed to solve complex mathematical problems directly from informal, natural language statements. The system features the Mathesis-Autoformalizer, which uses reinforcement learning to translate natural language problems into the Lean 4 formal language. The pipeline's performance is tested on the newly introduced Gaokao-Formal benchmark, a challenging set of 488 problems from China's national college entrance exam. The paper also presents LeanScorer, a novel framework for evaluating the semantic accuracy of these formalizations. When combined, the Mathesis components achieve state-of-the-art results, demonstrating a significant advancement in automated formal reasoning.

Here are the key highlights:

• Pioneering End-to-End System: Mathesis is the first theorem-proving pipeline that processes informal problem statements from start to finish.
• Advanced Autoformalizer: The Mathesis-Autoformalizer is the first of its kind to use reinforcement learning and Hierarchical Preference Optimization (HPO) to improve its ability to formalize natural language problems. It outperforms the best baseline by 22% in pass-rate on the Gaokao-Formal benchmark.
• New Challenging Benchmark: The paper introduces Gaokao-Formal, a benchmark with 488 complex problems from China's Gaokao exam, aimed at advancing research on formalizing diverse and intricate mathematical problems.
• Nuanced Evaluation Framework: The authors developed LeanScorer, a novel evaluation method that combines LLM-based analysis with a Sugeno Fuzzy Integral to assess formalization quality. It achieves a 0.92 F1 score, outperforming previous methods.