💬 NLP

Formalize Once, Edit the Rest: Efficient Lean-Based Answer Selection for Math Reasoning

本文介绍了 BASE，这是一个基于“生成与编辑”的流水线，它利用一个专门的重写模型（LEANSCRIBE）来形式化单个候选答案，并通过原地编辑高效地推导出剩余的 K-1 个形式化陈述，从而在显著降低计算成本的同时，提高了基于 Lean 的数学推理中的答案选择准确率。

原作者： Ji Feng, Zhouxing Shi

发布于 2026-06-16

📖 1 分钟阅读☕ 轻松阅读

CC BY 4.0

原作者： Ji Feng, Zhouxing Shi

原始论文采用 CC BY 4.0 许可（http://creativecommons.org/licenses/by/4.0/）。 ✨ 这是对下方论文的AI生成解释。它不是由作者撰写或认可的。如需技术准确性，请参阅原始论文。阅读完整免责声明

想象一下，你是一位正在批改一叠由一名聪明但有时会犯糊涂的学生（即 AI）撰写的 8 篇不同数学论文的老师。每篇论文都试图解决同一个问题，但它们最终得出的答案略有不同。你的任务是找出哪一个是真正正确的。

传统上，为了检查一个答案是否正确，你可能会向一个非常严谨、可由机器检查的数学机器人（称为 Lean）请求验证每一篇论文。但问题在于，在机器人检查论文之前，你必须将学生凌乱的自然语言手写体翻译成机器人的严格计算机代码语言。这个翻译过程缓慢、昂贵且需要大量的计算能力。如果你有 8 篇论文，你就必须为 8 次昂贵的翻译付费。

这篇论文介绍了一种名为 BASE（Base-and-Edit，基础与编辑）的新方法，它改变了游戏规则。与其从头开始翻译所有 8 篇论文，BASE 做了一件聪明的事：

1. “基础”（Base）的发现

首先，系统按置信度顺序查看论文（从学生认为最可能正确的论文开始）。它只将其中一篇翻译成机器人的语言，并询问机器人：“这是否有意义？”

如果机器人说“是的，这是一个有效的数学陈述”，那么这一篇就成为了基础（Base）。
如果机器人说“不”，它会尝试下一篇。
通常，第一次或第二次尝试就会成功。因此，你只需支付一次昂贵的翻译费用。

2. “编辑”（Edit，神奇的技巧）

现在，与其从头开始翻译剩余的 7 篇论文，BASE 意识到它们与第一篇几乎完全相同。它们共享相同的题目结构；只是结尾处的数字或答案有所不同。

把第一篇翻译好的论文想象成一个饼干模具。其他 7 篇论文只是同一个饼干形状，但换了不同的“馅料”（即答案）。

简单编辑： 如果答案的写法完全一致（例如“5”），BASE 只需更换数字。
智能编辑 (LEANSCRIBE)： 有时学生会以奇怪的方式书写答案（例如“13 的平方根乘以 3”）。机器人可能会将其翻译为一个复杂的代码块。BASE 使用一个名为 LEANSCRIBE 的特殊辅助模型来确定这个复杂代码块究竟在哪里，以及如何将其替换为新答案的代码。这就像拥有一位大师级厨师，他知道如何在不破坏整道菜的前提下，精准地更换食谱中的某一种食材。

结果：一种“帕累托改进”（Pareto Improvement）

论文声称这种方法是一种“帕累托改进”，这是一个高级说法，意思是：“我们在花费更少钱的同时，获得了更好的结果。”

更便宜： 与其支付 8 次翻译费用，他们只需支付 1 次翻译和 7 次廉价的编辑。这使成本降低了约 5 倍（具体来说，平均降低了 5.4 倍）。
更准确： 令人惊讶的是，这种方法找到正确答案的频率竟然比从头检查所有人还要高。为什么呢？因为通过复用机器人已经认可的“基础（Base）”，该系统避免了从头翻译新的、凌乱的论文时容易产生的错误。这就像是使用一个经过验证、坚固的房屋蓝图并仅仅更改油漆颜色，而不是每次都试图从零开始建造一座新房子。

核心结论

