⏶5
Mathesis：迈向从自然语言的形式化定理证明
发表
由 
Zhong 提交
Zhong 提交作者: 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
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摘要
大型语言模型在形式推理方面的最新进展显示出强大的前景。然而，大多数基于LLM的定理证明器长期以来一直受限于需要专家编写的形式化陈述作为输入，这限制了它们在以自然语言表达的实际问题中的适用性。我们通过Mathesis来解决这一差距，Mathesis是第一个处理非形式化问题陈述的端到端定理证明管道。它贡献了Mathesis-Autoformalizer，这是第一个使用强化学习增强自然语言问题形式化能力的自动形式化器，并辅以我们新颖的LeanScorer框架，用于细致入微的形式化质量评估。它还提出了一个Mathesis-Prover，可以从形式化陈述中生成形式化证明。为了评估端到端形式定理证明的实际适用性，我们引入了Gaokao-Formal，这是一个包含中国高考中488个复杂问题的基准。我们的方法经过精心设计，对每个组件进行了透彻研究。实验证明了Mathesis的有效性，其自动形式化器在Gaokao-Formal上的通过率比最佳基线高出22%。整个系统超越了其他模型组合，在MiniF2F上实现了64%的准确率（pass@32），并在Gaokao-Formal上实现了18%的最新水平。
本文介绍了 Mathesis，这是首个端到端定理证明流程，旨在直接从非正式的自然语言陈述中解决复杂的数学问题。该系统包含 Mathesis-Autoformalizer，它利用强化学习将自然语言问题转换为 Lean 4 形式语言。该流程的性能在最新引入的 Gaokao-Formal 基准测试中进行了验证，该基准测试包含来自中国高考的 488 道具有挑战性的问题。本文还提出了 LeanScorer，一个用于评估这些形式化结果语义准确性的新型框架。当 Mathesis 的各个组件结合使用时，取得了最先进的结果，显示了自动化形式推理的重大进展。
以下是主要亮点：
开创性的端到端系统：Mathesis 是首个从头到尾处理非正式问题陈述的定理证明流程。
先进的自动形式化器：Mathesis-Autoformalizer 是首个采用强化学习和分层偏好优化（HPO）来提高其形式化自然语言问题能力的系统。在 Gaokao-Formal 基准测试中，其通过率比最佳基线高出 22%。
新的挑战性基准：本文介绍了 Gaokao-Formal，一个包含 488 道中国高考复杂问题的基准测试，旨在推动在形式化多样和复杂数学问题方面的研究。
细致的评估框架：作者开发了 LeanScorer，一种新颖的评估方法，它结合了基于 LLM 的分析和 Sugeno 模糊积分来评估形式化质量。它达到了 0.92 的 F1 分数，优于以前的方法。