Mathesis: Towards Formal Theorem Proving from Natural Languages
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.
68492bf142e4f9106973f411
Yu Xuejun
68492bf142e4f9106973f412
Jianyuan Zhong
claimed_verified
2025-06-11T08:34:08.719Z
6608fa4f5baec84322ec85ea
/avatars/13bdaff931676b065fa1efef06fef922.svg
Zhong
user
Jianyuan1
68492bf142e4f9106973f413
Zijin Feng
68492bf142e4f9106973f414
Pengyi Zhai
68492bf142e4f9106973f415
Roozbeh Yousefzadeh
claimed_verified
2025-06-13T14:59:42.823Z
63319750b7b8e9d6e8994cc5
/avatars/0566f525ec383958e24ebf4952f9067f.svg
Roozbeh Yousefzadeh
user
roozbeh-yz
68492bf142e4f9106973f416
Wei Chong Ng
68492bf142e4f9106973f417
Haoxiong Liu
68492bf142e4f9106973f418
Ziyi Shou
68492bf142e4f9106973f419
Jing Xiong
68492bf142e4f9106973f41a
Yudong Zhou
68492bf142e4f9106973f41b
Claudia Beth Ong
68492bf142e4f9106973f41c
Austen Jeremy Sugiarto
68492bf142e4f9106973f41d
Yaoxi Zhang
68492bf142e4f9106973f41e
Wai Ming Tai
68492bf142e4f9106973f41f
Huan Cao
68492bf142e4f9106973f420
Dongcai Lu
68492bf142e4f9106973f421
Jiacheng Sun
68492bf142e4f9106973f422
Qiang Xu
68492bf142e4f9106973f423
Shen Xin
68492bf142e4f9106973f424
Zhenguo Li
Mathesis: Towards Formal Theorem Proving from Natural Languages
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.