首个自动评估数学证明形式化对齐的框架，提升机器验证可靠性。
FormalAlign: Automated Alignment Evaluation for Autoformalization
- 双损失机制联合训练形式化生成与语义对齐任务
- 在多个基准上超越GPT-4，最高提升11.58%对齐得分
- 适合需要高精度形式化验证的研究者与工具开发者
自动形式化旨在将非正式数学证明转换为机器可验证格式，弥合自然语言与形式语言之间的鸿沟。然而，确保非正式陈述与形式化结果之间的语义对齐仍具挑战性。现有方法严重依赖人工验证，限制了可扩展性。为此，我们提出 extsc{FormalAlign}，首个专为自动形式化中自然语言与形式语言对齐评估设计的自动化框架。 extsc{FormalAlign} 在形式化序列生成任务与输入输出表征对齐任务上联合训练，采用一对相互增强的双损失机制。在我们提出的误对齐策略增强的四个基准上进行评估， extsc{FormalAlign} 表现优异：在 orml-Basic 上对齐选择得分达 99.21%，比 GPT-4 高出 11.58%；在 MiniF2F-Valid 上达 66.39%，高出 3.19%。该对齐评估方法显著减少人工验证需求。数据集与代码已公开于~ exttt{https://github.com/rookie-joe/FormalAlign}。
原文摘要 · Abstract (English)
Autoformalization aims to convert informal mathematical proofs into machine-verifiable formats, bridging the gap between natural and formal languages. However, ensuring semantic alignment between the informal and formalized statements remains challenging. Existing approaches heavily rely on manual verification, hindering scalability. To address this, we introduce \textsc{FormalAlign}, the first automated framework designed for evaluating the alignment between natural and formal languages in autoformalization. \textsc{FormalAlign} trains on both the autoformalization sequence generation task and the representational alignment between input and output, employing a dual loss that combines a pair of mutually enhancing autoformalization and alignment tasks. Evaluated across four benchmarks augmented by our proposed misalignment strategies, \textsc{FormalAlign} demonstrates superior performance. In our experiments, \textsc{FormalAlign} outperforms GPT-4, achieving an Alignment-Selection Score 11.58\% higher on \forml-Basic (99.21\% vs. 88.91\%) and 3.19\% higher on MiniF2F-Valid (66.39\% vs. 64.34\%). This effective alignment evaluation significantly reduces the need for manual verification. Both the dataset and code can be accessed via~\url{https://github.com/rookie-joe/FormalAlign}.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。