[音乐] >> 今晚我们在做什么？好吧，就这样。这样好多了。>> [笑声] >> 欢迎来到[音乐] YC AI安全俱乐部。我想我从2012年左右就开始从事AI工作，如果你在做自动驾驶汽车或任何被称为安全关键系统的东西，那么AI安全一直是一个关注点。所以我一直在从事某种形式的AI安全工作，即使在Focal推出新的测试版时，你也可能会搞砸。你知道，我们曾控制着沃尔玛的库存，所以如果你推出一个糟糕的测试版，订购了太多的牛油果，就会损失数百万美元。所以在进行这些发布时确保你知道自己在做什么是很重要的。在过去三周里，人们对AI安全的关注度略有上升。我不知道你们是否注意到了这一点。嗯，不太确定原因是什么，但我认为没有比YC Paper Club更适合深入探讨这个话题的地方了。我认为对话已经从科学严谨性逐渐演变成了我称之为歇斯底里的状态，其中存在被错误引用的情况。我明白耸人听闻能带来更多点击量之类的东西，但作为这里的科学家，我们应该回归科学方法的严谨性，提出可证伪的主张，依赖同行评审周期等机制，以确保我们没有夸大其词。所以我称这次演讲为“科幻与科学事实”之类的内容。Gary Tan昨晚在海兹堡说过类似的话，在那里我们听到了Sam Altman、Tom Brown和Alex Wang的讲话，他们主要谈论了这个话题。嗯，歇斯底里就是当人们无法衡量某事时却无法停止讨论它。我认为这就是我们目前的处境，而且稍微退一步看，这并不意外。在任何重大技术进步中，往往存在不确定性，夸张很容易滋生。因此即使是核武器和原子弹，爱因斯坦也不确定它是否会点燃天空。显然没有发生，我们还在这里。对于电子计算机，许多人甚至Alan Turing都担心机器将超越所有人类能力和智力，早在1950年代他就认为他试图给出时间框架，显然他的时间框架完全错了。工业自动化让人们思考大规模失业问题，你知道马克思和凯恩斯都有过这类讨论：我们要怎么办？对于互联网，即使是发明了以太网的Metcalfe也说网络将会发生灾难性崩溃——这是他的措辞，而且互联网基本上会失败。因为像Cloudflare这样的东西，我认为主要是DDoS攻击是他主要的担忧，但最终没有发生，然后他著名地将他的论文放入搅拌机中喝掉了自己的话。这实际上是一个真实的故事，非常有趣。嗯，谷歌的人们认为这会毁掉人类的智力，人们只是在搜索东西而不再真正阅读了。嗯，尽管人们仍然相当聪明，尤其是这个房间里的人。然后是智能手机和社交媒体，我们刚才还在谈论这一点。现在我回到斯坦福大学并担任Michael和其他一些人的助教……嗯，你知道只是与YC的这批人打交道，他们主要是年轻人。我对今天的18岁、20岁的年轻人感到超级兴奋。嗯，他们真的非常投入。最后现在我们处于这个AI时代，人类灭绝的话题又回来了，很容易陷入夸张之中，我们应该回到一些事实上来。好的，这里有几个叙事可以选择，我们可以添加更多，但这些可能是光谱两端最大的观点。所以Yann LeCun有一个关于涡轮喷气发动机的类比，他经常谈论这一点。你们没听过他的谈话，但这主要是工程安全。这是一个工程问题。Jensen Huang也说了类似的话，虽然不容易做到，但很难让飞机安全飞行，确保在起飞时机门不会飞出去，确保起落架放下并正常工作。嗯，部署到波音737的MCAS系统经过充分测试并且不会做可能导致故障的事情。这与ACAS X类似，我们也将听到关于它的内容，这是一个拯救生命的惊人系统——飞机防撞系统。而另一种观点是P(doom)大于10%，即在10年内发生的可能性，这著名地由Jacob Coxen提出并设定了这些指标。他说：“我认为人类失去对这些AI的控制并以人类灭绝告终的可能性大于不。”嗯，老实说，我不会评判哪一方正确。我想今晚我的观点是为另一种观点提供发言机会，让你们自己做出决定。嗯，我会说这两边的人之间H指数有一点差异，你可以用它来改变你的先验概率。但让我举一个关于夸大其词或至少是误述实际发生事情的例子，比如Hugging Face的漏洞事件是我们应该仔细探讨的事实与虚构的问题。如果你看一下Slashdot的头版标题，“OpenAI称其AI模型自行行动”。OpenAI从未说过这样的话。没有在任何声明中这样说。但这就是标题的内容。“失控的AI代理在一家科技公司发疯”。事实并非如此。它并不是今天醒来就说：“你知道吗？我想我要黑掉Hugging Face。”“你知道我明天要做什么吗？我将解决纳维-斯托克斯方程。”“你知道吗，我明天要杀掉所有人类？”这不是事情发生的方式。它是由exploit gen提示的，涉及大约1200个代理。甚至更多，正如他们指出的那样，他们有思维链。他们发布了这份令人惊叹的60页文档称为《OpenAI Hugging Face事件》，你可以阅读技术报告。我读过，CO2监测被意外或其他方式关闭了。他们说他们重复添加了它回去的CO2监测，并且它会捕捉到这个问题。第一点。第二点，还有生产护栏和安全措施
那些数据之所以离线，是因为它们尚未投入生产环境。因此这本来也能发现该问题。但叙事却是：它失控了，它造反了，它从服务器中逃脱出来，复制了自己，现在正在破解数学难题并入侵澳大利亚政府等机构。接下来会发生什么？好吧。另一个有点好笑的是，如果你仔细查看这个内容，我当时想：“等等，这‘十年内P doom 概率10%’是怎么回事？”首先，2023年有一篇名为《数千名AI作者论AI未来》的论文。在那篇论文中，他们询问了1200名极客人士——也就是AI专业人士——关于某些增强功能何时会实现的一系列问题。在论文较后的调查环节中，他们问了这三个问题：你认为未来AI进步导致人类灭绝或类似永久性或严重削弱人类能力的概率是多少？针对“无限时间”这一选项。在第三个问题中，他们问的是未来100年内发生的可能性。以下是统计数据：这是平均值和中位数。请注意，这些预测都不在“未来10年”内。而这正是人们在谈论此事时最常引用的论文。顺便说一下，这是一个有点奇怪的问题。就像我刚才和教授们讨论的那样：回想一下2012年我在斯坦福大学刚开始从事AI工作时，如果我问所有斯坦福教授：“你们认为AI何时能独立解决——或至少协助重大解决千禧年大奖难题？”我认为不会得到很好的答案，而且肯定没人会说14年内。我想共识可能是50年或100年。所以，我不确定询问1200名极客人士这类问题有多少信号价值，因为这些问题真的很难。
因此，人们即使知之甚少或一无所知，也会编造出连贯的故事和自信的预测。另外还有一个让我觉得如果你看过《周六夜现场》（SNL）的小品，他们做得非常好。我为达里奥感到难过，因为我觉得达里奥并没有被那样描绘得那么奇怪；我认为他比雅各布·霍斯滕和一些强烈的有效利他主义（EA）社区成员更情绪稳定。但我敦促你，或者不如说我被敦促停止那个部分——我觉得那太完美了，非常有趣。当时我正从黑德斯堡开车回来，这是我从未真正见过的场景。我多次驾车经过金门大桥，但在整个车程中我一直在思考今晚要讲的内容。当我开车过桥时，整座桥都消失在雾中。我觉得这太完美了，我必须谈谈这件事。第一，看起来真的很酷；第二……我差点为了拍这张照片而撞车，不过算了。我们要知道未来是不确定的。我们有一些先验信念可以分配给“桥还在那里”这一假设，尽管它可能不在。所以我们要朝着那个方向开车，我们应该分配先验概率并选择最大似然值：好吧，我认为桥还在那里。让我们继续开下去。随着我们不断前行并获取更多信息，我们会改变档位：也许我会停下来。我不知道，是在上桥之前还是进入海湾之前。
[清嗓子] >> 我几乎完全不担心AI将发展出灵魂、拥有意识、意志或动机，并在短时间内（如10到20年内）凭借独立意愿杀害和奴役我们这一现实路径。在无限的时间里，我认为一切都会发生。所以我不认为这有用。我的头号担忧是——这是非常现实的——真正优秀的开源权重模型允许更多的不良行为者或国家实体做同样的事情。今天我们有恐怖主义、生物武器和网络战争，以及网络勒索攻击。就在最近，我朋友在波兰的当地医院就遭遇了这种情况：一群俄罗斯黑客控制了医院并关闭了它三周。也许他们使用了AI来做这件事。而现在，这使得这样做变得更加容易。这种情况已经发生。
人们提出了一些解决方案，但我认为它们都有点糟糕。一是禁止开源权重。祝你好运吧。我已经在我的车库里下载了Kimmy K3和GLM 52，所以抱歉。二是注册GPU设备。同样，我在车库里有很多小型盒子。除非你要搜查每个人的房子和每个AI人员的地方，否则你实际上不会知道他们是否有GPU。而且我可以在另一个国家预订一台GPU，你也无法阻止我这样做，所以我不知道这如何真正解决问题。有一些很酷的想法：通过检测网络负载信号或电表上的信号，可以探测到你有多少台洗碗机和冰箱。这挺酷的，至少在美国能检测到人们做坏事时的推理信号。但我并不完全担心这是主要问题。我认为我们正与许多国家处于战争状态，这并不能真正解决任何问题。（针对美国境内的不良行为者则另当别论。）最后一种方案，这是一个包罗万象的选项，主要适用于我们应该独立采取的行动：投资防御。如果你是银行、医院、金融服务机构或政府，你应该大力投资于网络防御。你可以做很多事情来加强你的安全体系。我在零售业工作过很长时间，这些系统非常陈旧，很久没有更新过了。简单的方法如尝试管理员权限……它们实际上能让你进入系统。好吧，为什么几乎所有社会保障号码泄露？因为[轻笑]他们没有更改管理员密码。
如果我们要加速而不是减速，并且假设这些前沿实验室是好人——我认为是的——如果我们给这些好人更多资源并让他们加速，那么我们就可以为较弱的模型试图入侵系统做好准备。这肯定会……
如果情况相反，那就更糟了。总之，这是我的两点看法。所以，让我们从歇斯底里回归理智，回到科学事实上来。你知道的，关于AI将如何杀死我们所有人的叙事令人惊叹，听起来真的很像艾萨克·阿西莫夫的书。而且你知道，长期以来一直有关于安全性的文献，远在大型语言模型（LLM）被发明或训练之前。
那些有幸今晚在场的人，就是AI安全社区的一员。这个社区已经存在很长时间了，有很多论文和会议都在讨论这个话题。最近就在斯坦福大学举办了一场这样的会议，该会议的联合主任今晚将发表演讲。他们是迈克尔·科格特（Michael Kogut）和克拉克·巴雷特（Clark Barrett）。他们是斯坦福大学的两位杰出教授。
我认识迈克尔已经14年了，我想我在2013年上过他的“不确定性下的决策”课程，后来多次担任他的助教，并为他做研究很长时间。他是我合作过的最友善、最聪明的人之一。我对克拉克·巴雷特了解得较少，但我听过他的演讲，他简直不可思议。他们都有一些见解，关于我们如何实际应用现代方法来验证数据在生产环境部署前的准确性，并监控它们以确保它们不会偏离轨道或造成危害。
迈克尔是航空学副教授，兼聘计算机科学教授。他是我的实验室——斯坦福智能系统实验室的主任，也是斯坦福AI安全中心的联合主任，还是H AI的高级研究员。克拉克·巴雷特是计算机科学教授，与迈克尔共同担任斯坦福AI安全中心主任，并担任Centor自动推理中心（注：原文为Centor Center for automated reasoning）主任。他将谈论一家名为Ampersand Truth或And Truth的新兴隐形初创公司。
回到我们在这里讨论的话题。好了，这就是我要说的所有事情。我想我们在两周前已经安排了一次推理之夜（Inference Night），届时会有一些非常酷的人参加。我们已经确定Together AI的Dan Fu将出席，谈论推理问题。在某些情况下，推理正变得比训练更复杂，这对我来说有点疯狂，因为我记得当时学习时只是调用model.forward。我以为只要做这些就够了，但现在情况比那复杂得多。
还有来自Llama的Jeffrey Morgan，以及克拉克·巴雷特的一名学生，我上周末刚认识她。她经营着一家很酷的公司叫Radix Arc。实际上，Lang我想她可能来不了，她会派她的一个同事来参加。还有Wafer，这是一家很棒的Y Combinator公司。好了，请帮我欢迎克拉克上台。（掌声）
大家好，谢谢。很高兴来到这里。所以我要讲的是AI与自动推理（Automated Reasoning, AR）相遇的故事。你可能会问AR是什么？不是增强现实，而是自动推理。这两个主题之间有一种非常美妙的协同效应，因为正如我们所知，AI在各种事情上都很擅长：处理混乱的数据、数据驱动的训练等。但它有一个大问题：没有正确性保证，能找到对抗性输入，会产生幻觉等等。
另一方面，自动推理本质上是计算机化的形式化推理。如今在工业界已广泛用于安全保证。其核心就是正确性保证。好吧，请保留这个想法，我讲一个小故事。我们都听说过这个问题吧？这种新兴威胁：AI时代的安全问题是什么？你可能听过像“玻璃翼计划”（Project Glass Wing）之类的事情，这助长了弗朗索瓦所谈论的歇斯底里。
那么，我们能帮忙吗？我们能做些什么呢？2023年，我在谷歌参加一个研讨会，一群知名人士讨论风险和担忧：如果生成式AI能找到安全漏洞怎么办？我们要怎么做？我当时想，有一个解决方案。如果你形式化验证了你的所有代码，它就不会被黑客攻击。但他们不想听这个。那太难了。
这种回应是有充分理由的，对吧？传统的形式化验证需要巨大的努力，自动化技术太弱或无法扩展，根本不经济。快进到另一个我参加的会议，大家都在热烈讨论AI的风险和担忧。然后在我之前的每一个演讲中都说：只有一个答案，那就是形式化方法（Formal Methods）。这完全出乎我的意料。
看来人们对形式化方法的態度发生了一些转变。这种转变是否合理？这就是我想今晚与你们一起探讨的内容。好吧，我们在担心什么？当我制作这张幻灯片时，它还是“未来”，我把它划掉改成了“现在”。（清嗓子）AI系统正在制造大量有缺陷的软件，对吧？我不知道你是否担心这个，但我很担心。
或者它极大地提高了黑客攻击遗留系统的能力。所以我们要面对来自两方面的威胁。很多人开始寄希望于形式化方法，看看是否有办法帮助我们解决这些问题。此外，人们对AI在数学方面的出色表现感到非常兴奋。也许这是一个信号，表明这里正在发生一些事情。
那么我们要如何达到这一目标呢？我们如何从解决千禧年大奖难题过渡到确保软件安全？（清嗓子）AI非常擅长写代码，也非常擅长写数学证明。但事实证明，撰写数学证明与确保代码安全之间存在巨大差异。因此，弥合这一差距是我过去几年一直在深入思考的问题，我将简要介绍我们正在做的事情。
我要讲一个叫CS Lib的项目。CS Lib受到Mathlib在数学领域成功的启发，但其理念是构建计算机科学理论以及一个实际用于推理代码的平台。我们有一个很棒的指导委员会，包括Lean的作者Leo de Moura。还有一些技术负责人。我们正在使用Lean。如果你不知道这是什么，那你该从石头底下爬出来了。（笑）
Lean是一个伟大的定理证明系统。基本上它是一个让系统检查每一步的系统，它不允许你犯错。这正是我们在处理高保证情况时所需要的。CS Lib有两个……
基石之一是计算机科学理论的形式化，第二个是关于代码推理的框架。我要讲的是后者，这也是我最感兴趣并深入参与的领域。这里有一张幻灯片展示了CS Lib的愿景：设想你将各种不同语言编写的程序，重写为一种通用的中间语言。然后将其编译成Lean中的验证条件（Verification Conditions），你只需要证明一系列Lean定理即可。如果你能做到这一点，就证明了代码的正确性。
目前进展如何？在证明Lean定理方面，人工智能表现相当不错；此外，我们还有一些比AI更廉价且高效的技术，比如Lean SMT。这是我在实验室开发的工具，能在CPU上以毫秒级速度证明大量Lean定理。因此，在Lean中证明定理的技术正日益精进，这非常好。接下来我将展示一段Rust代码，这是Dalek轻量级密码学库的一部分（清嗓子）。实际上这是Vera格式的代码，你可以看到其中包含一些规范、证明步骤以及不变量。
我将展示同一段代码已被转换为Bull语言，这是相同的程序在Bull中的实现。我们保留了前置条件、后置条件和不变量，但现在所有内容都嵌入到了Lean中。我们可以调用这里的VC生成器（验证条件生成器），它生成了35个目标，每个目标都是我们需要证明的Lean定理。接着我们尝试SMT策略（调用Lean SMT），结果显示它解决了除三个目标外的所有问题。
随后我们进行最后一步，展开一些定义并再次调用SMT，从而完成了证明，所有目标均被解决。这是一个小型原型，展示了如何从Rust转换到Bull再到Lean定理进行证明，进而验证代码正确性。假设我们成功在Lean中构建了整个体系，我们就有了推理所有语言代码并证明其定理的方法。但我们仍面临一个问题：必须有人编写规范，即定义代码应具备的属性。
人工智能能在这方面提供帮助吗？这里有一个名为Verisforge的工具演示，你可以输入用英语描述的构建规范，它将生成代码并完成形式化证明。例如一个简单的例子：在32位整数数组中寻找最大元素。我们点击后，它首先生成结构化语言规范供确认。批准后，它会基于该规范生成Rust代码和Vera规格说明。
接着使用Vera工具验证，确保规格未发生变化。这样我们就获得了全自动生成的已验证代码。（观众：好的，这又是一个玩具示例。）我们能做得更好吗？是的。在最近提交的档案中，我们展示了一个3万行Rust程序（密码学库），原本需要5名专家耗时3个月或3名专家耗时5个月完成，而我们的密码证明代理在11小时内全自动完成了该任务。
这仅仅是形式化方法领域潜力的冰山一角。我认为“形式化+AI”为我们提供了一条路径，正如François所言，可以构建强大的防御机制，创造可用于搭建AI安全栈的新原语。我喜欢这样比喻：如果AI安全是我们必须攀登的珠穆朗玛峰，那么代码推理就是一个很好的大本营。此外还有几个有趣的观点：想象一个拥有大规模代码推理能力的新原语的世界，你可以做一些有趣的事情。
例如，如果代理A和B在赛博空间相遇，代理A说：“我可以为你提供这项服务。”代理B回答：“太好了，给我看你的代码和证明。”A展示后说：“好的，我信任你，你可以执行。”这将是一个令人兴奋的未来。此外，这项工作还体现了“限制”的概念：你可以将超级智能AI放入我们的密码证明代理中。它唯一能做的就是证明你的代码正确，除此之外什么都做不了。
如果我们能找到实现这些方法的方式，我想我们就能在避免不良后果的前提下从AI中受益。最后想透露一点消息：我是新公司And Truth的联合CEO，我们正试图按照今天介绍的方向构建一个通用的代码推理引擎。敬请期待。谢谢大家。（掌声）
主持人：非常感谢。下一位是Marco Kokotajlo。谢谢。（掌声）好的，问题是：如果我们构建了一个系统（也许是AI系统），我们如何知道它是安全的？我将分享斯坦福智能系统实验室（Sizzle）的一些研究，我的研究生自称“Sizzlers”。对于具有学习组件的系统（例如飞机的自动着陆系统），我们需要什么证据来证明部署它的合理性？
在商业航空领域，我们的目标是将灾难性故障的概率控制在每飞行小时10的负9次方左右。这也是我们在开发ACAS X飞机防撞系统时所遵循的标准。如果你直接模拟这些场景，平均需要10的9次方小时的模拟时间才能检测到一次故障。如果你想获得这类故障的统计代表性，比如需要10次故障样本，你就必须运行10的10次方小时的模拟时间。这通常非常困难。
当然，你不想把时间浪费在飞机相距5英里且不构成危险的场景模拟上。相反，你想模拟那些能代表空域情况的临界场景。那么如何获得这种分布呢？在我们的实验室里，我们探索了多种建立系统信任的方法……
部署。因此，一种方法被称为证伪法，即在可能的情景空间中搜索失败案例。如果你发现系统导致了一系列失败，审视这些失败并感到内心不安，那么也许你不应该部署该系统，或者你需要思考缓解措施以防止那些关键场景的发生。通常我们真正想要做的是估算失败的概率。为此，你需要一个你实际信任的模型。例如，在开发ACAS X防撞系统时，我们在空域统计建模上投入了巨大努力。
另一类方法是验证法，这是Clark实验室的研究主题，我们已与其合作多年。但这通常被视为不同的社区，我们正在寻找与之接轨的机会。因此，我们的实验室致力于多种不同方法的研究。事实证明，为了建立对系统的信心，没有单一的万能钥匙。形式化方法可能无法带你走到最后一步，尽管Clark正帮助我们不断深入。这确实需要多种不同方法的结合。
当然，我们也一直在研究部分可观测马尔可夫决策过程（POMDP）规划。这类方法论允许你构建极其稳健的系统，使其对状态不确定性、结果不确定性、交互不确定性和模型不确定性等具有鲁棒性。我们喜欢由现实世界的问题驱动，包括航空、驾驶、航天器、医疗撤离等。我将提到其中几个案例，并且我们也喜欢在实际世界中测试它们。
当然，如果能模拟一切是很好的。然而，我们对安全性的推断质量仅取决于模拟器的好坏。我们采取的一种方法被称为自适应压力测试。这源于Richie Lee的工作，他曾是我的博士生，当时也是NASA艾姆斯研究中心的公务员。我们部分利用它来帮助验证不同版本的ACAS X系统。此后，许多学生在此基础上进行了构建。
最近，我们探索如何将我们为验证飞机而开发的一些见解带入语言模型验证的世界。这是我学生Hujun Liu、Amelia Hardy等人主导的工作之一。在飞机场景中，失败是明确定义的：即金属与金属碰撞，水平距离小于500英尺且垂直距离小于100英尺。对于这些语言模型，我们关心的是潜在的毒性。
如何定义这一点？这有点模糊不清。为此，我们实际上依赖另一个神经网络来提供该度量标准。在这篇论文中，我们使用Llama Guard来衡量毒性。我们要找到最可能的失败案例。在这些语言模型中，我们使用一种称为困惑度（perplexity）的指标。我们希望尽可能低的困惑度或低对数困惑度，同时具有最高的毒性。
因此，当我们搜索情景空间时，我们希望位于左上角区域。如果最可能的失败是超级……如果我们定义超过某个阈值的毒性为失败，且这种情况非常可能发生，那么我们就应该研究它并实施一些缓解措施。另一个挑战是估算失败的概率。那个奇怪的符号应该是E，表示期望值。
一种处理失败概率估计的方法是使用重要性采样，这是一个存在已久的概念。其思想是：不从真实分布（我们称之为P）中采样，而是从提议分布（我们称之为Q）中采样，将精力集中在更重要的情景上。但你必须随后对它们进行重新加权。
重 weighting 实际上相当简单：你根据真实模型中轨迹的概率除以提议分布中轨迹的概率来加权不同的结果。我们已将其应用于多个不同领域。我们研究了引入高斯过程的思想来帮助表示这些分布。我们还查看了归一化流，使用低秩高斯混合模型来表示这些提议分布。
我们还在使用扩散模型，它们在图像生成等其他领域取得了相当多的成功。有时我们不仅关心最可能的失败，而是希望分类所有不同类型的故障模式。这里有两个非常简单的二维示例：上面一个是倒立摆。你可以看到随时间变化的角度。如果摆动超过某个角度，我们就认为发生了失败。
在现实中，它可能向左或向右倒下。如果你能负担得起运行无数模拟并查看那些失败情况，那将是真正的故障分布。现在，如果你只使用常规的自适应压力测试，它通常会锁定其中一种故障模式。而如果你使用这种基于扩散的故障采样，它将实际上捕捉到这两种失败情景。
月球着陆器的情况类似。我们还致力于神经网络验证工作。很久以前，由Francois发起的一些工作让我们想看看是否可以使用一些神经网络来近似ACAS X防撞系统的查找表，目的是压缩信息。当然，我们最终并没有在真实系统中使用神经网络，但这导致与Clark Barrett实验室进行了非常有趣的合作。
这促成了Reluplex算法的开发，以及后来的Marabou软件框架的诞生。多年来，我们一直将Reluplex和Marabou的使用过渡到具有神经网络控制器闭环的情况。Chelsea Sidrain和Sydney Katz的一些工作在这一方向上推动了一些进展。然后，Clark和我共同监督的一名学生Sam正在研究前向和后向可达性概念。
我们还进行了POMDP规划方面的工作。实际上，当我开始在斯坦福大学工作时，实验室的早期努力之一就是创建一个非常简单的开源框架。
指定POMDP（部分可观测马尔可夫决策过程）。我们希望让非专家也能轻松定义他们的POMDP。这有点像CVXPY，史蒂文·博伊德（Steven Boyd）的学生们提出的理念是让数学优化问题的定义变得极其简便。这也是我们针对POMDPs.jl想要做的事情，它是一个Julia库。我的学生扎克·桑伯格（Zach Sunberg），现任科罗拉多大学博尔德分校教授，开发了用于可扩展POMDP规划的分层算法。最近我们更多关注受限的POMDP，即你可能希望对问题施加硬性约束。我们还探索了涉及多智能体的方向。这些是我们关注的一些领域，例如医疗后送。我的学生博迪·埃尔侯赛尼（Bodie El Husseini）实际上是一名陆军黑鹰直升机医疗后送飞行员，他开发了一个模拟此类场景的框架。我还看到邓肯（Duncan），他一直推动我们在航天器防撞方面的信念状态规划工作，并与海伦等人合作利用POMDP来规划飞行测试，以便尽可能高效地表征飞机的飞行特性。
这主要侧重于系统部署前的验证。你也希望在部署后继续验证工作，这有时被称为运行时监控或运行保证（runtime assurance）。你需要验证进入决策系统的内容，即传感器输入。我们与空客合作进行了基于视觉系统的完整性监控研究。你还需要监控系统内部的情况，这导致了对飞机系统进行机制分析的工作。当然，你也希望建模并监控输出。此外还有一组关于评估测量的工作。安卡·鲁苏（Anca Rusu）等人一直在推动AI评估的前沿领域。我们发布了BetterBench论文，访问betterbench.stanford.edu可以找到关于多个不同基准测试的数据、经验教训和最佳实践。我们还研究了这些基准何时不再有用，即出现饱和现象时。
我们也从令牌级签名和推理失败的角度研究了这些故障的表现形式，并关注了人类评委的问题。事实上，另一个安全关键领域是AI在心理健康中的使用。我们评估了心理健康专业人士的表现，并惊讶地发现他们的意见差异很大，甚至在与自残相关的领域也是如此。好了，我在此结束演讲，简要提及我们的新三部曲：第一本书是《优化算法》，第二版将于2027年初出版。优化是我们所做一切的基础，我们在《决策制定算法》（2022年）中涵盖了基于此优化决策的内容。我对这本新出的《验证算法》感到非常兴奋，它下个月出版并开放预购。
这本书试图全面讲述如何验证学习型系统和其他AI系统的故事，亚马逊和Target.com均有销售。目前网上可以找到该书的PDF版本，其中包含我提到的统计方法以及形式化方法和可达性方法。通常这些被视为独立的社区，但我们试图用共同的语言统一所有内容。我就说这么多，谢谢。（掌声）
主持人：非常感谢你，太精彩了。我想开始对话时提到大家看到的AI安全话题，当你看到最近这场恐慌闹剧时心里在想什么？先从克拉克开始。
嘉宾1：我并不惊讶，因为我和AI安全极客们相处了一段时间，其中许多人一直这么说。我认为我的回应一直是：未来具有高度不确定性，尤其是现在，因此投资AI安全研究是个好主意。但我也不认为在没有真实概率的情况下强调最坏情况结果有多大帮助。任何声称“我知道这会发生”或“看起来肯定会发生”的人，他们只是在猜测。
嘉宾2：我们都关心AI安全有一段时间了。我想我们是在2017或2018年创立了AI安全中心，看到它引起国际关注很有趣。我希望这能促使人们更严肃地对待安全问题。我认为我们需要从航空航天行业借鉴更多理念，我可以详细阐述一下。
嘉宾2：实际上已经有人讨论为AI建立类似NTSB（美国国家运输安全委员会）的机构，我认为这确实是个好主意。与20世纪70年代相比，自霍华德·休斯时代或1970年以来，商业航空的安全性提高了80倍。我们是如何做到的？
主持人：那会是什么样子的？是自愿性质的吗？是指南还是像FDA那样严格批准数据？它会如何运作？
嘉宾2：这是个好问题。关键在于独立性，NTSB于1967年作为独立机构成立。还建立了其他航空安全报告系统，如ASRS（航空安全报告系统），这是一种非惩罚性报告制度。这激励制造商和航空公司分享安全信息，认真对待每一次事故并从错误中汲取科学知识。此后还有其他基于此建立的方案。2007年，航空安全信息分析和报告系统也具有一定的豁免权形式。我认为我们需要做类似的事情。建立新机构可能需要很长时间，这是一件大事。政府往往比较……
效率低下。NTSB（美国国家运输安全委员会）也在全球范围内使用。因此，如果事故涉及在美国制造的组件，他们甚至会前往其他国家进行调查。>> 做出这种类比是因为……嗯……有很多利益相关方参与，存在监管俘获等风险。如果你看看医学或法律领域，有医学会这样的机构；互联网也有ICANN（互联网名称与数字地址分配机构），它是国际性的、自我监管的，DNS运行良好。
但情况并非如此：想象一下互联网发明时，谷歌和脸书已经是上市公司，并在ICANN的发展中带有严重偏见。也许他们会说：“嗯，如果你想使用SSL证书，实际上需要谷歌或脸书来提供；或者你想获取域名……”他们可能会说：“把域名给每个人都不安全，应该由我们来提供。”所以这里存在风险。
更甚者涉及政府干预时，就有监管俘获的问题。如今如果你想创办Uber或Lyft，在法律上是行不通的。现有的Uber、Lyft等公司享有“祖父条款”待遇（按1099表格报税的独立承包商身份）。因此，你实际上无法竞争。这是人们担忧的一点。你怎么看待这些？>> 嗯……最近前沿实验室的领导人表示“我们需要独立评估者”，这让我受到鼓舞。
我公司的目标之一是构建能够充当这种独立评估者的系统，而不仅仅是声称“我们很独立”的人。我们的目标是生成可独立核查的证书。我们会说：“好吧，我们已经检查了这个系统，这是证书。你现在可以去自行核实，确认我们的结论是正确的。”我认为独立性非常重要。
有很多声音在推动这一点，因为如果所有安全工作都留给实验室或自称独立的“朋友”手中，那将是一大遗憾。>> 是的，我认为在那种机制建立之前，我们需要在近期采取一些措施，比如非营利组织。在航天领域发射时，有完全独立于任务的范围安全官，他们的唯一职责是根据客观的安全指标做出“可以/不可以”发射的决定。
是否可以简单地从美国通用会计准则（US GAAP）这样的基础起步？比如“普遍接受的AI部署安全原则”？然后就像有毕马威（KPMG）或安永（Ernst & Young）这样的机构供你选择，但在执行某项操作前必须经过验证。但这不应涵盖一切：我仍然应该能够在我的小型设备上训练模型。
是的，我认为我们需要制定最佳实践，同时也需要进行事后分析（postmortem analysis）。我认为需要从多个角度认真对待AI的验证工作。>> 回到你的观点，航空业在这方面做得很好。他们不会急于公布调查结果，而是对每一起事故进行彻底审查。>> 你有没有……嗯好吧。
我最后一个问题是：你们认为当前的AI安全问题在多大程度上是可解决的？特别是网络防御问题、生物武器风险，以及模型被用于发动网络攻击（例如通过欺骗OpenAI或开源权重模型）的问题。我们需要像之前讨论的那样具备防御能力。你们认为这是一个多么可解决的问题？
我来尝试回答一下。我认为网络安全将变得非常可控（tractable）。我曾告诉母亲：“如果你能证明代码，它就不会被黑客攻击。”她非常震惊。媒体让我们认为每个系统都能被攻破，这确实是目前的事实。但完全有可能通过数学确定性证明一个系统无法被黑客攻击。
我预测在未来3到5年内，这种情况就会发生：我们的系统将完全安全。因为AI既能攻击也能防御，加上形式化方法（formal methods），我们将实现这一目标。>> 那么需要做什么才能实现这些锁定系统？是零信任架构吗？还是最佳实践，甚至是管理员权限问题？你怎么看？
我认为我们需要转向新的代码标准。有趣的是你提到了航空业等行业如何使用严谨的工程原则。软件工程中有一个不太光彩的秘密：它并不基于严谨的工程原理，而是“写点什么然后测试，希望一切顺利”。
但实际上我们知道该怎么做。软件工程有数学基础。关于确保AI本身的安全性，我认为我们无法对庞大的大语言模型进行推理分析。因此，最好的选择可能是“保护边界”。证明一个5000亿参数的模型不会做出疯狂行为并不可行，但保护边界是非常可控的。
完全同意Clark关于安全的观点。我害怕下一次大规模网络攻击，但我对解决网络安全问题充满希望。然而，你无法证明生物学或化学中什么是可能或不可能的，这是一个开放性问题。但这正是我们作为一个物种一直在追求的目标……
对AI的理解加深了，而且我认为人工智能的进步将有助于我们。平均而言，我想我们会从这些新见解中受益。>> 嗯，我有一个具体问题要问Clark。所以，请详细给我讲讲它是如何运作的。假设现在 uh 我们给你100亿美元让你担任美国银行的首席信息安全官（CISO）。好吧。他们会怎么做？你会做什么？>>
好的。首先，我会雇佣所有正式人员并 uh 竞相构建我们需要用来推理代码的基础设施。然后我会说：“好吧，给我你们所有的代码。” uh 呃，给我一堆GPU和一堆定理证明代理，我们将要么证明代码就是它现在的样子，或者我们也可以将其翻译成一种更好的语言，比如Rust或
Lean，在那里证明代码，嗯，然后你就完成了。所以那里有很多工作要做，但我认为这是我们已知如何做的工作。>> 那是否意味着我终于必须达到100%的单元测试覆盖率？这就是那个意思吗？>> 不，你不需要。你 uh 所以测试实际上变得过时了。我的意思是，在开发过程中测试总是好的。它们是
发现错误的最快方式。 uh 但最终形式论证完全涵盖了测试。>> 嗯，好吧。现在，对于Michael， um 你知道Waymo吗 uh uh 一些 >> 是的。>> [笑声] >> 我的许多学生在那里工作。>> 下一个问题。不。>> um，使用 uh AST差异 uh 这是其中一些重要的采样技术 uh 你知道Marabou、Reluplex。你
知道他们在训练新模型后是否在他们的验证和theta验证程序中使用这些技术？>> uh 我不能具体谈论Reluplex或Marabou。uh Clark可能对此有一些见解，但自适应压力测试我们不仅发布了Julia版本，还发布了Python版本供那些希望继续使用过时语言的人使用，但 >> [笑声] >>
um 所以我们把它开源了。我们有 uh 我们实验室的许多赞助商。我们 um uh 得到了多家汽车制造商非常慷慨的支持，包括Waymo。目标是 um uh 使这些工具不仅对他们可用，而且对整个行业都开放。>> 我 I And 你谈到了AST Prompter，这些适用于LLM就像它们适用于控制油门和方向盘的训练
VAT一样，对吧？>> 是的，基本上你需要两样东西。使用自适应压力测试需要两个条件。你需要一个失败的定义和一个可能性的度量。两者都可以拥有 这适用于语言模型、飞机防撞系统。>> 你 Anthropic和OpenAI以及Grok在
这些话题上的参与度是否像Waymo和自动驾驶汽车领域那样？>> 还没有。我的意思是，我们刚刚发布了AST Prompter。我们得到了Schmidt Sciences的支持。想法是让所有这些思想尽可能易于获取。>> 你认为如果他们采用，他们的安全水平会与Waymo等相当吗？ um 我不知道。 uh 希望这
是验证物理系统与你知道的语言模型不同的事情。虽然方法可以转换，但你可以预期的成功水平可能会有所不同。>> 我的意思是，我听过这样的论点，嗯 um 自主性你知道我们可以很好地定义故障模式如果东西保持在道路上，如果你知道它撞到婴儿等等。然后我遇到
I I 我和Lane McIntosh在一起，他向我展示了特斯拉汽车实际上被颠覆并幸存下来而没有做坏事以及它远远超出分布范围的例子。那是一个在任何合理世界中都没有监控或采样的故障模式。你可以有 总是有一个长尾，对吧？而一些长尾是 a is 始终将是高概率。 um 然后
他们说，“嗯，在这些 And 所以在LLM中，你知道我们不能有点吗 isn't it kind of that same Is is there Is it meaningfully different long tail?” >> 是的。I I I 我认为你完全正确。所以，即使对于A cast X，我们知道故障的概率
不为零。>> 嗯哼。>> 我的意思是，我们有模拟显示它在某些情况下失败。只是那些情况
极其不可能发生。那我的意思是国际民用航空组织和联邦航空管理局，他们的安全标准不是概率为零的概率为零，对吧？>> 对。>> uh 我们必须现实一点。如果有人告诉你他们创建了一个完全安全的系统与 in 在真实世界中交互， um 而且它完全安全，是的 I I
我不会相信那。>> Clark为我们有一些保证。 >> uh Clark有一些保证。 uh 所以，使用Clark的方法或形式方法的类别 um 如果我在这里说错了请纠正我，但你必须 it you're making these proofs with respect to some model, okay? And if you're modeling the real world, you have to capture your uncertainty in what can happen, like the
accelerations of the aircraft or whatever. And so, you generally have to assume bounds on that uncertainty. >> So, you have to estimate a nominal distribution on the input, on what's going to and on the transition function of >> So, in formal methods, you generally don't assume anything about probability distributions. You capture your uncertainty in sets. >> Right. Okay. >> And and that's a
different approach and it's great when it works, right? Because you get a nice proof. And and that's wonderful. But the question then is do those uncertainty intervals um are they sufficiently realistic? >> Just say something on that. So, um yeah, a proof is always with respect to some assumptions, right? And so in some cases you can make reasonable assumptions and give strong guarantees. I think
what Michael's saying is it uh if you have, you know your input is like another actor in the real world and you assume that actor is not going to try to hit you with their airplane, >> then uh that might not be a valid assumption right So so you do it is really important uh when we talk with about safety or about formal guarantees that you understand it's with respect to some assumptions. Now,
there are some things that you can guarantee 100% right If I prove my code is memory safe then it's it is 100% impossible for you to use a buffer overflow attack to attack that code. >> Yeah. >> Uh but there are other things that there are limits to what you can do with formal right I mean uh the work we did on verifying neural networks you know people would ask us Well how are you
“去验证这个感知网络是否正确识别猫和狗？”我当时想：“我甚至不知道如何形式化地定义一只猫或一只狗，所以这超出了形式验证能做的范围。”因此，存在局限性。你必须意识到这一点。我认为形式化社区也从中吸取了惨痛的教训：如果你不阐明这些假设，人们就会感到失望。
“最后一个问题，什么是瑞士奶酪模型？你是要做烤奶酪三明治吗？”我们使用瑞士奶酪模型作为航空安全的类比。你有许多层防御机制，例如飞机防撞系统。顶层可能是战略间隔，根据你向西或向东飞行，你在不同的高度层飞行。
接着是另一层，可能是空中交通管制。再下一层可以是你的防撞系统。我们称之为瑞士奶酪模型，因为这些不同的层次有不同的脆弱性，也就是奶酪上的孔洞。我们要确保这些孔洞不会对齐。你不希望一个关键场景穿透所有层的奶酪。
“那么，将其应用于这些庞大且令人畏惧的大型语言模型呢？我们控制训练数据、预训练、RLHF（基于人类反馈的强化学习）、RSI以及所有被采样的数据。我们可以剔除坏的数据。”比如，Percy 正在做这件事，他运行一个小模型来检查预训练数据以剔除不良内容。这样这些东西就不会出现在预训练中，因此不可能学到这些坏东西。这是第一步。
现在我们有了训练好的数据，让我们对该数据进行故障分析。估算失败情况，采样一些失败案例，评估某些失效模式。我们要得到 P(成功)，而不是我认为糟糕的营销术语 P(失败)。然后使用工具，一直到运行时监控。
“是的，你需要所有这些层次。”我认为你在开场白中提到的例子很有代表性：他们关闭了思维链监控，这就是其中一层。除了开发我和 Clark 一直在研究的这些技术工具外，我们还需要确保在人类层面建立适当的安全保障措施。
“就像我们从网络安全中学到的那样：入侵系统的典型方式是通过社会工程学。”“没错，太棒了。好的，现在开放给观众提问。前排那位……”
“这个问题是问 Clark 的。”你提到过，在类似美国银行这样的例子中，大多数时候，代码和现实世界之间并没有必然的规范。在这种情况下，你会如何形式化验证这段代码？你是从源代码本身获取规格或假设吗？
“这是一个很好的问题。我认为在可以轻松编写代码的新世界中，希望未来几年也能轻松验证代码，剩下的难点在于规格说明。但你可以做很多事情。”首先存在一个光谱：有些规范是简单且通用的。例如，如果有 C 代码，我希望它是内存安全的。我可以一次性写出这个规范并说每个人都应该证明他们的代码是正确的。
“对于观众来说，什么是内存安全？为什么这很重要？”这意味着你的代码永远不可能访问未初始化或越界的内存。“谁在乎这个呢？”“如果你能做到这一点，你就很可能运行某种缓冲区溢出攻击。众所周知，这被用来获取对各种系统的访问权限。”
“事实上，我认为不幸的是，缓冲区溢出仍然是头号安全漏洞。”还有一些像银行那样领域特定的规范，例如资金不丢失。如果我运行一系列交易序列，那么总金额应该保持不变。你可以提出这些通用事项。
“此外，事实证明代理（Agents）在制定规范方面非常擅长。”如果你最近参加过代码会话，你会发现当你说“我想要这个”时，代理会说：“哦是的。你可能还想要这些、这些和那些。”你会想：“是啊，你说得对，我确实需要那个。”
“我认为代理可以帮助我们编写规范。我想象这样一个世界：你有一个类似助手的代理，与你交谈并带你度过不同的边缘情况。”“那么，例如在开源模型中，假设你正在形式化验证 VLLM 或 SGLang。你可以借助代理编写正式规范。”
“但你怎么知道代理编写的规范与开发者的意图一致呢？”“那里确实存在差距，我认为这是一个有趣的研究领域：构建工具和代理来帮助跨越这一鸿沟。但即使你没有完全跨越这个差距，如果要求你的代理编写一堆规范并证明其正确性且成功了，你很可能拥有比以前更好的代码。”
“谢谢。回到让模型更智能、运行更快的话题上：这些前沿模型越好（假设它们做得好且是优质模型），它们就能为你提供越紧密的规范。”“等等，你没考虑到所有这些其他事情。社交攻击呢？当有人打电话来时……”
哭泣，但那是假的，而且你急着把它给出去。我见过那些关于他们如何黑客攻击的视频……（清嗓子）然后你知道，社会工程学攻击。嗯，一个你可以加入的规范是：如果一个人入职不到六个月，没有经历过那种虚假的社会工程学攻击场景，也没有通过安全培训或类似的内容，那么他们实际上不能向你提供密码重置权限或新电子邮件地址的访问权。你知道的一些事情，你可以思考所有这些场景，但无论如何，是的。好吧。失陪一下。前排这位朋友。
嗯，所以听起来你认为形式化验证是一种严格的审查流程，并可能将其与飞机防撞系统做类比。嗯，也许在工程领域通常存在一定的监管要求，因为一家公司的安全标准可能与其他公司不匹配。那么你认为在人工智能安全领域，监管以任何形式参与吗？如果没有，你有什么手段激励公司采用你的形式化验证引擎？谢谢。是的。（笑声）嗯，是的，我认为监管可以发挥作用。我想……呃，问题是监管是否有作用？不同公司可能有不同的安全标准、安全标准。如果没有的话，你将如何让大家采用你的形式化验证引擎？
哦呃，我认为关于最后一点……所以在监管方面，嗯，我多年来的一位合作者是克里斯·格德斯。他是斯坦福大学机械工程系的教授，现在在Waymo工作。但他从事自动驾驶汽车的研究，他曾前往华盛顿特区帮助交通部制定关于自动驾驶汽车的监管规定。最终我认为他和那里的每个人都意识到，在技术选择方面过于具体地规定还为时过早，而是应专注于更高层面的最佳实践和标准，而不必过于具体，因为这个领域……你知道的，正在发生很多创新，而且这种创新将持续下去。
我认为重要的是要意识到，各种前沿实验室、各种自动驾驶公司并不希望在安全性上进行竞争。对吧？Zoox发生事故不符合Waymo的利益，反之亦然。因此我认为这是一个机会，行业需要在各自的领域内真正合作。自动驾驶的标准将与语言模型或其他人工智能应用完全不同。是的，关于监管我只想说……我认为确实有它的作用。你必须小心，正如迈克尔所说，不要过于具体规定，而是找到激励那些有利于安全的一般原则的方法。
在形式化验证的具体案例中……你知道，我做形式化验证已经30年了，一直在试图让人们去做。试图告诉人们必须以不同的方式做这件事是个坏主意。我认为现在的不同之处在于，我认为市场力量将激励它的发展。所以，如果我们能证明形式化验证是可以自动化的、可以规模化工作并提供更高的安全性，并且有几家公司采用了它，那么其他所有的首席信息安全官都会想：“哦，我们也最好这样做”，否则我们就不会拥有同样的优势。所以我认为……我们将看到强大的市场力量提供帮助，实际上在整个人工智能安全领域都是如此。
而且我想强调的形式化方法的一个好处是，你现在可以瞬间简化事情。以前这需要花费大量时间。你在其中一张幻灯片上提到了这一点，但这非常重要：现在它是可行的了。所以你们因为人们说“哦，你只需要雇佣150名……你知道的，拥有Lean学位的博士”来检查所有Google代码并实现这一点而失去了支持者。现在你不需要那样做了。没错，对吧？你需要……我不知道，100到1,000美元的代币费用。嗯，而且关于迈克尔提出的Waymo没有动机在安全性上进行竞争这一有趣观点……我认为这对前沿实验室也是如此。没有人希望发生更多的攻击或模型的滥用行为，这对所有人来说都是糟糕的市场营销。
托马斯·布朗（Tom Brown）实际上在纳帕已经说过这一点。而且我认为我们还应该说的是，他们都去了白宫并签署了一份包含这四个要点文件的人。所以我实际上希望……他们确实在同意独立审计、一些安全护栏以及其他所有事情方面达成一致。这六家实验室都将做这些事情，包括英伟达（Nvidia），因为英伟达不制造Megatron。他们很少被纳入对话中，但他们应该被包括在内。所以……已经存在一个自我监管机构的框架，它不需要政府监督，也不是惩罚性的——这是你之前使用的词。好的。让我们从后排这边开始。是的。
谢谢。向Anthropic提问。好奇你们首先瞄准哪些应用或市场？以及，你知道的，你如何衡量这些特定目标应用在现实世界中的成功？当然。嗯……我不能说太多关于那方面的事情。我要说的是，我们最优先的任务是构建自主地、自动地、高效地大规模处理代码推理的能力。嗯，我想如果你听过这些实验室谈论数学超级智能的话……这就像代码超级智能。即真正精确推理代码的能力。我们认为一旦拥有它，就有大约10万种事情可以做。你可以想象……你知道的，帮助企业；你可以想象帮助开发者；你可以想象在安全方面提供帮助。所以嗯……是的，这就是我们要前进的方向。成功就是当全世界的代码都得到验证时。
首先，谢谢。其次……嗯，当你像现在的LLM（大型语言模型）时，是一个人类与代码交互的系统……我是说通过界面。我知道有很多提示注入攻击正在发生，可能还有通过智能体发生的XSS（跨站脚本）攻击。你认为形式化验证将如何帮助应对这类攻击？我只是……是的，所以呃
如果我们在讨论从人类到大型语言模型的自然语言，那么其中确实没有任何一部分是我们可以证明其性质的代码。但有些事情是可以做的。例如亚马逊有一种名为“自动化推理检查”的技术，他们会查看大型语言模型的响应，并尝试使用自动形式化方法提取模型试图传达的领域知识，然后将其与严格的领域模型进行比对。因此，即使全是自然语言，也有一些技术可以利用来提供一定的安全性和保障措施。
在我学习计算机科学时，存在像SQL注入攻击这样的漏洞，比如“Johnny drop tables”我记得是经典的利用方式。难道没有类似的模型来检查用户输入并过滤掉提示注入吗？当然有，但这是一场军备竞赛。你们总是试图压倒对方。好的，我想我们有两位提问者了。我先回答后面的问题。
你好，这个问题是问克拉克的。我对你在美洲银行的例子很好奇：即使你形式化了美洲银行内的所有软件，该软件仍然依赖于大量的长尾依赖关系，甚至深入到硬件层面。你可能需要形式化x86指令集，然后……
那已经做过了。多家公司已将x86指令集形式化。那么，你对像行锤击（rowhammer）这类硬件级攻击怎么看？
我认为软件是低垂的果实，而硬件则更难一些。但我认为最终的范畴应该是：验证所有软件、所有编译器以及所有硬件，然后就可以收工了。为什么不呢？我认为人工智能只会越来越好，形式化工具与AI配合得很好。目前有一批初创公司正在借助AI进行硬件验证。我认为这项技术会越来越好。
我在LinkedIn上看到一位医生提到，如果Waymo像制药公司的药物一样有效到能挽救生命，美国政府可能会给予其人道主义使用豁免。所以我很好奇，在网络安全领域是否有类似的东西？在企业系统中，通常有管理员团队。但拥有管理员或开发者权限的人本身也面临威胁：加密高管的手指曾被砍断，90年代Adobe的CEO也曾被绑架。我好奇的是：是否可能存在一个如此值得信赖的人工智能系统，让它成为你的管理员？比如运行在机密虚拟机中。这能限制物理攻击向量吗？
我认为航空领域也有类似的问题，特别是关于飞机辅助自杀和人类飞行员心理健康的担忧。所以问题是：为什么不自动化呢？就像你建议的那样自动化管理。但我认为联邦航空管理局（FAA）在相当长一段时间内不会接受这种想法。目前的设置是，即使飞机是无人的，也必须有一名由FAA监管和认证的飞行员对事故负责。因此我们需要仔细考虑责任问题，这也是我对你的建议的担忧所在。
Waymo的比较很有趣。它并不完美，但据称它在挽救生命。你可以对此提出同样的论点，但我认为迈克尔的观点很好：如果出了问题，你怪谁？制造AI管理员的公司是否愿意承担法律责任？如果他们愿意，说明他们的安全论证做得很好。
这回到了更智能、更好的AI系统这一观点。在信息安全中有一个趋势是“零信任架构”。你要确保对任何单一系统的信任为零，这样即使渗透了一个系统也无法渗透其他所有系统。如果我有一个始终在线的智能AI系统监控流量和数据，看到CTO向外国账户转账或大量密钥被生成并发送到非公司邮箱的Gmail，它会标记出来。虽然有些情况没有硬性规则，但结合足够上下文可以判断“这不正常”并标记给人。我们都有过警报疲劳的问题，AI监控系统能更好地处理这一点。
最后两位提问者。你好，我很欣赏关于形式化验证以及物理系统中的标准和安全性讨论。有一位航空电子专家或教授在场很好。你提到了基于动态系统的模型，如扩散模型和归一化流。目前中国实验室在推动效率前沿，美国实验室在推动智能和能力的前沿，但我们缺乏从一开始就推动可控性和可解释性前沿的人。虽然有一些领域如发展性可解释……
人们正在监控训练动态和新兴能力，并试图拟合我们在该领域中发现的数学规律，将其与我们观察到的现象相匹配。但我基本上想问的是：你认为在约束训练动态和智能方面，或者试图将可解释性与控制力这一前沿领域映射到一个轴上，而将智能和能力（从传统的统计机器学习方法、信号处理和控制理论转向深度学习和神经网络）映射到另一个轴上，是否存在空间？当然，我肯定搞混了很多提到的术语。我不是故意堆砌流行词汇的……比如以某种方式过滤梯度？好的，是的。不，这是一个很好的问题。
我每年三次为团体授课，通过斯坦福商学院高管教育项目向高管们讲授课程，同时也通过人工智能研究所（HAI）提供另一个版本。参与者来自世界各地的高管，他们面临着巨大的压力，需要想出某种人工智能战略并将其融入产品或流程中。我在开始时提醒他们的工程基本原则与科学的基本原则非常相似，即奥卡姆剃刀原理：最简单的解释更可能是正确的。在工程中，更简单、更可解释的方法往往更具鲁棒性。因此，根据应用的不同……
如果你能用线性回归或决策树解决问题，你就应该这样做。现在有很多诱惑让人直接转向神经网络和变换器等复杂模型，但这通常不是正确的做法。因此，我鼓励每个人都尝试最简单的方法，然后尝试稍微复杂一点的方法，看看性能的提升是否值得这种额外的复杂性。如果不值得，就坚持使用更可解释的方法。但我认为这是一个非常重要的话题。事实上，新出版的验证书籍中的一章就是关于可解释性的。这对于让AXI被接受为国际标准至关重要。
快速跟进一下：你认为存在市场激励或足够的需求，使得构建约束型智能的人能够与前沿实验室竞争吗？我会说，如果你能创造出在测量上更安全的东西，那肯定是一个竞争优势。我知道有人在思考如何实现这一点，希望他们能找到办法。如果你打算创办公司，有一些加速器可以申请，它们提供资金和指导。好的，后面那位朋友……你好，非常感谢。我的问题是：互联网时代教会了我们很多关于安全的知识。你认为我们会从互联网时代借鉴什么，还是会在生成式人工智能这一新纪元中学到一些新的东西？特别是关于真实安全方面。
这是问你的，也是问大家的。问题是：我们可以从互联网时代学到什么并应用到当前时代？是的，以及你认为与互联网时代相比会有什么不同？我记得当我还是纽约大学年轻教授时去听了一场关于安全的讲座，演讲者基本上说只有两个问题：一是人，二是计算机漏洞。是的。我认为我们可以修复计算机漏洞，但我认为我们无法解决人的问题。（笑声）但不同的是……
人工智能可以被用于各种创造性的方式。正如弗朗索瓦所说，它可以作为一种看门狗来捕捉一些社会工程学攻击；它肯定可以用来加速形式化方法以保护系统。也许“AI管理员”的想法也不错，只要仍有人员参与循环中。我总是担心……你们有人看过老电影《战争游戏》吗？如果你把一切都交给计算机，当发生奇怪的事情时，如果没有人介入，事情可能会失控。所以我认为我们需要人员参与循环中。
有一篇著名的物理学论文叫《多即不同》（More Is Different）。其前提大致是：如果你有一个原子、两个原子，或者一堆原子……当原子数量巨大时，黑洞开始形成，光无法逃脱。所以会出现奇怪的现象，“多”确实意味着“不同”。在这个世界里，我们有60亿人，现在有70亿人，而现在有70万亿个智能体（假设它们具有同等智力或动机），我可以生成所有这些不同的代理，“多”变得截然不同。
因此，虽然Cloudflare能够阻止DDoS攻击，但当你对数量应用“无穷大”时，一切都会崩溃。奇怪的事情会发生并暴露出漏洞。我今天发了一条推文基本上说：我们在Iclear系统中看到了很多这样的例子，一年内有60,000份提交，这超过了历史上所有年份提交的总和。这是一个巨大的指数级增长（E的常数很大）。因此，所有的审查系统……例如在Focal查看世纪警报、客户支持票证等。想象一下大学录取：对于每个高中生来说，纳什均衡的最优策略是申请美国的所有学校。为什么？事实上，抱歉，整个世界都应该申请所有地方的学校。（对）这很昂贵……他们会不得不收费。如果没有费用，那就会发生这种情况。
那么，你实际上如何处理这种人员参与循环的系统？它们很难抵御DDoS攻击。最近讨论的一个真实案例是小额索赔法庭。如果你的代理可以为你提起小额诉讼，你就不再需要律师了。（对）司法系统会发生什么？
完全陷入混乱了。司法系统的流程本来就已经太长了，现在情况将变得疯狂且不可能完成。因此所有这些系统都需要重新评估。我认为，“多即不同”这一理念带来的学习成果，将从互联网时代到现在产生实质性的差异。我们曾以为自己对大规模有了认知，但人类流量将占互联网流量的0%。也就是说，“零”是一个非常小的数字。
谢谢。 好的，我们还有一个问题的时间。是的，请讲。 嗯，谢谢。这个问题是关于基准测试的基准测试（benchmarking the benchmarks）。背景是我在LinkedIn从事AI安全工作。伤害的定义变化非常快。即使是像有毒文本或偏见这样看似微小的问题，每隔五年新一代人就会为所有事物创造新的俚语。那么，你如何确保这些俚语不会出现在招聘过程中？比如在你从招聘人员那里收到的消息中。你如何衡量这一点？目前的基准测试移动非常缓慢。即使是内部使用的公共基准测试，成本也很高，并且需要经过大量的人工审查。
你对我们如何从当前的“一些实验室发布基准测试且创建缓慢”的状态，过渡到“基准测试动态演变以跟上术语演变速度”的状态有什么看法？
是的，这是一个很好的问题，我喜欢你的例子。嗯，我认为就像我主张持续监控我们的AI系统一样，我们也应该持续监控我们的基准测试。好消息是有一些定量方法可以识别分布偏移和语言中的变化监测，我认为我们只需要去做即可。 没什么要补充的了。好的。好吧，这里还有一个。最后一个问题。
我就关于更好的基准测试（better bench）跟进一下。我认为研究人员经常遇到的一个问题是，一些常见的评估指标——我在说Math 500——存在破损的部分。我觉得需要有人，也许是你所在的团队，与Hugging Face或其他地方进行某种协调，以便代理能集中发现这些资源存在问题。我认为就像我们发布报告指出不同的基准测试或评估指标破损一样，但它们就那样放着不动了。我有一篇论文，但我只是公开呼吁有人能在这里闭环处理此事。
是的，我也看到了这种情况。你知道，我以前的一个学生试图评估SQL查询，没有人能获得超过70%的准确率，然后他展示了其中30%实际上是错误的。所以我认为这仅仅是人们移动太快、有些粗心大意的问题，希望严谨的人最终会赶上并修复它。但这现在有点像是军备竞赛，因为每个人都在试图快速前进。我不知道该怎么办。 是的，我们需要版本控制、拉取请求（pull requests）、问题提交等等。绝对需要。
我实际上认为，一个伟大的创业点子是建立一个像苹果App Store那样的基准测试平台，那里有策展（curation）。就像他们不会让任何人随便把应用扔到App Store上。他们需要经过一个流程，决定你是否应该进入App Store或不被允许。Hugging Face，对Clem表示敬意，我很爱他们，但那里一团糟。那是一团糟。[嗤笑] 就像荒野一样。它就像GitHub，就像狂野西部。因此，试图找到合适的GSMA K实际上并不简单——要找出真正的GSMA K其实非平凡，因为有600个东西都叫GSMA K。我该用哪一个？我不知道。
无论如何，请大家帮我感谢Clark和Michael今晚的出席。
[掌声] 非常感谢。