作者构建了一个不再浪费时间重复翻译同一个数学问题的系统。它找到一个“好”的版本，将其锁定，然后仅针对其余部分进行微调。这使得使用 AI 检查数学答案变得更快、更便宜，而且出人意料地更加可靠。

他们并未声称：

他们并没有说这能修复 AI 的数学能力；它只是有助于从列表中选出最佳答案。
他们并没有声称这适用于所有类型的题目（仅适用于那些答案在结构上看起来相似的题目）。
他们承认，虽然“翻译”过程得到了检查，但最终的“证明”（即逐步的逻辑推理）对于目前的机器人来说仍然很难快速完成，因此他们首先专注于检查答案在机器人的语言中是否“看起来”是正确的。

技术摘要：一次形式化，编辑其余部分 (BASE)

1. 问题陈述

随着大语言模型（LLMs）越来越多地应用于数学推理，它们通常会针对单个问题生成多个不同的推理路径和候选答案。一个关键的挑战在于答案选择：在测试时扩展（test-time scaling）过程中，如何在没有获取地面真值标签（ground-truth labels）的情况下验证哪个候选答案是正确的。

虽然现有的方法（如多数投票或学习型奖励模型）提供了统计信号，但它们缺乏形式化保证。近期的研究利用形式化证明助手（特别是 Lean 4）来验证候选答案。在这种范式中，“自动形式化器”（autoformalizer）将问题和候选答案翻译成一个 Lean 定理陈述，该陈述断言答案的正确性。随后，证明器尝试验证该陈述。

然而，存在一个显著的瓶颈：为了验证 $K$ 个候选答案，自动形式化器必须独立调用 $K$ 次。这产生了 $\Theta(K)$ 的计算成本，其规模随样本数量线性增长。作者观察到，对于同一个问题， $K$ 个形式化陈述几乎是完全相同的，它们共享相同的题目结构，仅在答案表达式上有所不同。核心问题在于如何利用这种共享结构，将形式化成本从 $\Theta(K)$ 降低到 $\Theta(1)$ ，且不牺牲选择的准确性。

2. 方法论：BASE 流水线

作者提出了 BASE（Base-and-Substitute-Edit，基准与替换-编辑）流水线，旨在形式化单个“基准”候选答案，并通过局部编辑导出剩余的 $K-1$ 个陈述。

2.1 基准发现 (Base Discovery)

流水线始于上游求解器生成的一个按置信度排序的 $K$ 个候选答案列表 $S(x) = (a_1, \dots, a_K)$ 。

系统按排名顺序遍历候选答案。
对于每个候选答案 $a_i$ ，它尝试将问题-答案对 $(x, a_i)$ 形式化为 Lean 陈述 $F_i$ 。
过程在第一个在 Lean 中成功通过类型检查（type-checks）的候选答案 $a_b$ 处停止。
$F_b$ 成为基准形式化陈述， $a_b$ 成为基准答案。
如果没有任何候选答案通过类型检查，系统则回退至排名第一的候选答案 $a_1$ 。

2.2 替换级联 (Substitution Cascade)

一旦建立了有效的基准 $F_b$ ，系统通过就地编辑 $F_b$ 来反映其他候选答案，从而生成剩余的 $K-1$ 个陈述。这通过一个两层级联处理：

第一层 (R1)：基于规则的直接定位
- 系统尝试通过在“门控区域”（定理主体，排除注释/头部）内进行精确字符串匹配来定位答案表达式。
- 如果找到唯一的匹配项，系统执行答案字符串的直接替换。
- 如果出现多个匹配项，则由一个小型的消歧模型选择正确的槽位。
- 此层级效率很高，但在自动形式化器以多样化的语法形式（例如，将元组 (3, 5) 编码为独立的绑定或 Prod 值，而非逐字字符串）对答案进行编码时会失效。
第二层 (R2)：LEANSCRIBE (学习型重写器)
- 对于 R1 失效的情况，系统调用 LEANSCRIBE，这是一个专门的微调 LLM。
- 输入： 问题 $x$ ，基准形式化 $F_b$ ，以及基准答案 $a_b$ 。
- 输出：
  - 一个局部块 $s$ ：包含答案相关表达式的 $F_b$ 的连续段。
  - 一个填充函数 $f$ ：一个轻量级的 Python 函数，负责将任何非形式化答案 $a_i$ 映射到替换 $s$ 后的对应 Lean 表达式。
