野外的自动形式化：评估 LLMs 在真实数学定义上的表现
计算与语言
2025-09-05 v3 形式语言与自动机理论
摘要
凭借其语言能力，LLMs 提供了通过自动形式化弥合非形式数学与形式语言之间差距的机会。然而，LLMs 在多大程度上能泛化到复杂且自然出现的数学陈述仍不清楚。为了弥补这一差距，我们研究了真实世界数学定义的自动形式化任务：这是数学论述的关键组成部分。具体而言，我们引入了两种新的自动形式化资源，分别从 Wikipedia（Def_Wiki）和 arXiv 论文（Def_ArXiv）收集定义。然后我们系统地评估了一系列 LLMs，分析它们将定义形式化为 Isabelle/HOL 的能力。此外，我们研究了增强 LLMs 性能的策略，包括通过证明辅助工具的外部反馈进行细化，以及定义锚定，即通过形式数学库中的相关上下文元素增强 LLMs 的形式化。我们的发现表明，与现有基准（如 miniF2F）相比，定义构成了更大的挑战。特别地，我们发现 LLMs 在自我纠正和与相关数学库对齐方面仍然存在困难。同时，结构化细化方法和定义锚定策略在自我纠正能力方面带来了高达 16% 的显著提升，在未定义错误减少方面带来了高达 43% 的提升，为在真实场景中增强基于 LLM 的自动形式化指明了有前景的方向。
引用
@article{arxiv.2502.12065,
title = {Autoformalization in the Wild: Assessing LLMs on Real-World Mathematical Definitions},
author = {Lan Zhang and Marco Valentino and Andre Freitas},
journal= {arXiv preprint arXiv:2502.12065},
year = {2025}
}
备注
EMNLP 2025 Camera-Ready Version