💬 NLP

Improving Lean4 Autoformalization via Cycle Consistency Fine-tuning

该论文提出利用基于循环一致性奖励的强化学习（GRPO）微调 Qwen3.5-2B 模型，在仅极小增加交叉熵损失的情况下，显著提升了自然语言到 Lean4 形式化翻译的语义保持能力，且优于监督微调及课程学习策略。

原作者： Arsen Shebzukhov

发布于 2026-03-26

📖 1 分钟阅读☕ 轻松阅读

原作者： Arsen Shebzukhov

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

这是一篇关于让 AI 更懂数学的研究报告。作者来自斯坦福大学，他解决了一个核心难题：如何让 AI 把人类写的“自然语言数学题”准确翻译成计算机能读懂的“形式化数学语言（Lean4）”。

为了让你轻松理解，我们可以把整个过程想象成**“翻译官与回译员”的特训营**。

1. 核心问题：AI 是个“只会背课文”的翻译官

想象一下，你有一个很聪明的翻译官（AI 模型），他能把中文数学题翻译成一种极其严谨的“计算机代码语言”（Lean4）。

现状：以前的 AI 翻译官，虽然能把句子翻译得语法通顺（代码能运行），但意思经常跑偏。就像把“苹果”翻译成了“香蕉”，虽然都是水果，但计算机验证时会发现逻辑不对。
目标：我们要训练这个翻译官，让他不仅语法对，意思也要完全一致。

2. 解决方案：神奇的“回译”循环（Cycle Consistency）

作者想出了一个绝妙的主意，叫**“循环一致性”。这就像是一个“翻译 - 回译”的闭环游戏**：

第一步（翻译）：翻译官把中文数学题（A）翻译成计算机代码（B）。
第二步（回译）：再请一位“回译员”（另一个 AI），把代码（B）翻译回中文（A'）。
第三步（检查）：比较原来的中文（A）和回译回来的中文（A'）。
- 如果 A 和 A' 意思几乎一样，说明翻译官翻译得很准。
- 如果 A 和 A' 风马牛不相及，说明翻译官胡编乱造。

比喻：这就像你给一个朋友讲了一个笑话，让他用另一种语言讲出来，再让另一个朋友翻回中文。如果翻回来的笑话大家还能笑，说明原意没丢；如果翻回来变成了“今天天气不错”，说明翻译过程丢了灵魂。

3. 三种训练方法的大比拼

作者给翻译官（AI 模型）设计了三种不同的训练方式，看看哪种最有效：

方法一：按难度循序渐进（SFT + 课程学习）

做法：像上学一样，先做简单的数学题（难度 1），再做难的（难度 10）。
比喻：就像小学生先学加减法，再学微积分。
结果：效果一般。在这个特定的任务中，按顺序做题并没有比乱序做题更有优势。

方法二：乱序刷题（SFT 无课程）

做法：把简单题和难题混在一起，随机练习。
结果：和“循序渐进”法差不多，没有明显区别。

方法三：强化学习 + 循环奖励（RL + GRPO）—— 大赢家

做法：这是本文的核心创新。
- AI 自己生成很多种翻译方案。
- 系统用上面的“回译”游戏来打分：回译得越像原题，得分越高。
- AI 根据得分不断调整策略，只保留那些能完美“回译”的翻译方案。
比喻：这不像死记硬背，而像**“试错游戏”**。AI 尝试了 8 种不同的翻译，系统告诉它：“第 3 种翻译回去后意思最准，奖励你！第 5 种意思全乱了，惩罚你！”AI 通过这种反馈，迅速学会了如何抓住数学题的“灵魂”。
结果：完胜！在保持代码语法正确的同时，数学含义的准确度大幅提升。

4. 实验结果：小模型也能逆袭

