Mathesis: Verso la dimostrazione formale di teoremi a partire dai linguaggi naturali
Mathesis: Towards Formal Theorem Proving from Natural Languages
June 8, 2025
Autori: 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
Abstract
I recenti progressi nei modelli linguistici di grandi dimensioni mostrano un forte potenziale per il ragionamento formale. Tuttavia, la maggior parte dei dimostratori di teoremi basati su LLM è stata a lungo limitata dalla necessità di utilizzare dichiarazioni formali scritte da esperti come input, riducendo così la loro applicabilità a problemi del mondo reale espressi in linguaggio naturale. Affrontiamo questa lacuna con Mathesis, la prima pipeline end-to-end per la dimostrazione di teoremi che elabora dichiarazioni informali di problemi. Mathesis introduce Mathesis-Autoformalizer, il primo autoformalizzatore che utilizza l'apprendimento per rinforzo per migliorare la capacità di formalizzazione di problemi in linguaggio naturale, supportato dal nostro nuovo framework LeanScorer per una valutazione sfumata della qualità della formalizzazione. Propone inoltre Mathesis-Prover, che genera dimostrazioni formali a partire dalle dichiarazioni formalizzate. Per valutare l'applicabilità nel mondo reale della dimostrazione formale end-to-end, introduciamo Gaokao-Formal, un benchmark di 488 problemi complessi tratti dall'esame di ammissione nazionale cinese per l'università. Il nostro approccio è progettato con cura, con uno studio approfondito di ciascun componente. Gli esperimenti dimostrano l'efficacia di Mathesis, con l'autoformalizzatore che supera il miglior baseline del 22% nel tasso di successo su Gaokao-Formal. Il sistema completo supera altre combinazioni di modelli, raggiungendo una precisione del 64% su MiniF2F con pass@32 e un risultato all'avanguardia del 18% su 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.