用循环一致性强化学习提升自然语言转形式化代码的准确率
Improving Lean4 Autoformalization via Cycle Consistency Fine-tuning
- 用循环一致性作为奖励，通过强化学习优化模型
- 在未见数据上循环一致性达0.669，显著优于监督训练
- 适合需要高保真数学语义转换的研究者
自动形式化——将自然语言数学文本自动翻译为形式化证明语言（如Lean4）——可加速人工智能辅助的数学研究，无论是证明验证还是证明搜索。本文使用LoRA对Qwen3.5-2B进行微调，在FineLeanCorpus上实现自然语言到Lean4的形式化。考虑三种训练策略：带课程学习（难度1到10）的监督微调（SFT）、无课程顺序的SFT，以及使用组相对策略优化（GRPO）和循环一致性奖励的强化学习（RL）。循环一致性衡量陈述在自然语言→Lean4→自然语言'循环中的语义保留程度，采用现成句子嵌入的余弦相似度计算。在未见的FineLeanCorpus子集（FLC）和PutnamBench上，强化学习显著优于两种监督训练方式（FLC上平均循环一致性0.669对比0.513；PutnamBench上0.561对比0.422），同时交叉熵损失仅增加0.011纳特，对形式化质量影响极小。课程学习相比随机训练并无明显优势。
原文摘要 · Abstract (English)
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.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。