Mathesis: Op weg naar formeel theorema bewijzen vanuit natuurlijke talen

Mathesis: Towards Formal Theorem Proving from Natural Languages

June 8, 2025

Auteurs: 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

Samenvatting

Recente ontwikkelingen in grote taalmodellen tonen veelbelovende mogelijkheden voor formeel redeneren. De meeste op LLM gebaseerde theoremaproeven zijn echter lange tijd beperkt geweest door de noodzaak van door experts geschreven formele statements als invoer, wat hun toepasbaarheid op real-world problemen uitgedrukt in natuurlijke taal beperkt. Wij pakken deze kloof aan met Mathesis, de eerste end-to-end theoremaproefpijplijn die informele probleemstellingen verwerkt. Het introduceert Mathesis-Autoformalizer, de eerste autoformalizer die reinforcement learning gebruikt om het formalisatievermogen van problemen in natuurlijke taal te verbeteren, ondersteund door ons nieuwe LeanScorer-framework voor genuanceerde kwaliteitsbeoordeling van formalisatie. Het stelt ook een Mathesis-Prover voor, die formele bewijzen genereert uit de geformaliseerde statements. Om de real-world toepasbaarheid van end-to-end formele theoremaproeven te evalueren, introduceren we Gaokao-Formal, een benchmark van 488 complexe problemen uit het nationale toelatingsexamen voor universiteiten in China. Onze aanpak is zorgvuldig ontworpen, met een grondige studie van elke component. Experimenten tonen de effectiviteit van Mathesis aan, waarbij de autoformalizer de beste baseline met 22% overtreft in slaagpercentage op Gaokao-Formal. Het volledige systeem overtreft andere modelcombinaties, met een nauwkeurigheid van 64% op MiniF2F met pass@32 en een state-of-the-art 18% op 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.