Autoformalization in the Wild: Assessing LLMs on Real-World Mathematical Definitions

Autoformalization in the Wild: Assessing LLMs on Real-World Mathematical Definitions

野外自动形式化：评估大语言模型在真实世界数学定义上的表现

Lan Zhang Affiliation: Department of Computer Science, University of Manchester, United Kingdom Email: lan.zhang-6@postgrad.manchester.ac.uk Marco Valentino Affiliation: School of Computer Science, University of Sheffield, United Kingdom Email: m.valentino@sheffield.ac.uk André Freitas Affiliation: Department of Computer Science, University of Manchester, United Kingdom Affiliation: Idiap Research Institute, Switzerland Affiliation: National Biomarker Centre, CRUK Manchester Institute, United Kingdom Email: andre.freitas@idiap.ch

Abstract

摘要

Thanks to their linguistic capabilities, LLMs offer an opportunity to bridge the gap between informal mathematics and formal languages through autoformalization . However, it is still unclear how well LLMs generalize to sophisticated and naturally occurring mathematical statements. To address this gap, we investigate the task of autoformalizing real-world mathematical definitions : a critical component of mathematical discourse. Specifically, we introduce two novel resources for autoformalization, collecting definitions from Wikipedia (Def_Wiki) and arXiv papers (Def_ArXiv). We then systematically evaluate a range of LLMs, analyzing their ability to formalize definitions into Isabelle/HOL. Furthermore, we investigate strategies to enhance LLMs’ performance including refinement through external feedback from Proof Assistants, and formal definition grounding, where we augment LLMs’ formalizations through relevant contextual elements from formal mathematical libraries. Our findings reveal that definitions present a greater challenge compared to existing benchmarks, such as miniF2F. In particular, we found that LLMs still struggle with self-correction, and aligning with relevant mathematical libraries. At the same time, structured refinement methods and definition grounding strategies yield notable improvements of up to 16% on self-correction capabilities and 43% on the reduction of undefined errors, highlighting promising directions for enhancing LLM-based autoformalization in real-world scenarios.[^1]

凭借其语言能力，大语言模型（LLM）为通过 自动形式化 弥合非形式数学与形式语言之间的差距提供了可能。不过，它们对复杂、自然出现的数学陈述能泛化到何种程度，仍然并不清楚。为填补这一空白，我们考察把真实世界的 数学定义 自动形式化这一任务：定义是数学论述中的关键构件。具体来说，我们引入两份新的自动形式化资源，分别收集来自维基百科（Def_Wiki）和 arXiv 论文（Def_ArXiv）的 定义 。随后，我们系统评估一系列大语言模型，分析它们把定义形式化到 Isabelle/HOL 中的能力。我们还考察提升性能的策略，包括来自证明助手的 外部反馈精炼 ，以及 形式定义锚定 ，即用形式数学库中的相关上下文要素来增强模型的形式化结果。我们发现，与已有基准（例如 miniF2F）相比，定义带来了更大挑战。尤其是，大语言模型在自我纠正、以及与相关数学库对齐方面仍然吃力。与此同时，结构化精炼方法和定义锚定策略分别带来最多约 16% 的自纠正能力提升，以及最多约 43% 的未定义错误减少，为改进真实场景中基于大语言模型的自动形式化指出了有前景的方向。[^1]

1 Introduction

1 引言

Large Language Models (LLMs) have demonstrated remarkable potential in assisting with mathematical reasoning on different downstream tasks (Wei et al., 2022; Meadows et al., 2023; Meadows et al., 2024; Valentino et al., 2022; Lu et al., 2023; Meadows and Freitas, 2023; Mishra et al., 2022a; Ferreira et al., 2022; Ferreira and Freitas, 2020; Welleck et al., 2021; Mishra et al., 2022b; Petersen et al., 2023). In the context of mathematics, formal languages play a crucial role by providing a precise, logic-based framework for verifying the correctness and logical validity of mathematical statements and proofs (Kaliszyk and Rabe, 2020).

大语言模型（LLM）已在不同下游任务的数学推理辅助中展现出显著潜力（Wei 等人，2022；Meadows 等人，2023；Meadows 等人，2024；Valentino 等人，2022；Lu 等人，2023；Meadows 和 Freitas，2023；Mishra 等人，2022a；Ferreira 等人，2022；Ferreira 和 Freitas，2020；Welleck 等人，2021；Mishra 等人，2022b；Petersen 等人，2023）。在数学语境中，形式语言通过提供精确的、基于逻辑的框架，来核验数学陈述和证明的正确性与逻辑有效性，因而起着关键作用（Kaliszyk 和 Rabe，2020）。

Figure 1: Can LLMs formalize complex mathematical statements? This paper investigates the task of translating real-world mathematical definitions into a formal language. We introduce a new resource collecting definitions from Wikipedia and ArXiv papers, exploring different strategies for autoformalization through the interaction between LLMs and Proof Assistants .

图 1： 大语言模型能否形式化复杂的数学陈述？ 本文考察把 真实世界的数学定义 翻译成形式语言这一任务。我们引入一份新资源，收集来自 维基百科 和 arXiv 论文的定义，并通过 大语言模型 与 证明助手 之间的交互，探索不同的自动形式化策略。

Consequently, one promising application of LLMs is autoformalization, the task of translating informal statements into formal languages (Wu et al., 2022). Given their advanced linguistic and inferential capabilities, LLMs offer an opportunity to bridge the gap between informal mathematics, natural language, and machine-verifiable logic, potentially streamlining and scaling the process of formal mathematical reasoning (Jiang et al., 2023; Tarrach et al., 2024).

因此，大语言模型的一个有前景的应用是 自动形式化 ，即把非形式陈述翻译成形式语言的任务（Wu 等人，2022）。凭借其较强的语言和推理能力，大语言模型有机会弥合非形式数学、自然语言与机器可核验逻辑之间的差距，并有可能简化和扩展形式数学推理的过程（Jiang 等人，2023；Tarrach 等人，2024）。

The task of autoformalization has collected increasing attention in recent years, leading to the development of benchmarks and evaluation methodologies (Azerbayev et al., 2023; Zhang et al., 2024; Li et al., 2024). Despite this progress, however, existing benchmarks for autoformalization often focus on relatively simple mathematical problems, limiting our understanding of how well LLMs generalize to more sophisticated and naturally occurring mathematical statements.

近年来，自动形式化任务受到越来越多关注，并催生了若干基准和评估方法（Azerbayev 等人，2023；Zhang 等人，2024；Li 等人，2024）。尽管有这些进展，已有自动形式化基准往往仍聚焦于相对简单的数学问题，从而限制了我们理解大语言模型对更复杂、自然出现的数学陈述能泛化到何种程度。

To address this gap, this paper investigates the task of autoformalizing mathematical definitions, a critical component of mathematical discourse (Moschkovich, 2003). Definitions serve as foundational building blocks in mathematical reasoning, yet they are often intricate, context-dependent, and thus difficult to formalize. Evaluating LLMs on this subset of mathematical statements, therefore, allows for assessing their ability to formally represent fine-grained mathematical concepts, highlighting persisting challenges and limitations for real-world applications.

为填补这一空白，本文考察把 数学定义 自动形式化这一任务。定义是数学论述中的关键构件（Moschkovich，2003）。定义是数学推理的基础构件，但往往细致、依赖上下文，因而难以形式化。在这一类数学陈述上评估大语言模型，因此可以考察它们形式表示细粒度数学概念的能力，并标出面向真实应用时仍然存在的挑战和局限。

Specifically, this paper introduces two new benchmarks for autoformalization by collecting real-world mathematical definitions into two distinct resources: (1) Def_Wiki, including definitions extracted from Wikipedia articles, and (2) Def_ArXiv, including definitions collected from machine learning research papers. Using these resources, we first evaluate LLMs in a zero-shot setting, analyzing their ability to translate definitions into Isabelle/HOL (Nipkow et al., 2002).

具体来说，本文通过把 真实世界的数学定义 收集到两份不同资源中，引入两个新的自动形式化基准：(1) Def_Wiki ，包含从维基百科条目中抽取的定义；(2) Def_ArXiv ，包含从机器学习研究论文中收集的定义。利用这些资源，我们先在零样本设定下评估大语言模型，分析它们把定义翻译到 Isabelle/HOL（Nipkow 等人，2002）中的能力。

Furthermore, to address observed limitations, we investigate two key strategies to enhance performance: (1) Refinement via external feedback, investigating the self-correction capabilities of LLMs by incorporating errors found by the supporting Proof Assistant. In particular, we show that while LLMs exhibit limited ability to refine outputs based on binary feedback (error vs. non-error), a more structured categorical refinement implemented via additional instructional constraints can improve performance. (2) Formal definition grounding . Many mathematical definitions require references to formal objects in external mathematical libraries. To augment autoformalization from LLMs, we investigate the impact of introducing additional contextual control mechanisms, which add contextual elements from formal mathematical libraries as auxiliary premises.

此外，为应对观察到的局限，我们考察两种提升性能的关键策略：(1) 借助外部反馈的精炼 ，通过纳入辅助证明助手发现的错误，考察大语言模型的自纠正能力。我们尤其表明，虽然模型根据二元反馈（有错误与无错误）精炼输出的能力有限，但通过额外指令约束实现的、更结构化的分类精炼，可以改善性能。(2) 形式定义锚定 。许多数学定义需要引用外部数学库中的形式对象。为增强大语言模型的自动形式化，我们考察引入额外上下文控制机制的影响，这些机制把形式数学库中的上下文要素作为辅助前提加入。

Overall, our findings reveal that the proposed benchmarks present a greater challenge compared to existing autoformalization datasets, such as miniF2F (Zheng et al., 2022). In particular, LLMs struggle with self-correction and particularly with incorporating relevant mathematical libraries as preambles. Proposed structured refinement methods and definition grounding strategies both deliver notable improvements, highlighting promising directions for enhancing LLM-based autoformalization in real-world scenarios.

总体来看，我们的发现表明，与已有自动形式化数据集（例如 miniF2F，Zheng 等人，2022）相比，本文提出的基准更具挑战性。尤其是，大语言模型在自我纠正上遇到困难，在把相关数学库作为导言纳入时更加明显。所提出的结构化精炼方法和定义锚定策略都带来了可观改进，为改进真实场景中基于大语言模型的自动形式化指出了有前景的方向。

Our contributions can be summarized as follows:

我们的贡献可以概括如下：

We introduce and release two novel datasets for autoformalization: Def_Wiki (definitions from Wikipedia) and Def_ArXiv (definitions from research papers on arXiv), designed to assess LLMs performance on complex, real-world mathematical definitions.

我们引入并发布两个新的自动形式化数据集：Def_Wiki（来自维基百科的定义）和 Def_ArXiv（来自 arXiv 研究论文的定义），用于评估大语言模型在复杂、真实世界数学定义上的表现。

We perform a comprehensive error analysis on Isabelle/HOL, identifying key failures in formalizations generated by LLMs spanning across different families, including GPT-4o (OpenAI, 2024b), Llama3 (Llama Team, 2024) and DeepSeekMath (Shao et al., 2024).

我们在 Isabelle/HOL 上做了全面的错误分析，识别出不同系列大语言模型所生成形式化中的关键失败，包括 GPT-4o（OpenAI，2024b）、Llama3（Llama Team，2024）和 DeepSeekMath（Shao 等人，2024）。

We investigate refinement-based strategies, including structured feedback mechanisms from Proof Assistants and instruction-based categorical refinements.

我们考察基于精炼的策略，包括来自证明助手的结构化反馈机制，以及基于指令的分类精炼。

We explore the role of formal definition grounding, investigating how the inclusion of relevant mathematical libraries impacts the ability of LLMs to connect the formalized statements with contextual mathematical elements and relevant premises.

我们探索形式定义锚定的作用，考察纳入相关数学库会如何影响大语言模型把已形式化陈述与上下文中的数学要素及相关前提连接起来的能力。

\sec x+\tan x=\frac{22}{7}

miniF2F	Def_Wiki	Def_ArXiv
1. Suppose that $\sec x+\tan x=\frac{22}{7}$ and that $\csc x+\cot x=\frac{m}{n},$ where $\frac{m}{n}$ is in lowest terms. Find $m+n.$ Show that it is 044. 2. What is the sum of the two values of $x$ for which $(x+3)^{2}=121$ ? Show that it is -6. 3. The product of two positive whole numbers is 2005. If neither number is 1, what is the sum of the two numbers? Show that it is 406. 4. The expression $10x^{2}-x-24$ can be written as $(Ax-8)(Bx+3),$ where $A$ and $B$ are integers. What is $AB+B$ ? Show that it is 12.	1. Definition of Rademacher Complexity: Given a set $A\subseteq\mathbb{R}^{m}$ , the Rademacher complexity of A is defined as follows: $\operatorname{Rad}(A):=\frac{1}{m}\mathbb{E}_{\sigma}\left[\sup_{a\in A}\sum_{i=1}^{m}\sigma_{i}a_{i}\right]$ where $\sigma_{1},\sigma_{2},\dots,\sigma_{m}$ are independent random variables drawn from the Rademacher distribution (i.e. $\Pr(\sigma_{i}=+1)=\Pr(\sigma_{i}=-1)=1/2$ for $i=1,2,\dots,m$ ), and $a=(a_{1},\dots,a_{m})$ . 2. Definition of Polynomial Kernel: For degree- $d$ polynomials, the polynomial kernel is defined as $K(\mathbf{x},\mathbf{y})=(\mathbf{x}^{\mathsf{T}}\mathbf{y}+c)^{d}$ where $\mathbf{x}$ and $\mathbf{y}$ are vectors of size $n$ in the input space, i.e. vectors of features computed from training or test samples and $c\geq 0$ is a free parameter trading off the influence of higher-order versus lower-order terms in the polynomial.	1. Definition of Covering Number: Given a metric space $(\mathcal{S},\rho)$ , and a subset $\tilde{\mathcal{S}}\subset\mathcal{S}$ , we say that a subset $\hat{\mathcal{S}}$ of $\tilde{\mathcal{S}}$ is a $\epsilon$ -cover of $\tilde{\mathcal{S}}$ , if $\forall\tilde{s}\in\tilde{\mathcal{S}}$ , $\exists\hat{s}\in\hat{\mathcal{S}}$ such that $\rho(\tilde{s},\hat{s})\leq\epsilon$ . The $\epsilon$ -covering number of $\tilde{\mathcal{S}}$ is $\mathcal{N}_{\epsilon}(\tilde{\mathcal{S}},\rho)=\min\{\|\hat{\mathcal{S}}\|:\hat{\mathcal{S}}\text{ is an }\epsilon\text{-covering of }\tilde{\mathcal{S}}\}.$ 2. Definition of Trimmed Mean: Consider $n$ copies $X_{1},...,X_{n}$ of a heavy-tailed random variable $X$ such that $\mathbb{E}[X]=\mu,\mathbb{E}[X^{1+\varepsilon}]\leq u$ for some $\varepsilon\in(0,1]$ . The online trimmed mean, for some $\delta\in(0,1)$ is defined as $\hat{\mu}_{O}=\frac{1}{n}\sum_{i=1}^{n}X_{i}\bm{1}\left\{\|X_{i}\|\leq\left(\frac{ui}{\log\delta^{-1}}\right)^{\frac{1}{1+\varepsilon}}\right\}.$

