Nemotron 3.5 Lightning微调模型，30B形式化证明胜过50倍

Reasonable 团队用 4B token 的合成 Verus 数据微调了 NVIDIA 最新开源模型 Nemotron 3.5 Lightning（30B）。微调后的模型在单次尝试通过率上超越了一个规模约 50 倍于它的模型，pass@3 则几乎持平。它的 token 生成速度也快于测试过的所有同尺寸开源模型。配套博客还分析了各模型在形式化证明中的失败方式、作弊行为，以及微调带来的影响。