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.