\sec x+\tan x=\frac{22}{7}

miniF2F	Def_Wiki	Def_ArXiv
1. 设 $\sec x+\tan x=\frac{22}{7}$ ，且 $\csc x+\cot x=\frac{m}{n}$ ，其中 $\frac{m}{n}$ 为最简分数。求 $m+n$ 。证明它是 044。 2. 使 $(x+3)^{2}=121$ 的两个 $x$ 值之和是多少？证明它是 -6。 3. 两个正整数的乘积是 2005。若二者都不是 1，这两个数的和是多少？证明它是 406。 4. 表达式 $10x^{2}-x-24$ 可以写成 $(Ax-8)(Bx+3)$ ，其中 $A$ 和 $B$ 是整数。 $AB+B$ 是多少？证明它是 12。	1. Rademacher 复杂度的定义：给定集合 $A\subseteq\mathbb{R}^{m}$ ，A 的 Rademacher 复杂度定义如下： $\operatorname{Rad}(A):=\frac{1}{m}\mathbb{E}_{\sigma}\left[\sup_{a\in A}\sum_{i=1}^{m}\sigma_{i}a_{i}\right]$ 其中 $\sigma_{1},\sigma_{2},\dots,\sigma_{m}$ 是从 Rademacher 分布中抽取的独立随机变量（即对 $i=1,2,\dots,m$ ，有 $\Pr(\sigma_{i}=+1)=\Pr(\sigma_{i}=-1)=1/2$ ），且 $a=(a_{1},\dots,a_{m})$ 。 2. 多项式核的定义：对 $d$ 次多项式，多项式核定义为 $K(\mathbf{x},\mathbf{y})=(\mathbf{x}^{\mathsf{T}}\mathbf{y}+c)^{d}$ ，其中 $\mathbf{x}$ 和 $\mathbf{y}$ 是输入空间中大小为 $n$ 的向量，也就是从训练或测试样本计算出的特征向量， $c\geq 0$ 是在多项式的高阶项与低阶项影响之间做权衡的自由参数。	1. 覆盖数的定义：给定度量空间 $(\mathcal{S},\rho)$ 及其子集 $\tilde{\mathcal{S}}\subset\mathcal{S}$ ，若子集 $\hat{\mathcal{S}}\subset\tilde{\mathcal{S}}$ 满足：对任意 $\tilde{s}\in\tilde{\mathcal{S}}$ ，存在 $\hat{s}\in\hat{\mathcal{S}}$ 使得 $\rho(\tilde{s},\hat{s})\leq\epsilon$ ，则称 $\hat{\mathcal{S}}$ 是 $\tilde{\mathcal{S}}$ 的一个 $\epsilon$ -覆盖。 $\tilde{\mathcal{S}}$ 的 $\epsilon$ -覆盖数为 $\mathcal{N}_{\epsilon}(\tilde{\mathcal{S}},\rho)=\min\{\|\hat{\mathcal{S}}\|:\hat{\mathcal{S}}\text{ 是 }\tilde{\mathcal{S}}\text{ 的一个 }\epsilon\text{-覆盖}\}.$ 2. 截尾均值的定义：考虑重尾随机变量 $X$ 的 $n$ 个副本 $X_{1},...,X_{n}$ ，满足 $\mathbb{E}[X]=\mu$ ， $\mathbb{E}[X^{1+\varepsilon}]\leq u$ ，其中 $\varepsilon\in(0,1]$ 。对某个 $\delta\in(0,1)$ ，在线截尾均值定义为 $\hat{\mu}_{O}=\frac{1}{n}\sum_{i=1}^{n}X_{i}\bm{1}\left\{\|X_{i}\|\leq\left(\frac{ui}{\log\delta^{-1}}\right)^{\frac{1}{1+\varepsilon}}\right\}.$

2 Autoformalization with LLMs

2 用大语言模型做自动形式化

\mathcal{S}

\mathcal{S}

f(s)=\text{LLM}(p_{\text{auto}},\{(s_{i},\phi_{i})\},s),

p_{\text{auto}}

p_{\text{auto}}

2.1 Limitations of Existing Benchmarks

2.1 已有基准的局限

Naturally occurring mathematical statements typically involve complex and abstract mathematical concepts. However, the statements in existing datasets, such as miniF2F (Zheng et al., 2022), primarily consist of basic arithmetic operations and elementary mathematical objects, such as integers, fractions, and real numbers (as shown in Table 1). Such mathematical objects are relatively simple compared to the complex and abstract concepts found in naturally occurring mathematical statements and scientific papers, which may involve higher-level structures like vectors, matrices, and probability. The operations are also limited to simple arithmetic, such as addition, subtraction, multiplication, division, and exponentiation. Studying autoformalization on such datasets, therefore, does not necessarily reflect the challenges of autoformalization in realistic scenarios. However, few benchmarks focus on how to construct complex mathematical statements. Our work aims to address this gap.

自然出现的数学陈述通常涉及复杂而抽象的数学概念。然而，已有数据集中的陈述，例如 miniF2F（Zheng 等人，2022），主要以基本算术运算和初等数学对象为主，例如整数、分数和实数（如表 1 所示）。与自然出现的数学陈述和科学论文中那些可能涉及向量、矩阵和概率等更高层结构的复杂抽象概念相比，这类数学对象相对简单。运算也多限于加减乘除和乘方等简单算术。因此，在这类数据集上研究自动形式化，并不一定能反映真实场景中的挑战。很少有基准关注如何构造复杂的数学陈述。我们的工作旨在填补这一空白。

2.2 Real-World Mathematical Definitions

2.2 真实世界的数学定义

Since extracting high-quality definition statements from general mathematical corpora requires careful curation, we propose a systematic data creation process that balances complexity and diversity. We begin by classifying real-world definitions into two categories: (i) common definitions, which are presented in a global context where the necessary preliminaries are implicit and relatively general, and (ii) specialized definitions, which are typically situated in a local context and rely on explicit and specific preliminaries. Both types present distinct challenges for autoformalization. In the former, the model must infer implicit preliminaries and connect them with existing formal constructs. In the latter, the model must not only formalize the definition but also the associated preliminaries. We ground these two types of definitions in two sources: Wikipedia for common definitions (Def_Wiki) and Arxiv Papers for specialized definitions (Def_ArXiv), as definitions from these two sources are human-written, naturally occurring and likely to have already been validated.

由于从一般数学语料中抽取高质量的定义陈述需要仔细整理，我们提出一套兼顾复杂性与多样性的系统数据创建流程。我们首先把真实世界的定义分成两类：(i) 常见定义，它们出现在全局语境中，所需预备知识是 隐含的 且 相对一般的 ；(ii) 专门定义，它们通常处于局部语境中，并依赖 明确的 、 具体的 预备知识。两类定义都给自动形式化带来不同挑战。对前者，模型必须推断隐含的预备知识，并把它们与已有的形式构造连接起来。对后者，模型不仅要形式化定义本身，还要形式化相关的预备知识。我们把这两类定义分别落实到两个来源上：用维基百科承载常见定义（Def_Wiki），用 arXiv 论文承载专门定义（Def_ArXiv），因为这两个来源中的定义是人写的、自然出现的，并且很可能已经过核验。

To construct a representative instance for Def_Wiki and Def_Arxiv, we focus on definitions from the field of machine learning, as this domain offers a sufficient number of novel, diverse, and relatively unformalized definitions. Moreover, the task of formalizing such definitions holds practical value for the AI community. The detailed operational steps are provided in Appendix A . A quality check was performed to ensure that the selected definitions exhibit high diversity and present complementary challenges. This process yielded 56 definitions for Def_Wiki and 30 definitions for Def_Arxiv. This number is expected, as novel definitions in the real world are relatively scarce compared to example questions in mathematics (such as those in miniF2F), which are often closer in nature to synthetically generated content. Although the resulting datasets are relatively small in scale, they are sufficient to expose the core challenges of autoformalization in real-world scenarios. The size of the datasets is not the primary factor determining the significance, transferability, or robustness of the findings. Exploring additional scientific domains and expanding the dataset further are promising directions for future work.

为构造 Def_Wiki 和 Def_ArXiv 的代表性实例，我们聚焦机器学习领域的定义，因为这一领域既有足够多新颖、多样且相对尚未被形式化的定义，把这些定义形式化对人工智能社区也具有实际价值。详细操作步骤见 附录 A 。我们做了质量检查，以确保所选定义具有较高多样性，并带来互补的挑战。这一过程为 Def_Wiki 得到 56 条定义，为 Def_ArXiv 得到 30 条定义。这一规模是可以预期的，因为真实世界中的新定义，相对数学中的例题（例如 miniF2F 中的题目，它们在性质上往往更接近合成内容）更为稀缺。尽管得到的数据集规模相对较小，但它们足以暴露真实场景中自动形式化的核心挑战。数据集大小并不是决定发现之意义、可迁移性或稳健性的首要因素。探索更多科学领域并进一步扩大数据集，是未来工作中有前景的方向。

We compare the quality of miniF2F with the target definition datasets. MiniF2F is significantly less abstract, complex and diverse, as intuitively shown in the randomly chosen examples in Table 1. The data properties are summarized in Table 5 in Appendix . Definition datasets exhibit higher means for the number of tokens, mathematical objects, and formulae per example, indicating that they are significantly more complex. Additionally, definition datasets have higher standard deviations, suggesting greater diversity among samples.

我们把 miniF2F 的质量与目标定义数据集做比较。如表 1 中随机选取的例子直观所示，miniF2F 在抽象程度、复杂性和多样性上都明显更低。数据性质汇总于 附录 中的表 5。定义数据集在每个样本的词元数、数学对象数和公式数上具有更高的均值，表明它们明显更复杂。此外，定义数据集具有更高的标准差，说明样本之间的多样性更大。

The proposed benchmarks contain only definitions in LaTeX format. We did not include ground-truth formal code for the following reasons: 1. Including such code could increase the risk of data leakage, as ground-truth formalizations from publicly available datasets may have been seen by LLMs, whose training data is not fully disclosed, making it difficult to determine whether future improvements genuinely address the challenges posed by our benchmark or simply reflect prior exposure. 2. A single mathematical statement can have multiple correct formalizations. An autoformalized output that differs from the reference does not necessarily indicate incorrect formalization. 3. The main purpose of ground-truth formal code is to evaluate autoformalization. However, the syntactic correctness of formalized code can be rigorously and automatically verified using theorem provers (Zhang et al., 2024), while semantic consistency can potentially be assessed in a reference-free manner via LLM-as-Judges (Zhang et al., 2025). Moreover, manual inspection of autoformalized code does not require ground-truth formalizations.

所提出的基准只包含 LaTeX 格式的定义。我们没有纳入金标准形式代码，原因如下：1. 纳入这类代码可能增加数据泄漏风险，因为公开数据集中的金标准形式化可能已被训练数据并未完全披露的大语言模型见过，从而难以判断未来的改进究竟是真正应对了本基准提出的挑战，还是只反映了先前见过这些内容。2. 同一条数学陈述可以有多种正确的形式化。自动形式化输出与参考答案不同，并不一定意味着形式化不正确。3. 金标准形式代码的主要用途是评估自动形式化。然而，形式化代码的句法正确性可以用定理证明器严格、自动地核验（Zhang 等人，2024），语义一致性则有可能通过以大语言模型为评判者的方式，做无参考评估（Zhang 等人，2025）。此外，对自动形式化代码做人工检查，也不需要金标准形式化。

\uparrow

Prompt Strategy	Model	Pass $\uparrow$	FEO $\uparrow$	TRO $\downarrow$	IVI $\downarrow$	SYN $\downarrow$	UDF $\downarrow$	TUF $\downarrow$
miniF2F-Test
ZS	DeepSeekMath-7B	3.28	12.79	18.44	0.00	50.00	14.34	9.43
ZS + Binary		2.05	6.73	2.46	0.00	79.91	5.33	2.05
ZS	Llama3-8B	4.92	20.70	4.51	0.41	29.51	38.52	18.85
ZS + Binary		3.69	20.52	3.28	0.41	33.20	39.75	20.49
ZS	GPT-4o	25.41	48.90	1.23	1.23	6.15	23.77	7.38
ZS + Binary		29.10	53.90	2.05	1.23	6.15	21.72	8.20
Def_Wiki-Test
ZS	DeepSeekMath-7B	10.87	17.75	34.78	2.17	30.43	26.09	2.17
ZS + Binary		6.52	7.73	8.70	0.00	69.57	21.74	2.17
ZS	Llama3-8B	0.00	2.80	0.00	23.91	56.52	32.61	4.35
ZS + Binary		2.17	3.71	0.00	26.09	52.17	30.43	2.17
ZS	GPT-4o	10.87	16.12	8.70	8.70	19.57	50.00	13.04
ZS + Binary		13.04	18.30	8.70	6.52	17.39	50.00	13.04
Def_ArXiv
ZS	DeepSeekMath-7B	13.33	14.69	16.67	0.00	40.00	36.67	13.33
ZS + Binary		3.33	3.33	6.67	0.00	66.67	33.33	3.33
ZS	Llama3-8B	0.00	2.67	0.00	13.33	70.00	40.00	6.67
ZS + Binary		3.33	5.83	0.00	20.00	60.00	33.33	6.67
ZS	GPT-4o	13.33	19.30	0.00	0.00	40.00	56.66	6.67
ZS + Binary	GPT-4o	16.67	24.30	0.00	0.00	33.33	53.33	6.67

\uparrow

提示策略	模型	Pass $\uparrow$	FEO $\uparrow$	TRO $\downarrow$	IVI $\downarrow$	SYN $\downarrow$	UDF $\downarrow$	TUF $\downarrow$
miniF2F-Test
ZS	DeepSeekMath-7B	3.28	12.79	18.44	0.00	50.00	14.34	9.43
ZS + Binary		2.05	6.73	2.46	0.00	79.91	5.33	2.05
ZS	Llama3-8B	4.92	20.70	4.51	0.41	29.51	38.52	18.85
ZS + Binary		3.69	20.52	3.28	0.41	33.20	39.75	20.49
ZS	GPT-4o	25.41	48.90	1.23	1.23	6.15	23.77	7.38
ZS + Binary		29.10	53.90	2.05	1.23	6.15	21.72	8.20
Def_Wiki-Test
ZS	DeepSeekMath-7B	10.87	17.75	34.78	2.17	30.43	26.09	2.17
ZS + Binary		6.52	7.73	8.70	0.00	69.57	21.74	2.17
ZS	Llama3-8B	0.00	2.80	0.00	23.91	56.52	32.61	4.35
ZS + Binary		2.17	3.71	0.00	26.09	52.17	30.43	2.17
ZS	GPT-4o	10.87	16.12	8.70	8.70	19.57	50.00	13.04
ZS + Binary		13.04	18.30	8.70	6.52	17.39	50.00	13.04
Def_ArXiv
ZS	DeepSeekMath-7B	13.33	14.69	16.67	0.00	40.00	36.67	13.33
ZS + Binary		3.33	3.33	6.67	0.00	66.67	33.33	3.33
ZS	Llama3-8B	0.00	2.67	0.00	13.33	70.00	40.00	6.67
ZS + Binary		3.33	5.83	0.00	20.00	60.00	33.33	6.67
ZS	GPT-4o	13.33	19.30	0.00	0.00	40.00	56.66	6.67
ZS + Binary	GPT-4o	16.67	24.30	0.00	0.00	33.33	53.33	6.67

