NL2AGBench：针对 AlphaGeometry 的 LLM 自动形式化基准评测

大型语言模型（LLMs）的最新进展已展示出强大的自然语言理解和数学推理能力。然而，它们将非正式数学问题转化为形式化表示的能力仍缺乏充分研究。这一局限对于诸如 AlphaGeometry 之类的神经符号几何系统尤为重要，因为其定理证明引擎需要以一种专门的领域特定语言（DSL）作为输入。尽管 AlphaGeometry 已达到接近 IMO 金牌得主的表现，但将自然语言问题手动转换为其形式化语法仍然是一个显著的可用性瓶颈。为应对这一挑战，我们提出了 Natural Language to AlphaGeometry Benchmark（NL2AGBench），用于评估 LLMs 将英文几何问题翻译为与 AlphaGeometry 兼容的形式化表示的能力。NL2AGBench 采用 AlphaGeometry 内部基于执行的验证来评估翻译质量，而不仅仅依赖文本相似度。我们在多个参数规模上评测了十个最先进的开源和闭源 LLM，并分析了可执行翻译准确率、语法正确性和错误特征。实验结果揭示了闭源模型与开源模型之间显著的性能差距：领先的闭源模型可实现超过 80% 的可执行翻译率，而即使是最大的开源模型，也难以持续保留几何约束并生成有效的形式化表示。我们提出了一种区分语法错误和逻辑错误的错误分类体系，并研究了包括 few-shot 提示、微调和人工引导提示在内的缓解策略，这些策略在多个模型家族上都带来了可衡量的改进。