评测与安全AI 资源
dawnr：以七种证明器形式化验证为门槛的可信代码助手
trestoncuzzort/dawnr · An assistant built to be trusted by proof, not by sounding right: a small language model trained from random weights on one machine, running with nothing behind it, whose programs carry specifications checked by seven provers (Dafny, Verus, SPARK, Frama-C, Lean 4, Rocq, F*), each also refuting a sabotaged twin. It learns only from what was proved.
ELI5：它是什么，解决什么问题
dawnr 是一个以“先证明、后采信”为核心原则的助手项目，用小型语言模型生成带规格说明的程序，再交由 Dafny、Verus、SPARK、Frama-C、Lean 4、Rocq、F* 七种独立证明器检查。材料记录了学生模型在给定规格时的证明通过率、七证明器一致性门槛、构造性反例（被篡改孪生程序）检验、规格与问题一致性的额外检查，以及在本地硬件上以量化方式运行的整体流程。仓库同时包含从零训练核心模型、用已验证数据微调开源权重、强化学习与门控反馈成新数据、个人记忆与适配器、检索/语音/视觉/工具调用等实验性模块，并声明各项进展与已知失败模式。
# verification-gates# formal-verification# code-generation# small-language-models# specification-language
核心能力与快速开始
★ 4 · Python
- 能做什么
- 提供一套以形式化证明为采信门槛的助手流程：将程序表示为带前置与保证的规格语言 t；把每个程序下放到 Dafny、Verus、SPARK、Frama-C、Lean 4、Rocq、F* 七种证明器验证，并额外要求各证明器否决人工篡改的反例孪生程序；对规格是否真正描述原问题做单独检查；只有通过全部检查的程序才被记为 clean 并进入训练语料。材料还描述了从零训练核心模型、在开源权重上微调、以证明器作为奖励的强化学习、门控判定结果回流为新数据、个人记忆与适配器、以及检索/语音/视觉/工具调用等实验模块。
- 适用场景
- 适合关注程序合成可信度、形式化验证流水线、小语言模型在有限硬件上运行、以及用多证明器交叉检查防止“证明正确但规格错误”的研究与工程场景；也可作为学习多证明器（Dafny、Verus、SPARK、Frama-C、Lean 4、Rocq、F*）协同校验、规格检查与拒绝机制设计的参考资料。材料显示有按规格求解、修复失败证明、由 Python 参考解生成规格、以及门控判定回流扩充训练池等具体做法。
- 项目形态
- 研究实现
- 部署方式
- 材料说明可在单机上以量化方式运行：一颗 Q8_0 的 4.48 GB 学生模型文件在 12 个 CPU 线程上约 15 tokens/秒，纯 CPU 即可运行学生模型与基础模型（4 bit），七种证明器在同一台机器上；也未说明网络依赖或云端服务。但未给出完整安装步骤、支持的操作系统或容器化方式。
- 主要依赖
- 材料提到小硬件场景（如 16 GB 显卡用于训练），训练更大的核心需要 30 GB 显卡，目前该实验尚未运行；未说明具体 CPU 型号、内存下限、磁盘空间、证明器各自版本与安装方式。
- 使用限制
- 材料明确记录多项未解决问题：从零训练的核心模型在所有留出评测上仍为零；在给定期望规格时，微调 4B 在 33 个留出问题上有 28 个被全部七种证明器证明，但同一晚发现其中若干依赖的规格对多种错误答案也成立，按更严格口径合格数量下降；规格与问题一致性仍是薄弱环节，无参考答案时门控识别正确回答的能力有限；300 个答案中 197 个不是合法 t 程序；100 个开发问题中有 3 个因测试对类型判断不一致而无法被任何答案通过；基础模型的视觉、检索与工具调用在被注入指令时表现不稳。此外许可证状态为 NOASSERTION，材料未说明是否可商用。
- 许可证
- NOASSERTION
- 最近推送
- 2026-10-02 06:35
资料检查：2026-10-02 07:00 · 卡片整理：2026-10-02 07:00
卡片由 AI 根据仓库资料整理，未进行安装或运行验证 · 本次更新未完成，保留上次成功内容
讨论 0
登录后参与讨论，阅读资讯无需注册。
还没有评论，来分享第一个看法。