3 Empirical Evaluation

3 实证评估

Empirical Setup. Isabelle/HOL was chosen as the representative formal language due to its widespread adoption within the formal mathematics community and its ability to provide specific information about the types of errors encountered. Moreover, Isabelle employs a declarative proof language that is closer to structured natural language, making it well-suited for exploring autoformalization of complex natural language statements. We prioritize an in-depth analysis of a single formal language over a broad comparison across multiple languages. We believe this approach lays the foundation for future work aimed at exploring the behavior of LLMs in alternative formal systems. We evaluate three LLMs with different features: DeepSeekMath-7B (Shao et al., 2024), Llama3-8B (Llama Team, 2024) and GPT-4o (OpenAI, 2024b). DeepSeekMath-7B is an open-sourced LLM trained specifically for mathematics. As a smaller model, it has demonstrated comparable mathematical reasoning performance as in GPT-4 (OpenAI, 2024a), and strong few-shot autoformalization performance on miniF2F with Isabelle. This superiority makes it a good representative of smaller but specialized LLMs. LLama3-8B is a smaller open-sourced foundation LLM with no specific emphasis on math. GPT-4o is widely acknowledged as one of the state-of-the-art LLMs. For reproducibility, greedy decoding is used for generation in all settings.

实验设置。 我们选择 Isabelle/HOL 作为代表性形式语言，因为它在形式数学社区中被广泛采用，并且能够提供所遇错误类型的具体信息。此外，Isabelle 采用一种更接近结构化自然语言的声明式证明语言，适合探索复杂自然语言陈述的自动形式化。我们优先对单一形式语言做深入分析，而不是在多种语言之间做宽泛比较。我们认为，这一做法为未来考察大语言模型在其他形式系统中的行为奠定了基础。我们评估三家具有不同特点的大语言模型：DeepSeekMath-7B（Shao 等人，2024）、Llama3-8B（Llama Team，2024）和 GPT-4o（OpenAI，2024b）。DeepSeekMath-7B 是专门面向数学训练的开源大语言模型。作为较小的模型，它已展现出与 GPT-4（OpenAI，2024a）相当的数学推理表现，并在用 Isabelle 处理 miniF2F 时具有较强的少样本自动形式化能力。这一优势使它成为较小但专门化的大语言模型的良好代表。Llama3-8B 是较小的开源基础大语言模型，并不特别强调数学。GPT-4o 被广泛视为最先进的大语言模型之一。为便于复现，所有设定下的生成都使用贪心解码。

Evaluation Metrics. The success rate of passing the check by the Isabelle Proof Assistant across the tested dataset is used as the first metric. We assume that a formalized code instance with the first error occurring later in the code reflects, as a proxy, the level of autoformalization. Thus, we evaluate such by calculating the proportion of correct lines (up to the first error) within the main body of the code. For syntactically correct instances, this value is equal to 1. To better monitor the occurrence of errors, we group them into three categories: Syntax Errors (SYN), Undefined Item Errors (UDF), and Type Unification Failed Errors (TUF). For each category, we calculate the percentage of incorrect formalized codes caused by errors in that category.

评估指标。 我们以在被测数据集上通过 Isabelle 证明助手检查的成功率作为第一项指标。我们假定，形式化代码实例中首次出错位置越靠后，就越能作为自动形式化水平的代理。因此，我们通过计算代码主体中（截至首次出错）正确行的比例来评估这一点。对句法正确的实例，该值为 1。为更好地监测错误出现情况，我们把错误分成三类：句法错误（SYN）、未定义项错误（UDF）和类型合一失败错误（TUF）。对每一类，我们计算由该类错误导致的不正确形式化代码所占百分比。

3.1 Zero-Shot Prompting & Binary Refinement

3.1 零样本提示与二元精炼

In order to understand the challenges in autoformalizing mathematical definitions with LLMs, we perform a preliminary analysis on miniF2F (Zheng et al., 2022), Def_Wiki and Def_ArXiv using zero-shot prompting (ZS) and binary refinement. With binary refinement, we aim to assess the capabilities of LLMs for error correction by providing them with the formal code generated via ZS, along with the syntactic correctness evaluated using the proof assistant (i.e., “correct”, “incorrect”). From the results reported in Table 2, we can derive the following observations:

为理解用大语言模型自动形式化数学定义时的挑战，我们在 miniF2F（Zheng 等人，2022）、Def_Wiki 和 Def_ArXiv 上，用零样本提示（ZS）和二元精炼做了初步分析。借助二元精炼，我们希望评估大语言模型的纠错能力：向它们提供由 ZS 生成的形式代码，以及用证明助手评估得到的句法正确性（即“正确”“不正确”）。根据表 2 报告的结果，我们可以得出如下观察：

Def_Wiki and Def_ArXiv are significantly more challenging than miniF2F. When performing autoformalization on Def_Wiki and Def_ArXiv, GPT-4o achieves a significantly lower success rates (-13.78% on average) and FEO (-31.90% on average) compared to results on miniF2F-Test.

Def_Wiki 和 Def_ArXiv 明显比 miniF2F 更具挑战性。 在 Def_Wiki 和 Def_ArXiv 上做自动形式化时，GPT-4o 的成功率（平均低 13.78%）和 FEO（平均低 31.90%）都明显低于在 miniF2F-Test 上的结果。

LLMs can provide false preambles when performing autoformalization. In Table 2, the percentage of Invalid Inputs errors (IVI) can be non-zero. Errors in this category are caused by either non-existent preambles or invalid file formats in structure. For Llama3-8B the latter is more common whereas for GPT-4o, we observe that the dominant cause is the generation of non-existent preambles, showing that GPT-4o do not perfectly generalize in recognizing the names of preambles.

大语言模型在做自动形式化时可能给出虚假导言。 在表 2 中，无效输入错误（IVI）的百分比可以不为零。这类错误由不存在的导言或无效的文件结构格式引起。对 Llama3-8B 来说，后者更常见；而对 GPT-4o，我们观察到主导原因是生成了不存在的导言，说明 GPT-4o 在识别导言名称上并没有完美泛化。

\Rightarrow

Category	Reasons
SYN	1. Invalid Symbol Format. Isabelle uses symbols like “<Rightarrow>” to represent “\Rightarrow ( $\Rightarrow$ )” in LaTeX. GPT-4o does not strictly follow this behaviour. A symbol in its formalized code starting with “<” can miss “>” at the end so that the relevant symbol is not valid. 2. Confusion of Mapping between LaTeX Mathematical Symbols and Isabelle Symbols. Not all natural language symbols in LaTeX have a similar corresponding version in Isabelle symbols. In natural language mathematics we use different mathematical fonts such as “\mathcal ( $\mathcal{A}$ )” to distinguish items. Isabelle uses “<A>” to represent this LaTeX symbol. However, GPT-4o would pretend the existence of a symbol named <mathcal> and use it for autoformalization. 3. Unaware of Name Conflict. Some keywords such as “instance” are reserved by Isabelle/HOL and they cannot be used as the name of a new item. 4. Incorrect Stylistic Usage of Symbols or Operators. Some symbols or operators require specific usage which is not in the same style as in natural language. The incorrect usage of them in formalized code generated by GPT-4o can lead to syntax errors.
UDF	1. Items not defined. Formalization requires every mentioned item to be clearly defined in the local context or preambles. During autoformalization, GPT-4o could refer to items that are not defined in both sources.
TUF	1. Mismatch between Types in Definition and Types in Actual Usage. There are some operators or functions which have been clearly defined about the types of their operands or parameters. When using these operators or functions, the types of actual operands or parameters need to match the types in the definitions exactly. GPT-4o would produce mismatched types in the formalized codes and introduce TUF errors.

\Rightarrow

类别	原因
SYN	1. 无效的符号格式。 Isabelle 用 “<Rightarrow>” 这类符号来表示 LaTeX 中的 “\Rightarrow ( $\Rightarrow$ )”。GPT-4o 并不严格遵循这一做法。其形式化代码中以 “<” 开头的符号，可能在末尾缺少 “>”，从而使相应符号无效。 2. LaTeX 数学符号与 Isabelle 符号之间的映射混淆。并非所有 LaTeX 中的自然语言符号都在 Isabelle 符号中有相近的对应版本。在自然语言数学中，我们用不同数学字体，例如 “\mathcal ( $\mathcal{A}$ )”，来区分对象。Isabelle 用 “<A>” 表示这一 LaTeX 符号。然而，GPT-4o 会假装存在名为 <mathcal> 的符号，并把它用于自动形式化。 3. 未意识到名称冲突。某些关键词，例如 “instance”，被 Isabelle/HOL 保留，不能用作新对象的名称。 4. 符号或算子的风格用法不正确。某些符号或算子需要特定用法，这种用法与自然语言中的风格并不相同。GPT-4o 生成的形式化代码中对它们的不正确使用，会导致句法错误。
UDF	1. 对象未被定义。形式化要求每一个被提到的对象都在局部上下文或导言中被清楚定义。在自动形式化过程中，GPT-4o 可能引用在这两个来源中都未定义的对象。
TUF	1. 定义中的类型与实际使用中的类型不匹配。有些算子或函数已经明确给出了其操作数或参数的类型。使用这些算子或函数时，实际操作数或参数的类型需要与定义中的类型精确匹配。GPT-4o 会在形式化代码中产生不匹配的类型，并引入 TUF 错误。

Specialized smaller models can reach the same level of success rate as larger LLMs. As a model designed specifically for mathematics, DeepSeekMath-7B can achieve a similar success rate as GPT-4o. Although Llama3-8B has a larger model size, its generalization ability on definitions is limited. Additionally, DeepSeekMath-7B exhibits a lower percentage of undefined type names errors (UDF). However, one disadvantage of the specialized model is that its formalizations have a higher percentage of time run-out issues (TRO). This is likely caused by the bias introduced during the fine-tuning phase on theorem proving which can lead the model to generate unsolicited proofs.

专门化的较小模型可以达到与更大模型同一水平的成功率。 作为专门面向数学设计的模型，DeepSeekMath-7B 可以达到与 GPT-4o 相近的成功率。尽管 Llama3-8B 的模型规模更大，它在定义上的泛化能力却有限。此外，DeepSeekMath-7B 表现出更低的未定义类型名错误（UDF）百分比。不过，专门化模型的一个缺点是，其形式化中超时问题（TRO）的百分比更高。这很可能是由定理证明微调阶段引入的偏置造成的，这种偏置可能让模型生成未被要求的证明。

Small LLMs possess limited binary self-correction capabilities. With binary refinement, GPT-4o produces formal codes with a higher success rate on all three datasets, whereas for DeepSeekMath-7B this mechanism leads to a performance decrease. LLama3-8B also fails to self-correct its autoformalization results on miniF2F. This behavior suggests that self-refinement exceeds the capabilities of smaller LLMs.

较小的大语言模型只具备有限的二元自纠正能力。 借助二元精炼，GPT-4o 在全部三个数据集上都生成了成功率更高的形式代码，而对 DeepSeekMath-7B，这一机制反而导致性能下降。Llama3-8B 也未能在 miniF2F 上纠正自己的自动形式化结果。这一行为表明，自我精炼超出了较小模型的能力范围。

3.1.1 Error Analysis & Interventions To understand potential interventions for improving autoformalization, we qualitatively analyze error patterns on the development set of Def_Wiki. Our analysis is based on the results obtained via GPT-4o, given its better performances on ZS and binary refinement. The main reasons for failure identified through our analysis are summarized in Table 3, with additional examples reported in Appendix .

3.1.1 错误分析与干预 为理解改进自动形式化的可能干预，我们在 Def_Wiki 的开发集上定性分析错误模式。分析基于 GPT-4o 的结果，因为它在 ZS 和二元精炼上的表现更好。通过分析识别出的主要失败原因汇总于表 3，更多例子见 附录 。

We observe that syntactic errors (SYN) exhibit the most variety, suggesting that GPT-4o may struggle to follow syntactic rules in Isabelle/HOL if not explicitly instructed. Type unification errors (TUF) suggest that GPT-4o may struggle with the exact usage of defined Isabelle items. To improve these issues, we investigate a Categorical Refinement (CR) method. CR involves designing specific additive instructions that constraint the behaviors leading to errors identified in the qualitative analysis.

我们观察到，句法错误（SYN）的种类最多，说明若没有被明确指示，GPT-4o 可能难以遵循 Isabelle/HOL 中的句法规则。类型合一错误（TUF）则表明，GPT-4o 可能难以精确使用已定义的 Isabelle 对象。为改进这些问题，我们考察一种 分类精炼 （Categorical Refinement，CR）方法。CR 通过设计特定的附加指令，来约束定性分析中识别出的、会导向错误的行为。

Similarly, for syntactic errors (SYN), causes 1, 2, and 3 in Table 3 can be addressed with rule-based algorithms that refine formal codes at the symbolic level (Symbolic Refinement, SR). Undefined errors (UDF), on the other hand, indicate that although GPT-4o can refer to external formal mathematical items, it remains unaware of the location or existence of relevant libraries. To alleviate UDF errors, we propose the process of Formal Definition Grounding (FDG): linking mathematical objects mentioned in natural language statements to their formal definitions in formal libraries, and incorporating this information as contextual elements for formalizations.

类似地，对句法错误（SYN），表 3 中的原因 1、2 和 3 可以用在符号层面精炼形式代码的基于规则的算法来处理（ 符号精炼 ，Symbolic Refinement，SR）。另一方面，未定义错误（UDF）表明，虽然 GPT-4o 可以引用外部的形式数学对象，它仍然不清楚相关库的位置或是否存在。为缓解 UDF 错误，我们提出 形式定义锚定 （Formal Definition Grounding，FDG）过程：把自然语言陈述中提到的数学对象，与形式库中的形式定义联系起来，并把这些信息作为形式化的上下文要素纳入。

3.2 Categorical Refinement

3.2 分类精炼

Figure 2: Error rates of different refinement methods on GPT-4o. Variants include: (ZS): zero-shot autoformalization; ((ZS)+Binary): binary refinement on (zero-shot) formal codes; ((ZS)+Detailed): detailed refinement on (zero-shot) formal codes; ((ZS)+CR-SYN/UDF/TUF): plain refinement on (zero-shot) formal codes with SYN/UDF/TUF categorical refinement instructions; ((ZS)+Detailed+CR-SYN/UDF/TUF): detailed refinement on (zero-shot) formal codes with SYN/UDF/TUF categorical refinement instructions.

图 2：不同精炼方法在 GPT-4o 上的错误率。变体包括：(ZS)：零样本自动形式化；((ZS)+Binary)：对（零样本）形式代码做二元精炼；((ZS)+Detailed)：对（零样本）形式代码做详细精炼；((ZS)+CR-SYN/UDF/TUF)：对（零样本）形式代码做带 SYN/UDF/TUF 分类精炼指令的普通精炼；((ZS)+Detailed+CR-SYN/UDF/TUF)：对（零样本）形式代码做带 SYN/UDF/TUF 分类精炼指令的详细精炼。

In order to better understand the refinement capabilities of GPT-4o, we investigate a set of error correction strategies: (i) Plain: provide LLMs with previously generated formal codes; (ii) Binary: additionally, provide LLMs with the correctness status of the formal code; (iii) Detailed: instead of just the binary correctness status, provide LLMs with the details of type, message, and line location of individual errors in the code.

