3000 条 Verus 证明后训练，开源模型证明通过率升至 73%

Ferenc Huszár 旗下 Reasonable 团队与 NVIDIA 合作，获得 Nemotron 3.5 Super VL 的早期访问权，测试其为 TLA+ 规约编写有难度的 Verus 形式化证明的能力。团队自建新数据集，用约 3000 条 Verus 证明对模型进行后训练，将证明通过率从 43% 提升至 73%（pass@1 达 73.3%），并开源了相关数据集。

2026-10-15 ~ 2026-10-16 · 2 条相关