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-Autoformalizer — первый автоформализатор, использующий обучение с подкреплением для улучшения способности формализации задач на естественном языке, поддерживаемый нашей новой структурой LeanScorer для тонкой оценки качества формализации. Также предлагается Mathesis-Prover, который генерирует формальные доказательства из формализованных утверждений. Для оценки применимости сквозного формального доказательства теорем в реальных условиях мы представляем Gaokao-Formal — эталонный набор из 488 сложных задач из национального вступительного экзамена в вузы Китая. Наш подход тщательно разработан, с детальным изучением каждого компонента. Эксперименты демонстрируют эффективность Mathesis: автоформализатор превосходит лучший базовый метод на 22% по проходному баллу на Gaokao-Formal. Полная система превосходит другие комбинации моделей, достигая 64% точности на MiniF2F с pass@32 и рекордных 18% на 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.