把 AI 安全作为工程：证明、压力测试与事故调查

在这期 2026 年 10 月的 YC Paper Club 中，介绍为 Francois 的主持人与斯坦福研究人员 Clark Barrett 和 Mykel Kochenderfer 将 AI 安全作为工程和研究问题讨论。他们的预测与判断是活动中的观点，并非已经确定的结果。

开场将推测性的灾难叙事与构建和评估安全关键系统的实际工作作比较。主持人主张提出明确的论断并谨慎处理证据。

主持人讨论有关 OpenAI–Hugging Face 事件的报道，认为一些标题夸大了独立自主行动的程度。这是主持人对报道事件的解读，并非完整的独立调查。

他分析有关 AI 灾难性风险的调查问题如何表述，并提醒不要把调查回答转换成针对不同时间范围的精确预测。

Barrett 介绍自动推理如何检查形式化陈述的性质，并介绍连接规格、代码与证明的 CSlib 和相关工具。他展示了一个小示例：自然语言请求被转化成形式化规格和经过验证的代码。

证明确立的是形式模型和假设下指定性质成立，并不自动证明规格涵盖所有需求，也不能证明整个部署系统不会被攻破。

Kochenderfer 追问部署带有学习组件的安全关键系统需要什么证据。他介绍航空防撞系统的安全目标，以及测试极罕见故障的挑战。

自适应压力测试寻找可能导致故障的情景，借鉴航空研究并探索在语言模型上的应用。它补充其他证据，而不是证明不存在任何故障。

他还介绍神经网络验证和运行时监控。讨论强调检查相关性质，并在系统运行期间持续收集信号。

嘉宾讨论借鉴航空实践建立独立事故调查机构，以及自愿报告机制。这是一项提议，其范围、治理和效果取决于实施方式。

Barrett 预测 AI 与形式化方法可能在几年内让系统完全安全。这是他的乐观预测；形式化验证覆盖的是已陈述的性质和假设，而运维、人员和供应链风险仍然存在。

Kochenderfer 使用瑞士奶酪类比：多层防御各有弱点，目标是避免这些弱点恰好对齐。纵深防御仍需要理解各层如何相互作用。

在问答中，研究人员讨论为现有系统编写规格的困难和人工监督的作用。验证器只能检查提供给它的性质，因此规格质量仍是核心。

观众讨论能力、可解释性和控制之间的取舍，以及监督大量 AI 辅助行动的实际困难。