通过符号等价和语义一致性自动形式化数学陈述

自动形式化，即自动将自然语言描述翻译成形式语言的任务，在各个领域，尤其是在数学领域，构成了一个重大挑战。大型语言模型（LLMs）的最新进展揭示了它们甚至能够形式化竞赛级别的数学问题的潜力。然而，我们观察到在LLM生成的形式化结果中，pass@1和pass@k准确率之间存在显著差异。为了解决这一差距，我们引入了一个新颖的框架，该框架基于两种互补的自一致性方法：符号等价和语义一致性，对k个自动形式化候选结果进行评分并选择最佳结果。具体而言，符号等价使用自动定理证明器识别自动形式化候选结果之间的逻辑同质性，而语义一致性则通过将候选结果非形式化并计算原始文本与非形式化文本嵌入之间的相似度来评估原始意义的保留程度。我们在MATH和miniF2F数据集上的大量实验表明，我们的方法显著提高了自动形式化的准确性，在各种LLM和基线方法上实现了高达0.22-1.35倍的相对改进。