可证明安全 AI · 形式化保障

今天说一个 AI 系统「安全」，依据是它在测试里没出事——这和上世纪凭经验造桥没有本质区别。可证明安全 AI 路线（如英国 ARIA 的 Safeguarded AI 计划）要给 AI 套上数学可证明的安全包络：先为目标环境建立可验证的世界模型，再形式化地证明 AI 的输出永远不会把系统推出安全边界。如果成功，电网调度、药物设计、自主实验室这类高风险场景就能放心接入强 AI 能力，而不是因不敢用而白白锁死收益。这是「AI 安全」从红队测试的手艺升级为土木工程式学科的那一跃。

最硬的卡点是为开放物理世界建立既足够忠实、又可被形式化验证的世界模型——真实世界不是芯片电路，没有干净的规格说明书；证明的规模化路径完全未知，现有形式化验证在千万行代码级别就已吃力，遑论前沿模型。批评者认为该路线在通用场景根本不可行，这本身说明它是一个值得判定的开放问题。

英国 ARIA（davidad 主持的 Safeguarded AI 计划）、学界的可证明安全路线（Tegmark、Omohundro 等人的倡议与合作者）

读方向：形式化验证/定理证明（Lean、Coq 一类工具）+ 概率世界模型，两边都懂的人全球屈指可数。切入点：挑一个封闭度高的真实场景（如某类电网控制或化学合成约束），做出第一个「带机器可查证安全证明的 AI 控制器」端到端 demo；ARIA Safeguarded AI 的资助项目群是当下最集中的入口。