用符号等价与语义一致性提升数学表述自动形式化准确率
Autoformalize Mathematical Statements by Symbolic Equivalence and Semantic Consistency
- 通过自动化定理证明器检测候选形式化结果的逻辑一致性
- 在MATH和miniF2F数据集上实现最高1.35倍的准确率提升
- 适合需要高精度数学形式化的研究者和AI系统开发者
自动形式化任务旨在将自然语言描述自动转换为形式语言，尤其在数学领域面临巨大挑战。尽管大语言模型（LLMs）展现出处理竞赛级数学问题的潜力，但其生成结果在pass@1与pass@k准确率间存在显著差距。为此，本文提出一种新框架，基于符号等价与语义一致性两种互补的自一致评估方法，从k个候选结果中筛选最优解。符号等价利用自动化定理证明器检测候选结果间的逻辑同构性；语义一致性则通过将形式化结果反向非形式化，并计算原始文本与重构文本嵌入向量间的相似度，评估意义保留程度。在MATH和miniF2F数据集上的大量实验表明，该方法显著提升自动形式化准确率，在不同LLM和基线方法上实现0.22至1.35倍的相对改进。
原文摘要 · Abstract (English)
Autoformalization, the task of automatically translating natural language descriptions into a formal language, poses a significant challenge across various domains, especially in mathematics. Recent advancements in large language models (LLMs) have unveiled their promising capabilities to formalize even competition-level math problems. However, we observe a considerable discrepancy between pass@1 and pass@k accuracies in LLM-generated formalizations. To address this gap, we introduce a novel framework that scores and selects the best result from k autoformalization candidates based on two complementary self-consistency methods: symbolic equivalence and semantic consistency. Elaborately, symbolic equivalence identifies the logical homogeneity among autoformalization candidates using automated theorem provers, and semantic consistency evaluates the preservation of the original meaning by informalizing the candidates and computing the similarity between the embeddings of the original and informalized texts. Our extensive experiments on the MATH and miniF2F datasets demonstrate that our approach significantly enhances autoformalization accuracy, achieving up to 0.22-1.35x relative improvements across various LLMs and baseline methods.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。