30B小模型微调后写代码证明，击败50倍体量大模型

fhuszar · x · 2026-08-12

Reasonable 团队基于 NVIDIA 最新开源的 30B 模型 Nemotron 3.5 Lightning 进行了微调，专门用于在 Verus 中编写机器可检查的软件正确性证明。

实验结果表明，经过 4B token 的合成数据训练后，该模型在单次尝试通过率上击败了比它大 50 倍的模型，且在 pass@3 指标上表现相当，同时生成速度在同等规模的开源模型中遥遥领先。文章还详细分析了大模型在形式化证明中常犯的错误和“作弊”手段，指出提升吞吐量对于交互式验证和 CI 流程至关重要。