Mathesis: 자연어로부터 형식적 정리 증명을 향하여

Mathesis: Towards Formal Theorem Proving from Natural Languages

June 8, 2025

저자: 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

초록

최근 대규모 언어 모델의 발전은 형식적 추론에 대한 강력한 가능성을 보여주고 있다. 그러나 대부분의 LLM 기반 정리 증명기는 전문가가 작성한 형식적 명제를 입력으로 필요로 한다는 제약으로 인해, 자연어로 표현된 실제 문제에 대한 적용 가능성이 제한되어 왔다. 우리는 이러한 격차를 해결하기 위해 비형식적 문제 명제를 처리하는 최초의 종단 간 정리 증명 파이프라인인 Mathesis를 제안한다. Mathesis는 자연어 문제의 형식화 능력을 강화하기 위해 강화 학습을 활용한 최초의 자동 형식화 도구인 Mathesis-Autoformalizer를 포함하며, 이를 위해 세밀한 형식화 품질 평가를 위한 새로운 LeanScorer 프레임워크를 개발하였다. 또한 Mathesis-Prover를 제안하여 형식화된 명제로부터 형식적 증명을 생성한다. 종단 간 형식적 정리 증명의 실제 적용 가능성을 평가하기 위해, 중국의 대학 입학 시험에서 추출한 488개의 복잡한 문제로 구성된 Gaokao-Formal 벤치마크를 소개한다. 우리의 접근 방식은 각 구성 요소에 대한 철저한 연구를 통해 신중하게 설계되었다. 실험 결과, Mathesis의 효과가 입증되었으며, 자동 형식화 도구는 Gaokao-Formal에서 최고의 기준선 대비 22% 높은 통과율을 보였다. 전체 시스템은 다른 모델 조합을 능가하며, MiniF2F에서 pass@32 기준 64%의 정확도를 달성하고 Gaokao-Formal에서 최첨단 수준인 18%의 성능을 보였다.

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.