- 执行： LEANSCRIBE 每个问题仅运行一次。生成的函数 $f$ 随后被应用于所有剩余的候选答案 $a_i$ ，以生成它们的正式陈述 $F_i = f(a_i)$ 。这通过将模型调用成本分摊到所有 $K-1$ 个候选答案上实现了成本摊销。

2.3 验证与选择

流水线依赖陈述级类型检查作为主要的选择信号。

如果候选答案的正式陈述 $F_i$ 通过类型检查（即是一个良构的命题），则认为该候选答案被“验证”了。
系统选择排名最高的候选答案 $a_j$ ，使其满足 $F_j$ 通过类型检查。
如果没有候选答案通过类型检查，则回退至排名第一的候选答案 $a_1$ 。
作者指出，虽然证明级验证（运行证明器）更为严谨，但目前的证明器 Pass@1 率较低，因此在预算受限的情况下，陈述级类型检查是更实用的选择信号。

3. 核心贡献

BASE 流水线： 第一个通过在多个候选答案间共享单个已验证基准陈述，将形式化成本从 $\Theta(K)$ 降低到 $\Theta(1)$ 的实现形式化成本摊销的工作。
LEANSCRIBE 模型： 一种学习型重写器，经过训练可定位答案相关块并生成可重用的编辑函数，能够处理基于规则的替换无法处理的多样化语法编码。
帕累托改进 (Pareto Improvement)： 该方法在所有测试配置下均实现了更高的选择准确率，同时显著降低了计算成本。

4. 实验结果

作者在四个基准测试（MATH-500, OlympiadBench, AMC-AIMO, AIME 2024）上评估了 BASE，使用了三种不同的上游求解器（Gemini 3 Pro, Qwen3-8B, DeepSeek-R1-Qwen3-8B），设置 $K=8$ 个候选答案。

准确率： 与独立形式化相比，BASE 在所有 12 个（数据集，求解器）配置中都提高了选择准确率（Acc），增幅在 +0.7 到 +23.3 个百分点之间。
鲁棒性： “金标答案通过率”（GT-pass，即正确答案的陈述通过类型检查的比例）显著提升（最高达 +33.3 点），在许多情况下达到了 96–100%。这表明，通过共享一个经过验证的基准，可以使正确答案的形式化更加稳健。
成本效率： 在 $K=8$ 时，BASE 将自动形式化器的调用次数减少了约 5.4 倍（平均减少 4.7–6.5 倍）。其成本随 $K$ 的变化呈 $\Theta(1)$ 规模，而非 $\Theta(K)$ 。
消融实验： 若移除学习型重写器（LEANSCRIBE）而仅依赖基于规则的替换（R1），会导致候选覆盖率大幅下降（下降 8–22 个百分点），这证明了学习组件在处理多样化语法编码方面的必要性。
证明级分析： 即使使用证明器（DeepSeek-Prover-V2）且每个候选答案仅进行一次尝试，BASE 在 12 个配置中的 11 个中都提高了证明级准确率，这表明结构更好的正式陈述有助于下游证明器。

5. 重要性与主张

论文声称 BASE 代表了基于 Lean 的答案选择的一种 帕累托改进。通过“一次形式化，编辑其余部分”，该方法同时：

降低成本： 大幅降低了形式化验证的推理成本，使得使用大 $K$ 进行测试时扩展（test-time scaling）变得更加可行。
提高准确率： 增强了选择正确答案的可靠性，这可能是因为共享的基准结构降低了自动形式化器在处理正确候选答案时的方差和失败率。

作者强调，这种方法是现有流水线（通过集成到 FANS 流水线中得到证明）中形式化阶段的“即插即用式替代品”，且其收益是由验证器在利用共享、已验证的脚手架（scaffold）时能更有效地保留正确答案所驱动的，而非由上游求解器的生成能力变化所驱动。

该工作承认了局限性，指出由于目前的证明器限制，其研究重点在于陈述级类型检查，并假设候选答案共享问题侧的结构。它并不声称解决了自动形式化的忠实度问题（即错误答案仍可能通过类型检查），但指出结合求解器排名可以减轻这一风险。