数据表现：使用“强化学习 + 回译”训练的 AI，在测试题上的表现比传统训练方法高出了很多（分数从 0.51 提升到了 0.67）。
有趣发现：
- 大模型 vs 小模型：作者发现，一个小模型（2B 参数）经过这种“回译特训”后，表现甚至超过了大模型（9B 参数）仅仅靠“死记硬背”（传统训练）的效果。这说明训练方法比模型大小更重要。
- 不同领域的差异：这种训练方法在代数、数论等逻辑严密、符号清晰的领域效果最好；而在微积分、概率等需要大量文字描述和复杂定义的领域，效果稍弱（因为回译时容易把复杂的定义搞混）。

5. 总结与启示

这篇论文告诉我们：

不要只盯着模型大小：有时候，改变训练策略（比如引入“回译”检查机制）比单纯堆砌算力更有效。
自我验证很重要：让 AI 自己检查“翻译回去对不对”，是一种低成本、高效率的纠错手段。
未来方向：虽然这个方法很棒，但它主要检查的是“意思像不像”，还没完全解决“数学证明对不对”的问题。未来的目标是结合计算机编译器的反馈，让 AI 不仅能“说得像”，还能“做得对”。

一句话总结：
作者给 AI 翻译官装了一个“回译检查镜”，通过让它不断练习“翻译 - 回译”的闭环游戏，成功让一个小模型在数学翻译任务上实现了超水平发挥，比传统的死记硬背训练法聪明得多。

这是一份关于论文《Improving Lean4 Autoformalization via Cycle Consistency Fine-tuning》（通过循环一致性微调提升 Lean4 自动形式化能力）的详细技术总结。

1. 研究背景与问题定义 (Problem)

核心挑战：
自动形式化（Autoformalization）旨在将自然语言（NL）的数学文本自动翻译成形式化证明语言（如 Lean4）。尽管大语言模型（LLM）在推理方面取得了进展，但自动形式化仍然困难。模型经常生成语法正确但语义错误的 Lean4 代码，即代码能编译但未能捕捉到预期的数学含义。

具体目标：
本研究旨在探索不同的训练策略，以提高从自然语言到 Lean4（NL $\to$ Lean4）的翻译质量。主要关注点是如何在缺乏人工标注的语义验证信号的情况下，优化模型的语义保真度。

2. 方法论 (Methodology)

作者提出了一种基于**循环一致性（Cycle Consistency）**的强化学习（RL）微调框架，具体步骤如下：

2.1 模型架构与设置

基础模型：使用 Qwen3.5-2B 作为基座模型。
参数高效微调：采用 LoRA (Low-Rank Adaptation) 技术，仅对前馈网络（FFN）子层进行更新，参数量约为 940 万（总参数量 20 亿），可在单张 GPU 上运行。
双模型设置：
1. $f_\theta$ (NL $\to$ Lean4)：可训练的主模型。
2. $g_\phi$ (Lean4 $\to$ NL)：反向翻译器。在监督微调（SFT）阶段训练，在强化学习阶段冻结。

2.2 循环一致性指标 (Cycle Consistency Metric)

定义了一个循环一致性分数 $C_\theta(s)$ 来衡量翻译质量：
$C_\theta(s) = \cos(e(s), e(g_\phi(f_\theta(s))))$
其中：

$s$ 是原始自然语言陈述。
$f_\theta(s)$ 是生成的 Lean4 代码。
$g_\phi(f_\theta(s))$ 是将 Lean4 代码回译后的自然语言 $NL'$。
$e(\cdot)$ 是使用现成模型 all-MiniLM-L6-v2 生成的句子嵌入。
逻辑：如果回译后的 $NL' $与原始$ s$ 的语义相似度高（余弦相似度高），则说明形式化过程较好地保留了原意。

2.3 训练阶段

研究对比了三种训练体制：

监督微调 (SFT) - 课程学习：按难度（1-10）顺序训练，从易到难。
监督微调 (SFT) - 无课程：在打乱顺序的相同数据集上训练（作为消融实验）。
强化学习 (RL) - GRPO：
- 算法：使用 Group Relative Policy Optimization (GRPO)，无需单独的 Critic 模型，通过组内奖励归一化计算优势值。
- 奖励函数：直接使用上述的循环一致性分数 $C_\theta(s)$ 作为奖励。
- KL 惩罚：防止策略偏离 SFT 初始策略过远。
- 数据：使用 FineLeanCorpus (FLC) 的未见部分作为 RL 提示集，PutnamBench 作为独立测试集。

