形式化一次，编辑其余部分：基于精益的高效数学推理答案选择

随着 大语言模型 (LLM) 越来越多地应用于数学推理，可以利用 Lean 等形式证明助手以机器可检查的严格性来验证推理输出，从而实现使用案例，例如使用 K 个采样候选答案在测试时间缩放中选择答案。然而，采用精益要求首先对最初采用自然语言的 LLM 输出进行形式化。现有的基于精益的答案选择工作使用自动形式化模型为每个候选答案独立生成精益形式的正式陈述，从而产生大量的计算成本。我们提出了 BASE，这是一个基础和编辑管道，它形式化每个问题的单个基础候选，并通过就地编辑答案表达式来导出剩余的 K-1 语句。为了实现这一点，我们训练了一个重写器模型 LEANSCRIBE，以在基本形式化中本地化答案，并为其他 K-1 候选者生成可重用的编辑函数。 BASE 同时提高了选择准确性并降低了形式化成本 - 这是一种帕累托改进，适用于四个基准测试和三个求解器的所有 12 种配置（数据集、求解器），在 K=8 时将自动形式化器调用减少约 5 倍，随着 K 的增长，减少量预计会更大。代码可在 https://github.com/ucr-rai/base-and-edit 获取。