微调后开源模型 Verus 证明通过率从 43% 升至 73%
fhuszar · x · 2026-10-15
ReasonableIO 团队测试了 NVIDIA Nemotron 3.5 Super VL 能否为 TLA+ 规约编写有难度的 Verus 形式化证明，结论是可以。通过自建新数据集做微调后，模型在最难基准上的通过率从 43% 提升到 73%。团队发布了完整报告，涵盖数据集构建、微调方法，以及弥合形式化验证与真实软件工程之间差距的路径。
所属事件:3000 条 Verus 证明后训练，开源模型证明通过率升至 73%(2 条相关)→
「研究」频道最新
- 数据量决定智能边界：按数据排序后锯齿前沿变螺旋 — sebkrier · 2026-10-16
- Doc2Harness 基准：19 个前沿模型测编码 Agent，最高通过率仅 53% — _akhaliq · 2026-10-16
- 李飞飞团队开源 OpenWAM：统一世界-动作模型框架，让机器人视频预训练成大脑 — jiqizhixin · 2026-10-16
- NVIDIA TacitVLA：动作不读思维链，推理收益保留、延迟最高降 3.4 倍 — arankomatsuzaki · 2026-10-16
- Cohere Labs 世界模型公开课第 4 期：一文理清 DreamerV1-V4 架构演进 — Cohere_Labs · 2026-10-16
- GPT-6.1 审查 arXiv：6% 论文主定理有错，近两月降至 1.5% — nitarshan · 2026-10-16