Saved in:
| Main Authors: | , , , , , , , , , , , , , , , , , , , |
|---|---|
| Format: | Preprint |
| Published: |
2025
|
| Subjects: | |
| Online Access: | https://arxiv.org/abs/2506.07047 |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866909642459709440 |
|---|---|
| author | Xuejun, Yu Zhong, Jianyuan Feng, Zijin Zhai, Pengyi Yousefzadeh, Roozbeh Ng, Wei Chong Liu, Haoxiong Shou, Ziyi Xiong, Jing Zhou, Yudong Ong, Claudia Beth Sugiarto, Austen Jeremy Zhang, Yaoxi Tai, Wai Ming Cao, Huan Lu, Dongcai Sun, Jiacheng Xu, Qiang Xin, Shen Li, Zhenguo |
| author_facet | Xuejun, Yu Zhong, Jianyuan Feng, Zijin Zhai, Pengyi Yousefzadeh, Roozbeh Ng, Wei Chong Liu, Haoxiong Shou, Ziyi Xiong, Jing Zhou, Yudong Ong, Claudia Beth Sugiarto, Austen Jeremy Zhang, Yaoxi Tai, Wai Ming Cao, Huan Lu, Dongcai Sun, Jiacheng Xu, Qiang Xin, Shen Li, Zhenguo |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2506_07047 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | Mathesis: Towards Formal Theorem Proving from Natural Languages Xuejun, Yu Zhong, Jianyuan Feng, Zijin Zhai, Pengyi Yousefzadeh, Roozbeh Ng, Wei Chong Liu, Haoxiong Shou, Ziyi Xiong, Jing Zhou, Yudong Ong, Claudia Beth Sugiarto, Austen Jeremy Zhang, Yaoxi Tai, Wai Ming Cao, Huan Lu, Dongcai Sun, Jiacheng Xu, Qiang Xin, Shen Li, Zhenguo Artificial Intelligence 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. |
| title | Mathesis: Towards Formal Theorem Proving from Natural Languages |
| topic | Artificial Intelligence |
| url | https://arxiv.org/abs/2506.07047 |