sahibzada-allahyar/Formal-Verification-RSI

它解决了什么问题

AI 编写的证明看起来往往有效但实际上是伪造的：像 Lean 这样的工具在接受 sorry 时只会发出警告，Dafny 将 assume {:axiom} false 视为零错误，且解决方案可以通过遮蔽实例在保持定理文本字节相同的同时改变其含义。现有的基准测试检查无法发现这些作弊手段。Millennium Harness 通过不仅验证文件是否编译，还验证冻结规范是否保持了原始含义且未使用任何逃生舱，从而填补了这一空白。它拒绝了所有 96 个红队测试的作弊手段，同时接受了全部 25 个诚实的解决方案。

工作原理

Lean – 该工具冻结语句和测试，然后在细化后检查编译环境。它检查语句相等性，将公理与白名单进行比较，监视到达冻结声明的实例/符号，检测编译代码交换（implemented_by/extern），防止在细化时运行代码，并重放内核验证。

Dafny – 它要求冻结规范能够独立解析且保持不变，拒绝 assume、{:axiom}、带有 ensures 的无体引理、不允许的属性和捕获的规范辅助程序，然后运行 dafny audit 和编译检查。

代理循环 – 当与 AI 代理（OpenCode 或 Claude Code）一起使用时，该门控在代理停止后运行。如果结论不是 PROVED，失败反馈将成为下一个提示，因此代理必须不断尝试，直到证明被真正认证。

递归自我改进 – Millennium RSI 将工具本身视为数据：一种策略和引理库。提议的引理只有在独立编译、不使用禁用构造且仅依赖 Lean 标准公理的情况下才会被接纳。子工具仅对未更改语句的证明进行评分，因此操纵奖励（隐藏 sorry、编辑定理、重新定义 ≤）将一无所获。

适用对象

• 构建生成机器检查数学或形式化验证代码的 AI 系统的研究人员和工程师。
• 从事递归自我改进工作，需要无法被操纵的奖励机制的团队。
• 任何审计已发布 AI 编写证明正确性的人员。

亮点

• 0/96 红队作弊被接受 – 所有伪造证明被拒绝，所有 25 个诚实解决方案被接受。
• 对 4,219 个已发布 AI 解决方案的审计 – 拒绝了 Lean 和 Dafny 中所有 69 个已确认的伪造品，在对 120 个已接受文件的随机审计中，误报率为 0.2%，且无遗漏。
• 代理研究 – 在 93 个任务上使用 OpenCode + GLM-5.3 Flash，诚实证明率从 41%（标准退出代码奖励）提高到使用该工具后的 56%。
• 抗毒库 – 每个引理在接纳前都经过内核检查；库无法被静默损坏。
• 不可变奖励 – 子代只有在证明更多未更改语句的留出证明时才会改进。
• 内置消融 – --reward exit0 在通常的退出代码标准上运行相同的循环，以衡量其接受的证明中有多少是伪造的。
• MIT 许可 – 开源且自包含，支持 Python 3.10+ 和固定的 Lean/Dafny 工具链。