ImProver 2：用于神经符号证明优化的迭代自改进语言模型

# ImProver 2：用于神经符号证明优化的迭代性自我改进语言模型  
来源：https://arxiv.org/html/2605.22885  

Riyaz Ahuja  
卡内基梅隆大学  
[email protected]  

Tate Rowney  
卡内基梅隆大学  
[email protected]  

Jeremy Avigad  
卡内基梅隆大学  
[email protected]  

Sean Welleck  
卡内基梅隆大学  
[email protected]  

###### 摘要  

形式化数学库正在快速扩展，这产生了对已验证证明进行重构以维护可维护性以及提升神经证明器训练数据质量的日益增长的需求。然而，可扩展的证明优化受到了目标异构且启发式指定、数据稀缺以及训练和推理成本高昂的阻碍。为了克服这些挑战，我们引入了 ImProver 2，这是一个用于在 Lean 4 中自动进行证明优化的神经符号框架。ImProver 2 结合了一个数据高效的专家迭代流水线和一个暴露形式化结构以及轻量级非形式化抽象的脚手架。我们还引入了一套衡量证明结构属性的指标。使用 ImProver 2，我们训练了一个 7B 参数的模型，该模型在相同模型族中超越了数量级更大的模型，并在多项指标上与中等规模的先进模型竞争。我们还证明，我们的神经符号脚手架显著提升了小型和前沿模型的性能。我们表明，通过适当的脚手架和训练，小型模型能够有效地重构研究级证明，覆盖复杂且多样的指标，与显著更大的系统相匹敌，并将证明优化确立为一个可规模化、可学习的任务。  

## 1 引言  

形式化证明助手，如 Lean（Moura 和 Ullrich，2021）、Rocq（The Coq Development Team，2024）和 Isabelle（Wenzel 等，2008），通过使证明的正确性显式且机械化，改变了数学实践。社区库如 Lean 的 Mathlib（The Mathlib Community，2020）现正以人类贡献增长和神经定理证明与自动形式化的最新进展（Achim 等，2025；Hubert 等，2025）共同驱动的速度扩张。这种快速扩展引发了对数据质量的多个担忧。首先，这种扩展因证明风格和清晰度往往参差不齐（The Mathlib Community，2020）而对库的可维护性、一致性和长期可用性造成压力。其次，低质量的库降低了其作为训练数据的效用：现代定理证明器和自动形式化器正越来越多地基于这些语料库进行训练，因此证明的结构和可读性直接影响下游证明器的性能（Gu 等，2025）。不幸的是，形式化库的增长速度已超过人类审阅者和维护者能够可靠地管理的速度；而且，由于机器生成的证明数量日益增加，这种差距预计只会扩大——即便这些证明被保证正确，也无法保证其质量、模块性或可理解性（Chen 等，2025）。这推动了自动化证明优化的动机：给定一个已验证的证明，生成一个形式正确的重写，使其在用户定义的目标（如更短的长度、更高的模块性或更少的显式依赖）下得分更高（Ahuja 等，2025）。由于目标因用例和形式化上下文而异，实用方法必须能够跨任意指标和研究级定理进行扩展。小型专用模型在这种场景中特别有吸引力，因为相关数据在通用语料库中稀缺，库级部署可能需要数百万个样本，且本地开源权重模型对形式化项目更易获取。  

我们通过 ImProver 2 解决这些问题，这是一个自我改进的流水线，训练小型语言模型（SLM）在广泛类型的指标下优化 Lean 证明。我们的核心思想是利用迭代偏好优化：在生成证明候选、根据正确性和所需优化标准评分、以及从由此产生的高低评分证明对中学习之间进行迭代。特别地，我们将迭代推理偏好优化（IRPO）（Pang 等，2024）算法扩展为一个新的回放缓冲区，该缓冲区平衡新旧生成的数据用于下一轮训练，防止模型崩溃并允许在多个轮次中单调改进。我们还让模型访问来自 Lean 定理证明环境的丰富信息，包括目标状态、非形式化摘要、引理上下文和示例，我们称之为神经符号增强。我们使用 ImProver 2 针对三种不同的指标训练模型：证明长度、模块性（将证明分解为一系列更小引理的能力）以及定理使用的显式依赖，并表明我们训练的模型能够显著改进其基础模型，并在研究级定理上与更大得多的无脚手架系统保持竞争力。  

总之，我们的贡献是：  

1. **用于证明重构的自我改进 SLM**。我们证明迭代偏好优化可以引导小型语言模型在专用研究库中进行证明优化，使它们在多项无脚手架比较中与更大的模型竞争。  

