Mathesis : Vers la démonstration formelle de théorèmes à partir des langues naturelles

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

Résumé

Les récentes avancées dans les modèles de langage de grande taille montrent un fort potentiel pour le raisonnement formel. Cependant, la plupart des démonstrateurs de théorèmes basés sur ces modèles ont longtemps été limités par la nécessité de disposer d'énoncés formels rédigés par des experts en entrée, ce qui restreint leur applicabilité aux problèmes du monde réel exprimés en langage naturel. Nous abordons cette lacune avec Mathesis, le premier pipeline de démonstration de théorèmes de bout en bout traitant des énoncés de problèmes informels. Il introduit Mathesis-Autoformalizer, le premier autoformaliseur utilisant l'apprentissage par renforcement pour améliorer la capacité de formalisation des problèmes en langage naturel, soutenu par notre nouveau cadre LeanScorer pour une évaluation nuancée de la qualité de la formalisation. Il propose également Mathesis-Prover, qui génère des preuves formelles à partir des énoncés formalisés. Pour évaluer l'applicabilité réelle de la démonstration de théorèmes formels de bout en bout, nous introduisons Gaokao-Formal, un benchmark de 488 problèmes complexes issus de l'examen national d'entrée à l'université en Chine. Notre approche est soigneusement conçue, avec une étude approfondie de chaque composant. Les expériences démontrent l'efficacité de Mathesis, avec l'autoformaliseur surpassant le meilleur modèle de référence de 22 % en taux de réussite sur Gaokao-Formal. Le système complet surpasse les autres combinaisons de modèles, atteignant une précision de 64 % sur MiniF2F avec pass@32 et un résultat de pointe de 18 % sur 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.