(特性)假设与正确性:神经符号验证体系结构

**具体问题。** 风险分数、严重性等级和LLM检测过滤器是承载安全性的核心逻辑，目前它们由基于示例的测试进行保护。对于一个完全依靠可信的工具来说，这种缺口就是问题。**这不是理论上的问题，考古学已经发现了两个问题。** 在阅读评分代码时，我们发现（1）评分依赖于同等严重性的检测结果的输入顺序，因此添加一个低置信度的检测结果可能会降低评分（`report.py:111-135`），以及（2）0-100转换为[0,1]的置信度规则在不同调用点之间不一致（`>1.0`与历史的`>2.0`）。这两个问题正是一种潜在缺陷，如果有明确的、经过检查的规范，就可以发现它。而示例测试并没有发现它。**为什么这种方法是可信的，而不是学术性的。** 它采用了AWS在生产环境中使用的方法（Cedar）：一个小的可执行模型作为真实的来源，通过在CI中进行差异性随机测试来保持其真实性。我们在这里将其应用于现实情况 - 首先使用Python参考模型（没有新的工具链，可以在OSS同步合并中生存），重量级的证明（Lean/Dafny）保留用于实际需要的那一个深层定理（对抗性神经网络的包围）。我们还画出了一个诚实的界限：LLM本身不在正式范围内；我们验证的是符号保护，而不是模型。**为什么这是一个好的开源项目。** 它是自给自足的（位于`tests/`中，并有一个规范模块，不涉及生产行为），自然地分层了不同级别的贡献者（属性测试 → 参考模型 + DRT → 可选定理证明），并生成了持久的成果 - 一个可读的规范和一个CI闸门，这些成果超越了任何一个贡献者。它也是一个强大的展示："对一个AI安全性工具进行持续的形式验证"是一个招聘和信誉的胜利，对于…