给 AI 沙箱做形式化验证是不是千禧年大奖级难题？

teortaxesTex · x · 2026-10-23

转发的一条技术挑战提议：针对运行日益强大、可能具对抗性的 AI agent 的 KVM 沙箱，能否形式化证明「无论 agent 在 VM 内执行什么代码都无法逃逸并危害宿主机」？这需要验证整个相关软件栈——KVM、CPU 虚拟化、内核、可能影响隔离性的虚拟设备。发帖人认为其难度堪比千禧年大奖难题，并提问：能否从数学上确立验证这种复杂度体系在计算上是否可行？作者呼吁进入 AI 对齐领域的数学家考虑这一挑战。