Mathesis: Rumos à Demonstração Formal de Teoremas a partir de Linguagens Naturais

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

Resumo

Os recentes avanços em modelos de linguagem de grande escala mostram um forte potencial para o raciocínio formal. No entanto, a maioria dos provadores de teoremas baseados em LLM tem sido limitada pela necessidade de declarações formais escritas por especialistas como entradas, restringindo sua aplicabilidade a problemas do mundo real expressos em linguagem natural. Nós abordamos essa lacuna com o Mathesis, o primeiro pipeline de prova de teoremas de ponta a ponta que processa declarações informais de problemas. Ele contribui com o Mathesis-Autoformalizer, o primeiro autoformalizador que usa aprendizado por reforço para aprimorar a capacidade de formalização de problemas em linguagem natural, auxiliado pelo nosso novo framework LeanScorer para avaliação detalhada da qualidade da formalização. Ele também propõe um Mathesis-Prover, que gera provas formais a partir das declarações formalizadas. Para avaliar a aplicabilidade no mundo real da prova de teoremas formal de ponta a ponta, introduzimos o Gaokao-Formal, um benchmark de 488 problemas complexos do exame nacional de admissão ao ensino superior da China. Nossa abordagem é cuidadosamente projetada, com um estudo detalhado de cada componente. Os experimentos demonstram a eficácia do Mathesis, com o autoformalizador superando a melhor linha de base em 22% na taxa de aprovação no Gaokao-Formal. O sistema completo supera outras combinações de modelos, alcançando 64% de precisão no MiniF2F com pass@32 e um estado da arte de 18% no 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.