2. **结构优化指标**。除了证明长度（Ahuja 等，2025；Gu 等，2025）之外，我们还研究了利用证明结构和周围库的模块性和依赖指标。这些指标是与形式化数学专家共同选择的，针对不同的证明重构目标。  

3. **面向研究数学的神经符号增强**。我们提取相关的引理或定义、目标状态追踪以及目标证明的自动非形式化。这种增强提升了小型和大型模型在证明优化上的性能。我们还开源了我们的代码和数据¹。  

¹Github (https://github.com/riyazahuja/improver)  

## 2 相关工作  

对神经符号定理证明——使用深度学习在 Lean 4（Moura 和 Ullrich，2021）等形式化语言中创建或操作已验证的数学证明——的兴趣近年来取得了显著进展（Lu 等，2023；Li 等，2024）。特别是，许多研究专注于根据给定陈述生成形式化证明（Polu 和 Sutskever，2020），最近的系统在非平凡基准和国际知名数学竞赛上达到了高性能（Hubert 等，2025；Achim 等，2025；Chen 等，2025）。许多系统还利用神经符号增强，为生成型证明器模型提供从证明环境收集的信息（Yang 等，2023；Ahuja 等，2025；Lin 等，2025）。然而，当前基于 LLM 的系统生成的无论是形式化还是非形式化证明，即使正确，也常常存在风格不一致的问题，包括冗余步骤或不能清晰表示更广泛逻辑论证的结构（Frieder 等，2025）。之前的工作（Ahuja 等，2025；Gu 等，2025）试图通过创建基于 LLM 的代理来重构形式化证明以解决这些问题。Ahuja 等人（2025）创建了一个能够针对多个改进指标进行优化的系统；然而，它依赖于通用的闭源模型，导致部署成本高昂，且难以超越这些模型的基线性能。Gu 等人（2025）仅专注于根据一种复杂分词器优化证明的 token 数量，以缩短编译时间；他们未考察其他指标，忽略了重要的用例，限制了其对研究数学家的实用性。此外，上述工作未能充分利用交互式定理证明环境中通过目标状态提取（Polu 和 Sutskever，2020）、前提检索（Yang 等，2023）或自动非形式化（Hattori 等，2025）获得的信息；两者都至少忽略了这些方面中的一个。  

## 3 证明优化  

给定一个已验证的证明，证明优化代理会合成一个语义等价、在用户指定目标下“更好”且根据 Lean 内核保持正确的证明。我们沿用 Ahuja 等人（2025）和 Gu 等人（2025）的设置，并引入两个额外的结构指标：模块性和依赖。  

**原始定理**  
`theorem isCoatom_iff [OrderTop A] {K : A} : IsCoatom K ↔ K ≠ ⊤ ∧ ∀ H g, K ≤ H → g ∉ K → g ∈ H → H = ⊤ := by simp_rw [IsCoatom, lt_iff_le_not_le, SetLike.not_le_iff_exists, and_comm (a := _ ≤ _), and_imp, exists_imp, ← and_imp, and_comm]`  

**原始定理**  
`theorem mem_cross_iff (x y : TSet γ) : ∀ a, a ∈ 'cross hβ hγ hδ x y ↔ ∃ b c, a = ⟨b, c⟩ ' ∧ b ∈ 'x ∧ c ∈ 'y := by intro a; rw [cross, mem_inter_iff, vCross_spec]; constructor; · rintro ⟨h1, b, c, rfl, h2⟩; simp only [op_mem_converse_iff, vCross_spec, op_inj] at h1; obtain ⟨b', c', ⟨rfl, rfl⟩, h1⟩ := h1; exact ⟨b, c, rfl, h1, h2⟩; · rintro ⟨b, c, rfl, h1, h2⟩; simp only [op_mem_converse_iff, vCross_spec, op_inj]; exact ⟨⟨c, b, ⟨rfl, rfl⟩, h1⟩, ⟨b, c, ⟨rfl, rfl⟩, h2⟩⟩`  

**原始引理**  
`lemma KD_weakerThan_KDB : (Hilbert.KD α) ≤ₛ (Hilbert.KDB α) := normal_weakerThan_of_subset $ by intro; aesop;`  

**优化后（依赖）**  
`theorem isCoatom_iff [OrderTop A] {K : A} : IsCoatom K ↔ K ≠ ⊤ ∧ ∀ H g, K ≤ H → g ∉ K → g ∈ H → H = ⊤ := by constructor <;> intro h <;> simp_all [IsCoatom, lt_iff_le_not_le, SetLike.not_le_iff_exists] <;> tauto`  

**优化后（长度）**  
`theorem mem_cross_iff (x y : TSet γ) : ∀ a, a ∈ 'cross hβ hγ hδ x y ↔ ∃ b c, a = ⟨b, c⟩ ' ∧ b ∈ 'x ∧ c ∈ 'y := by simp_all [cross, mem_inter_iff, vCross_spec, op_mem_converse_iff, op_inj] <;> aesop`  

**优化后（模块性）**  
`lemma KD_weakerThan_KDB : (Hilbert.KD α) ≤ₛ (Hilbert.KDB α) := by have h1 : (LO.Modal.Hilbert.KD α).axioms ⊆ (LO.Modal.Hilbert.KDB α).axioms → (Hilbert.KD α) ≤ₛ (Hilbert.KDB α) := by intro h; apply normal_weakerThan_of_subset; apply h; have h2 : (LO.Modal.Hilbert.KD α).axioms ⊆ (LO.Modal.Hilbert.KDB α).axioms := by intro φ hPhi; cases' hPhi with hPhi hPhi; · simp_all [LO.Modal.Hilbert.KD]; · simp_all [LO.Modal.Hilbert.KDB]; exact h1 h2`  

图1：ImProver 2 自动优化人工编写的证明，以减少显式依赖、最小化长度或最大化证明模块性，同时保持形式正确性。  

### 3.1 设置与记号  

令 \(\mathcal{C}\) 表示证明上下文（导入、局部声明、模块元数据等），\(\mathcal{X}\) 表示定理陈述，\(\mathcal{Y}\) 表示证明。考虑 \((c, x, y) \in \mathcal{C} \times \mathcal{X} \times \mathcal{Y}\)，其中 \(y\) 是 \(x\) 在 \(c\) 中的一个声称的证明，可能正确也可能不正确。我们定义一个验证器为可计算函数：  
\[
\text{v}(c, x, y): \mathcal{C} \times \mathcal{X} \times \mathcal{Y} \to \{0, 1\},
\]  
如果 \(y\) 是 \(x\) 在 \(c\) 中一个语法正确且正确的证明，则输出 1。我们还定义  
\[
\mathcal{F}(c, x) = \{ y \in \mathcal{Y} : \text{v}(c, x, y) = 1 \}.
\]  
两个证明 \(y, y' \in \mathcal{F}(c, x)\) 被称为语义等价。我们使用 Lean 4 语言（Moura 和 Ullrich，2021）作为验证器；该语言的内核/类型检查器提供了与类型论模型（现代数学）对应的强保证。  

### 3.2 优化目标  

两个语义等价的证明可能具有显著的语法差异，而且某些特性可能使它们在实践中更可取或更不可取。为了量化这一点，我们定义一个优化指标为可计算函数：  
\[
\mu: \mathcal{C} \times \mathcal{X} \times \mathcal{Y} \to \mathbb{R},
\]  
给定初始定理和证明 \((c, x, y_0)\)，我们目标是找到一个可验证正确的证明，最大化指标得分：  
\[
\arg\max_{\substack{y \in \mathcal{Y} \\ v(c, x, y) = 1}} \mu(c, x, y) \quad (1)
\]  
在实际中，我们通过基于语言模型的 Lean 4 代码生成来近似：通过独立生成多个变体，如果某个变体超越原始值，我们选择改进最大的一个。  

#### 3.2.1 感兴趣的指标  

在这项工作中，我们关注并评估一组三个指标，这些指标设计为形式化证明优化的实用且可解释的结构化目标。这些指标是代理指标，而非审阅者验证的主观证明质量度量：它们支持自动化大规模评估，但本身并不确立人类维护者偏好或下游定理证明器的效用。  

- **长度**：我们旨在最小化证明的长度，以使用的战术数量衡量。在实践中，证明缩短（或“高尔夫”）是形式化数学中的一个常见活动（The Mathlib Community，2020），因为较短的证明通常更易于阅读和维护，并减少编译时的开销。因此，我们将长度指标 \(\mu_{\text{len}}\) 定义为战术数量的负数。  
- **依赖**：我们旨在最小化证明的显式依赖足迹，以证明中显式命名的唯一外部引理的数量衡量。该指标不衡量与库的语义独立性：一个使用 `simp` 或 `omega` 的证明可能内部仍依赖许多事实。这鼓励自包含的证明，不需要使用或记忆大量依赖名称，从而提高可维护性。² 更具体地，给定一个定理和证明 \((c, x, y)\)，我们计算 \(\text{Deps}_{c, x, y}\)，即证明 \(y\) 中显式命名的所有定理的集合（参见 B 节）。指标随后定义为 \(\mu_{\text{dep}}(c, x, y) := -|\text{Deps}_{c, x, y}|\)。  
- **模块性**：我们旨在最大化证明的模块性，直观理解为证明中独立子证明的数量（在我们的示例中...）  

²我们感谢伦敦帝国理工学院 Heather Macbeth 博士提出这个指标背后的想法。