Mathesis: Auf dem Weg zur formalen Theorembeweisführung aus natürlichen Sprachen

Mathesis: Towards Formal Theorem Proving from Natural Languages

June 8, 2025

Autoren: Yu Xuejun, Jianyuan Zhong, Zijin Feng, Pengyi Zhai, Roozbeh Yousefzadeh, Wei Chong Ng, Haoxiong Liu, Ziyi Shou, Jing Xiong, Yudong Zhou, Claudia Beth Ong, Austen Jeremy Sugiarto, Yaoxi Zhang, Wai Ming Tai, Huan Cao, Dongcai Lu, Jiacheng Sun, Qiang Xu, Shen Xin, Zhenguo Li

cs.AI

Zusammenfassung

Jüngste Fortschritte bei großen Sprachmodellen zeigen vielversprechende Ansätze für formales Schließen. Die meisten auf LLM basierenden Theorembeweiser waren jedoch lange Zeit durch die Notwendigkeit von von Experten verfassten formalen Aussagen als Eingaben eingeschränkt, was ihre Anwendbarkeit auf reale Probleme, die in natürlicher Sprache formuliert sind, begrenzte. Wir adressieren diese Lücke mit Mathesis, der ersten End-to-End-Theorembeweis-Pipeline, die informale Problemstellungen verarbeitet. Sie beinhaltet den Mathesis-Autoformalizer, den ersten Autoformalizer, der Verstärkungslernen nutzt, um die Formalisierungsfähigkeit von Problemen in natürlicher Sprache zu verbessern, unterstützt durch unser neuartiges LeanScorer-Framework zur differenzierten Bewertung der Formalisierungsqualität. Zudem wird ein Mathesis-Prover vorgeschlagen, der formale Beweise aus den formalisierten Aussagen generiert. Um die praktische Anwendbarkeit des End-to-End-formalen Theorembeweisens zu bewerten, führen wir Gaokao-Formal ein, einen Benchmark mit 488 komplexen Problemen aus der nationalen Hochschulaufnahmeprüfung Chinas. Unser Ansatz ist sorgfältig gestaltet, mit einer gründlichen Untersuchung jeder Komponente. Experimente demonstrieren die Wirksamkeit von Mathesis, wobei der Autoformalizer den besten Baseline-Wert in der Erfolgsquote auf Gaokao-Formal um 22 % übertrifft. Das vollständige System übertrifft andere Modellkombinationen und erreicht eine Genauigkeit von 64 % auf MiniF2F mit pass@32 sowie einen state-of-the-art-Wert von 18 % auf Gaokao-Formal.

English

Recent advances in large language models show strong promise for formal reasoning. However, most LLM-based theorem provers have long been constrained by the need for expert-written formal statements as inputs, limiting their applicability to real-world problems expressed in natural language. We tackle this gap with Mathesis, the first end-to-end theorem proving pipeline processing informal problem statements. It contributes Mathesis-Autoformalizer, the first autoformalizer using reinforcement learning to enhance the formalization ability of natural language problems, aided by our novel LeanScorer framework for nuanced formalization quality assessment. It also proposes a Mathesis-Prover, which generates formal proofs from the formalized statements. To evaluate the real-world applicability of end-to-end formal theorem proving, we introduce Gaokao-Formal, a benchmark of 488 complex problems from China's national college entrance exam. Our approach is carefully designed, with a thorough study of each component. Experiments demonstrate Mathesis's effectiveness, with the autoformalizer outperforming the best baseline by 22% in pass-rate on Gaokao-Formal. The full system surpasses other model combinations, achieving 64% accuracy on MiniF2F with pass@32 and a state-of-the-art 18% on Gaokao-Formal.