Mathesis: Hacia la Demostración Formal de Teoremas a partir de Lenguajes Naturales

Mathesis: Towards Formal Theorem Proving from Natural Languages

June 8, 2025

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

Resumen

Los avances recientes en los modelos de lenguaje de gran escala muestran un fuerte potencial para el razonamiento formal. Sin embargo, la mayoría de los demostradores de teoremas basados en LLM han estado limitados durante mucho tiempo por la necesidad de declaraciones formales escritas por expertos como entradas, lo que restringe su aplicabilidad a problemas del mundo real expresados en lenguaje natural. Abordamos esta brecha con Mathesis, la primera pipeline de demostración de teoremas de extremo a extremo que procesa enunciados informales de problemas. Contribuye con Mathesis-Autoformalizer, el primer autoformalizador que utiliza aprendizaje por refuerzo para mejorar la capacidad de formalización de problemas en lenguaje natural, apoyado por nuestro novedoso marco LeanScorer para la evaluación matizada de la calidad de la formalización. También propone un Mathesis-Prover, que genera demostraciones formales a partir de las declaraciones formalizadas. Para evaluar la aplicabilidad en el mundo real de la demostración formal de teoremas de extremo a extremo, presentamos Gaokao-Formal, un benchmark de 488 problemas complejos del examen nacional de ingreso a la universidad en China. Nuestro enfoque está cuidadosamente diseñado, con un estudio exhaustivo de cada componente. Los experimentos demuestran la efectividad de Mathesis, con el autoformalizador superando al mejor modelo de referencia en un 22% en la tasa de aprobación en Gaokao-Formal. El sistema completo supera a otras combinaciones de modelos, logrando un 64% de precisión en MiniF2F con pass@32 y un 18% de vanguardia en 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.