Improving Lean4 Autoformalization via Cycle Consistency Fine-tuning

📄 arXiv: 2603.24372v1 📥 PDF

作者: Arsen Shebzukhov

分类: cs.CL

发布日期: 2026-03-25

备注: 10 pages, 10 figures, pages 10-27 appendix

💡 一句话要点

通过循环一致性微调提升Lean4自动形式化能力

🎯 匹配领域: 支柱二：RL算法与架构 (RL & Architecture)

关键词: 自动形式化 Lean4 循环一致性 强化学习 自然语言处理 数学推理 Qwen3.5-2B

📋 核心要点

  1. 自动形式化旨在将自然语言数学文本转化为形式化语言，但现有模型在语义理解和形式化转换方面存在挑战。
  2. 论文提出利用循环一致性作为奖励信号，通过强化学习微调语言模型，以提升自动形式化的准确性和语义保留能力。
  3. 实验表明，基于循环一致性奖励的强化学习方法，在循环一致性指标上显著优于监督微调，且对形式化质量影响小。

📝 摘要（中文）

自动形式化，即将自然语言数学文本自动翻译成如Lean4等形式化证明语言，有助于加速AI辅助的数学研究，无论是通过证明验证还是证明搜索。本文在FineLeanCorpus上，使用LoRA对Qwen3.5-2B进行微调，用于自然语言到Lean4的形式化。考虑了三种训练方案：使用课程学习（难度1到10）的监督微调（SFT）、不使用课程排序的SFT，以及使用循环一致性奖励和群体相对策略优化（GRPO）的强化学习。循环一致性衡量一个语句的含义在NL到Lean4到NL的循环中被保留的程度，计算为现成的句子嵌入的余弦相似度。在FineLeanCorpus（FLC）和PutnamBench的未见子集上，强化学习显著优于两种SFT变体（FLC上的平均循环一致性为0.669 vs. 0.513；PutnamBench上为0.561 vs. 0.422），同时交叉熵损失仅增加0.011 nats，对形式化质量的影响极小。课程排序没有提供超过随机训练的可衡量的好处。

🔬 方法详解

问题定义：论文旨在解决自然语言数学文本到Lean4形式化语言的自动翻译问题。现有方法，如直接的监督微调，可能无法充分捕捉数学语句的深层语义，导致翻译后的形式化代码在语义上与原始语句不一致。此外，形式化语言的复杂性也使得训练高质量的翻译模型具有挑战性。

核心思路：论文的核心思路是利用循环一致性来指导模型的训练。具体来说，就是将自然语言翻译成Lean4形式化语言，然后再将Lean4形式化语言翻译回自然语言，通过比较原始自然语言和翻译回的自然语言之间的语义相似度，来衡量翻译过程中的语义保持程度。如果翻译过程能够很好地保持语义，那么循环一致性就会很高。

技术框架：整体框架包含三个主要部分：自然语言到Lean4的翻译模型（基于Qwen3.5-2B）、Lean4到自然语言的翻译模型（使用预训练的语言模型，未明确说明具体模型，但用于生成自然语言描述）、以及循环一致性计算模块。训练过程使用强化学习，其中翻译模型作为策略网络，循环一致性作为奖励信号。

关键创新：最重要的创新点在于将循环一致性引入到自动形式化的训练过程中，并将其作为强化学习的奖励信号。这种方法能够有效地提高翻译的语义一致性，从而提升自动形式化的质量。与传统的监督微调方法相比，该方法能够更好地捕捉数学语句的深层语义。

关键设计：论文使用Qwen3.5-2B作为基础模型，并使用LoRA进行微调。强化学习算法采用群体相对策略优化（GRPO）。循环一致性通过计算原始自然语言和翻译回的自然语言的句子嵌入的余弦相似度来衡量。课程学习策略被尝试，但没有观察到明显效果。损失函数包括交叉熵损失和强化学习的奖励函数。

🖼️ 关键图片

fig_0
fig_1
fig_2

📊 实验亮点

实验结果表明，基于循环一致性奖励的强化学习方法在FineLeanCorpus和PutnamBench数据集上，循环一致性分别提升了0.156和0.139，显著优于监督微调方法。同时，交叉熵损失仅略微增加0.011 nats，表明该方法在提升语义一致性的同时，没有显著降低形式化翻译的准确性。

🎯 应用场景

该研究成果可应用于AI辅助数学研究，例如自动验证数学证明、辅助数学家进行定理证明和公式推导。通过自动将数学文本转化为形式化语言，可以降低数学研究的门槛，并加速数学知识的传播和应用。未来，该技术有望应用于智能教育、科学计算等领域。

📄 摘要（原文）

Autoformalization - automatically translating natural language mathematical texts into formal proof language such as Lean4 - can help accelerate AI-assisted mathematical research, be it via proof verification or proof search. I fine-tune Qwen3.5-2B with LoRA for natural language to Lean4 formalization on FineLeanCorpus and consider three training regimes: supervised fine-tuning (SFT) with curriculum learning (difficulty 1 to 10), SFT without curriculum ordering, and reinforcement learning using group relative policy optimization (GRPO) with a cycle consistency reward. Cycle consistency measures how well the meaning of a statement is preserved through a NL to Lean4 to NL' loop, computed as cosine similarity of off-the-shelf sentence embeddings. On an unseen subset of FineLeanCorpus (FLC) and on PutnamBench, RL substantially outperforms both SFT variants (mean cycle consistency 0.669 vs. 0.513 on FLC; 0.561 vs. 0.422 on PutnamBench), while increasing cross-entropy loss by only 0.011 nats, with minimal impact on formalization quality. Curriculum ordering provides no measurable benefit over shuffled training.