3. 关键贡献 (Key Contributions)

构建微调管道：建立了基于 LoRA 的 Qwen3.5-2B 自动形式化微调流程，并实施了针对 PutnamBench 的数据去污染（Decontamination）处理。
课程学习消融研究：通过对比“按难度排序”与“随机打乱”的 SFT 训练，发现对于 2B 参数量的模型和当前数据规模，课程学习并未带来显著收益。
基于循环一致性的 RL 微调：证明了使用 GRPO 和循环一致性作为奖励信号，能显著提升模型在未见数据上的表现，且仅以极小的交叉熵损失为代价。

4. 实验结果 (Results)

实验在 FineLeanCorpus (FLC) 的未见子集和 PutnamBench（竞赛级难题）上进行评估。

模型/方法	FLC 循环一致性 ( $\bar{C}$ )	PutnamBench 循环一致性 ( $\bar{C}$ )	交叉熵损失 (CE Loss)
Base 2B (Few-shot)	0.093	0.034	-
SFT (无课程) 2B	0.519	0.432	0.640
SFT (课程) 2B	0.513	0.422	0.680
RL (GRPO) 2B	0.669	0.561	0.691
SFT (课程) 9B	0.585	0.548	-

主要发现：

RL 显著优于 SFT：在 FLC 上，RL 比 SFT 课程学习提高了 0.156 的循环一致性；在 PutnamBench 上提高了 0.139。统计检验（Mann-Whitney U）显示差异极显著 ( $p < 10^{-56}$ )。
课程学习无效：SFT 课程版与无课程版在统计上无显著差异，表明在此规模下，难度排序并未带来额外收益。
规模 vs. RL：9B 模型的 SFT 表现优于 2B 的 SFT，但仍低于 2B 的 RL 模型（在 FLC 上）。这表明 RL 信号带来的提升比单纯增加参数（从 2B 到 9B）更有效，尤其是在分布内数据上。
损失控制：RL 训练仅使交叉熵损失增加了 0.011 nats，说明模型的基础语言能力未受明显损害。
领域差异：离散和代数类问题（如数论、组合数学）的表现优于连续数学（如微积分、分析），因为后者生成的 Lean4 结构更复杂，导致回译噪声更大。

5. 意义与局限性 (Significance & Limitations)

意义：

无需编译器反馈的语义优化：传统方法依赖 Lean4 编译器反馈（仅检查语法/类型），而本文提出的循环一致性奖励关注语义保真度，且无需运行耗时的 Lean4 REPL。
低成本高效益：利用 2B 小模型配合 RL 即可达到甚至超过更大模型（9B）SFT 的效果，证明了 RL 在数学形式化任务中的高效性。
通用性：该方法不依赖特定的人工标注，利用现成的嵌入模型即可构建奖励信号。

局限性与未来工作：

奖励黑客（Reward Hacking）：循环一致性是一个代理指标。模型可能通过生成语法正确但数学空洞的代码，或者让回译模型直接“回声”原始语句来获得高分，而非真正理解数学。
回译偏差：评估和奖励均依赖同一个冻结的 $g_\phi$ 模型，如果该模型存在系统性偏差，会影响所有模型的评估结果。
未来方向：结合 Lean4 编译器反馈作为硬约束，扩大模型规模至 9B 进行 RL，以及使用更强的语义等价性检查替代简单的句子嵌入相似度。

总结：
该论文证明了通过引入基于循环一致性的强化学习（GRPO），可以显著提升小参数模型在数学自动形式化任务中的语义准确性，且无需昂贵的编译器反馈或大规模参数，为 AI 辅助数学研究提供了一种高效的新范式。