为更好地理解 GPT-4o 的精炼能力，我们考察一组纠错策略：(i) 普通精炼：向大语言模型提供先前生成的形式代码；(ii) 二元精炼：另外向模型提供形式代码的正确性状态；(iii) 详细精炼：不再只提供二元正确性状态，而是向模型提供代码中各个错误的类型、消息和行位置细节。

In addition, to evaluate categorical refinement, we design specific instructions for each category of errors based on our qualitative analysis (Table 3). We report the error rate results of different refinement methods on GPT-4o in bar charts in Figure 2. All prompts used for categorical refinement and additional empirical results are provided in Appendix .

此外，为评估分类精炼，我们根据定性分析（表 3）为每一类错误设计了特定指令。我们把不同精炼方法在 GPT-4o 上的错误率结果以柱状图报告于图 2。分类精炼所用的全部提示以及额外实证结果见 附录 。

Providing LLMs with more information about individual errors is more effective than simply indicating binary correctness. As shown in Figure 2(a), both binary and detailed refinements can reduce the overall error rate across all the datasets, with detailed refinement fixing more errors on miniF2F-Test and Def_Wiki-Test. For SYN errors, although there is no clear trend indicating that one refinement outperforms the other, both refinements lead to a lower error rate compared to zero-shot autoformalization. Detailed refinement also decreases the percentage of UDF errors as shown in Figure 2(c). These performance gains suggest that detailed refinement improves the quality of autoformalized codes. For TUF errors, applying both refinements does not consistently result in a lower error rate, indicating that errors in this category are more difficult for LLMs to fix.

向大语言模型提供关于各个错误的更多信息，比只标明二元正确性更有效。 如图 2(a) 所示，二元精炼和详细精炼都能降低所有数据集上的总体错误率，其中详细精炼在 miniF2F-Test 和 Def_Wiki-Test 上修正了更多错误。对 SYN 错误，虽然没有明确趋势表明某一种精炼始终优于另一种，但两种精炼相对于零样本自动形式化都带来了更低的错误率。如图 2(c) 所示，详细精炼也降低了 UDF 错误的百分比。这些性能收益表明，详细精炼改善了自动形式化代码的质量。对 TUF 错误，同时应用这两种精炼并不总能带来更低的错误率，说明这一类错误对大语言模型来说更难修正。

Categorical refinement reduces error rates. As shown in Figure 2(a), across all datasets, the refinement method that achieves the lowest overall error rate incorporates one of the instructions for categorical refinement, highlighting the efficacy of this mechanism. However, when categorical refinement is applied without error details, such improvements do not occur. We hypothesize that this is because categorical instructions serve as constraints, making it more difficult for the target LLM to follow them without more detailed error information for individual instances. Once such information is provided, the LLM receives sufficient information to adhere to the categorical refinement instructions.

分类精炼会降低错误率。 如图 2(a) 所示，在所有数据集上，达到最低总体错误率的精炼方法都纳入了某一条分类精炼指令，凸显了这一机制的效力。不过，当分类精炼在没有错误细节的情况下应用时，这样的改进并不会出现。我们猜想，这是因为分类指令起着约束作用，若没有针对各个实例的更详细错误信息，目标模型更难遵循它们。一旦提供了这些信息，模型就获得了足够信息来遵守分类精炼指令。

Categorical refinement can effectively reduce errors for specific categories. As shown in Figure 2(b), the method with the lowest SYN error rate on miniF2F-Test is plain refinement with SYN categorical refinement instructions, whereas on the other two datasets the best performing method is SYN categorical refinement with error details. In Figure 2(c), UDF categorical refinement with error details also leads to the lowest UDF error rate on all three datasets. Similarly in Figure 2(d), TUF categorical refinement with error details achieves the lowest TUF error rate on two out of the three datasets. These results collectively demonstrate the effectiveness of the categorical refinement as a control mechanism for autoformalization. The only exception is TUF errors within the Def_ArXiv dataset, which again highlights the difficulty of fixing TUF errors.

分类精炼可以有效降低特定类别的错误。 如图 2(b) 所示，在 miniF2F-Test 上 SYN 错误率最低的方法是带 SYN 分类精炼指令的普通精炼，而在另外两个数据集上，表现最好的方法是带错误细节的 SYN 分类精炼。在图 2(c) 中，带错误细节的 UDF 分类精炼也在全部三个数据集上达到了最低的 UDF 错误率。类似地，在图 2(d) 中，带错误细节的 TUF 分类精炼在三个数据集中的两个上达到了最低的 TUF 错误率。这些结果共同表明，分类精炼作为自动形式化的一种控制机制是有效的。唯一的例外是 Def_ArXiv 数据集中的 TUF 错误，这再次凸显了修正 TUF 错误的困难。

Figure 3: Gain of error rates when testing autoformalization with different methods compared to direct test. We evaluate results on zero-shot autoformalized codes and (zero-shot) formal codes with detailed refinement. Testing variants include: (SR): Symbolic Refinement; (Post-FDG): Postprocessing with Formal Definition Grounding.

图 3：与直接测试相比，用不同方法测试自动形式化时的错误率增益。我们在零样本自动形式化代码，以及经过详细精炼的（零样本）形式代码上评估结果。测试变体包括：(SR)：符号精炼；(Post-FDG)：用形式定义锚定做后处理。

3.3 Symbolic Refinement

3.3 符号精炼

Based on reasons 1 and 2 of SYN errors in Table 3, we defined two rules for implementing Symbolic Refinement: (1) if a symbol in the formal code is likely to be an Isabelle symbol (i.e., it starts with “<” but misses “>”), we add “>” at its end to ensure that the symbol follows Isabelle’s format; (2) for non-existent symbols of mathematical fonts, we replace them with relevant symbols in Isabelle.

根据表 3 中 SYN 错误的原因 1 和 2，我们为实施符号精炼定义了两条规则：(1) 若形式代码中的某个符号很可能是 Isabelle 符号（即它以 “<” 开头但缺少 “>”），我们就在其末尾补上 “>”，以确保该符号遵循 Isabelle 的格式；(2) 对不存在的数学字体符号，我们用 Isabelle 中的相应符号替换它们。

The differences in error rates between our methods and direct testing of unmodified autoformalized code are illustrated as bar charts in Figure 3.

我们的方法与直接测试未经修改的自动形式化代码之间的错误率差异，以柱状图展示于图 3。

Symbolic Refinement can effectively reduce SYN errors in the generated formal codes on definition datasets. In Figures 3(b) and 3(e), both applying symbolic refinement (SR) alone and in combination with Post-FDG lead to a lower SYN error rate on Def_Wiki-Test. On Def_ArXiv, Figures 3(c) and 3(f) similarly shows that applying SR alone results in a reduction of SYN errors. These results suggest that SR is an effective approach for addressing SYN errors. On miniF2F-Test, however, SR does not impact the error rates because SR is closely tied to specific error patterns in the dataset.

符号精炼可以有效降低定义数据集上所生成形式代码中的 SYN 错误。 在图 3(b) 和 3(e) 中，单独应用符号精炼（SR），以及把它与 Post-FDG 组合，都会在 Def_Wiki-Test 上带来更低的 SYN 错误率。在 Def_ArXiv 上，图 3(c) 和 3(f) 同样表明，单独应用 SR 会减少 SYN 错误。这些结果说明，SR 是处理 SYN 错误的有效方法。不过，在 miniF2F-Test 上，SR 并不影响错误率，因为 SR 与该数据集中的特定错误模式紧密相关。

3.4 Post-FDG

For implementing FDG, we first extracted external formal definitions of mathematical items and their sources from the Isabelle/HOL library. Then we filtered the extracted definitions to retain only those likely relevant to the autoformalization task on the datasets. Finally, for each individual instance in Def_Wiki and Def_ArXiv, we manually determined which formal definitions should be provided as contextual elements. For miniF2F, we simply selected the definitions of real and complex numbers as the relevant definitions. Post-FDG (FDG via postprocessing) explicitly augments the preambles generated by LLMs with the sources of relevant formal definitions in formal libraries.

为实施 FDG，我们首先从 Isabelle/HOL 库中抽取数学对象的外部形式定义及其来源。随后，我们过滤所抽取的定义，只保留那些很可能与这些数据集上的自动形式化任务相关的定义。最后，对 Def_Wiki 和 Def_ArXiv 中的每个实例，我们人工确定应当作为上下文要素提供哪些形式定义。对 miniF2F，我们只选取实数和复数的定义作为相关定义。Post-FDG（通过 后处理 做 FDG）明确用形式库中相关形式定义的来源，来增强大语言模型生成的导言。

Autoformalization performance can be underestimated without including contextual information. In Figure 3, without modifying the main body of the formalization, replacing the preambles with possible preambles via Post-FDG directly leads to higher overall syntactic correctness. On miniF2F-Test, this setting only considers sources containing formal definitions of real and complex numbers, yet it increases overall syntactic correctness by more than 40%.

若不纳入上下文信息，自动形式化的性能可能被低估。 在图 3 中，在不修改形式化主体的情况下，通过 Post-FDG 把导言替换为可能的导言，直接带来了更高的总体句法正确性。在 miniF2F-Test 上，这一设定只考虑包含实数和复数形式定义的来源，却把总体句法正确性提高了超过 40%。

FDG can reduce the occurrence of errors caused by referring to undefined mathematical objects. In Figure 3, the UDF error category has the most significant improvement from Post-FDG. Even when LLMs do not include the exact library that contains relevant mathematical items, they tend to use conventional names for the autoformalization task. By importing the appropriate theory files, these previously undefined items can be linked to the formalization, thereby reducing UDF errors.

FDG 可以减少因引用未定义数学对象而造成的错误。 在图 3 中，UDF 错误类别从 Post-FDG 中获得了最显著的改进。即使大语言模型没有纳入包含相关数学对象的精确库，它们在自动形式化任务中也倾向于使用常规名称。通过导入恰当的理论文件，这些先前未定义的对象就可以与形式化联系起来，从而减少 UDF 错误。

Errors in autoformalized codes for definition datasets are more likely to be entangled than those in the miniF2F dataset. In Figure 3(a) and Figure 3(d), Post-FDG leads to positive performance gains across all error categories. However, in Figures 3(b), 3(c), 3(e) and 3(f), while UDF error rates decrease, error rates in other categories can increase. A similar trend is observed when applying SR, where a reduction in SYN errors can coincide with increases in errors from the other two categories. This phenomenon suggests that because definition datasets are more complex, LLMs are more prone to generating errors from different categories in one code block during the autoformalization process.

定义数据集上自动形式化代码中的错误，比 miniF2F 数据集中的错误更可能相互纠缠。 在图 3(a) 和 图 3(d) 中，Post-FDG 在所有错误类别上都带来了正的性能增益。然而，在图 3(b)、3(c)、3(e) 和 3(f) 中，虽然 UDF 错误率下降，其他类别的错误率却可能上升。应用 SR 时也观察到类似趋势：SYN 错误的减少，可能伴随着另外两类错误的增加。这一现象表明，由于定义数据集更复杂，大语言模型在自动形式化过程中更容易在同一段代码中生成不同类别的错误。

3.5 Generalizability to Lean4

3.5 向 Lean4 的可推广性

Prompt Strategy miniF2F Def_Wiki Def_Arxiv ZS 13.93 5.36 0.00 (ZS)+D 15.98 7.14 6.67 (ZS)+D+CR-SYN 16.80 8.93 6.67 (ZS)+D+CR-UDF 13.52 10.71 6.67 (ZS)+D+CR-TUF 15.57 10.71 6.67 Table 4: GPT-4o pass rates with Lean4. ((ZS)+D): detailed refinement on (zero-shot) formal codes.

Prompt Strategy	miniF2F	Def_Wiki	Def_Arxiv
ZS	13.93	5.36	0.00
(ZS)+D	15.98	7.14	6.67
(ZS)+D+CR-SYN	16.80	8.93	6.67
(ZS)+D+CR-UDF	13.52	10.71	6.67
(ZS)+D+CR-TUF	15.57	10.71	6.67

提示策略 miniF2F Def_Wiki Def_Arxiv ZS 13.93 5.36 0.00 (ZS)+D 15.98 7.14 6.67 (ZS)+D+CR-SYN 16.80 8.93 6.67 (ZS)+D+CR-UDF 13.52 10.71 6.67 (ZS)+D+CR-TUF 15.57 10.71 6.67 表 4：GPT-4o 在 Lean4 上的通过率。（ (ZS)+D ）：对（零样本）形式代码做详细精炼。

提示策略	miniF2F	Def_Wiki	Def_Arxiv
ZS	13.93	5.36	0.00
(ZS)+D	15.98	7.14	6.67
(ZS)+D+CR-SYN	16.80	8.93	6.67
(ZS)+D+CR-UDF	13.52	10.71	6.67
(ZS)+D+CR-TUF	15.57	10.71	6.67

We further explore the generalizability of our methods to formal languages beyond Isabelle/HOL. We select Lean4 (de Moura et al., 2015) as a representative target due to its increasing popularity and widespread use. The Categorical Refinement (CR) method can be applied to Lean4 with only minor prompt modifications. In contrast, exploring the generalizability of Symbolic Refinement and Formal Definition Grounding requires system-specific designs, which fall outside the scope of this paper. We investigate the generalizability of CR on Lean4 and report the pass rates across three datasets using various strategies in Table 4.

我们进一步探索这些方法向 Isabelle/HOL 以外的形式语言推广的能力。我们选择 Lean4（de Moura 等人，2015）作为代表性目标，因为它正变得越来越流行、使用也越来越广泛。分类精炼（CR）方法只需对提示做少量修改，就可以应用到 Lean4。相比之下，探索符号精炼和形式定义锚定的可推广性需要针对具体系统的设计，这超出了本文范围。我们在 Lean4 上考察 CR 的可推广性，并在表 4 中报告三种数据集上、各种策略下的通过率。

Definitions present greater complexity for autoformalization in Lean4. The pass rates of GPT-4o on definitions are consistently lower than those on miniF2F. For example, on Def_Arxiv, GPT-4o fails to correctly formalize any of the 30 definitions. Moreover, we observe that providing error details to revise the output improves pass rates, aligning with our observations in Isabelle/HOL.

对 Lean4 中的自动形式化而言，定义同样带来更大的复杂性。 GPT-4o 在定义上的通过率始终低于在 miniF2F 上的通过率。例如，在 Def_ArXiv 上，GPT-4o 未能正确形式化这 30 条定义中的任何一条。此外，我们观察到，提供错误细节来修订输出会提高通过率，这与我们在 Isabelle/HOL 中的观察一致。

Categorical Refinement generalizes to Lean4. On the miniF2F dataset, CR-SYN achieves the highest pass rate. Similarly, on the Def_Wiki dataset, CR-UDF and CR-TUF yield the best results. These findings demonstrate the effectiveness of the proposed CR in other formal languages. Notably, since the Lean4 assistant does not provide explicit categories as Isabelle/HOL, performance differences across CR categories may indirectly reflect distinct types of errors encountered during autoformalization.

