事件经过
由RAND公司AI、安全和技术中心于2026年6月4日发布的这份同行评审研究报告调查了来自形式化方法、AI基础设施、网络安全、硬件架构和政策领域的23位专家，评估数学验证技术是否能有意义地降低AI训练和推理栈中的风险。核心发现是形式化方法在ML基础设施的特定、范围明确的组件（特别是内存管理子系统、管理程序和硬件-软件接口）中在技术上是可行的，但面临重大采纳障碍，包括工具链不成熟、大型模型训练的随机性以及缺乏行业激励。威胁模型的一个新颖维度是明确的：该报告将风险框架化不仅为外部对手盗取模型权重，还包括不对齐的AI系统利用其自身基础设施中的漏洞绕过安全监测器或自我泄露。作者为前沿AI实验室、硬件供应商、形式化方法研究人员和政府机构提供了初步的社区技术路线图。
影响分析
对于首席信息安全官和AI安全负责人而言，这是首份RAND认可的调查，用于界定形式化验证在当今AI栈中实际可部署的位置与仍在理想化的位置——直接为基础设施加固优先级和供应商采购标准提供信息。明确包含不对齐AI自我泄露作为威胁模型，使其超越了传统网络安全框架。
建议行动
向首席信息安全官和AI基础设施团队分发；使用报告的组件级可行性地图审计您自身ML训练和推理栈的哪些层是形式化验证控制的候选对象，并向您的硬件和云供应商标记差距。