NL2AGBench：AlphaGeometry 的 LLM 自动形式化基准测试

大语言模型（LLM）的最新进展展示了在自然语言理解和数学推理方面的强大能力。然而，他们将非正式数学问题转化为正式表示的能力仍未得到充分探索。这种限制对于 AlphaGeometry 等神经符号几何系统尤其重要，其定理证明引擎需要以专门的领域特定语言 (DSL) 进行输入。尽管 AlphaGeometry 实现了接近 IMO 金牌的性能，但手动将自然语言问题转换为其形式语法仍然是一个重大的可用性瓶颈。为了应对这一挑战，我们引入了 Natural Language to AlphaGeometry Benchmark (NL2AGBench)，该基准评估 LLM 将英语几何问题转换为与 AlphaGeometry 兼容的形式表示的能力。 NL2AGBench 在 AlphaGeometry 中使用基于执行的验证来评估翻译质量，而不是仅仅依赖文本相似性。我们在多个参数范围内评估十个最先进的开源和闭源 LLM，并分析可执行翻译的准确性、语法正确性和错误特征。我们的实验揭示了闭源模型和开源模型之间存在巨大的性能差距：领先的闭源模型实现了 80% 以上的可执行转换率，而即使是最大的开源模型也难以始终如一地保留几何约束并生成有效的形式化。我们引入了一种区分语法和逻辑错误的错误分类法，并研究了缓解策略，包括几次提示、微调 和人工引导提示，这些策略在多个模型系列中产生了可衡量的改进。