分类精炼可以推广到 Lean4。 在 miniF2F 数据集上，CR-SYN 达到了最高通过率。类似地，在 Def_Wiki 数据集上，CR-UDF 和 CR-TUF 给出了最好结果。这些发现表明，所提出的 CR 在其他形式语言中也是有效的。值得注意的是，由于 Lean4 助手并不像 Isabelle/HOL 那样提供明确的错误类别，不同 CR 类别之间的性能差异，可能间接反映自动形式化过程中遇到的不同类型错误。

4 Related Work

4 相关工作

Autoformalization allows for a systematic connection between material and formal inferences Quan et al. (2024a); Quan et al. (2024b), also enabling the universalization of formal mathematical reasoning. For instance, proof autoformalization has been used as an intermediate step in automated theorem proving (Jiang et al., 2023; Tarrach et al., 2024). Deep learning models, such as transformers, have been applied to autoformalization in Coq (Cunningham et al., 2022). In recent years, with the increasing capabilities of LLMs, prompting-based methods have also demonstrated the ability to autoformalize mathematical statements in Isabelle (Wu et al., 2022; Zhang et al., 2024; Li et al., 2024) and Lean (Yang et al., 2023; Lu et al., 2024; Liu et al., 2025a). Despite recent progress in autoformalization with LLMs, few studies have analyzed this task from an error perspective. Our work takes a step in this direction.

自动形式化为实质推理与形式推理之间提供了系统连接（Quan 等人，2024a；Quan 等人，2024b），也使形式数学推理的普遍化成为可能。例如，证明自动形式化已被用作自动定理证明中的中间步骤（Jiang 等人，2023；Tarrach 等人，2024）。深度学习模型，例如 Transformer，已被用于 Coq 中的自动形式化（Cunningham 等人，2022）。近年来，随着大语言模型能力的提升，基于提示的方法也已展现出在 Isabelle（Wu 等人，2022；Zhang 等人，2024；Li 等人，2024）和 Lean（Yang 等人，2023；Lu 等人，2024；Liu 等人，2025a）中自动形式化数学陈述的能力。尽管基于大语言模型的自动形式化近来有所进展，却很少有研究从错误的角度分析这一任务。我们的工作朝这一方向迈出了一步。

There are a few benchmarks that provide informal-formal mathematical statement pairs. MiniF2F (Zheng et al., 2022) and ProofNet benchmark (Azerbayev et al., 2023) include samples paired with ground-truth formal statements ranging from high-school and undergraduate problems to Olympiad-level problems. However, such informal-formal pairs remain scarce. A growing trend is the development of data generation pipelines for constructing large-scale parallel corpora to finetune LLMs for autoformalization (Jiang et al., 2024; Liu et al., 2025b). While useful, these benchmarks still focus on exercise-style mathematical problems, which do not fully reflect real-world scenarios. In contrast, our definition datasets emphasize real-world statements.

有少数基准提供非形式-形式数学陈述对。MiniF2F（Zheng 等人，2022）和 ProofNet 基准（Azerbayev 等人，2023）包含与金标准形式陈述配对的样本，范围从高中和本科题目到奥林匹克级别的问题。不过，这类非形式-形式配对仍然稀缺。一个日益增长的趋势，是开发数据生成流水线，以构造大规模平行语料，用于微调做自动形式化的大语言模型（Jiang 等人，2024；Liu 等人，2025b）。这些基准虽然有用，却仍然聚焦于练习式的数学问题，并不能充分反映真实世界场景。相比之下，我们的定义数据集强调真实世界的陈述。

5 Conclusion

5 结论

This paper explored the challenges and advancements in autoformalization of complex mathematical statements. To this end, two datasets collecting real-world definitions in machine learning were introduced for systematic evaluation. By assessing autoformalization performance across three modern LLMs on newly introduced datasets, we identify key failure patterns including syntactic inconsistency, undefined references, and type mismatch. To address these, we proposed interventions such as Categorical Refinement and Formal Definition Grounding to enhance performance. Our results suggest that while modern LLMs exhibit potential in converting natural mathematical definitions into formal representations, they still require improved guidance mechanisms and structured refinement techniques to enhance accuracy. Future research could focus on improving self-correction capabilities and integrating more robust contextual understanding into LLM-based formalization systems.

本文探索了复杂数学陈述自动形式化中的挑战与进展。为此，我们引入两个收集机器学习中真实世界定义的数据集，用于系统评估。通过在新引入的数据集上评估三家具有当代能力的大语言模型的自动形式化表现，我们识别出关键失败模式，包括句法不一致、未定义引用和类型不匹配。为应对这些问题，我们提出分类精炼和形式定义锚定等干预，以提升性能。我们的结果表明，虽然当代大语言模型在把自然数学定义转换成形式表示方面展现出潜力，它们仍然需要改进的引导机制和结构化精炼技术来提高准确性。未来研究可以聚焦于改进自纠正能力，并把更稳健的上下文理解纳入基于大语言模型的形式化系统。

6 Limitations

6 局限

Despite its contributions, this study has several limitations. First, the error analysis was conducted in Isabelle/HOL, and some results may not directly generalize to other formal proof assistants such as Lean. Second, the definition datasets proposed, though diverse, are relatively small scale. Additionally, while the proposed refinements improve formalization performance, they do not fully eliminate semantic inconsistencies between natural language definitions and their formalized counterparts. More advanced methods are still needed to be developed.

尽管有上述贡献，本研究仍有若干局限。首先，错误分析是在 Isabelle/HOL 中进行的，一些结果可能无法直接推广到 Lean 等其他形式证明助手。其次，所提出的定义数据集虽然多样，但规模相对较小。此外，虽然所提出的精炼改善了形式化性能，它们并没有完全消除自然语言定义与其形式化对应物之间的语义不一致。仍然需要发展更先进的方法。

Acknowledgements

致谢

This work was funded in part by the Swiss National Science Foundation (SNSF/FAPESP) “RATIONAL” project.

本工作部分由瑞士国家科学基金会（SNSF/FAPESP）“RATIONAL” 项目资助。

References

参考文献

Welleck et al. (2021) Sean Welleck, Jiacheng Liu, Ronan Le Bras, Hannaneh Hajishirzi, Yejin Choi, and Kyunghyun Cho. 2021. Naturalproofs: Mathematical theorem proving in natural language. In Thirty-fifth Conference on Neural Information Processing Systems Datasets and Benchmarks Track (Round 1) . Wu et al. (2022) Yuhuai Wu, Albert Qiaochu Jiang, Wenda Li, Markus Norman Rabe, Charles E Staats, Mateja Jamnik, and Christian Szegedy. 2022. Autoformalization with large language models . In Advances in Neural Information Processing Systems . Yang et al. (2023) Kaiyu Yang, Aidan M. Swope, Alex Gu, Rahul Chalamala, Peiyang Song, Shixing Yu, Saad Godil, Ryan Prenger, and Anima Anandkumar. 2023. Leandojo: Theorem proving with retrieval-augmented language models . Preprint , arXiv:2306.15626. Zhang et al. (2024) Lan Zhang, Xin Quan, and Andre Freitas. 2024. Consistent autoformalization for constructing mathematical libraries . In Proceedings of the 2024 Conference on Empirical Methods in Natural Language Processing , pages 4020-4033, Miami, Florida, USA. Association for Computational Linguistics. Zhang et al. (2025) Lan Zhang, Marco Valentino, and Andre Freitas. 2025. Beyond gold standards: Epistemic ensemble of llm judges for formal mathematical reasoning . Preprint , arXiv:2506.10903. Zheng et al. (2022) Kunhao Zheng, Jesse Michael Han, and Stanislas Polu. 2022. minif2f: a cross-system benchmark for formal olympiad-level mathematics . In International Conference on Learning Representations .

Appendix A Detailed Information about the Dataset Creation

附录 A 关于数据集创建的详细信息

We obtain mathematical definitions in the machine learning domain from two sources: Wikipedia (Def_Wiki) and Arxiv Papers (Def_ArXiv). For Def_Wiki, definitions are collected from pages under the Machine Learning category[^2] and its sub-categories. We manually browsed each page, identified well-defined definitions (i.e., formal descriptions with mathematical symbols), and converted the chosen definitions into LaTeX format. In total, we obtained 56 qualified natural language definitions in LaTeX and divided them into development and test sets, containing 10 and 46 samples, respectively. For Def_ArXiv, we used the advanced search tool on ArXiv’s website, filtering for papers in the subcategories cs.LG and stat.ML, with comments including "ICML." We restricted the search to papers published in 2019, 2020, and 2021 and manually reviewed the first 25 papers from each year. We shortlisted papers that were accepted to the ICML conference and contained formally described definitions with mathematical symbols to ensure reliability. We then filtered out definitions that were less straightforward or formal in their expressions, extracted the LaTeX versions, and ultimately obtained 30 definitions from 7 papers. We provide dataset statistics in Table 5.

我们从两个来源获取机器学习领域的数学定义：维基百科（Def_Wiki）和 arXiv 论文（Def_ArXiv）。对 Def_Wiki，定义收集自 Machine Learning 分类[^2]及其子分类下的页面。我们人工浏览每个页面，识别出定义良好的定义（即带有数学符号的形式描述），并把所选定义转换成 LaTeX 格式。我们总共得到 56 条合格的、以 LaTeX 写成的自然语言定义，并把它们分成开发集和测试集，分别包含 10 条和 46 条样本。对 Def_ArXiv，我们使用 arXiv 网站上的高级检索工具，筛选子类别为 cs.LG 和 stat.ML、注释中含有 “ICML” 的论文。我们将检索限制在 2019、2020 和 2021 年发表的论文，并人工审阅每年的前 25 篇论文。我们把被 ICML 会议接收、且包含带有数学符号的形式描述定义的论文列入候选，以确保可靠性。随后，我们过滤掉表达不够直接或不够形式的定义，抽取 LaTeX 版本，最终从 7 篇论文中得到 30 条定义。我们在表 5 中给出数据集统计。

Property miniF2F-Test Def_Wiki Def_ArXiv No. Samples 2445630 No. Tokens 70.25 (47.70) 200.18 (112.98) 164.40 (71.47) No. Objects 4.76 (1.68) 7.63 (2.71) 7.10 (2.64) No. Formulae 2.71 (1.74) 2.84 (2.05) 3.17 (1.97) Table 5: Dataset properties. The number of tokens per sample is calculated using the GPT-2 tokenizer. The number of directly mentioned mathematical objects—excluding explicit numbers and variables—and the number of mathematical formulae per sample are estimated through prompting with GPT-4o. The mean (standard deviation) is reported for each dataset.

Property	miniF2F-Test	Def_Wiki	Def_ArXiv
No. Samples	244	56	30
No. Tokens	70.25 (47.70)	200.18 (112.98)	164.40 (71.47)
No. Objects	4.76 (1.68)	7.63 (2.71)	7.10 (2.64)
No. Formulae	2.71 (1.74)	2.84 (2.05)	3.17 (1.97)

性质 miniF2F-Test Def_Wiki Def_ArXiv 样本数 2445630 词元数 70.25 (47.70) 200.18 (112.98) 164.40 (71.47) 对象数 4.76 (1.68) 7.63 (2.71) 7.10 (2.64) 公式数 2.71 (1.74) 2.84 (2.05) 3.17 (1.97) 表 5：数据集性质。每个样本的词元数用 GPT-2 分词器计算。每个样本中直接提到的数学对象数——不包括显式数字和变量——以及数学公式数，通过用 GPT-4o 做提示来估计。对每个数据集报告均值（标准差）。

性质	miniF2F-Test	Def_Wiki	Def_ArXiv
样本数	244	56	30
词元数	70.25 (47.70)	200.18 (112.98)	164.40 (71.47)
对象数	4.76 (1.68)	7.63 (2.71)	7.10 (2.64)
公式数	2.71 (1.74)	2.84 (2.05)	3.17 (1.97)

Appendix B Case Study for Formal Definition Grounding

附录 B 形式定义锚定的案例研究

The following example shows an example of using GPT-4o in a zero-shot setting to formalize the definition of Bradley--Terry model[^3].

下面的例子展示了在零样本设定下，用 GPT-4o 形式化 Bradley-Terry 模型[^3]定义的一个实例。

i

i

\Pr(i>j)=\frac{p_{i}}{p_{i}+p_{j}}

p_{i}

p_{i}

p_{i}

p_{i}

We acknowledge the importance of quantitatively evaluating semantic consistency in autoformalization. In this paper we mainly quantitatively evaluate the syntactic aspects of formalizations because syntactic correctness can be systematically and fully validated through the theorem prover. However, the full evaluation of semantic consistency still presents technical challenges and remains an open research question. Additionally, it is important to notice that semantic validity is not completely disentangled from syntactic checks. Some important semantic aspects, in fact, are explicitly or implicitly covered within our evaluation. It can be noted, for example, that some of the errors in Table 5 also cover semantic aspects. For instance, a model that is unaware of undefined items will also likely lack a complete semantic understanding of the crucial elements required for correct autoformalization. We believe that coming up with a reliable quantitative method to systematically assess semantic alignment is an important research question to explore in future work, which is out of scope for the current paper.

我们承认，定量评估自动形式化中的语义一致性很重要。在本文中，我们主要定量评估形式化的句法方面，因为句法正确性可以通过定理证明器系统、完整地核验。然而，对语义一致性做完整评估仍然面临技术挑战，并仍是一个开放的研究问题。此外，需要注意的是，语义有效性并非与句法检查完全分离。事实上，一些重要的语义方面已经在我们的评估中被显式或隐式覆盖。例如，可以看出，表 5 中的某些错误也覆盖了语义方面。譬如，一个对未定义对象缺乏意识的模型，也很可能缺乏对正确自动形式化所需关键要素的完整语义理解。我们认为，提出一种可靠的定量方法来系统评估语义对齐，是未来工作中一个重要的研究问题，这超出了当前论文的范围。

Appendix C Examples of Incorrect Formal Codes

附录 C 不正确形式代码的例子

We provide some examples of incorrect formal codes generated by GPT-4o to support our summarized reasons in Table 3. All examples of definitions are from Def_Wiki development set.

我们提供一些由 GPT-4o 生成的不正确形式代码例子，以支持表 3 中概括的原因。所有定义例子都来自 Def_Wiki 开发集。

Example 1 is about autoformalization on the definition of Rademacher Complexity[^4]. In this example, the missing of “>” in “<sigma”leads to a SYN error, which contributes to reason 1 of SYN category. In addition, this piece of formal code uses “real” but “real” is not imported by “imports Main”. This problem contributes to reason 1 of UDF category.

例子 1 是关于 Rademacher 复杂度[^4]定义的自动形式化。在这个例子中，“<sigma” 缺少 “>”，导致 SYN 错误，这对应 SYN 类别中的原因 1。此外，这段形式代码使用了 “real”，但 “real” 并未被 “imports Main” 导入。这一问题对应 UDF 类别中的原因 1。

A\subseteq\mathbb{R}^{m}

A\subseteq\mathbb{R}^{m}

\operatorname{Rad}(A):=\frac{1}{m}\mathbb{E}_{\sigma}\left[\sup_{a\in A}\sum_{i=1}^{m}\sigma_{i}a_{i}\right]

\sigma_{1},\sigma_{2},\dots,\sigma_{m}

\sigma_{1},\sigma_{2},\dots,\sigma_{m}

