arXiv:2406.07222v2 宣告类型: replace-cross 摘要：自动形式化，即将不受约束的自然语言自动翻译为形式语言，由于其在定理证明、形式验证和LLM输出检查方面的潜在应用而引起了广泛关注。在本文中，我们分析了当前的自动形式化方法以及用于评估这些方法的过程，重点关注Lean 4定理证明语言。我们展示了在现有方法的基础上，使用自一致性技术扩展类型检查过滤器可以显著提高性能，在ProofNet上的绝对准确率提高了18.4%。为了支持可重复性和进一步的研究，我们发布了我们的代码，其中包括对Lean公式的新符号等价性。我们还发布了新的基准测试：一个新的研究级数学数据集RLM25，修正后的ProofNet，以及包含正确和错误自动形式化配对的ProofNetVerif，用于评估指标。