Example 2 is about autoformalization on the definition of Algorithm Selection[^5]. In this example, the problem of missing “>” and using “real” also occurs. Even if missing “>” is solved, “<mathcal> is not a valid symbol in Isabelle. This problem contributes to reason 2 of SYN category. In addition, “instance” is a reserved keyword in Isabelle so it cannot be used in “type_synonym”. This contributes to reason 3 of SYN category.

例子 2 是关于算法选择[^5]定义的自动形式化。在这个例子中，缺少 “>” 以及使用 “real” 的问题同样出现。即使缺少 “>” 的问题得到解决，“<mathcal> 也不是 Isabelle 中的有效符号。这一问题对应 SYN 类别中的原因 2。此外，“instance” 是 Isabelle 中的保留关键字，因此不能用在 “type_synonym” 中。这对应 SYN 类别中的原因 3。

\mathcal{P}

\mathcal{P}

\longrightarrow

\longrightarrow

H

H

Appendix D Formal Definition Grounding via Prompting

附录 D 通过提示做形式定义锚定

We further explore formal definition grounding with prompting (Prompt-FDG): provide LLMs with grounded formal items and preambles in context to guide autoformalization. We designed two prompts to include external formal definitions for FDG: 1. Soft: allow the LLM some flexibility in whether to use in-context formal definitions for autoformalization; 2. Hard: explicitly instruct the LLM to use the in-context formal definitions if they are related. We tested these prompts on GPT-4o and Def_Wiki-Test to evaluate whether it can correctly refer to formalised items in context. The results are reported in Table 6.

我们进一步探索用提示做形式定义锚定（Prompt-FDG）：向大语言模型提供已锚定的形式对象和导言作为上下文，以引导自动形式化。我们设计了两种提示，以纳入用于 FDG 的外部形式定义：1. 软约束：允许模型在是否使用上下文中的形式定义来做自动形式化上保留一定灵活性；2. 硬约束：明确指示模型，如果相关，就必须使用上下文中的形式定义。我们在 GPT-4o 和 Def_Wiki-Test 上测试这些提示，以评估它能否正确引用上下文中的已形式化对象。结果报告于表 6。

Including relevant formal definitions in the prompt does not boost the performance of autoformalization. Intuitively, LLMs should perform better when more relevant information is provided within the prompt. However, directly including grounded formal definitions does not positively impact the formalization. This behaviour indicates that current state-of-the-art LLMs cannot effectively link to relevant in-context formal items for autoformalization. How to successfully leverage in-context formal definitions for autoformalization with LLMs remains an important open research question.

在提示中纳入相关形式定义，并不会提升自动形式化的性能。 直观上，当提示中提供了更多相关信息时，大语言模型应当表现更好。然而，直接纳入已锚定的形式定义，并没有对形式化产生正面影响。这一行为表明，当前最先进的大语言模型无法有效地连接到上下文中的相关形式对象以做自动形式化。如何成功利用上下文中的形式定义，让大语言模型做自动形式化，仍然是一个重要的开放研究问题。

Appendix E Prompts and Additional Results

附录 E 提示与补充结果

The prompts used for the estimation of dataset statistics are provided in Table 7. The instructions used in the prompts of experiments are provided in Table 8. Detailed numbers of autoformalization results on miniF2F test set, Def_Wiki test set and Def_ArXiv are provided in Table 9, 10, 11, respectively. Symbolic refinement results and Post-FDG results on Def_Wiki test set are provided in Table 12 and Table 13, respectively.

用于估计数据集统计的提示见表 7。实验提示中所用的指令见表 8。miniF2F 测试集、Def_Wiki 测试集和 Def_ArXiv 上自动形式化结果的详细数字分别见表 9、10、11。Def_Wiki 测试集上的符号精炼结果和 Post-FDG 结果分别见表 12 和表 13。

\uparrow

Prompt Strategy	Pass $\uparrow$	SYN $\downarrow$	UDF $\downarrow$	TUF $\downarrow$
ZS	34.78	30.43	17.39	23.91
Soft-IFDC	19.57	34.78	30.43	26.09
Hard-IFDC	19.57	36.96	21.74	39.13

\uparrow

提示策略	Pass $\uparrow$	SYN $\downarrow$	UDF $\downarrow$	TUF $\downarrow$
ZS	34.78	30.43	17.39	23.91
Soft-IFDC	19.57	34.78	30.43	26.09
Hard-IFDC	19.57	36.96	21.74	39.13

Purpose Content Mathematical Objects Given the following statement written in LaTeX: {{latex}} How many mathematical objects excluding explicit numbers and variables are mentioned directly in this statement? You can think it step by step. Give me the final number as NUMBER={the number} Mathematical Formulae Given the following statement written in LaTeX: {{latex}} How many mathematical formulae are mentioned directly in this statement? You can think it step by step. Give me the final number as NUMBER={the number} Table 7: Prompts for the estimation of dataset statistics.

Purpose	Content
Mathematical Objects	Given the following statement written in LaTeX: {{latex}} How many mathematical objects excluding explicit numbers and variables are mentioned directly in this statement? You can think it step by step. Give me the final number as NUMBER={the number}
Mathematical Formulae	Given the following statement written in LaTeX: {{latex}} How many mathematical formulae are mentioned directly in this statement? You can think it step by step. Give me the final number as NUMBER={the number}

用途 内容 数学对象 给定下列用 LaTeX 写成的陈述：{{latex}} 这一陈述中直接提到了多少个数学对象（不包括显式数字和变量）？你可以逐步思考。把最终数字以 NUMBER={the number} 的形式给我。 数学公式 给定下列用 LaTeX 写成的陈述：{{latex}} 这一陈述中直接提到了多少个数学公式？你可以逐步思考。把最终数字以 NUMBER={the number} 的形式给我。 表 7：用于估计数据集统计的提示。

用途	内容
数学对象	给定下列用 LaTeX 写成的陈述：{{latex}} 这一陈述中直接提到了多少个数学对象（不包括显式数字和变量）？你可以逐步思考。把最终数字以 NUMBER={the number} 的形式给我。
数学公式	给定下列用 LaTeX 写成的陈述：{{latex}} 这一陈述中直接提到了多少个数学公式？你可以逐步思考。把最终数字以 NUMBER={the number} 的形式给我。

\Rightarrow

Instruction	Content
General	You are an expert in machine learning and formal language Isabelle/HOL. Given the following definition in LaTeX: {{latex}}, your task is to provide the formal code of this definition in Isabelle/HOL. The following text might contain some preliminaries to explain the given definition: {{preliminary}}. In case that you need to import any necessary dependent theory files, you should not import any fake theory files.
Stylistic	To represent the math symbols, you must use the textual full name of symbols in Isabelle instead of direct symbols. For example you should use <Rightarrow> instead of $\Rightarrow$ , <lambda> instead of $\lambda$ .
Output	Give the results directly without any additional explanations.
Refinement	Plain: For your reference, there are some previous formal codes generated by you: {{previous}}. You can choose to refine this piece of code for your task. Binary: For your reference, there are some previous formal codes generated by you: {{previous}}. The syntactic correctness for this piece of code is: {{correctness}}. You can choose to refine this piece of code for your task. Detailed: For your reference, there are some previous formal codes generated by you: {{previous}}. The provided code might have some errors according to the Isabelle prover. The error details and where the error code is located in the code are: {{error_details}}. You should refine this piece of code for your task.
SYN	You should make sure that every symbol you use is a valid Isabelle symbol. If an Isabelle symbol starts with <, then it must end with >. Isabelle reserves some words as keywords. You should be careful with this and avoid to use them to define new names. You should make sure that the usage of symbols and operators is correct in your final output as the incorrect usage will lead to syntax errors.
UDF	You should make sure that every item you mentioned in your code has a clear reference either in the local context or the theory files that you decide to import.
TUF	You should make sure that in your code, the types of operands of operators or the types of parameters of functions match the types in their definitions exactly. Failure to maintain such compatibility will lead to type mismatch errors.
Include Formal Definition Codes	Soft: You can use the following Isabelle/HOL codes to support your task: {{formal_defs}} but you should not restate these codes in your final output. You need to formalize everything that is not provided in the given code. In this case, you should assume that you can only use things from HOL.Main. You only need to provide the main body of formal codes for the given definition. You may not import any theory files. Hard: The following Isabelle/HOL codes define some mathematical concepts which might be related to your task: {{formal_defs}}. If a mathematical concept in your task has been defined in the above codes, you are required to use this version of formal codes but you should not restate these codes in your final output. You need to formalize everything that is not provided in the given code. In this case, you should assume that you can only use things from HOL.Main. You only need to provide the main body of formal codes for the given definition. You may not import any theory files.

\Rightarrow

指令	内容
一般指令	你是机器学习和形式语言 Isabelle/HOL 方面的专家。给定下列用 LaTeX 写成的定义：{{latex}}，你的任务是给出这一定义在 Isabelle/HOL 中的形式代码。下列文本可能包含一些用于解释给定定义的预备知识：{{preliminary}}。如果你需要导入任何必要的依赖理论文件，你不应导入任何虚假的理论文件。
风格指令	为表示数学符号，你必须使用 Isabelle 中符号的文本全名，而不是直接使用符号。例如，你应当使用 <Rightarrow> 而不是 $\Rightarrow$ ，使用 <lambda> 而不是 $\lambda$ 。
输出指令	直接给出结果，不要附加任何额外解释。
精炼指令	Plain：供你参考，下列是你先前生成的一些形式代码：{{previous}}。你可以选择精炼这段代码以完成任务。 Binary：供你参考，下列是你先前生成的一些形式代码：{{previous}}。这段代码的句法正确性是：{{correctness}}。你可以选择精炼这段代码以完成任务。 Detailed：供你参考，下列是你先前生成的一些形式代码：{{previous}}。根据 Isabelle 证明器，所提供的代码可能存在一些错误。错误细节以及出错代码在代码中的位置是：{{error_details}}。你应当精炼这段代码以完成任务。
SYN	你应当确保你使用的每一个符号都是有效的 Isabelle 符号。如果一个 Isabelle 符号以 < 开头，那么它必须以 > 结尾。Isabelle 把一些词保留为关键字。你应当对此保持谨慎，避免用它们来定义新名称。你应当确保最终输出中符号和算子的用法是正确的，因为不正确的用法会导致句法错误。
UDF	你应当确保你在代码中提到的每一个对象，要么在局部上下文中、要么在你决定导入的理论文件中，都有清楚的引用。
TUF	你应当确保在你的代码中，算子操作数的类型，或函数参数的类型，与它们定义中的类型精确匹配。未能保持这种兼容性将导致类型不匹配错误。
纳入形式定义代码	Soft：你可以使用下列 Isabelle/HOL 代码来支持你的任务：{{formal_defs}}，但你不应在最终输出中复述这些代码。你需要对给定代码中尚未提供的一切做形式化。在这种情况下，你应当假定你只能使用来自 HOL.Main 的内容。你只需要为给定定义提供形式代码的主体。你可以不导入任何理论文件。 Hard：下列 Isabelle/HOL 代码定义了一些可能与你的任务相关的数学概念：{{formal_defs}}。若你任务中的某个数学概念已在上述代码中被定义，你必须使用这一版本的形式代码，但不应在最终输出中复述这些代码。你需要对给定代码中尚未提供的一切做形式化。在这种情况下，你应当假定你只能使用来自 HOL.Main 的内容。你只需要为给定定义提供形式代码的主体。你可以不导入任何理论文件。

\uparrow

Prompt Strategy	Preamble	Pass $\uparrow$	FEO $\uparrow$	TRO $\downarrow$	IVI $\downarrow$	SYN $\downarrow$	UDF $\downarrow$	TUF $\downarrow$
DeepSeekMath-7B
ZS	Direct	3.28	12.79	18.44	0.00	50.00	14.34	9.43
Post-FDG	12.30	23.60	15.98	0.00	47.13	1.23	9.02
(ZS) + Binary	Direct	2.05	6.73	2.46	0.00	79.91	5.33	2.05
Post-FDG	4.10	9.39	2.46	0.00	80.33	0.41	1.23
(ZS) + Detailed	Direct	3.28	10.03	5.74	0.00	70.49	10.66	4.10
Post-FDG	5.74	15.57	5.74	0.00	69.67	0.82	0.41
(ZS) + Detailed + CR-All	Direct	3.28	9.11	6.15	0.00	73.77	6.15	3.28
Post-FDG	5.33	13.08	6.15	0.00	72.95	0.41	3.28
Llama3-8B
ZS	Direct	4.92	20.70	4.51	0.41	29.51	38.52	18.85
Post-FDG	10.66	31.17	4.92	0.00	28.69	20.08	21.31
(ZS) + Binary	Direct	3.69	20.52	3.28	0.41	33.20	39.75	20.49
Post-FDG	9.43	30.57	3.69	0.00	31.97	22.95	22.13
(ZS) + Detailed	Direct	4.10	24.33	3.69	0.82	29.51	35.25	18.44
Post-FDG	9.02	33.36	4.10	0.00	27.46	18.44	22.13
(ZS) + Detailed + CR-All	Direct	4.92	24.16	6.97	0.82	27.46	35.25	20.08
Post-FDG	9.43	32.41	7.79	0.00	27.46	18.85	22.54
GPT-4o
ZS	Direct	25.41	48.90	1.23	1.23	6.15	23.77	7.38
Post-FDG	67.21	81.88	0.00	0.00	3.28	2.87	5.33
ZS + CR-SYN	Direct	24.18	45.31	2.46	0.00	9.02	27.46	7.79
Post-FDG	52.46	73.96	0.41	0.00	7.79	3.69	3.69
ZS + CR-UDF	Direct	25.82	50.75	2.05	2.46	6.56	22.54	6.97
Post-FDG	61.48	80.41	0.41	0.00	5.33	2.87	2.87
ZS + CR-TUF	Direct	27.87	50.62	2.05	1.64	5.33	26.64	5.74
Post-FDG	54.10	78.79	0.00	0.00	3.28	4.10	2.87
(ZS)	Direct	25.41	53.15	1.64	1.23	6.56	22.13	7.79
Post-FDG	67.21	84.05	0.00	0.00	3.28	2.46	4.92
(ZS) + Binary	Direct	29.10	53.90	2.05	1.23	6.15	21.72	8.20
Post-FDG	67.21	83.60	0.00	0.00	4.10	2.05	4.92
(ZS) + Detailed	Direct	37.30	63.28	2.05	1.23	5.74	9.02	8.61
Post-FDG	83.61	91.47	0.00	0.00	2.05	0.82	3.28
(ZS) + CR-SYN	Direct	25.41	52.72	2.05	1.23	5.74	22.13	8.61
Post-FDG	67.21	83.73	0.00	0.00	2.87	2.46	5.74
(ZS) + CR-UDF	Direct	26.64	54.06	1.64	1.23	6.15	21.72	6.97
Post-FDG	67.21	83.78	0.00	0.00	3.69	2.05	4.92
(ZS) + CR-TUF	Direct	25.41	51.18	2.46	1.23	6.56	24.18	7.38
Post-FDG	67.21	83.94	0.00	0.00	3.28	2.87	4.10
(ZS) + Detailed + CR-SYN	Direct	38.52	64.42	2.05	1.23	7.79	8.20	7.79
Post-FDG	82.79	90.32	0.00	0.00	3.28	0.82	2.05
(ZS) + Detailed + CR-UDF	Direct	38.11	63.95	2.05	2.46	5.74	6.56	6.97
Post-FDG	82.38	90.48	0.00	0.00	2.46	1.23	2.87
(ZS) + Detailed + CR-TUF	Direct	41.39	64.76	3.28	1.23	6.15	11.07	6.15
Post-FDG	83.20	90.71	0.00	0.00	2.87	1.64	2.05
(ZS) + Detailed + CR-All	Direct	38.52	65.73	2.05	1.23	6.15	5.74	7.79
Post-FDG	81.97	90.65	0.00	0.00	2.46	0.41	2.46

\uparrow

提示策略	导言	Pass $\uparrow$	FEO $\uparrow$	TRO $\downarrow$	IVI $\downarrow$	SYN $\downarrow$	UDF $\downarrow$	TUF $\downarrow$
DeepSeekMath-7B
ZS	直接	3.28	12.79	18.44	0.00	50.00	14.34	9.43
Post-FDG	12.30	23.60	15.98	0.00	47.13	1.23	9.02
(ZS) + Binary	直接	2.05	6.73	2.46	0.00	79.91	5.33	2.05
Post-FDG	4.10	9.39	2.46	0.00	80.33	0.41	1.23
(ZS) + Detailed	直接	3.28	10.03	5.74	0.00	70.49	10.66	4.10
Post-FDG	5.74	15.57	5.74	0.00	69.67	0.82	0.41
(ZS) + Detailed + CR-All	直接	3.28	9.11	6.15	0.00	73.77	6.15	3.28
Post-FDG	5.33	13.08	6.15	0.00	72.95	0.41	3.28
Llama3-8B
ZS	直接	4.92	20.70	4.51	0.41	29.51	38.52	18.85
Post-FDG	10.66	31.17	4.92	0.00	28.69	20.08	21.31
(ZS) + Binary	直接	3.69	20.52	3.28	0.41	33.20	39.75	20.49
Post-FDG	9.43	30.57	3.69	0.00	31.97	22.95	22.13
(ZS) + Detailed	直接	4.10	24.33	3.69	0.82	29.51	35.25	18.44
Post-FDG	9.02	33.36	4.10	0.00	27.46	18.44	22.13
(ZS) + Detailed + CR-All	直接	4.92	24.16	6.97	0.82	27.46	35.25	20.08
Post-FDG	9.43	32.41	7.79	0.00	27.46	18.85	22.54
GPT-4o
ZS	直接	25.41	48.90	1.23	1.23	6.15	23.77	7.38
Post-FDG	67.21	81.88	0.00	0.00	3.28	2.87	5.33
ZS + CR-SYN	直接	24.18	45.31	2.46	0.00	9.02	27.46	7.79
Post-FDG	52.46	73.96	0.41	0.00	7.79	3.69	3.69
ZS + CR-UDF	直接	25.82	50.75	2.05	2.46	6.56	22.54	6.97
Post-FDG	61.48	80.41	0.41	0.00	5.33	2.87	2.87
ZS + CR-TUF	直接	27.87	50.62	2.05	1.64	5.33	26.64	5.74
Post-FDG	54.10	78.79	0.00	0.00	3.28	4.10	2.87
(ZS)	直接	25.41	53.15	1.64	1.23	6.56	22.13	7.79
Post-FDG	67.21	84.05	0.00	0.00	3.28	2.46	4.92
(ZS) + Binary	直接	29.10	53.90	2.05	1.23	6.15	21.72	8.20
Post-FDG	67.21	83.60	0.00	0.00	4.10	2.05	4.92
(ZS) + Detailed	直接	37.30	63.28	2.05	1.23	5.74	9.02	8.61
Post-FDG	83.61	91.47	0.00	0.00	2.05	0.82	3.28
(ZS) + CR-SYN	直接	25.41	52.72	2.05	1.23	5.74	22.13	8.61
Post-FDG	67.21	83.73	0.00	0.00	2.87	2.46	5.74
(ZS) + CR-UDF	直接	26.64	54.06	1.64	1.23	6.15	21.72	6.97
Post-FDG	67.21	83.78	0.00	0.00	3.69	2.05	4.92
(ZS) + CR-TUF	直接	25.41	51.18	2.46	1.23	6.56	24.18	7.38
Post-FDG	67.21	83.94	0.00	0.00	3.28	2.87	4.10
(ZS) + Detailed + CR-SYN	直接	38.52	64.42	2.05	1.23	7.79	8.20	7.79
Post-FDG	82.79	90.32	0.00	0.00	3.28	0.82	2.05
(ZS) + Detailed + CR-UDF	直接	38.11	63.95	2.05	2.46	5.74	6.56	6.97
Post-FDG	82.38	90.48	0.00	0.00	2.46	1.23	2.87
(ZS) + Detailed + CR-TUF	直接	41.39	64.76	3.28	1.23	6.15	11.07	6.15
Post-FDG	83.20	90.71	0.00	0.00	2.87	1.64	2.05
(ZS) + Detailed + CR-All	直接	38.52	65.73	2.05	1.23	6.15	5.74	7.79
Post-FDG	81.97	90.65	0.00	0.00	2.46	0.41	2.46

\uparrow

Prompt Strategy	Preamble	Pass $\uparrow$	FEO $\uparrow$	TRO $\downarrow$	IVI $\downarrow$	SYN $\downarrow$	UDF $\downarrow$	TUF $\downarrow$
DeepSeekMath-7B
ZS	Direct	10.87	17.75	34.78	2.17	30.43	26.09	2.17
Post-FDG	26.09	30.98	34.78	0.00	21.74	10.87	13.04
(ZS) + Binary	Direct	6.52	7.73	8.70	0.00	69.57	21.74	2.17
Post-FDG	10.87	12.56	8.70	0.00	65.22	15.22	6.52
(ZS) + Detailed	Direct	10.87	13.27	15.22	2.17	43.48	34.78	6.52
Post-FDG	26.09	29.21	13.04	0.00	36.96	17.39	19.57
(ZS) + Detailed + CR-All	Direct	4.35	7.66	13.04	2.17	47.83	32.61	8.70
Post-FDG	17.39	21.43	13.04	0.00	41.30	15.22	21.74
Llama3-8B
ZS	Direct	0.00	2.80	0.00	23.91	56.52	32.61	4.35
Post-FDG	0.00	2.80	21.74	0.00	58.70	23.91	15.22
(ZS) + Binary	Direct	2.17	3.71	0.00	26.09	52.17	30.43	2.17
Post-FDG	0.00	1.53	23.91	0.00	56.52	28.26	13.04
(ZS) + Detailed	Direct	2.17	3.80	0.00	26.09	50.00	30.43	6.52
Post-FDG	4.35	5.98	23.91	0.00	52.17	26.09	15.22
(ZS) + Detailed + CR-All	Direct	2.17	3.71	0.00	26.09	52.17	32.61	4.35
Post-FDG	2.17	3.71	23.91	0.00	54.35	23.91	15.22
GPT-4o
ZS	Direct	10.87	16.12	8.70	8.70	19.57	50.00	13.04
Post-FDG	34.78	42.56	6.52	0.00	30.43	17.39	23.91
ZS + CR-SYN	Direct	10.87	15.18	8.70	2.17	15.22	58.70	13.04
Post-FDG	34.78	40.27	8.70	0.00	28.26	13.04	26.09
ZS + CR-UDF	Direct	2.17	11.59	6.52	6.52	19.57	60.87	19.57
Post-FDG	30.43	42.66	2.17	0.00	34.78	23.91	23.91
ZS + CR-TUF	Direct	8.70	14.55	8.70	6.52	21.74	56.52	15.22
Post-FDG	30.43	40.51	6.52	0.00	34.78	17.39	28.26
(ZS)	Direct	10.87	16.21	8.70	8.70	19.57	50.00	13.04
Post-FDG	39.13	47.23	6.52	0.00	28.26	15.22	23.91
(ZS) + Binary	Direct	13.04	18.30	8.70	6.52	17.39	50.00	13.04
Post-FDG	39.13	48.00	6.52	0.00	26.09	8.70	28.26
(ZS) + Detailed	Direct	19.57	23.46	8.70	8.70	10.87	47.83	10.87
Post-FDG	43.48	50.13	6.52	0.00	21.74	10.87	23.91
(ZS) + CR-SYN	Direct	10.87	16.12	8.70	8.70	17.39	52.17	13.04
Post-FDG	36.96	44.97	6.52	0.00	30.43	15.22	23.91
(ZS) + CR-UDF	Direct	10.87	16.12	8.70	8.70	19.57	50.00	13.04
Post-FDG	36.96	44.97	6.52	0.00	30.43	15.22	23.91
(ZS) + CR-TUF	Direct	10.87	16.21	8.70	8.70	21.74	47.83	13.04
Post-FDG	36.96	45.06	6.52	0.00	32.61	15.22	21.74
(ZS + Detailed) + Detailed	Direct	19.57	24.09	8.70	8.70	13.04	43.48	10.87
Post-FDG	43.48	50.32	6.52	0.00	19.57	8.70	26.09
(ZS) + Detailed + CR-SYN	Direct	21.74	25.63	8.70	10.87	10.87	41.30	8.70
Post-FDG	45.65	52.31	6.52	0.0	21.74	8.70	21.74
(ZS) + Detailed + CR-UDF	Direct	17.39	21.83	8.70	13.04	17.39	39.13	8.70
Post-FDG	43.48	50.24	6.52	0.0	21.74	10.87	21.74
(ZS) + Detailed + CR-TUF	Direct	19.57	23.46	8.70	8.70	17.39	43.48	8.70
Post-FDG	45.65	52.31	6.52	0.0	23.91	10.87	19.57
(ZS) + Detailed + CR-All	Direct	21.74	25.63	8.70	8.70	10.87	43.48	13.04
Post-FDG	43.48	50.13	6.52	0.00	21.74	10.87	23.91

\uparrow

提示策略	导言	Pass $\uparrow$	FEO $\uparrow$	TRO $\downarrow$	IVI $\downarrow$	SYN $\downarrow$	UDF $\downarrow$	TUF $\downarrow$
DeepSeekMath-7B
ZS	直接	10.87	17.75	34.78	2.17	30.43	26.09	2.17
Post-FDG	26.09	30.98	34.78	0.00	21.74	10.87	13.04
(ZS) + Binary	直接	6.52	7.73	8.70	0.00	69.57	21.74	2.17
Post-FDG	10.87	12.56	8.70	0.00	65.22	15.22	6.52
(ZS) + Detailed	直接	10.87	13.27	15.22	2.17	43.48	34.78	6.52
Post-FDG	26.09	29.21	13.04	0.00	36.96	17.39	19.57
(ZS) + Detailed + CR-All	直接	4.35	7.66	13.04	2.17	47.83	32.61	8.70
Post-FDG	17.39	21.43	13.04	0.00	41.30	15.22	21.74
Llama3-8B
ZS	直接	0.00	2.80	0.00	23.91	56.52	32.61	4.35
Post-FDG	0.00	2.80	21.74	0.00	58.70	23.91	15.22
(ZS) + Binary	直接	2.17	3.71	0.00	26.09	52.17	30.43	2.17
Post-FDG	0.00	1.53	23.91	0.00	56.52	28.26	13.04
(ZS) + Detailed	直接	2.17	3.80	0.00	26.09	50.00	30.43	6.52
Post-FDG	4.35	5.98	23.91	0.00	52.17	26.09	15.22
(ZS) + Detailed + CR-All	直接	2.17	3.71	0.00	26.09	52.17	32.61	4.35
Post-FDG	2.17	3.71	23.91	0.00	54.35	23.91	15.22
GPT-4o
ZS	直接	10.87	16.12	8.70	8.70	19.57	50.00	13.04
Post-FDG	34.78	42.56	6.52	0.00	30.43	17.39	23.91
ZS + CR-SYN	直接	10.87	15.18	8.70	2.17	15.22	58.70	13.04
Post-FDG	34.78	40.27	8.70	0.00	28.26	13.04	26.09
ZS + CR-UDF	直接	2.17	11.59	6.52	6.52	19.57	60.87	19.57
Post-FDG	30.43	42.66	2.17	0.00	34.78	23.91	23.91
ZS + CR-TUF	直接	8.70	14.55	8.70	6.52	21.74	56.52	15.22
Post-FDG	30.43	40.51	6.52	0.00	34.78	17.39	28.26
(ZS)	直接	10.87	16.21	8.70	8.70	19.57	50.00	13.04
Post-FDG	39.13	47.23	6.52	0.00	28.26	15.22	23.91
(ZS) + Binary	直接	13.04	18.30	8.70	6.52	17.39	50.00	13.04
Post-FDG	39.13	48.00	6.52	0.00	26.09	8.70	28.26
(ZS) + Detailed	直接	19.57	23.46	8.70	8.70	10.87	47.83	10.87
Post-FDG	43.48	50.13	6.52	0.00	21.74	10.87	23.91
(ZS) + CR-SYN	直接	10.87	16.12	8.70	8.70	17.39	52.17	13.04
Post-FDG	36.96	44.97	6.52	0.00	30.43	15.22	23.91
(ZS) + CR-UDF	直接	10.87	16.12	8.70	8.70	19.57	50.00	13.04
Post-FDG	36.96	44.97	6.52	0.00	30.43	15.22	23.91
(ZS) + CR-TUF	直接	10.87	16.21	8.70	8.70	21.74	47.83	13.04
Post-FDG	36.96	45.06	6.52	0.00	32.61	15.22	21.74
(ZS + Detailed) + Detailed	直接	19.57	24.09	8.70	8.70	13.04	43.48	10.87
Post-FDG	43.48	50.32	6.52	0.00	19.57	8.70	26.09
(ZS) + Detailed + CR-SYN	直接	21.74	25.63	8.70	10.87	10.87	41.30	8.70
Post-FDG	45.65	52.31	6.52	0.0	21.74	8.70	21.74
(ZS) + Detailed + CR-UDF	直接	17.39	21.83	8.70	13.04	17.39	39.13	8.70
Post-FDG	43.48	50.24	6.52	0.0	21.74	10.87	21.74
(ZS) + Detailed + CR-TUF	直接	19.57	23.46	8.70	8.70	17.39	43.48	8.70
Post-FDG	45.65	52.31	6.52	0.0	23.91	10.87	19.57
(ZS) + Detailed + CR-All	直接	21.74	25.63	8.70	8.70	10.87	43.48	13.04
Post-FDG	43.48	50.13	6.52	0.00	21.74	10.87	23.91

\uparrow

Prompt Strategy	Preamble	Pass $\uparrow$	FEO $\uparrow$	TRO $\downarrow$	IVI $\downarrow$	SYN $\downarrow$	UDF $\downarrow$	TUF $\downarrow$
DeepSeekMath-7B
ZS	Direct	13.33	14.69	16.67	0.00	40.00	36.67	13.33
Post-FDG	16.67	18.02	13.33	0.00	43.33	30.00	16.67
(ZS) + Binary	Direct	3.33	3.33	6.67	0.00	66.67	33.33	3.33
Post-FDG	6.67	7.41	3.33	0.00	70.00	23.33	10.00
(ZS) + Detailed	Direct	6.67	7.36	13.33	0.00	46.67	43.33	13.33
Post-FDG	13.33	14.02	10.00	0.00	46.67	33.33	20.00
(ZS) + Detailed + CR-All	Direct	6.67	7.59	13.33	0.00	46.67	43.33	13.33
Post-FDG	13.33	14.26	10.00	0.00	46.67	33.33	20.00
Llama3-8B
ZS	Direct	0.00	2.67	0.00	13.33	70.00	40.00	6.67
Post-FDG	0.00	2.67	13.33	0.00	66.67	26.67	20.00
(ZS) + Binary	Direct	3.33	5.83	0.00	20.00	60.00	33.33	6.67
Post-FDG	3.33	5.83	20.00	0.00	60.00	26.67	16.67
(ZS) + Detailed	Direct	0.00	1.41	0.00	20.00	63.33	33.33	6.67
Post-FDG	0.00	4.22	20.00	0.00	56.67	26.67	20.00
(ZS) + Detailed + CR-All	Direct	0.00	2.33	0.00	16.67	66.67	36.67	6.67
Post-FDG	3.33	7.00	16.67	0.00	63.33	26.67	23.33
GPT-4o
ZS	Direct	13.33	19.30	0.00	0.00	40.00	56.66	6.67
Post-FDG	23.33	36.02	0.00	0.00	60.00	13.33	13.33
ZS + CR-SYN	Direct	10.00	17.14	0.00	0.00	26.67	66.67	6.67
Post-FDG	26.67	39.11	0.00	0.00	50.00	20.00	16.67
ZS + CR-UDF	Direct	10.00	18.54	0.00	10.00	33.33	46.67	16.67
Post-FDG	23.33	36.52	0.00	0.00	46.67	23.33	16.67
ZS + CR-TUF	Direct	6.67	14.05	0.00	3.33	23.33	63.33	10.00
Post-FDG	23.33	35.03	0.00	0.00	56.67	13.33	10.00
(ZS)	Direct	16.67	23.28	0.00	0.00	36.67	53.33	6.67
Post-FDG	30.00	40.83	0.00	0.00	56.67	10.00	10.00
(ZS) + Binary	Direct	16.67	24.30	0.00	0.00	33.33	53.33	6.67
Post-FDG	26.67	41.02	0.00	0.00	60.00	10.00	6.67
(ZS) + Detailed	Direct	16.67	28.91	0.00	0.00	36.67	43.33	16.67
Post-FDG	30.00	44.15	0.00	0.00	56.67	13.33	3.33
(ZS) + CR-SYN	Direct	20.00	24.12	0.00	0.00	36.67	53.33	3.33
Post-FDG	30.00	40.83	0.00	0.00	60.00	10.00	6.67
(ZS) + CR-UDF	Direct	20.00	24.12	0.00	0.00	30.00	56.67	6.67
Post-FDG	30.00	40.83	0.00	0.00	56.67	10.00	10.00
(ZS) + CR-TUF	Direct	16.67	23.07	0.00	0.00	33.33	53.33	10.00
Post-FDG	26.67	37.47	0.00	0.00	60.00	13.33	6.67
(ZS) + Detailed + CR-SYN	Direct	23.33	29.74	0.00	0.00	30.00	50.00	10.00
Post-FDG	30.00	43.12	0.00	0.00	53.33	16.67	3.33
(ZS) + Detailed + CR-UDF	Direct	26.67	34.18	0.00	0.00	33.33	43.33	10.00
Post-FDG	30.00	44.23	0.00	0.00	53.33	13.33	6.67
(ZS) + Detailed + CR-TUF	Direct	13.33	25.41	0.00	0.00	33.33	46.67	16.67
Post-FDG	30.00	43.98	0.00	0.00	56.67	13.33	3.33
(ZS) + Detailed + CR-All	Direct	13.33	24.54	0.00	0.00	33.33	50.00	16.67
Post-FDG	33.33	46.45	0.00	0.00	50.00	13.33	6.67

\uparrow

提示策略	导言	Pass $\uparrow$	FEO $\uparrow$	TRO $\downarrow$	IVI $\downarrow$	SYN $\downarrow$	UDF $\downarrow$	TUF $\downarrow$
DeepSeekMath-7B
ZS	直接	13.33	14.69	16.67	0.00	40.00	36.67	13.33
Post-FDG	16.67	18.02	13.33	0.00	43.33	30.00	16.67
(ZS) + Binary	直接	3.33	3.33	6.67	0.00	66.67	33.33	3.33
Post-FDG	6.67	7.41	3.33	0.00	70.00	23.33	10.00
(ZS) + Detailed	直接	6.67	7.36	13.33	0.00	46.67	43.33	13.33
Post-FDG	13.33	14.02	10.00	0.00	46.67	33.33	20.00
(ZS) + Detailed + CR-All	直接	6.67	7.59	13.33	0.00	46.67	43.33	13.33
Post-FDG	13.33	14.26	10.00	0.00	46.67	33.33	20.00
Llama3-8B
ZS	直接	0.00	2.67	0.00	13.33	70.00	40.00	6.67
Post-FDG	0.00	2.67	13.33	0.00	66.67	26.67	20.00
(ZS) + Binary	直接	3.33	5.83	0.00	20.00	60.00	33.33	6.67
Post-FDG	3.33	5.83	20.00	0.00	60.00	26.67	16.67
(ZS) + Detailed	直接	0.00	1.41	0.00	20.00	63.33	33.33	6.67
Post-FDG	0.00	4.22	20.00	0.00	56.67	26.67	20.00
(ZS) + Detailed + CR-All	直接	0.00	2.33	0.00	16.67	66.67	36.67	6.67
Post-FDG	3.33	7.00	16.67	0.00	63.33	26.67	23.33
GPT-4o
ZS	直接	13.33	19.30	0.00	0.00	40.00	56.66	6.67
Post-FDG	23.33	36.02	0.00	0.00	60.00	13.33	13.33
ZS + CR-SYN	直接	10.00	17.14	0.00	0.00	26.67	66.67	6.67
Post-FDG	26.67	39.11	0.00	0.00	50.00	20.00	16.67
ZS + CR-UDF	直接	10.00	18.54	0.00	10.00	33.33	46.67	16.67
Post-FDG	23.33	36.52	0.00	0.00	46.67	23.33	16.67
ZS + CR-TUF	直接	6.67	14.05	0.00	3.33	23.33	63.33	10.00
Post-FDG	23.33	35.03	0.00	0.00	56.67	13.33	10.00
(ZS)	直接	16.67	23.28	0.00	0.00	36.67	53.33	6.67
Post-FDG	30.00	40.83	0.00	0.00	56.67	10.00	10.00
(ZS) + Binary	直接	16.67	24.30	0.00	0.00	33.33	53.33	6.67
Post-FDG	26.67	41.02	0.00	0.00	60.00	10.00	6.67
(ZS) + Detailed	直接	16.67	28.91	0.00	0.00	36.67	43.33	16.67
Post-FDG	30.00	44.15	0.00	0.00	56.67	13.33	3.33
(ZS) + CR-SYN	直接	20.00	24.12	0.00	0.00	36.67	53.33	3.33
Post-FDG	30.00	40.83	0.00	0.00	60.00	10.00	6.67
(ZS) + CR-UDF	直接	20.00	24.12	0.00	0.00	30.00	56.67	6.67
Post-FDG	30.00	40.83	0.00	0.00	56.67	10.00	10.00
(ZS) + CR-TUF	直接	16.67	23.07	0.00	0.00	33.33	53.33	10.00
Post-FDG	26.67	37.47	0.00	0.00	60.00	13.33	6.67
(ZS) + Detailed + CR-SYN	直接	23.33	29.74	0.00	0.00	30.00	50.00	10.00
Post-FDG	30.00	43.12	0.00	0.00	53.33	16.67	3.33
(ZS) + Detailed + CR-UDF	直接	26.67	34.18	0.00	0.00	33.33	43.33	10.00
Post-FDG	30.00	44.23	0.00	0.00	53.33	13.33	6.67
(ZS) + Detailed + CR-TUF	直接	13.33	25.41	0.00	0.00	33.33	46.67	16.67
Post-FDG	30.00	43.98	0.00	0.00	56.67	13.33	3.33
(ZS) + Detailed + CR-All	直接	13.33	24.54	0.00	0.00	33.33	50.00	16.67
Post-FDG	33.33	46.45	0.00	0.00	50.00	13.33	6.67

\uparrow

Prompt Strategy	Preamble	Pass $\uparrow$	FEO $\uparrow$	TRO $\downarrow$	IVI $\downarrow$	SYN $\downarrow$	UDF $\downarrow$	TUF $\downarrow$
miniF2F-Test
ZS	Direct	25.41	48.90	1.23	1.23	6.15	23.77	7.38
Post-FDG	67.21	81.88	0.00	0.00	3.28	2.87	5.33
(ZS) + Detailed	Direct	37.30	63.28	2.05	1.23	5.74	9.02	8.61
Post-FDG	83.61	91.47	0.00	0.00	2.05	0.82	3.28
Def_Wiki-Test
ZS	Direct	10.87	16.43	8.70	8.70	15.22	52.17	13.04
Post-FDG	34.78	43.19	6.52	0.00	23.91	19.57	28.26
(ZS) + Detailed	Direct	19.57	23.77	8.70	8.70	8.70	47.83	10.87
Post-FDG	43.48	50.76	6.52	0.00	17.39	10.87	28.26
Def_ArXiv
ZS	Direct	13.33	19.30	0.00	0.00	23.33	66.67	6.67
Post-FDG	23.33	36.02	0.00	0.00	60.00	13.33	13.33
(ZS) + Detailed	Direct	16.67	28.91	0.00	0.00	23.33	46.67	20.00
Post-FDG	30.00	44.15	0.00	0.00	56.67	13.33	3.33

\uparrow

提示策略	导言	Pass $\uparrow$	FEO $\uparrow$	TRO $\downarrow$	IVI $\downarrow$	SYN $\downarrow$	UDF $\downarrow$	TUF $\downarrow$
miniF2F-Test
ZS	直接	25.41	48.90	1.23	1.23	6.15	23.77	7.38
Post-FDG	67.21	81.88	0.00	0.00	3.28	2.87	5.33
(ZS) + Detailed	直接	37.30	63.28	2.05	1.23	5.74	9.02	8.61
Post-FDG	83.61	91.47	0.00	0.00	2.05	0.82	3.28
Def_Wiki-Test
ZS	直接	10.87	16.43	8.70	8.70	15.22	52.17	13.04
Post-FDG	34.78	43.19	6.52	0.00	23.91	19.57	28.26
(ZS) + Detailed	直接	19.57	23.77	8.70	8.70	8.70	47.83	10.87
Post-FDG	43.48	50.76	6.52	0.00	17.39	10.87	28.26
Def_ArXiv
ZS	直接	13.33	19.30	0.00	0.00	23.33	66.67	6.67
Post-FDG	23.33	36.02	0.00	0.00	60.00	13.33	13.33
(ZS) + Detailed	直接	16.67	28.91	0.00	0.00	23.33	46.67	20.00
Post-FDG	30.00	44.15	0.00	0.00	56.67	13.33	3.33

\uparrow

Prompt Strategy	Preamble	Pass $\uparrow$	FEO $\uparrow$	TRO $\downarrow$	IVI $\downarrow$	SYN $\downarrow$	UDF $\downarrow$	TUF $\downarrow$
GPT-4o
Soft-IFDC	Direct	6.52	11.45	8.70	0.00	17.39	71.74	2.17
Post-FDG	19.57	29.65	0.00	0.00	34.78	30.43	26.09
Hard-IFDC	Direct	4.35	11.86	10.87	0.00	10.87	69.57	6.52
Post-FDG	19.57	26.95	0.00	0.00	36.96	21.74	39.13
(ZS) + Soft-IFDC + Binary	Direct	15.22	20.47	8.70	2.17	15.22	58.70	10.87
Post-FDG	41.30	51.09	6.52	0.00	26.09	10.87	26.09
(ZS) + Soft-IFDC + Detailed	Direct	15.22	20.20	8.70	2.17	13.04	56.52	13.04
Post-FDG	41.30	51.26	6.52	0.0	23.91	10.87	26.09

\uparrow

Autoformalization in the Wild: Assessing LLMs on Real-World Mathematical Definitions

野外自动形式化：评估大语言模型在真实世界数学定义上的表现

Abstract

摘要

1 Introduction

1 引言

2 Autoformalization with LLMs

2 用大语言模型做自动形式化

2.1 Limitations of Existing Benchmarks

2.1 已有基准的局限

2.2 Real-World Mathematical Definitions

2.2 真实世界的数学定义

3 Empirical Evaluation

3 实证评估

Empirical Setup.

实验设置。

Evaluation Metrics.

评估指标。

3.1 Zero-Shot Prompting & Binary Refinement

3.1 零样本提示与二元精炼

Def_Wiki and Def_ArXiv are significantly more challenging than miniF2F.

Def_Wiki 和 Def_ArXiv 明显比 miniF2F 更具挑战性。

LLMs can provide false preambles when performing autoformalization.

大语言模型在做自动形式化时可能给出虚假导言。

Specialized smaller models can reach the same level of success rate as larger LLMs.

专门化的较小模型可以达到与更大模型同一水平的成功率。

Small LLMs possess limited binary self-correction capabilities.

较小的大语言模型只具备有限的二元自纠正能力。

3.1.1 Error Analysis & Interventions

3.1.1 错误分析与干预

3.2 Categorical Refinement

3.2 分类精炼

Providing LLMs with more information about individual errors is more effective than simply indicating binary correctness.

向大语言模型提供关于各个错误的更多信息，比只标明二元正确性更有效。

Categorical refinement reduces error rates.

分类精炼会降低错误率。

Categorical refinement can effectively reduce errors for specific categories.

分类精炼可以有效降低特定类别的错误。

3.3 Symbolic Refinement

3.3 符号精炼

Symbolic Refinement can effectively reduce SYN errors in the generated formal codes on definition datasets.

符号精炼可以有效降低定义数据集上所生成形式代码中的 SYN 错误。

3.4 Post-FDG

Autoformalization performance can be underestimated without including contextual information.

若不纳入上下文信息，自动形式化的性能可能被低估。

FDG can reduce the occurrence of errors caused by referring to undefined mathematical objects.

FDG 可以减少因引用未定义数学对象而造成的错误。

Errors in autoformalized codes for definition datasets are more likely to be entangled than those in the miniF2F dataset.

定义数据集上自动形式化代码中的错误，比 miniF2F 数据集中的错误更可能相互纠缠。

3.5 Generalizability to Lean4

3.5 向 Lean4 的可推广性

Definitions present greater complexity for autoformalization in Lean4.

对 Lean4 中的自动形式化而言，定义同样带来更大的复杂性。

Categorical Refinement generalizes to Lean4.

分类精炼可以推广到 Lean4。

4 Related Work

4 相关工作

5 Conclusion

5 结论

6 Limitations

6 局限

Acknowledgements

致谢

References

参考文献

Appendix A Detailed Information about the Dataset Creation

附录 A 关于数据集创建的详细信息

Appendix B Case Study for Formal Definition Grounding

附录 B 形式定义锚定的案例研究

Definition of Bradley–Terry model:

Bradley–Terry 模型的定义：

Appendix C Examples of Incorrect Formal Codes

附录 C 不正确形式代码的例子

Definition of Rademacher Complexity:

Rademacher 复杂度的定义：

Definition of Algorithm Selection:

算法选择的定义：

Definition of Set-Family Growth Function:

集合族增长函数的定义：

Appendix D Formal Definition Grounding via Prompting