AI 安全的事实与想象：从形式验证到运行时保障 | YC Paper Club

简要说明Brief Description

AI安全：事实还是虚构 | YC论文俱乐部AI Safety Fact vs. Fiction | YC Paper Club

目录Table of Contents

• 科幻与科学事实
  Science fiction vs. science fact
• 工程问题，还是 P(doom)
  Engineering problem, or P(doom)
• Hugging Face 究竟发生了什么
  What actually happened at Hugging Face
• “10 年增长 10%”的由来
  Where "10% in 10 years" comes from
• 真正的风险：开放权重落入不当之人手中
  The real risk: open weights in the wrong hands
• Clark Barrett：当人工智能遇上自动推理
  Clark Barrett: when AI met automated reasoning
• CSLib：在 Lean 中证明代码正确性
  CSLib: proving code correct in Lean
• 一键将英文规范转化为经过验证的代码
  From English spec to verified code in one click
• Mykel Kochenderfer：我们如何知道一个系统是安全的？
  Mykel Kochenderfer: how do we know a system is safe
• 自适应压力测试：从飞机到大语言模型
  Adaptive stress testing, from aircraft to LLMs
• 验证神经网络
  Verifying neural networks
• 运行时监控与 BetterBench
  Runtime monitoring and BetterBench
• 小组讨论：回顾过去三周的反应
  Panel: reacting to the past three weeks
• 人工智能领域的 NTSB
  An NTSB for AI
• 网络安全能在五年内解决吗？
  Is cybersecurity solvable in five years
• 如果你是美国银行的首席信息安全官 (CISO)”】【
  If you were CISO of Bank of America
• 瑞士奶酪模型
  The Swiss cheese model
• 观众问答
  Audience Q&A

科幻与科学事实Science fiction vs. science fact

主持人：我们今晚要做什么？好，这就对了。好多了。Host: What are we doing tonight? All right, there you go. That's better.

主持人：欢迎来到 YC AI Safety Club。我想我从 2012 年左右就开始从事 AI 相关工作了。如果你在做自动驾驶汽车或其他一些人所说的安全关键系统，AI 安全一直都是一个值得关注的问题。所以我一直在做一些 AI 安全方面的工作。即使是在 Focal，推出新的测试版时，也真的可能搞砸。你知道，我们曾负责沃尔玛的库存管理，所以如果推出一个糟糕的测试版，就可能订购太多牛油果，造成数百万美元的损失。因此，在进行这类部署时，确保自己清楚正在做什么非常重要。过去三周里，嗯，大家对 AI 安全的关注度稍微提高了一些。不知道你们有没有注意到。嗯，我也不太清楚为什么，不过我想，深入探讨这个话题，没有比 YC Paper Club 更好的地方了。Host: Welcome to YC AI Safety Club. I've been doing AI I guess since about 2012 and AI safety has always been a concern if you're doing self-driving car or any safety critical system as some would call it. And so I've been working on some semblance of of AI safety and even at Focal when we're rolling out new betas, you can really mess up. You know, we were we were in control of Walmart's inventory and so if you roll out a bad beta, you order too many avocados and you blow millions of dollars. And so like things have it's important when you're doing these rollouts to make sure you you know what you're doing. In the past three weeks, um there's been a little bump in focus on AI safety. I don't know if you guys have noticed that. Um not really sure why, but so I figured uh there's no place better than YC Paper Club to dive deep into it.

我觉得这场对话有点偏离了科学严谨性，退化、退化、退化了一些，越来越像我大概会称之为歇斯底里的东西：人们不断被错误地引用。我明白，耸人听闻的内容更能吸引点击，诸如此类。但你知道，作为科学家，我们应该回到科学方法的严谨性上，提出可证伪的主张，依靠同行评审流程以及诸如此类的机制，确保我们没有夸大其词。所以我把这场演讲称作“科幻与科学事实”之类的主题。Gary Tan 昨晚在希尔兹堡谈到过这句话。嗯，我们在那里听到了 Sam Altman、Tom Brown 和 Alex Wang 发言，我们大体上就是围绕这个、这个话题展开讨论的。嗯，所以，所谓歇斯底里，就是人们无法测量某种东西，却又忍不住一直谈论它。I think the conversation has kind of devolved devolved devolved a little bit away from scientific rigor and more into what I would probably call hysteria where things are being mis-misquoted and I get it sensationalism gets more clicks and all that kind of stuff, but you know, as scientists here we should like get back to the rigor of scientific method and make falsifiable claims, depend on the peer-review cycle and those kinds of things to make sure that we're not overstating things. So I call this talk like the science fiction versus science facts kind of stuff. Gary Tan kind of said this line up in Healdsburg yesterday night. Um and where we where we got to hear Sam Altman speak and Tom Brown and Alex Wang and we about these these about this topic largely. Um and so hysteria is when people can't measure something but they can't stop talking about it.

我觉得这大概就是我们目前的处境。而且，稍微把视野放宽一点看，这其实并不是什么意料之外的事。每当出现重大技术进步，往往都会伴随着不确定性，也很容易出现夸大其词的说法。比如核技术和原子弹，当时就连爱因斯坦也不确定它会不会点燃天空。显然，天空并没有被点燃，我们现在还在这里。再比如电子计算机，很多人都担心机器会超越人类的一切能力和智能，连艾伦·图灵在20世纪50年代都担心过这一点。他还试着估算过实现这一目标的时间，显然，他的估算差得很远。至于工业自动化，人们也曾担心会导致大规模失业。马克思和凯恩斯都讨论过这类问题：我们该怎么办？And I think that's kind of the situation that we're in and there's and it's not you know to zoom out a little bit this is like not um unexpected. With any major technology advancement it's very often the case that um there's uncertainty and it's easy for hyperbole to set in. And so even if and with the nuclear with the atom bomb uh even Einstein was unsure whether or not uh uh it was going to ignite the sky. And so clearly it didn't we're still here um with electronic computers many people uh even Alan Turing was concerned that machines were going to surpass uh all um uh human uh capabilities and intelligence even back in 1950s um he thought you know he tried to put time frames on it obviously his time frames were were much uh were way off. Um industrial automation people thought about mass unemployment you know uh um Marx and Keynes uh all have those kinds of kind of conversations what are we going to do?

就连互联网这件事，呃，真正发明了以太网的 Metcalfe 都说，网络将会发生灾难性的崩溃——大概就是这个说法。呃，他觉得互联网基本上会瘫痪，因为像 Cloudflare 这样的因素。我想，他主要担心的是 DDoS 攻击。结果这事并没有发生。后来他还出了名地把自己的论文放进搅拌机里，然后把自己说过的话喝了下去。这其实是真事，特别好笑。呃，Google 那边的人觉得，这会毁掉人类的智力：人们只会用 Google 搜索东西，不再真正阅读了。呃，不过大家的智力还是相当不错的，尤其是这个房间里的各位。然后是智能手机和社交媒体，呃，我们刚才还在聊这个。现在我回到斯坦福了，一直在帮 Michael 的课当助教，另外还，呃，你知道的，和 YC 的这一届创业者打交道，他们大多都比较年轻。With the internet even uh Metcalfe who actually invented Ethernet said that um there was going to be catastrophic collapse was the was the phrasing uh on the network and um that the internet was going to basically fail and because of things like Cloudflare I think it was DDoS's was mainly his main concern it ended up not happening and then he famously um put his paper into a blender and then drank his own words. This is actually a true story it's very funny. Um Google people thought this is this is ruining human intelligence people are just Googling things and not actually reading anymore, um, which people are still pretty intelligent, especially in this room. And then smartphones and social media, um, we were just talking about this. Now that I'm back at Stanford and I've been TA-ing classes for Michael, um, and some other, uh, um, you know, just interfacing with with, um, the the the batch at YC, who is predominantly younger younger folks.

我真的、真的特别为如今的18岁、20岁的年轻人感到兴奋。嗯，他们真的特别能干。然后，终于，我们现在进入了这个人工智能时代，关于人类灭绝的讨论又回来了，很容易就会夸大其词，我们大概还是应该回到一些事实。好，有几种说法要……I am like super super excited about the the the the 18-year-olds, 20-year-olds, um, of today. Um, they're just so, um, on it. And then finally now we're in this AI era and the talk of human extinction is back and it's it's easy to jump to hyperbole and we should probably get back to some facts. Okay, so there's a few narratives to

工程问题，还是 P(doom)Engineering problem, or P(doom)

可以从中选择，我们还可以补充更多内容，但这些大概是最重要的两个极端。雅恩·勒昆经常拿涡轮喷气发动机作类比。你们没听他讲过这个，不过归根结底，这就是通过工程手段保障安全。这是一个工程问题。黄仁勋刚才也说了类似的话：这并不容易。让飞机安全很难；要确保飞机起飞时舱门不会脱落、起落架能够放下并正常工作，还要确保部署在波音 737 上的 MCAS 系统经过全面测试，不会做出可能导致故障的操作。这和我们接下来要听到的 ACAS X 类似。它是一个了不起的系统，能够拯救生命，也就是飞机防撞系统。choose from and there's more that we could add but these are the probably the the biggest, um, ends of the spectrum. So, Yann LeCun has this, uh, analogy to the turbojet that he's talked about a lot. You guys didn't hear him talk about it, but it's largely just safety through engineering. This is an engineering problem. Jensen Huang just, uh, said something similar where it's not easy. It's difficult. It's difficult to make planes safe, to make sure the doors don't fly off when you're taking off, make sure the landing gear goes down, the landing gear works, um, that, uh, the MCAS system that deployed to the Boeing 737, um, is fully tested and and doesn't, uh, do things that, you know, can cause failure. And it's similar with ACAS X, which we're going to hear about, too, which is an amazing system that saves lives, uh, the aircraft collision avoidance system.

嗯，另一种说法是，P(doom)在10年内超过10%。众所周知，雅各布·考克森刚刚提出了这个观点，并给出了这些判断。他说：“我认为，人类更有可能失去对这些人工智能的控制，最终导致人类灭绝。”嗯，说实话，我不会评判哪一方。我想今晚的重点是给另一种观点一些发言机会，让你们自己做决定。嗯，我想说的是，在这里光谱两端的这两个人，H指数有一点差异，你们可以据此调整自己的先验判断。嗯，不过让我举个例子……Um, and the alternative, uh, is this P(doom) uh, is greater than 10% within 10 years that, uh, famously, uh, Jacob Coxen just kind of came out and and is setting these things and he said, "I think it's more likely than not that humanity loses control to these AIs and could end in human extinction." Um, you know, honestly, I'm not going to judge one way or the other. I think my point of tonight is to give airtime to an alternative point of view and allow you guys to make your decision. Um I will say that there is a small difference in H index between the two people here on this on on these sides of the spectrum, which you can use to change your priors. Um but let me give an example of the the

Hugging Face 上究竟发生了什么？What actually happened at Hugging Face

夸大其词，或者至少是对实际发生的事情的歪曲或错误陈述。比如，Hugging Face 数据泄露事件就是另一个需要仔细辨析事实与虚构的例子。看看 Slashdot 的标题：“OpenAI 称其 AI 模型自行采取了行动。”OpenAI 从未这么说过。没有任何一份声明这么说过。但这就是当时的标题。嗯，“失控的 AI 智能体在一家科技公司里大闹。”事情并不是这样的。它不是今天突然醒来，然后说：“你知道吗？我想入侵 Hugging Face。你知道我明天要做什么吗？我要解决纳维–斯托克斯方程。你知道我明天还要做什么吗？我要杀光所有人。”你知道，事情根本不是这样发生的。它是被提示出来的。它是在大约 1,200 个智能体参与的 exploit gen 中被提示出来的。hyperbole or at least the misrep or a misstatement um on the things that actually happened. So like the hugging face breach is is is another fact versus fiction thing that we should double click into. If you look at the slashdot headline, OpenAI says its AI models acted on its own. OpenAI never said that. Not in one statement. But this is what was the headline. Um rogue AI agent went haywire at a tech company. It's not what happened. It didn't just wake up today and say, "You know what? I think I'm going to hack hugging face. You know what I'm going to do tomorrow? I'm going to solve Navier-Stokes. You know what I'm going to do tomorrow? I'm going to kill all humans." You know, this is not not the way it happened. It was prompted. It was prompted by exploit gen um in with about 1,200 agents.

而且更重要的是，正如他们指出的那样，他们有思维链——呃，他们发布了一份很棒的、呃，差不多 60 页的文件，叫《OpenAI 与 Hugging Face 事件》。你可以去读那份技术报告，我读过了。CO2 监控是被意外关掉的，或者说，可能是出于其他原因关掉的。他们还说，他们后来重新加上了 CO2 监控，这样就能发现这个问题。第一。第二，还有生产环境的防护措施和安全保障，但当时它们都没启用，因为系统不在生产环境中。所以这些也能发现这个问题。嗯，但这个说法却变成了：它失控了，叛变了，逃出了服务器，复制了自己，现在还在悄悄解数学题、入侵东西、入侵澳大利亚政府——接下来又会怎样？好吧。还有一个挺好笑的地方，如果你真的仔细看看这件事，我当时就想：“好吧，这个‘十年内末日概率 10%’是怎么回事？”And even more, as they did point out, they had chain of thought uh they released this amazing uh um like 60-page document um called the OpenAI hugging face incident that you can read the technical report that I I read and the CO2 monitoring was turned off accidentally or or otherwise. And and it and they said that they repeated they added it back the CO2 monitoring and it would have caught the issue. Number one. Number two, there's also prod guardrails and safeguards that were off cuz it wasn't in prod. And so that would have also caught the issue. Um but the the narrative isn't is that it got it went haywire, it went rogue, it escaped from the servers, made copies of itself, and and now is soft solving math and hacking things, Australian governments, and what next? Okay. The other one that's kind of funny, if you actually double click into this, I was like, "Okay, what's this Pdoom 10% in 10 years thing?"

首先，2023 年有一篇论文，题为《数千名人工智能作者论人工智能的未来》。First of all, there was this paper in 2023 called Thousands of AI Authors on the Future of AI.

“10 年达到 10%”的说法从何而来Where "10% in 10 years" comes from

在那篇论文里，他们询问了大约 1,200 位 Nerbs 人士，嗯，也就是 AI 专业人士，呃，你知道的，问了他们一大堆问题，涉及某些进步会在什么时候实现。后来，在论文中靠后的一个调查问题里，他们问了这三个问题。你认为未来 AI 的进步导致人类灭绝，或以类似方式永久性或严重削弱人类物种的权能，这种情况发生的概率是多少？针对 T 无限，也就是永远。第三个问题问的是未来 100 年内。以下是统计结果。这是平均值，这是……这是中位数。嗯，这些情况都不是发生在未来 10 年内。而这就是人们谈论这个话题时引用最多的那篇论文。顺便说一句，你知道，这个问题有点奇怪。比如说，这个概率到底该怎么估？我刚才还在和教授们聊这个。比如回想一下，我 2012 年开始在斯坦福研究 AI 时，要是我问所有斯坦福教授：“AI 什么时候会独立……解出，或者至少大力协助解出一道千禧年大奖难题？”And in that paper, they asked ner- 1,200 Nerbs folks, um AI professionals, uh you know, these a bunch of questions about when certain enhance- enhancements are going to happen and in in one of the later uh uh survey questions, way later in the paper, they uh asked these three questions. What probability do you put on future AI advances causing human extinction or similarly permanent or severe disempowerment of the human species for T infinity? For all time. In question three, they asked in the next 100 years. And these are the stats. This is the mean and this is the the the the the median. Um and none of that is in the next 10 years. And that was this is the paper that most people are quoting when they're talking about this. Which by the way, you know, if it's kind of a weird question and like how much if I were I was just talking to the professors about this, like if I flash back to when I started in in in at Stanford in 2012 in AI, um when would um if they if I ask all the Stanford professors, "When would uh AI indepen- solve or at least assist majorly in solving a millennium prize problem?"

我觉得你得不到特别好的答案，而且对方肯定不会说是14年之内。我想，大家可能会普遍认为要50年或100年，不过你知道，所以我也不知道问1200个书呆子这类问题能得到多少有用信息，因为这确实是个很难的问题。人们会编出条理清晰的故事，也会自信地做出预测，即使他们对这件事知之甚少，甚至一无所知。我觉得另一个值得一提的是，如果你看过《周六夜现场》的小品，他们做得真是太棒了。我挺替达里奥感到遗憾的，因为我觉得达里奥本人并不是……他们把达里奥塑造得非常古怪，而我觉得他比雅各布·考克森以及EA社群里一些立场强硬的人要平和一些。不过，“我催你让我停下来”这句，我觉得简直太妙了，特别好笑。I don't think you get a very good answer and it definitely wasn't going to say in in 14 years. I think it might have been said 50 years or 100 years would be maybe the consensus, but you know, and so like I don't know if there's very much signal in asking 1,200 Nerbs people um any of these kinds of questions cuz it's really hard question. Um and so people come up with coherent stories and confident predictions even when they know little or nothing about it. Um and so the the other one that I thought if if you've seen the SNL skit, man, they did such a good job. And I feel bad for Dario, cuz I don't think Dario is actually um um They they portrayed Dario in a very very weird light, and I think that he's a little bit more um even keeled than Jacob Coxson and some of the strong EA community. Um but the I urge you to urge me to stop, I thought was just too perfect, was very funny.

所以，我当时正开车从希尔兹堡回来，这事我以前真的从来没见过。我开车经过金门大桥很多次了，嗯，整个车程中我都在想今晚要说些什么。我开车经过金门大桥时，整座桥都被浓雾吞没了。我觉得这简直太完美了，我一定得聊聊这件事。呃，第一，它看起来真的很酷。第二，嗯，我拍这张照片时差点撞车，不过算了。呃，我们知道未来并不确定。我们可以设定一个先验，认为桥还在那里。它也可能不在。所以，我们会朝它开过去，应该分配先验，然后选择概率的 argmax，也就是，你知道吗，我觉得桥还在那儿。我们就继续开吧，然后你知道吗，我们继续往前开，随着我们不断前进、获得更多信息，我们就会调整策略，也许我会停下来。So, I was driving back from Healdsburg, and this is I've never actually seen this. I've driven over the Golden Gate many times, and um I was thinking about what I was going to say tonight uh the whole drive, and I was driving over the Golden Gate, and the entire bridge was gone in fog. And I thought this was like so perfect, I have to talk about this. Uh one, it looks really cool. The second, um which I almost crashed taking this picture, but anyway. Uh the we know the future isn't certain. I we have some prior we can allocate that the bridge is still there. It may not be. So, we're going to drive toward it, and we should allocate the prior and choose the argmax probability that, you know what, I think that the bridge is still there. Let's just keep driving, and you know what, we'll keep going, and as we keep driving and the get more information, then we'll we'll change gears, maybe I'll stop.

我不知道，在我上桥之前，或者进入……进入海湾之前。嗯，所以，I don't know, before I get on the the bridge or go into the into the bay. Um so,

客人：[清了清嗓子]Guest: [clears throat]

主持人：我几乎完全不担心这种可能性，也就是 AI 会发展出灵魂、拥有意识、拥有某种意志和动机，并因此在不久之后，比如 10 到 20 年内，凭借自己的独立意志杀害并奴役我们。时间无限长的话，我觉得什么事都会发生。所以，我不确定这有什么用。嗯，我最主要的担忧是，而且……Host: I'm not concerned uh almost at all uh with this path, this reality that um AI is going to develop a soul, has consciousness, is has some will, has some motivation, and um and thus killing and enslaving us uh with its own independent volition um in some short period of time, such as 10 and 20 years. In infinite time, I think everything happens. Um so, I'm not sure that's useful. Um number my number one concern is, and

真正的风险：开放权重落入不当之手The real risk: open weights in the wrong hands

这确实是个非常现实的问题。开源权重模型真的很棒吗？它们会让坏人、流氓行为者或民族国家更容易大规模做出同样的事。所以，如今我们面临恐怖主义、生物武器、网络战争、网络勒索攻击。我的一位朋友在波兰当地的医院刚刚就遭遇了这种事：一群俄罗斯黑客控制了医院，让医院停摆了三周。他们也许是用 AI 做到的。而接下来会发生的是，这会让做这种事变得更容易。这样的事情已经会发生了。嗯，针对这个问题，人们提出了几个解决方案，我觉得它们都挺糟糕的。一个是禁止开放权重模型。祝你好运。我已经把 Kimmy K3 和 GLM 52 下载到了我的……车库里，所以抱歉了。第二个方案是登记 GPU。this is very real, is that really great open weight models allows for a lot more of the same from this from bad bad rogue actors or nation states. So, today we have terrorism, we have uh bio weapons, we have uh uh cyber warfare, ran cyber ransom attacks. It just happened to my friend's local hospital in Poland where a bunch of Russian hackers took control of a hospital and shut down the hospital for 3 weeks. And maybe they used AI to do it. And what's going to happen now is it makes it easier to do that. And and so that's going to happen already. Um and there's a couple solutions to this that people have proposed and I think they all kind of suck. One is banning open weights. Good luck with that. I've already downloaded Kimmy K3 and GLM 52 already in my um in my garage, so sorry. Second is registering the GPUs.

再说一次，我车库里有一堆小盒子。你知道，除非你打算搜查每一个人的家，以及每一个 AI 从业者，否则你也不可能知道他们有没有 GPU。嗯，而且我还可以在另一个国家预订一块 GPU，你也没法阻止我，所以我也不知道这到底能解决什么问题。有些很酷的想法，比如公用事业公司可以根据电网上的负载信号，检测你家有多少台洗碗机、多少台冰箱。嗯，在你的电表上检测这些，这还挺酷的。你可以检测到有人在进行推理时发出的信号，从而发现他们在做坏事，至少在美国是这样。但我并不是……我并不是特别担心这会是主要问题。我觉得，你知道，我们正和许多……许多民族国家处于战争状态，而这并不能真正解决任何问题。Again, I have a bunch of tiny boxes in my garage. You know, unless you're going to search every single person's house and every AI person, you know, it's uh you're not really going to know that they have GPUs or not. Um and also I can just book a GPU in another country that you can't stop me from doing, so I'm I don't know how that really solves anything. There is some cool ideas where you have utilities that can detect how many dishwashers and how many refrigerators you have based on the signal of the the load on the network uh on the on your um on your meter. And you know, that's kind of cool. You can detect inference signals that people are doing bad things, at least in America. But I'm I'm not I'm I'm not entirely concerned that that's the main concern. I think you know, there's a lot of of you know, we're we're at war with a lot of um nation states that this doesn't doesn't really solve anything.

嗯，美国的恶意行为者，好吧。最后一项有点像兜底措施，基本上能解决各种问题，而且我们应该独立采取这项措施，那就是投资防御。所以，如果你是银行、医院、金融服务机构，或者政府，都应该大力、大力、大力投资网络防御。嗯，有很多办法可以加强自身防护。我在零售行业工作了很长时间，那些系统都非常过时，很久没人维护了。像试试 admin admin 这样简单的方法，实际上就能让你进入系统。好吧，为什么几乎所有社保号码都遭到了泄露？那是因为 [嗤笑] 他们没有更改 admin admin 密码。嗯，如果我们采用更智能的模型，真正加快速度，不但不放慢脚步，反而加速推进，让好人——假设这些前沿实验室里的人是好人，我觉得他们是——能够更快行动。Um rogue actors in in America, okay. And the last one, which is kind of a catch-all, serves uh it solves mostly anything and we should be doing it independently, is invest in defense. And so, if you are a bank, you are a hospital, you are a uh you know, financial service, you're a government, you should be investing heavily heavily heavily into into uh cyber defense. Um And there's a lot of things that you can do to tighten up your ship. I worked in in retail for a long time. These are very antiquated systems that haven't been touched in a long time. And simple methods such as trying admin admin work. They actually get you into the system. Okay, why is it almost all the social security numbers breached? It's cuz [snorts] they didn't change the admin admin password. Um and with smarter models, if we actually go faster and we don't decelerate but accelerate where the good people, presuming that these frontier labs are the good people, which I think so.

呃，如果我们给这些好人更多资源，让他们进展得更快、再快一些，那么我们就能为一个试图入侵系统的更笨的模型做好准备。嗯，如果情况反过来，那肯定会更糟。所以，嗯，这就是我的一点看法。回到理性，摆脱歇斯底里，回归科学事实。你知道，关于这件事会如何杀死我们所有人的种种惊人叙事层出不穷，听起来真的很像艾萨克·阿西莫夫的小说。嗯，你知道，早在大型语言模型被发明或训练出来之前，关于安全性的文献就已经积累了很久。我想，今晚我们有幸请到的正是这些人。人工智能安全社区已经存在很长时间了，有很多论文，也有相关的会议。嗯，其中一场会议刚刚就在斯坦福举行。Uh if we give these good people even more resources and they go faster and they go faster, then we can prepare for a dumber model trying to hack the system. Um it would definitely be worse if it were flipped. So, anyway, that's my my two cents. So, getting back to sanity out of hysteria into science facts. You know, I there's amazing narratives on how this was going to kill us all and they they really sound like an Isaac Asimov book. Um and and I and you know, I wanted there's there's been a whole literature for a very long time about safety well before LLMs were invented or trained. And those are the people that were lucky enough to have tonight. This AI safety community has been around for a long time. There's a lot of papers. There's conferences on this. Um and one of those just actually happened at at Stanford.

那次会议的联合主席今晚会来演讲。下面有请 Michael Kogut 和 Clark Barrett。他们是斯坦福大学两位非常出色的教授。我认识 Michael 已经 14 年了。我记得我在 2013 年上过他的《不确定性下的决策》课，后来还多次给他当助教，也长期为他做研究。他是我共事过的最友善、最聪明的人之一。我对 Clark Barrett 没那么熟悉，但听过他的演讲，他确实非常了不起。他们两位都想谈谈如何运用现代方法，在数据投入生产前对其进行验证，并持续监控，确保数据不会偏离正轨、惹出麻烦。Michael 是航空航天学副教授，同时也在计算机科学系任职。And the co-directors from that conference are going to be speaking tonight. And so, here's Michael Kogut and Clark Barrett. They're two amazing professors at Stanford. I've known Michael for 14 years. I think I took his class decision making under uncertainty in 2013 and then I TA'd him TA'd for him many times and I've done research for him for a long time. He's one of the nicest and smartest human beings I've ever worked with and I know Clark Barrett less well but I've listened to his talks and he's just incredible and they both have some something to say about how we can actually apply modern methods to validate data before they're put into production and then monitor them to make sure they don't don't go off the rails and do bad things. Michael is an associate professor in aeronautics and then by courtesy is that in CS.

他是我所在实验室——斯坦福智能系统实验室的主任，也是斯坦福人工智能安全中心的联合主任，同时还是 HAI 的高级研究员。Clark Barrett 是计算机科学教授，与 Michael 共同担任斯坦福人工智能安全中心的联合主任，同时也是自动推理中心的主任。他将介绍一家名为 Ampersand Truth 或 And Truth 的新隐形初创公司。回到我们刚才的话题。好了，我要说的就这些。我想我们已经安排好两周后举办一场推理之夜，届时会有一些非常非常厉害的人来参加。Dan Fu 已经确认会代表 Together AI 来谈推理。如今在某些情况下，推理变得比训练还复杂，这让我觉得挺不可思议的，因为我学的时候，推理通常就是这样：model.forward。He's a director of my lab Stanford intelligent systems lab co-director of the Stanford Center for AI safety and senior fellow at H AI. And Clark Barrett is professor in computer science co-director of the Stanford Center for AI safety with Michael and then director of the the Centor Center for automated reasoning and he'll be talking about a new stealth startup called Ampersand Truth or And Truth. Back to what we're talking about here. Okay, that is all I got. I think we have scheduled already in 2 weeks a inference night and there's some really really cool people coming. We already have Dan Fu committed from Together AI to talk about inference. Inference is becoming more complex in some cases than training which is kind of crazy to me cuz it's usually when I learned it it was just you know model.forward.

我原以为你只要做这些就行了，但现在事情变得有点复杂了。然后是 Jeffrey Morgan，他在一家名为 Llama 的公司；还有 Clark Barrett 的一位学生，我这个周末刚认识她，她经营着一家很酷的公司，叫 Radix Arc。其实，Lang，我觉得她来不了，她会派她的同事来。然后还有 Wafer，另一家很棒的 YC 公司。好了，行。请大家欢迎 Clark。I thought that's all you had to do but it's a little bit more complicated than that now and then Jeffrey Morgan at a llama and then one of Clark Barrett's students who I just met this weekend runs this cool company called Radix Arc. Actually Lang I don't think she can make it she's going to have one of her folks make it and then Wafer another great YC company. Okay, all right. Please help me in welcoming Clark.

Clark Barrett：当人工智能遇上自动推理Clark Barrett: when AI met automated reasoning

嘉宾：好的，谢谢。很高兴来到这里。今天我要跟大家讲讲 AI 遇上 AR 的故事。你可能会想，AR 是什么？它不是增强现实，而是自动推理。这两个主题之间有一种很棒的协同效应，因为我们都知道，AI 很擅长处理各种各样的事情，比如杂乱的数据、数据驱动的任务，还可以训练模型。但它有一个很大的问题：没有正确性保证；你可能会发现对抗性输入，它也会产生幻觉，诸如此类。另一方面，自动推理本质上是计算机化的形式推理。如今，它已广泛应用于工业领域，用于安全保障。而它的核心就在于提供正确性保证。好了，先记住这一点，我给大家讲个小故事。Guest: All right, thank you. And it's a pleasure to be here. So, I'm going to tell you about when AI met AR. You might be wondering what AR is. Not augmented reality, it is automated reasoning. And uh there's a very nice kind of synergy between these two topics because as we know, AI is great with all sorts of things, messy data, data driven, you can train stuff. But it has this sort of one big problem which uh you know, no correctness guarantees, you can find adversarial inputs, it hallucinates, all this kind of stuff. On the other hand, automated reasoning is uh essentially computerized formal reasoning. Uh there's extensive use uh already today in industry for safety assurance. And that's that's what it's all about is correctness guarantees. All right. So, hold that thought and I'll tell you a little story.

好吧。我们都知道这件事，对吧？这种新兴威胁——在 AI 时代，安全该怎么办？你可能听说过 Project Glass Wing 之类的项目，你知道，这类事情也助长了 Francois 刚才提到的那种恐慌。那我们能帮上忙吗？我们能做点什么吗？嗯，2023 年我参加了 Google 的一次研讨会，当时有不少知名人士在谈论风险和担忧：如果生成式 AI 能发现安全漏洞，那我们该怎么办？嗯，我当时就想，有办法啊。如果你把所有代码都做正式验证，那它就不会被黑。对，他们可不想听这个。嗯，因为这太难了。而他们会这么回应也是有充分理由的，对吧？传统的正式验证需要付出巨大的努力，自动化技术要么能力太弱，要么无法扩展，根本不具备经济可行性。Okay. So, we all know about this, right? This emerging threat, what about security in the age of AI? You probably heard about things like Project Glass Wing, you know, and this kind of uh feeds into the hysteria that uh Francois was talking about. Uh well, can can there can we help? Can we do something about this? Um back in 2023, I was at a workshop at Google and uh a bunch of notable people there talking about risks and worries and hey, what if gen AI can find security vulnerabilities? What are we going to do? Um well, I was like, there is a solution. If you formally verify all your code, then it cannot be hacked. Yeah, they didn't want to hear that. Uh that's like too hard. And there's good reason for that response, right? Um the traditional formal verification requires monumental effort, the automated techniques are too weak or they don't scale, just not economically viable.

好，快进到我参加的另一场会议。大家讨论了很多关于人工智能风险和担忧的话题。然后，在我发言之前的每一场演讲都说，只有一个答案，而这个答案就是形式化方法。好吧，我可没料到会这样。所以，人们对形式化方法的态度或许有了一点转变。这种转变有道理吗？今晚我想和大家稍微探讨一下。好，那么我们担心的是什么呢？嗯，我们担心的是——我做这张幻灯片时，写的是“未来”，我把它划掉，改成了“现在”。Well, fast forward to another conference I was at. Lots of discussion about risks and worries of AI. And then every talk before mine says they there is only one answer and the answer is formal methods. Okay, that was not expecting that. So, there has been maybe a little bit of a shift in the attitude towards formal methods. Is this warranted? That's what I want to explore with you a bit tonight. Okay, so what what are we concerned about? Well, we're concerned about when I made this slide it was future, I crossed it out, present.

主持人：[清了清嗓子]Host: [clears throat]

嘉宾：AI 系统会制造出海量有 bug 的软件，对吧？我不知道你是否担心这个问题，我是挺担心的。或者它会大幅提升黑客攻击遗留系统的能力。所以，你知道，我们正受到两面夹击。很多人都在关注形式化方法，想着这里面是不是有办法能帮到我们。大家也对 AI 在数学方面有多么出色感到兴奋。好吧，也许这是个信号，说明这里确实有些事情正在发生。好吧，但我们该怎么做到呢？我们怎么才能从解决一个千年难题，走到让你的软件变得安全？嗯，[清了清嗓子]所以 AI 确实是……Guest: Where AI systems create mountains of buggy software, right? I don't know if you're worried about that, I'm worried about that. Or it dramatically increases the capabilities of hackers to attack legacy systems. So, we've got we're you know, we're being threatened on both sides here. And a lot of people are sort of looking to formal methods like is there maybe something here that can help us? There's also a lot of excitement about how great AI is at mathematics. Okay, maybe that's a signal that something's going on here. Okay, but how do we get there? How do we get from, you know, solving a millennium problem to making your software secure? Well, [clears throat] so AI is really

CSLib：在 Lean 中证明代码正确性CSLib: proving code correct in Lean

它擅长编写代码，也非常擅长撰写数学证明。但事实证明，撰写数学证明和保障代码安全之间有很大的区别。因此，弥合这一差距，是我过去几年一直在认真思考的事情。接下来我会简单介绍一下我们在做什么。好，我要向你介绍一个名为 CS lib 的项目。CS lib 的灵感来自 Mathlib 在数学领域的成功，但我们的想法是构建计算机科学理论，并打造一个真正能够对代码进行推理的平台。嗯，好吧，我们有一个很棒的指导委员会，其中包括 Lean 的作者 Leo de Moura。我们还有一些技术负责人。我们使用 Lean。如果你不知道它是什么，那就从岩石底下爬出来吧。不过，Lean 是一个很棒的定理证明系统。基本上，它会检查——系统本身会检查每一个步骤。good at writing code, it's really good at writing math proofs. But it turns out there's a big difference between writing math proofs and securing code. And so, bridging this gap is actually something I've been thinking a lot about last few years and I'll tell you a little bit about what we're doing. Okay, so I'm going to tell you about a project called CS lib. CS lib is inspired by the success of math lib for mathematics, but the idea is to build computer science theory and also a a platform for actually reasoning about code. Um Okay, and we've got this great steering committee including Leo de Moura, the author of Lean. Uh we've got some tech leads. We're using Lean. If you don't know what that is, you know, climb out from under a rock, but um Lean is a great theorem proving system. It basically is a system that lets you check the system itself checks every step.

它不允许你犯错。呃，这正是我们在处理高保证性场景时所需要的。好，CS lib 有两大支柱。第一是 CS 理论的形式化，第二是用于推理代码的框架。我来介绍第二个，这也是我最感兴趣、参与最多的部分。好，下面这张幻灯片讲的是 CS lib 的愿景。设想一下，你可以把各种不同语言编写的程序，改写成这种通用的中间语言。然后，你就可以把它编译成 Lean 中的验证条件，接下来只需要证明一系列 Lean 定理。如果能做到这一点，就证明了你的代码是正确的。好，我们目前进展如何？嗯，就在 Lean 中证明定理而言，AI 表现相当不错，但我们也有一些比 AI 成本低得多、效果更好的技术，比如 Lean SMT。它是我们实验室开发的工具。It doesn't let you make a mistake. Uh and this is really what we need when we're dealing with uh you know, high assurance situations. Okay, so CS lib has two pillars. The first is formalization of CS theory and the second is framework for reasoning about code. I'm going to tell you about the second one. This is what I'm most interested in and involved with. All right, here's one slide about the vision for CS lib. The idea is maybe you take programs in all sorts of different languages. You would rewrite them in this uh common intermediate language. You can then compile it down to verification conditions in Lean and then all you have to do is prove a bunch of Lean theorems. If you can do that, you showed that your code is correct. Okay. How far along are we on this? Well, um in terms of proving theorems in Lean, you know, the AI is pretty good, but also we have some techniques that are much cheaper and better than AI like Lean SMT, which is tool that we built in my lab.

呃，它能在 CPU 上以毫秒为单位证明很多 Lean 定理，你知道。所以，Lean 中证明定理的技术正变得越来越好。这很棒。嗯，现在我来给你介绍一下。这里有一些代码。这是用 Rust 写的，是 Dalek 轻量级密码学库的一部分。然后，[清嗓子]嗯，实际上这是 Vera，所以你可以看到这里有一些规格说明、一些证明步骤和一个不变量。嗯，现在我要给你看的是，同一段代码已经被翻译成 Bull 语言了。这是 Bull 中的同一个过程。你可以看到，我们保留了前置条件、后置条件和不变量。不过现在这一切都嵌入在 Lean 中了。所以，我们可以在这里调用 VC 生成器。你可以看到，它生成了 35 个目标。Uh it can prove a lot of Lean theorems, you know, in in milliseconds on on a CPU. So, uh the techniques for proving theorems in Lean are just getting better and better. So, that's great. Um and now I'm going to tell you about So, here we have um some code. This is in Rust. This is part of the Dalek light uh cryptography library. And [clears throat] um actually this is uh Vera, so you can see it has uh some specifications, uh uh some proof steps here and an invariant. Um now what I'll show you is um that same code uh has been translated into the Bull language. So, this is um the same procedure in Bull. You see we preserve the uh pre- and post-conditions and the invariants. Um but this is all now embedded inside of Lean. And so, we can call our VC gen uh VC generator here. And you can see that this generates 35 goals.

嗯，每个目标都是一个 Lean 定理，我们必须证明它。然后，嗯，我们会尝试使用 SMT tactic。这会调用 Lean SMT。你可以看到，嗯，它解决了除三个以外的所有目标。接着我们再做一步，展开一些定义，再次调用 SMT。嗯，这样就完成了证明。所有目标都已解决。好。所以，这是我们一起搭建的一个小型原型，展示了如何从 Rust 到 Bull，再到 Lean 定理，证明这些 Lean 定理，这样你就能够证明代码是正确的。嗯，好。太好了。现在，假设我们成功了，并在 Lean 中构建了这一整套东西。我们就有办法对各种语言中的所有代码进行推理，并证明相关定理。但我们仍然面临一个问题：总得有人来编写规约。总得有人说明代码应该具备哪些性质。Uh each goal is a Lean theorem that we have to prove. And then um we'll try the SMT tactic. This calls Lean SMT. And you see that um that solves all but three of the goals. And then we do one more step where we unfold some definitions, call SMT again. Uh and that completes the proof. All the goals are are solved. Okay. So, what this is a little prototype that we put together showing how you can go from Rust to Bull to Lean theorems, prove the Lean theorems, and now you are able to show that the code is correct. Um okay. So, that's great. Now, suppose we succeed and build this whole thing in Lean. We have a way to reason about all code uh in every language and prove theorems about it. We still have a problem, which is somebody's got to write the specifications. Someone's got to say what it are the properties that that code should have.

那么，嗯，AI 或许能帮我们解决这个问题吗？So, can um maybe AI help us with this?

一键将英文规格转化为经过验证的代码From English spec to verified code in one click

好了，这里我们演示一下名为 Verisforge 的工具。你可以用英语输入一份规格说明，描述你想构建什么。然后，它会生成代码并进行形式化证明。我们可以试一个简单的例子：找出一个 32 位整数数组中的最大元素。我们点击这里，它首先会生成一份结构化语言编写的规格说明。我们可以看一下，然后说“是的，我们认可”。接下来，它会根据这份结构化语言规格说明生成 Rust 代码和一份 Vera 规格说明。然后，它会使用 Vera 工具对代码进行验证，并检查规格说明是否保持不变。这样，我们就得到了一段完全自动验证后生成的代码。Okay, here we have a demo of our tool called Verisforge. And what you can do is enter uh a specification in English of what you would like to build. And then it will uh build the code and do the formal proof. So, we can do a simple example. Uh says find the maximum element in an array of 32-bit integers. So, we click here and first thing it will do is it will generate a specification in structured language here. Um we can look at this and say yes, uh we approve. And then what it will do is go ahead and generate uh Rust code and a Vera specification um based on that uh structured language specification. And then it actually uh verifies it with the Vera tool and checks that the spec uh is unchanged. And so, now we have uh fully automatically verified uh code that has been generated.

主持人：好，这又是一个玩具示例。呃，我们能不能做得更好？嗯，能。实际上，呃，在最近一次档案提交中，我们展示了一个有 3 万行代码的 Rust 程序——一个加密库。原本需要五位专家花三个月，或者三位专家花五个月才能完成的工作，我们的加密证明器代理只用了 11 个小时就全自动完成了。Host: Okay, so that's a toy example again. Uh can we do better? Well, yes. Actually, um in a recent uh archive submission, uh we showed that uh 30,000 line Rust program, which is a crypto library, took uh five experts 3 months or three three experts 5 months to do were able to do it in 11 hours fully automatically with our crypto prover agent.

客人：[清了清嗓子]Guest: [clears throat]

主持人：好。所以这只是我认为形式化方法领域能够做到的一点初步展示。我认为，形式化方法加上 AI，能让我们以一种方式——就像 François 刚才说的那样——真正构建强大的防御，呃，创造一些新的基本构件，用来搭建 AI 安全技术栈。我喜欢这样说：如果 AI 安全是一座我们必须攀登的珠穆朗玛峰，那么我认为代码推理就是一个不错的大本营。嗯，还有几件非常有意思的事。想象一下，如果我们能将大规模代码推理作为一种新的基本构件，就可以做一些有趣的事情。比如，在一个这样的世界里，智能体 A 和智能体 B 在网络空间相遇，智能体 A 说：“嘿，智能体 B，我可以为你提供这项服务。”智能体 B 说：“太好了，给我看看你的代码和证明。”于是 A 把它们展示出来，说：“好，太好了，我信任你。”Host: Okay. So, that's just like a taste of what I think can be done in the formal methods space. I think formal plus AI gives us a way to, you know, what François was talking about, actually build some really strong defense, uh create some new primitives that could be used to build up uh an AI safety stack. I like to say that if AI safety is a Mount Everest we have to climb, I think that code reasoning is a good base camp. Um there's also a couple of really interesting things. So, if you imagine a world where you have code reasoning at scale as a new primitive, there are interesting things you could do. For example, if agents A and B meet each other in cyberspace, and agent A says, "Hey, I can provide this service to you, agent B." Agent B says, "Great, show me your code and your proof." And an A shows it and says, "Great, okay, I trust you.

你可以做到这一点。”呃，这会是一个很酷的未来。我觉得这项工作另一个有意思的地方在于，它是一个“能力限制”的例子。比如，你可以把一个超级智能 AI 放进我们的加密证明代理里。它唯一能做的就是证明你的代码正确，除此之外什么也做不了。所以，如果我们能想出办法实现这类事情，我认为我们就能从 AI 中受益，同时避免出现不好的结果。好，我最后想告诉你一件事，就当作一个预告吧。呃，我是 And Truth 这家新公司的联席 CEO。我们正尝试构建一种通用代码推理引擎，方向就是我今天跟你讲的这些。所以，呃，敬请关注。我的分享就到这里，谢谢。You can do that." Uh that would be a cool uh future. And the other thing that I kind of like about this work is it's uh an example of containment. So, you could put a super intelligent AI into our crypto prover agent. The only thing it can do is prove your code correct. It can't do anything else. That So, if we can imagine ways to do those kinds of things, I think uh we'll be able to benefit from AI without you know, having a a bad outcome. Okay. Last thing I want to tell you is just a teaser. Um I'm co-CEO of a new company called And Truth. We are trying to build a universal code reasoning engine along the lines of what I told you uh today. So, uh keep an eye out for that. And I'll end there. Thanks.

嘉宾：非常感谢。好的。好。接下来，有请 Marco Koken Derfer。Guest: Thank you so much. Okay. All right. Next up, Marco Koken Derfer.

Mykel Kochenderfer：我们如何知道一个系统是安全的Mykel Kochenderfer: how do we know a system is safe

主持人：好。那么问题是这样的：如果我们构建一个系统，也许是一个 AI 系统，我们怎么知道它是安全的？我来介绍一下我们在斯坦福智能系统实验室（Sizzl）开展的一些研究。我的研究生们自称“Sizzlers”。对于一个包含学习组件的系统，比如飞机自动着陆系统，要提供什么证据才能证明部署它是合理的？对于商业航空交通，我们的目标是每飞行小时发生灾难性故障的概率约为 10 的负 9 次方。在 ACASX 飞机防撞系统的研发过程中，我们也被要求达到这一标准。现在，如果直接模拟这些场景，那么平均而言，你需要模拟大约 10 的 9 次方小时，才能检测到一次故障。Host: All right. Uh so, here here's the question. Uh if we build a system, maybe it's an AI system, how do we know it's going to be safe? And I'll tell you about some of the research we've been doing in the Stanford Intelligent Systems Laboratory or Sizzl. My graduate students call themselves Sizzlers. And uh for a system with learned components, um maybe it's a auto landing system for an aircraft, what evidence do you need to justify deploying it? So, for commercial air traffic, what we're aiming for is about a 10 to the minus nine probability of catastrophic failure per flight hour. So, that's what we were held to in the development of the ACASX uh aircraft collision avoidance system. Now, if you were to directly simulate these uh scenarios, then you would need about 10 to the nine simulated uh hours before you detect a on average a a single failure.

如果你想获得这类故障的统计表征，就需要——比如说，如果需要 10 次故障样本，就得先模拟 10 的 10 次方个小时，才能得到这 10 次故障。所以这通常并不容易。当然，你不会想把时间花在模拟那些飞机相隔 5 英里、并没有真正构成危险的情况上。相反，你想模拟能够代表空域情况的关键场景。那么，如何获得这种分布呢？在我们的实验室里，我们会探索多种不同的方法，以便在系统部署前建立对它的信任。其中一种方法称为证伪，即在可能的场景空间中搜索故障。And if you want to get a statistical representation of these types of failures, you're you're going to need like like if you need 10, then you need to run 10 to the 10 uh simulated hours before you get get those 10. So, that's typically not super easy. Of course, you don't want to spend your time simulating situations where the aircraft are I don't know separated by 5 miles and don't really present a hazard. Um instead you want to simulate critical scenarios that are representative of of let's say the airspace. So, how do you get that that distribution? Okay, we're in in our lab we explore a number of different kinds of approaches to establishing trust in a system before deployment. So, one approach is just known as falsification where you search the space of possible scenarios for failures.

如果你发现你的系统导致了大量失败，而你审视这些失败时心里感到不踏实，那么也许你就不应该部署这个系统，或者需要考虑采取缓解措施，帮助避免那些、呃，关键场景。我们通常真正想做的是估算失败的概率。为此，你需要有一个自己确实信得过的模型。因此，在开发 ACAS X 碰撞避免系统时，我们投入了大量精力对空域进行统计建模。然后，呃，另一个类别是验证，这也是克拉克实验室的研究主题，我们实际上已经合作了好几年。不过，这通常被视为另一个领域，而我们正在寻找机会与之建立联系。And if you find that your system results in a bunch of failures and you look at those failures and you have a bad feeling in your heart, then maybe you should just not deploy that system or you need to think about mitigations to help prevent those those uh critical scenarios. Often what we want to do is actually estimate that probability of failure. And for this, you need to have a model that you actually trust. So, for the development of the ACAS X collision avoidance system, we poured a huge amount of effort into the statistical modeling of the airspace. Then uh another category is verification, which is the the subject of of Clark's lab and we've actually collaborated for a number of years. But the this is often treated as a different community and we're finding opportunities to to bridge into that.

所以，我们实验室研究各种不同的方法。事实证明，要建立对一个系统的信心，并没有什么一招制胜的办法。形式化方法可能无法带你走完整个过程。不过，Clark 正在帮助我们不断取得更大进展。这确实需要多种不同类型的方法。我们当然也一直在研究 POMDP 规划，即部分可观测马尔可夫决策过程。这类方法能让你构建极其稳健的系统，使其能够应对状态不确定性、结果不确定性、交互不确定性、模型不确定性，等等。我们还喜欢以现实世界的问题为导向，包括航空器、驾驶、航天器、医疗后送等。我会介绍其中几个例子。So our lab works on a variety of different methods. So it turns out that in order to establish confidence in a system, there there is no one silver bullet. Probably formal methods won't take you the whole way there. Um although Clark is helping us get further and and further. Uh it really requires a number of different kinds of approaches. Uh we've also been looking at of course palm DP planning, partially observable Markov decision processes and these kinds of methodologies allow you to build extremely robust systems that are robust to state uncertainty, outcome uncertainty, interaction uncertainty, model uncertainty and and so forth. And we like to be driven by real-world problems uh including aircraft, driving, spacecraft, medical evacuation and so forth. And I'll mention a few of these.

我们也喜欢在现实世界中测试它们。当然，如果能把一切都模拟出来，那就太好了。但我们对安全性的推断，最多也只能和模拟器一样可靠。我们曾经采用的一种、一种方法是……And uh we like testing them also in the real world. Of course it's great if we can simulate everything. Uh but our inferences about safety is only as good as the simulator. One One kind of approach that we've

自适应压力测试：从飞机到大语言模型Adaptive stress testing, from aircraft to LLMs

这种方法称为自适应压力测试（adaptive stress testing）。这项工作源自 Richie Lee 的研究。他曾是我的一名博士生，当时也是 NASA Ames 的公务员。我们实际上部分借助这项工作，帮助验证 ACAS X 系统的不同版本。此后，不少学生在这项工作的基础上进一步开展了研究。最近，我们一直在探索如何将一些为验证飞机而形成的见解，应用到语言模型验证领域。这是我的学生 Hujun Liu、Amelia Hardy 等人牵头开展的一些工作。在飞机场景中，故障的定义比较明确，对吧？就是金属与金属发生碰撞，也就是飞机的水平间距小于 500 英尺、垂直间距小于 100 英尺。taken is known as adaptive stress testing. So this came out of the work of Richie Lee. He was one of my PhD students and at the time he was also uh civil servant at NASA Ames. And we actually used it in part to help with the validation of different flavors of the ACAS X system. And uh since then a number of students have uh, since built a upon this this work. So, uh, recently we've been exploring how can we take some of these insights that we developed for the purpose of validating aircraft and bring it into the the world of validating language models. So, this is some of the work that my students, uh, Hujun Liu and, um, and, uh, Amelia Hardy and and others have been leading. So, with in the aircraft scenario, a failure is kind of well defined, right? It's metal on metal collision where they come within 500 ft horizontally and 100 ft vertically.

对于这些语言模型，我们关注的可能是毒性。那么，如何定义毒性呢？这就比较难以明确界定了。为此，我们实际上依赖另一个神经网络来提供衡量指标。在这篇论文中，我们使用 Llama Guard 来衡量毒性。现在，我们想找出最有可能发生的故障。在这些语言模型中，我们使用一种称为困惑度的指标。因此，我们希望困惑度尽可能低，或者说对数困惑度尽可能低，同时毒性尽可能高。也就是说，在搜索各种场景时，我们希望落在这里的左上角。如果最有可能发生的故障特别严重——如果我们把毒性超过某个阈值定义为故障，而这种情况确实很可能发生——那么我们就应该研究它，并采取一些缓解措施。For these language models, what we care about is, uh, potentially toxicity. So, how do you define that? That's a little bit more nebulous to define. And for that, we actually rely upon another neural network to to provide that measure. And for this, uh, for this paper, we were using Llama Guard to measure toxicity. Now, we want to find the most likely failure. And in these language models, we use something known as perplexity. So, we want something that's as low perplexity as possible or low log perplexity and as toxic as possible. So, we want to be up in in the top left corner here, uh, when we, uh, search the space of scenarios. And if the most likely failure is super, uh, if we define a failure as a toxicity above some threshold, if that's really likely, then we should study it and put in place some mitigations.

另一个挑战是估计失效概率。好吧，那里那个奇怪的符号应该是 E，表示期望。估计失效概率的一种方法是使用重要性采样，这个概念已经存在很久了。它的思路是，不从真实分布（我们称之为 P）中采样，而是从一个提议分布（我们称之为 Q）中采样，把采样重点放在更重要的情景上。不过之后你得对它们重新加权。重新加权其实相当简单：只要用真实模型下这条轨迹的概率，除以提议分布下这条轨迹的概率，作为权重即可。Another challenge is estimating the probability of failure. And, okay, that the weird, uh, symbol there should be an E. It's an expectation. One way to approach failure probability estimation is to use a important sampling, which is an idea that has been around for a super long time. The idea there is instead of sampling from the the true distribution, we'll call it P, you sample instead from a proposal distribution, we'll call it Q, that focuses the effort on on scenarios that that are more significant. But you have to then re-weight them. And the re-weighting is actually quite simple. You just weight it by the different results by the probability of your uh trajectory according to the true model divided by the probability of the trajectory according to your uh your proposal distribution.

我们已经将它应用于许多不同的领域。我们尝试引入高斯过程中的思想，来帮助表示这些分布。我们也研究了归一化流，以及使用低秩高斯混合模型来表示这些提议分布。我们还一直在使用扩散模型，它们在图像生成等其他领域已经取得了相当大的成功。 有时，我们关注的不只是最可能发生的故障，而是想对各种不同的故障模式进行分类。这里展示的只是两个非常简单的二维示例。上面的例子是一个倒立摆。你可以看到随时间变化的角度。如果摆角超过某个阈值，就会发生故障。实际上，摆可能向左倒，也可能向右倒。And we've applied it to a number of different uh domains. We've looked at um uh bringing ideas from Gaussian processes to help represent uh these distributions. We've also looked at uh normalizing flows, the use of low-rank Gaussian mixture models to represent these proposal distributions. Uh we've also been using uh diffusion models, which has um they have seen quite a bit of success in other domains like image generation. So, sometimes we don't just care about the most likely failure. Instead, we want to categorize all the different kinds of failure modes. And these are just two very simple two-dimensional examples. The top one is an inverted pendulum. And uh what you can see here is uh over time the angle. And we have a failure if if the pendulum uh exceeds an angle. So, in reality, it can fall over to the left or or to the right.

如果你能负担得起运行海量模拟，而且嗯，观察这些失败情况，那就能得到真实的故障分布。现在，如果你只使用常规的自适应压力测试，它通常会集中在其中一种故障模式上。而如果你使用这种基于扩散模型的故障采样，它实际上会捕捉到这两种故障场景。月球着陆器的情况也类似。If if you could afford to run a gazillion simulations and um and you look at the failures that that would be the the true failure distribution. Now, if you use just regular adaptive stress testing, it'll typically zero in on one of those failure modes. Whereas, if you use this uh diffusion-based failure sampling, it will actually pick on uh pick up on both of those uh failure scenarios. And similar kind of story for the lunar lander.

验证神经网络Verifying neural networks

嗯，我们也一直在研究神经网络验证。嗯，前些年，实际上是弗朗索瓦发起的一项工作，我们想看看能否用一些神经网络来近似 ACASX 碰撞规避系统的查找表，目的是压缩信息。当然，我们最终并没有在实际系统中使用神经网络，但这促成了我们与克拉克·巴雷特实验室一次非常有趣的合作，并推动了 Reluplex 算法以及后来的 Marabou 软件框架的开发。多年来，我们一直在逐步将 Reluplex 和 Marabou 应用于神经网络控制器处于控制环路中的场景。切尔西·西德雷恩和悉尼·卡茨等人的一些工作，也推动了这一方向的进展。Uh we've also been working on neural network verification. Uh so, uh a while ago, actually, some work initiated by Francois, um we wanted to see if we can approximate the lookup tables for the ACASX uh collision avoidance system. I just using some neural networks to to with with the idea of compressing the information. Now, of course, we we didn't actually end up using neural networks for the real system, but it led to a really fun collaboration with uh Clark Barrett's lab. And led to the development of the Reluplex algorithm and and later on the the Marabou uh software framework. And over the years, we've been uh transitioning the the use of Reluplex and and Marabou to situations where you have a neural network controller in the loop. And uh some of the work by uh Chelsea Sidrain and and Sydney Katz um um pushed some advances in in that direction.

然后，呃，一位学生 Sam——Clark 和我正在指导他——正在研究前向和后向可达性的概念。我们也一直在开展 POMDP 规划方面的工作。呃，实际上，我刚到斯坦福时，实验室最早开展的工作之一，就是创建一个非常简单的开源框架，用于描述 POMDP。我们希望让非专业人士也能轻松描述自己的 POMDP。这个想法有点像 CVXPY：Steven Boyd 的学生希望让人们能够轻松描述数学优化问题。我们希望用 POMDPs.jl 实现同样的目标。它是一个 Julia 库。呃，我的学生 Zach Sunberg（现在是科罗拉多大学博尔德分校的教授）开发了 POMCPow 算法，用于可扩展的 POMDP 规划。最近，我们也开始研究受约束的 POMDP。And then uh a student, Sam, who Clark and I are supervising, are looking at uh forward and backward reachability uh concepts. We've also been doing work on POMDP planning. Uh actually, one of our first efforts in the lab when I started at Stanford was to create a a very uh simple open source framework for specifying POMDPs. We wanted to make it really easy for non-experts to specify their their POMDPs. Kind of like for CVXPY, uh the idea of Steven Boyd's students was to make it really easy to specify mathematical optimization problems. So, that's what we wanted to do with POMDPs.jl. It's a a Julia library. And uh my student Zach Sunberg, who's now a professor at CU Boulder, uh developed the POMCPow algorithm for scalable POMDP planning. Uh we've more recently been looking at constrained POMDPs.

因此，你可能想对问题施加硬约束。我们也一直在探索涉及多个智能体的方向。以下是我们一直在研究的一些领域。嗯，医疗后送方面，我的学生巴迪·埃尔·侯赛尼·侯赛尼实际上是一名陆军黑鹰直升机医疗后送飞行员，他开发了一个用于模拟这类情景的框架。嗯，我看到邓肯一直在推动我们的工作，致力于将信念状态规划用于航天器碰撞规避。此外，我们还与海伦及其他人合作，利用 POMDP 来规划飞行测试，从而尽可能高效地表征飞机的飞行特性。好，这些工作主要侧重于系统部署前的验证。系统部署后，你也希望继续进行验证。So, you might want to impose a hard constraint on on your problem. And we have also been exploring directions involving multiple agents. These are some of the domains we've been looking at. Uh medical evacuation, my student Body El Husseini Husseini, he's actually a uh an Army Black Hawk uh medevac pilot, and uh he has developed a a framework for uh simulating these kinds of scenarios. Uh I saw Duncan, he's been uh pushing our efforts towards uh belief state planning for spacecraft collision avoidance. And also working with Helen and and others on using POMDPs to plan out uh flight tests so that you can as efficiently as possible uh characterize the flight characteristics of your aircraft. Okay, so that has largely focused on validation prior to deployment of your system. You also want to continue the validation effort after deployment.

好的，这有时被称为运行时监控或运行时保障。呃，你想验证输入到决策系统中的内容。所以，传感器输入方面，我们做过一些工作……Okay, and this is sometimes called runtime monitoring or runtime assurance. Uh you want to validate uh what's going into your decision system. So, the the sensor inputs, we've done some work with

运行时监控与 BetterBenchRuntime monitoring and BetterBench

空客在基于视觉的系统完整性监测方面的工作。呃，你还想监测系统内部正在发生什么。这促成了一些针对飞机系统开展的机制分析工作。当然，你也想对输出进行建模和监测。好，接下来还有另一类工作，关注如何评估测量结果。安卡·鲁苏（Anca Rusu）等人一直在推动 AI 评估的前沿。我们发布了论文《BetterBench》。访问 betterbench.stanford.edu，就能找到关于多个不同基准的所有数据，以及从中总结出的经验教训和最佳实践。我们也一直在研究这些基准什么时候会失去效用，什么时候会出现饱和。我们还在研究这些失败表现出什么样的特征，比如 token 级特征和推理失败。Airbus on integrity monitoring of vision-based systems. Uh you also want to monitor what is happening in the internals of of the system. And this has led to some work on uh mechanistic analysis uh for an aircraft system. And of course, you also want to model uh and monitor the outputs. Okay, then there's a another uh set of work on assessing the measurements. So, uh Anca Rusu and and others have been uh pushing the the frontier on AI evaluation. Um uh we released the paper BetterBench. If you go to betterbench.stanford.edu, you can find uh all of the data about a number of different benchmarks uh and uh a number of lessons learned and best practices there. Uh we've also been studying when do these benchmarks stop being useful? When do we have these uh saturations in these benchmarks? Uh we've also been looking at what What do these failures look like um in terms of token-level signatures, uh reasoning failures.

我们还研究了人类评审者方面的问题。事实上，另一个安全关键领域是将 AI 用于心理健康。我们一直在评估心理健康专业人士。令我们颇感意外的是，我们发现心理健康专业人士的意见差异很大，包括在涉及自残的领域。好了，我就讲到这里，最后简单介绍一下我们的新三部曲。第一本是《优化算法》，第二版将于 2027 年初很早的时候出版。优化是我们在这里所做一切的基础，也是优化决策所依据的基础；这方面的内容收录在我们 2022 年出版的《决策算法》一书中。我对这本新书《验证算法》特别期待，目前已经开放预售。And we've also been looking at issues of uh human judges. So, in fact, another safety-critical area is the use of AI for mental health. And we've been looking at evaluations of mental health professionals. And we have been actually quite surprised to find that um human mental health professionals actually their opinions vary widely uh including in in domains related to uh self-harm. All right, I'll wrap it up here just mentioning our new trilogy uh So, the the first book is Algorithms for Optimization. The the second edition will come out in uh very early 2027. Uh optimization is fundamental to everything that that we do here. Um and it's a basis upon which we optimize decisions and that's covered in our 2022 Algorithms for Decision Making book. I'm super excited about this new book Algorithms for Validation, which is available for pre-order.

它下个月就要出版了。这本书试图全面讲述如何验证具备学习能力的系统以及其他类型的 AI 系统。嗯，这本书可以在亚马逊上买到，后来发现 Target.com 上也有。现在你已经可以在网上找到这本书的 PDF。书中既包括我刚才提到的统计方法，也包括形式化方法和可达性分析方法。通常，这些方法分别属于不同的社群，但我们尝试用一种共同的语言将它们统一起来。我的分享就到这里，谢谢大家。It's coming out next month. And it tries to provide a comprehensive story about how to go about validating uh learning-enabled systems and and other kinds of uh AI systems. Um it's available from Amazon and also turns out target.com. Uh you can find the PDF of the book online right now. And it includes both the statistical methods that I mentioned here as well as formal methods and reachability methods as well. Normally, these are treated as separate communities, but we tried to unify everything into a common language. And I'll wrap it up here. Thanks.

小组讨论：回顾过去三周的情况Panel: reacting to the past three weeks

嘉宾：好的。非常感谢大家。太棒了。嗯，那我想我们就从这场对话的开头说起吧。你们也看到了这一整套人工智能安全相关的事。你们看到最近这场歇斯底里的风波时，心里在想什么？要不我们先从克拉克开始。Guest: Okay. Thank you guys so much. That was amazing. Um So, I guess really to start the conversation uh you know, you guys saw this whole AI safety stuff. You know, what what was going through your mind when you saw this latest uh uh hysteria um saga going on? Maybe let's start with Clark.

主持人：所以，所以我并不惊讶，因为我跟 AI 安全领域的极客们打交道已经有一段时间了，其中有不少人早就在这么说了。嗯，你知道，我的回应一直是，未来存在很大的不确定性，尤其是现在。所以，投资 AI 安全研究是个好主意。嗯，但我也觉得，在你根本不知道实际概率是多少的情况下，强调最坏的结果并没有多大帮助。嗯，而且，你知道，我觉得任何人如果说“我知道这一定会发生”，或者“你知道，这似乎肯定会发生”，那都只是在猜测。就这样。Host: So So, I was not surprised because I've been hanging out with AI safety geeks for a while, and there's a good chunk of them that have been saying this for a while. And um you know, I think my response has always been the future is has high uncertainty, especially now. And so, it's a good idea to invest in AI safety research. Um but I also think it's not super helpful to emphasize like worst-case outcomes when you have no idea what the real probabilities are. Um and uh you know, any I think anyone who says, "I know that this is going to happen." or, "You know, it seems certain this is going to happen." They're They're just guessing. So.

嘉宾：呃，我们俩都关注 AI 安全有一段时间了。我想我们创办 AI 安全中心是在 2018 年，还是 2017 年？能看到它引起了国际关注，真是很有意思。呃，我希望这能让大家更加认真地看待安全问题。我觉、我、我觉得我们需要从航空航天业借鉴更多理念。我可以详细谈谈这个……好吧，行，我来谈。呃，请说。Guest: Uh we've both both cared about AI safety for some time. I think we started the Center for AI safety was a 2018, 2017? And uh it's fascinating to see that it has captured international attention. And uh I hope that this will uh lead to taking safety more seriously. I kind I I think that we need to borrow more ideas from the aerospace industry. And I can elaborate on uh Okay, fine, I will. Uh Please do.

主持人：确实，确实，确实有人讨论过为人工智能设立类似 NTSB 的机构，我觉得这实际上可能是个好主意。嗯，所以，与 20 世纪 70 年代相比，如今商业航空的安全性提高了 80 倍。Host: There There There has actually been some discussion of creating something like the NTSB uh for AI, and I think that could actually be a a good idea. Um So, compared to the 1970s, we're 80 times safer uh in commercial aviation uh

AI 领域的 NTSBAn NTSB for AI

比我们现在更安全。自霍华德·休斯时期，呃，或者说自20世纪70年代以来。从20世纪70年代到现在，我们的安全性提高了80倍。那我们是怎么做到的？所以……than we are. Since Howard Hughes or uh since the 1970s. 1970s to now, we're 80 times safer. And how did how did we get there? So

嘉宾：那它会是什么样子？它会是什么？会是什么样子？它会是什么样子？会是类似自愿加入的机制吗？会是一些指导方针吗？会像 FDA 直接审批数据那样严格吗？它会如何运作？Guest: And what what would it what would it what would it look like? What would it be Would it be like an opt-in kind of thing? Would it be like guidelines Would it be strict like the FDA literally approving data? How would it work?

主持人：呃，这是个好问题。我认为这里的关键是独立性。NTSB 于 1967 年成立，是一个独立机构。后来还设立了其他航空安全报告系统，比如 ASRS，它是一个非惩罚性的报告系统。这激励了所有制造商和航空公司共享安全信息，认真对待每一起事故，并从事故原因中尽可能汲取科学知识。如今，还有其他一些制度是在此基础上发展起来的。2007 年左右，也有一个航空安全信息分析与报告系统，或者类似这样的系统，其中也包含某种形式的豁免。我认为我们需要采取类似的做法。建立一个新的机构会需要很长时间，可能太久了。Host: Uh that that's a good question. So the the key thing here I think is independent. So NTSB was set up as an independent agency in 1967. And uh there were put in place other aviation safety reporting systems like ASRS and that was a non-punitive reporting system. So that incentivized all the manufacturers, the airlines to share safety information. And to really take every single accident seriously and draw as much scientific knowledge from from what went wrong. Now it take that there are other systems that uh were schemes that have built upon this. In 2007, there there was also the uh aviation safety information analysis and reporting system or something like that that also had some form of immunity. And I think we need to do something like that. It's it's going to take a long maybe uh too long of a time to set up a new agency.

这可是件大事。呃，政府机构往往效率不高。嗯，NTSB 也在全球范围内开展工作。嗯，如果事故涉及在美国制造的部件，他们实际上会前往其他国家进行调查。嗯。That's that's a big deal. Uh governments tend to be somewhat inefficient. Um the NTSB is also used globally. Um so if an accident involves a component manufactured in in the United States, they'll actually go go to other countries and investigate. Um

嘉宾：之所以打这个比方，是因为这里的风险很高，嗯，利益相关方也非常多。存在监管俘获之类的风险。你看医学领域，或者法律领域，都有医学委员会。就连互联网也有 ICANN，对吧？它也是国际性的、自我监管的。DNS 一直运行得很好。嗯，不过事情并非如此：想象一下，如果互联网发明的时间，恰好是 Google 和 Facebook 已经成为上市公司，而且它们在 ICANN 的发展过程中有很大影响力的时候。也许它们会说：“嗯，如果你想要 SSL，那就得由 Google 或 Facebook 来给你颁发 SSL 证书。或者你想要一个域名？那其实不能安全地把域名发给所有人。”Guest: To draw that analogy because it's such a high um hm there's so much interested parties. There is risk of regulatory capture and things like that. And then like, you know, if you look at uh medicine or you look at legal, there's the aboard of medicine. Even the internet has ICANN, right? It which is also international, self-regulated. DNS has been working great. Um and there hasn't but like it wasn't the case that, you know, imagine the internet invent was invented that same time that Google and Facebook were like already public companies and they were heavily biased in the development of ICANN. And maybe they said, "Hm, well, if you want SSL, you actually need um Google or Facebook to be the ones to give you SSL certs. Or you want a domain name, well, you really it's not safe to give everyone domain names.

“就像是我们应该成为给你提供域名的人。”所以，这里面确实有一些风险。再进一步说，政府干预还会带来一个问题，就是所谓的监管俘获。就拿现在来说吧，如果你想创办 Uber 或 Lyft，在法律上是行不通的。Uber、Lyft、DoorDash 和 Instacart 都凭借 1099 身份获得了祖父条款保护。所以，实际上你根本没法竞——没法竞争，对吧？这就是有些人担心的地方。你怎么看这些问题？我想，或许先从 Clark 开始。Like we we should be the ones to give you domain names." So, there's some risk there. And then even more so like um having government intervention, there's uh uh this idea of regulatory capture, which today, right now, if you want to start Uber or Lyft, you can't legally. Uber, Lyft, DoorDash, Instacart are grandfathered in on 1099. So, you actually can't com- compete. Right? And that's the concern that some people have. How do you think about all that stuff? I Maybe start with Clark.

主持人：嗯，是的，所以，呃，最近前沿实验室的负责人说“是的，我们需要独立评估方”，这让我受到了鼓舞。所以，我想说，我公司的目标之一就是打造能够充当这种独立评估方的系统。而且，不只是找一个人说“哦，我们是独立的，所以你们相信我们就行了”。我们的目标实际上是出具可独立核验的证书。也就是说，我们会说：“好了，我们已经检查过这个系统了，这是证书。现在你们可以自己去检查，并确认我们做得对不对。”所以我认为，独立性真的非常重要。我觉得有很多人在推动这件事，因为我认为，如果所有安全工作都交由实验室，甚至交由一些自称独立的实验室友人来负责，那实在太可惜了。Host: Uh yeah, so uh I I was encouraged, you know, by the recent um Frontier Lab leaders saying, "Yeah, we need independent evaluators." So, I'll just say one one of the goals of my company is to build systems that can be that independent evaluator. And not just not just someone that says, "Oh, well, we're independent, so take our word for it." Our goal is actually to produce independently checkable certificates. So, we would say, "All right, we've checked this system, and here's the certificate. You can now go check it yourself, and you can confirm uh that we got that right." So, I I think uh independence is really important. Um I I I there a lot of voices pushing for that because I think it would be uh you know a real shame if all of the safety was left in the hands of the labs or or even some um some friends of the labs who claim they're independent.

是的。Yeah.

嘉宾：是的，我我我觉得，在那种机制建立起来之前，我们近期需要先有个什么安排。它可以是非营利组织之类的。我的意思是，在航天产业里，进行太空发射时，对吧？会有一位完全独立于任务团队的发射场安全官。他唯一的职责，就是根据客观的安全指标，做出是否放行的决定。Guest: Yeah, I I I think we need something in the very near term before something like that could could be set up. It could be a not-for-profit or or something like that. I mean, in in the space industry, when you have a space launch, right? You have a range safety officer who's completely independent of the the mission. Their only job is to make a go no go go call based on objective safety metrics.

主持人：有没有可能把起点设得很简单，比如只采用美国 GAAP，也就是美国那种——呃，嗯，那个——会计原则，呃，公认会计原则？也可以是关于部署 AI 安全的公认 AI 原则。嗯，然后还有毕马威，还有，呃，你知道，呃，嗯，安达信，或者你知道，随便什么。就像，你知道，呃，安永之类的，你可以选择，但在你做某件事之前，必须先经过验证。比如，不应该什么都被限制。我还是应该能在我那个，你知道，小盒子上训练 theta。Host: Could it be as simple as a starting position as just US GAAP, which is like the US kind of the the uh um uh accounting principles uh generally accepted accounting principles? It could be generally accepted AI principles of like deploying AI safety. Um and then there's a KPMG and there's a uh you know, uh um Arthur Andersen or you know, whatever. That's like, you know, uh uh Ernst & Young that's going to be that you can choose, but you have to be validated um before you do something. Like, it shouldn't be everything. I should still be able to train the theta on my, you know, tiny box.

嘉宾：是的，我我我我认为我们需要制定最佳实践，呃，当然，但我觉得我们也需要进行事后复盘分析。我认为我们需要从多个不同角度认真对待 AI 验证。Guest: Yeah, I I I I I think we need to develop, you know, best practices, uh of course, but I think we also need like a postmortem analysis as well. I think we we need to take the validation of AI seriously from a number of different perspectives.

主持人：不过，回到你刚才的观点，我是说，我觉得，嗯，呃，航空业在这方面做得真的非常非常好。他们不会急着把事故经过公之于众。他们会……每发生一起事故，都会进行全面彻底的审查。对吧？Host: But, back to your point, I mean, I think um uh aircraft the airline industry does that really really well. They don't rush to print what happened. They do a They have a full thorough review process of every single accident that happens. Right?

嘉宾：你们有什么……嗯，好吧。那我给你们两位的最后一个问题是，你们真的认为目前这些 AI 安全方面的担忧有多容易解决？具体来说，也许是网络防御问题、某些生物武器问题，还有网络攻击方面的问题：模型可能让我用 OpenAI 发起网络攻击，或者我可以想办法诱使它这么做；或者我可以拿一个开放权重模型来用，然后我还需要一些我们之前谈到过的防御能力。嗯，你们觉得整个问题有多容易解决？Guest: Do you have any Um okay. So, uh my last question for the both of you is how tractable do you really believe these current AI safety um concerns to be? Specifically, maybe the cyber uh defense issue, some of the bioweapon issue, on the cyber offense stuff where the models I can use a open AI to make a you know, a cyber attack, or I can use I can trick it to to doing so, or I can um take an open weight model, and then I I I would need some defensive capabilities as we talked about earlier. Um how the whole thing, how do you think how tractable of a problem is is this?

网络安全能否在五年内得到解决？Is cybersecurity solvable in five years

主持人：是啊，我来试着回答一下。我觉得，嗯，网络安全会变得非常容易处理。我想，呃，就像现在，我跟我妈妈说：“嘿，只要证明代码正确，它就不可能被黑。”她听了简直惊呆了，说：“真的吗？”你知道，媒体和电视让我们觉得，所有系统都能被黑。当然，现在确实是这样。不过，呃，要用数学上的确定性证明一个系统不可能被黑，是完全有可能的。我预测，未来三到五年内，我觉得，这种情况就会实现。也就是说，我们所有的系统都会变得完全安全。因为人工智能既能发动攻击，也能进行防御。而人工智能防御结合形式化方法，应该能让我们实现这一点。Host: Yeah, I'll take a stab at that. So, I I think um cybersecurity is going to become very tractable. I think uh like right now, you know, I was telling my mother, um "Hey, if you prove the code, it can't be hacked." And she was just stunned, like, "Really?" You know, we're trained by the media and by television that like every system can be hacked. And well, of course, it is true right now. But uh it's quite possible, you know, you can prove with mathematical certainty that that you can't hack a system. And I I I will predict that within the next, I would say, 3 to 5 years, um that'll just happen. Like, all our systems will be completely secure. Because it it with AI can attack, but AI can also defend. And and the AI defense plus formal methods should get us there.

主持人：那么，那么要实现这一点需要什么？要采用这些封锁系统吗？这类似零信任架构吗？类似这些最佳实践——甚至管理员、管理员权限的问题？嗯，你怎么看？Host: So, what what is needed to get us there? To to have these lockdown systems? Is it like zero trust architectures? Is it like these best prac- even the admin admin issue? Um how do you think about it?

嘉宾：是啊，我的意思是，我觉得我们只需要转向一种新的代码标准。其实，你提到航空公司和其他行业如何运用非常扎实的工程原则，这还挺有意思的。我喜欢说，软件工程有个不太光彩的小秘密：它并不是建立在扎实的工程原则之上，而更像是随便写点东西、测试一下，然后祈祷一切顺利。不过，我们其实知道该怎么做。我的意思是，软件工程是有数学基础的。我想我们可能得朝这个方向看看。还有一点我想说的是，关于让 AI 本身变得可保障这件事是否可行，我不认为我们能推理这些庞大的大型语言模型。所以我认为，最好的选择可能是更像保障边界安全的做法。Guest: Yeah, I mean, I think we just need to move to a new standard of code. Actually, it's interesting you're bringing up uh how how airlines and and other industries use, you know, very sound engineering principles. Uh I like to say there's a little dirty secret about software engineering, which is it's not based on sound engineering principles, it's based on like, just write something and test it and hope for the best. Uh but we actually do know how to do that. I mean, there is a mathematical foundation for software engineering. I think we'll have to see uh maybe to that. And And one other thing I want to say in terms of tractability of like securing AI itself, uh I don't think we'll be able to reason about, you know, these massive large language models. So, I think our best uh option is something more like securing the boundaries.

嗯，而且确保边界安全也相当可行。嗯，试图证明一个拥有 5000 亿参数的模型不会做出什么疯狂的事——我觉得这并不太可行。Uh And securing the boundaries is also very tractable. Um trying to prove that, you know, a 500 billion parameter model isn't going to do something crazy, uh I think that's that's not really tractable.

主持人：我完全同意Clark关于安全问题的看法。比如说，我很害怕，嗯，你知道，接下来会发生一件大事——一场大规模网络攻击。不过我想，我同意Clark的看法，对此我抱有很大希望。嗯，但你无法证明生物学或化学领域什么是可能的、什么是不可能的，对吧？呃，这是一个尚无定论的问题。但我认为，作为一个物种，我们一直在努力追求的是更深入的理解。我认为，AI的进步平均而言会对我们有所帮助。总体来说，我认为我们会从这些新见解中受益。Host: Completely agree with Clark on the security thing. Like, I'm terrified of um you know, the next big thing being a massive cyber attack. And but I think I I would agree with Clark that I have a lot of hope for that. Um but you can't prove what's possible or what's not possible with biology or chemistry, right? Uh that is uh that's an open question. But I think that's what we have been striving for as a species, where increased understanding. And I think that advances in AI will help us um on average. I think on average we're going to benefit from these new insights.

如果你是美国银行的首席信息安全官（CISO）If you were CISO of Bank of America

嘉宾：嗯，我有个问题想专门问问克拉克。嗯，具体给我讲讲这事是怎么运作的。假设现在我们给你100亿美元，让你去美国银行担任首席信息安全官。好，他们会怎么做？你会怎么做？Guest: Um I have a question specifically for um Clark here. So, um exactly walk me through how it works. Let's say that um you are now uh we give you $10 billion to be the CISO for Bank of America. Okay. What do they do? What's What would you do?

主持人：好。那么，首先我会聘用所有正规的人员，然后，呃，争分夺秒地搭建我们所需的基础设施，以便对那些代码进行推理。接着我会说：“好，把你们所有的代码都给我。呃，给我一大堆 GPU，再配上一大堆定理证明智能体，我们就可以，要么直接证明现有代码，要么把它翻译成更好的语言，比如 Rust 或 Lean，然后在那里证明代码。这样，呃，就大功告成了。所以，这方面还有很多工作要做，但我认为，呃，这是我们知道该怎么做的工作。”Host: Okay. So, first I would hire all the formal people and uh race race to build uh the infrastructure that we need to reason about that code. Then I would say, "Okay, give me all of your code. Uh uh, give me a whole bunch of GPUs and a whole bunch of theorem proving agents and we're going to just, um, either prove the code as it is or we could also just translate it into a better language like Rust or Lean, prove the code there and, um, and then you're done. So, there there's a lot of work to do there, but I think it's, uh, it's work that we know how to do.

主持人：这是不是意味着我终于得把单元测试覆盖率提高到 100%？这到底是什么意思？Host: And does that mean I have to finally get to 100% unit test coverage? Is that Is that what that means?

嘉宾：不，并非如此。你，呃，所以测试实际上会变得过时。我的意思是，测试……在开发过程中，测试总是有益的。它们是发现 bug 最快的方式。呃，但归根结底，形式化论证完全涵盖了测试。Guest: No, you don't. You, uh, so tests actually become obsolete. I mean, tests are Tests are always good as you're developing. They're like the fastest way to find bugs. Uh, but ultimately the formal argument completely subsumes the tests.

主持人：嗯，好吧。现在，迈克尔，嗯，你了解 Waymo 吗？嗯，你知道，呃，呃，一些……Host: Um, all right. Now, for Michael, um, are you aware of Waymo, um, you know, uh, uh, some of the the

嘉宾：是的。Guest: Yes.

主持人：我的不少学生在那里工作。Host: A number of my students work there.

嘉宾：下一个问题。不。Guest: Next question. No.

主持人：嗯，使用 AST 差异，这是一些重要的采样内容。嗯，你知道 Marabou、Reluplex 吗？你知道他们在训练出一个新模型之后，会在验证和 θ 验证流程中使用这些方法吗？Host: Um, using, uh, AST diffs, uh, this is some of the important sampling stuff, uh, you know, Marabou, Reluplex. Are you aware that they're using this in their validation and and their their theta validation procedures after they train a new a new model?

嘉宾：呃，我不能具体谈 Reluplex 或 Marabou。呃，Clark 可能对此有些见解，不过我们发布的自适应压力测试不仅有 Julia 版本，也有 Python 版本，供那些想继续使用过时语言的人使用，但是】【。Guest: Uh, I can't speak specifically about Reluplex or Marabou. Uh, Clark might have some insights there, but adaptive stress testing we released not just a Julia version, but also a Python versions for those who want to continue using obsolete languages, but

主持人：嗯，所以我们把它开放出来了。我们的实验室有不少赞助方。我们得到了多家汽车制造商非常慷慨的支持，其中包括 Waymo。嗯，目的是让这些工具不仅对他们开放，也能让整个行业都用得上。Host: um, so we we we made it open. We've had, uh, a number of sponsors of our lab. We we've been, uh, supported by very generously by a number of different automotive manufacturers including Waymo. Um, with the aim to, um, uh, make these tools accessible not just to them, but to the entire industry.

主持人：然后我、我……你提到了 AST Prompter，这些同样适用于 LLM，就像适用于经过训练、能够控制油门和方向盘的 VAT 一样，对吧？Host: And I I And you talked about AST Prompter, these are applicable to LLMs as just as they are to a trained VAT that would control a gas pedal and a steering wheel, right?

嘉宾：是的，基本上你需要两个……要使用自适应压力测试，你需要两样东西。你需要定义什么是故障，还需要一个可能性度量。而这两者你都可以具备。这适用于语言模型、飞机防撞系统。Guest: Yeah, basically you need two You need two things to use adaptive stress testing. You need a definition of a failure and you need a measure of likelihood. And you can have both This works for language models, aircraft collision avoidance systems.

主持人：那么，你……你在这些话题上从 Anthropic、OpenAI 和 Grok 获得的互动，和从 Waymo 及自动驾驶汽车行业获得的一样多吗？Host: And are you Do you have as much engagement from Anthropic and OpenAI and Grok on those topics as you do as Waymo and the autonomous vehicle sector?

嘉宾：还没有。我的意思是，我们刚刚发布了 AST Prompter。我们得到了 Schmidt Sciences 的支持。我们的想法是尽可能让所有这些理念都更容易被人们接触和理解。Guest: Not yet. I mean, we we just published AST Prompter. We've been supported by the Schmidt Sciences. And the idea is to make all these ideas as accessible as possible.

主持人：你觉得他们采用这种技术后，安全水平能和 Waymo 之类的公司一样吗？嗯，我不知道。希望验证物理系统和验证语言模型是两码事。不过，方法或许可以互通，但预期的成功程度可能会有所不同。Host: And do you think that they did adopt they would have equal levels of safety as the Waymos and and things like that? Um I don't know. Uh hopefully that it's it's a different thing validating physical systems than you know, language models. Although the methods can translate, the level of success that you can anticipate might vary a bit.

嘉宾：我的意思是，我听过一些观点，说，嗯，自动驾驶的失效模式其实我们可以界定得相当清楚，比如车一直在路上行驶，如果它撞上了婴儿，或者发生这类事情。而且后来我见了 Lane McIntosh，和他一起待了一会儿，他给我看了一些例子，说明特斯拉汽车实际上是如何应对并化险为夷、没有做出坏事的，而这些情况远远超出了分布范围。这是一种在任何合理的情境下都不会受到监测或采样的失效模式。你知道，总会有长尾，对吧？而且长尾中的一些情况总是会有很高的概率。嗯，然后他们就说：“那么，在这些……所以对于 LLM 来说，你知道，我们能不能说情况也差不多？这是不是同一种长尾？它们的长尾有实质性的区别吗？”Guest: I mean, I've heard arguments that well, um autonomy you know, we can define the failure modes pretty well if the thing stays on the on the road, if it you know, if it hits a baby and this and that. And like and then I meet I I hang out with Lane McIntosh and he shows me examples of what the Tesla car actually subverted and survived and didn't do the bad thing and it was well outside the distribution. It was a failure mode that was not monitored or sampled in any reasonable world. You could have There's always a long tail, right? And some of the long tail is a is always going to be a high probability. Um and and then they say, "Well, in in these And so in the LLMs, you know, can't we kind of isn't it kind of that same Is is there Is it meaningfully different long tail?"

主持人：是的。我我我觉得你说得完全正确。所以，即便对于 A cast X，我们也知道失败的概率并非为零。Host: Yes. I I I think you're exactly right. So, I even for A cast X, we know that the probability is of failure is not zero.

嘉宾：嗯。Guest: Mhm.

主持人：我的意思是，我们有模拟结果表明，它在某些情况下会失效。只不过那些情况发生的可能性实在是微乎其微。也就是说，国际民用航空组织和美国联邦航空管理局的安全标准，并不是要求事故发生的概率为零，对吧？Host: I mean, we have simulations that show that it fails in certain situations. It's just that those situations are just so incredibly unlikely. That That I mean, the International Civil Aviation Organization and the Federal Aviation Administration, their their standard for safety is not probability of zero probability being zero, right?

嘉宾：对。Guest: Right.

主持人：呃，我们得现实一点。如果有人告诉你，他们已经创建了一个与现实世界互动、完全安全的系统，嗯，而且它绝对安全，那我……我可不会相信。Host: Uh we have to be realistic. If anyone tells you they have created a a completely safe system that interacts with the in the real world, um and it's fully safe, yeah, I I I would would not believe that.

嘉宾：克拉克给我们做了一些保证。Guest: Clark's got some guarantees for us.

主持人：嗯，Clark 有一些保证。嗯，要使用 Clark 的方法，或者说用于形式化方法的一类方法，呃，如果我没说错的话，你得针对某个模型来做这些证明，对吧？如果你是在对现实世界建模，就必须把可能发生情况中的不确定性纳入模型，比如飞机的加速度之类的。所以通常你必须假设这种不确定性的范围。Host: Uh Clark has some guarantees. Uh so, to use Clark's method and or category of of methods for formal methods, um and correct me if I'm wrong here, but you have to it you're 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 or whatever. And so, you generally have to assume bounds on that uncertainty.

嘉宾：所以，你必须估计输入的名义分布，估计接下来会发生什么，以及……的转移函数。Guest: So, you have to estimate a nominal distribution on the input, on what's going to and on the transition function of

主持人：所以，在形式化方法中，你通常不会对概率分布作任何假设。你用集合来表示不确定性。Host: So, in formal methods, you generally don't assume anything about probability distributions. You capture your uncertainty in in sets.

嘉宾：对。好的。Guest: Right. Okay.

主持人：而且，而且这是一种不同的方法，奏效时确实很棒，对吧？因为你能得到一个很漂亮的证明。而且，这很棒。但问题是，这些不确定性区间是否足够贴近现实？Host: And and that that's a different approach and it's great when it works, right? Because you get a nice proof. And and that that's wonderful. But the the question then is do those uncertainty intervals um are they sufficiently realistic?

嘉宾：就这个说几句吧。所以，嗯，是的，证明总是基于某些假设，对吧？有些情况下，你可以做出合理的假设，并给出强有力的保证。我觉得迈克尔想说的是，如果你知道，你的输入就像现实世界中的另一个行动者，而你假设那个行动者不会试图用他们的飞机撞你，Guest: 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 that actor is not going to try to hit you with their airplane,

主持人：那么，呃，这可能不是一个有效的假设，对吧？所以，呃，当我们讨论安全性或形式化保证时，真正重要的是要明白，这些保证都是基于某些假设的。当然，有些事情你可以百分之百保证，对吧？如果我证明我的代码是内存安全的，那么你就绝对不可能通过缓冲区溢出攻击来攻击这段代码。Host: 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.

客人：是的。Guest: Yeah.

主持人：呃，不过还有其他一些事情，是形式化方法能力有限、做不到的，对吧？我是说，呃，我们之前做神经网络验证工作时，人们会问我们：“那么，你们要怎么验证这个感知网络能正确识别猫和狗呢？”我当时就想：“嗯，我甚至不知道该如何对猫和狗进行形式化描述，所以这超出了形式化方法的能力范围。”所以，确实有局限。你必须意识到这一点。我觉得形式化方法领域也确实从中吸取了惨痛教训：必须把这些假设说清楚，否则人们就会失望。Host: 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 going to verify that this perception network correctly identifies cats and dogs?" And I was like, "Well, I don't even know how to formally specify a cat and dog, so that's beyond what formal can do." So, so there are limits. You have to be aware of that. That's something that I think the formal community has also really learned uh hard lessons that you have to state those assumptions or else people will be disappointed.

主持人：嗯，那么，我最后一个问题，嗯，什么是瑞士奶酪模型？你们是在做烤奶酪三明治之类的吗？那是什么？Host: Um so, last question for me, um what's the Swiss cheese model? Are you making like grilled cheese sandwiches or something? What's What's that?

瑞士奶酪模型The Swiss cheese model

嘉宾：所以，呃，我们在航空安全中会用瑞士奶酪模型来打比方，对吧？我们有多个防御层。比如说飞机防撞，对吧？嗯，最上面一层可能是战略间隔，对吧？根据你是向西飞还是向东飞，你会飞在不同的高度层。然后，另外一层可能是空中交通管制。嗯，再一层可能就是你的防撞系统。我们之所以称之为瑞士奶酪，是因为这些不同的层各有各的薄弱之处，对吧？那些就是奶酪上的孔洞。我们要做的就是确保这些孔洞不会对齐。明白吗？我们不希望关键情景一路穿过奶酪的所有层。Guest: So, uh we use the Swiss cheese model as an analogy in aviation safety, right? You have a number of layers of defense. So, like for aircraft collision avoidance, right? Um maybe the top layer is like strategic separation, right? Depending on whether you're flying west or east, you fly at different altitude layers. And then you then you have another layer, which might be air traffic control. Um and then another layer could be your collision avoidance system. And we call it Swiss cheese because these different layers have different vulnerabilities, right? Those are the the holes in the cheese. And what we want to do is make sure that the holes don't line up. Okay? You don't want a critical scenario to make its way through all the layers of of the cheese.

主持人：而且，那么把这个应用到这些又大又吓人的大型语言模型上，我的意思是，我们可以控制训练数据、预训练、RLHF、RSI，以及所有正在采样的数据。我们可以把坏数据剔除。比如，Percy现在就在这么做：他用一个小模型检查预训练数据，把其中不好的内容剔除。好吧？这样一来，那些内容就永远不会出现在预训练数据里，所以模型根本不可能学到那些坏东西。然后你……这就像是第一步。现在，你有了经过训练的数据。我们来对这些数据做一次失败分析。好吧，我们来估算失败情况。我们来抽样看看失败案例。我们来估算一下各种失败模式。我们来得出一个 P fail，我觉得吧，这个说法营销效果不好。我们来得出一个 1 减 P fail，也就是 P success。Host: And and is so then applying this to these [clears throat] big large language models that are big and scary, I mean we control the training data, pre-train the RLHF, the RSI, all the data that's being sampled. We can take out the bad data. We can run So, like Percy Percy's doing this right now, where he's running a small little model to look over the pre-train data to take out bad stuff out of the pre-train. Okay? Then it's that stuff's never in the pre-train, so it can't possibly learn those bad things. And then you So, that's like step number one. Now, you have a trained data. Let's do a failure analysis on that data. Okay, let's estimate failures. Let's let's sample some failures. Let's estimate some failure modes. Let's get to a P fail, which I think, you know, bad marketing. Let's get to one minus P fail, which is P success.

然后是工具，再到运行时监控，对吧？你之前提到过这一点，而且它也确实会发生。嗯，你对此有什么看法？And then tools, and then all the way to runtime monitoring, right? Which you mentioned earlier and happens as well. Um yeah, what are your thoughts on that?

嘉宾：是的，你需要所有这些层面的防护。嗯，我觉得你在开场发言中举的例子里，他们把思维链监控器关掉了，对吧？这就是其中一个层面。我觉得，除了开发克拉克和我一直在研究的这些技术工具，我们还需要确保在人为层面设置适当的防护措施，对吧？嗯，我的意思是，我们从网络安全领域学到了这一点，对吧？入侵系统的一种常见方式就是通过社会工程学。Guest: Yeah, you you need all these layers. Um I I think the example you gave in your opening remarks, they had like the chain of thought monitor turned off, right? That that would be one of those layers. And I I think in addition to developing these technical tools that Clark and I have been working on, we also need to make sure we put in the the proper safeguards on the human level, right? Um So, like I mean, we've learned this from cybersecurity, right? A way to the typical way of breaking into a system is through human engineering.

主持人：对。Host: Yep.

嘉宾：对。太棒了。好，现在我把时间交给现场观众。嗯，好，前排这位。Guest: Yep. Awesome. Okay, I'll open up to the audience now. Um okay, in the front.

主持人：[嗤笑声]Host: [snorts]

嘉宾：迈克也要来了。Guest: And we got Mike coming.

观众问答Audience Q&A

主持人：嗯，我是说，这个问题是问 Clark 的。你提到，在美国银行这样的例子中，大多数时候，价格代码和现实世界中的代码不一定有规范。那么，在这种情况下，你会如何形式化地验证这段代码？你会从源代码本身获取规范或假设吗？还是会怎么做？Host: Um I mean, this this question is for Clark. So, you mentioned that um you know, in a Bank of America like uh example I mean, most of the time, you know, then the price code and the real world code doesn't necessarily have a specification. So, in that case, like how would you um formally verify this code? Would you you know, get the I don't know, like spec or a assumption assumptions from the the source code itself or how would you do that?

嘉宾：是的，这是个很好的问题。我觉得，在这个能轻松编写代码、而且希望未来几年内也能轻松验证代码的新世界里，剩下最难的事情就是编写规范。不过，有很多事情都可以做。首先，这里有一个从易到难的范围。有些规范既简单又通用，对吧？比如说，如果我有 C 代码，我希望它是内存安全的，对吧？我可以一劳永逸地写好这条规范，然后直接说，每个人都应该证明自己的代码符合这条规范。嗯，至于……Guest: Yeah, that's a great question. So, I think uh in the new world where it's easy to write code and hopefully in the next couple years it's easy to verify code, the thing that's left that's hard is the specification. But uh there are a lot of things you can do. So, first of all, there's a spectrum. Some specifications are easy and universal, right? So, if I have C code, I would like it to be memory safe. Right? I can write that specification once and for all and just say everybody should, you know, prove this is correct for their code. Um and for

主持人：对于观众来说，内存安全是什么意思？这为什么重要？Host: the audience, what does it what does a memory safe mean and why is that important?

嘉宾：对，对。所以，这只是意味着你的代码永远不可能访问未初始化或越界的内存。Guest: Yeah, yeah. So, that just just means that it's never possible for your code to access uninitialized or out of bounds memory.

主持人：谁在乎那个？Host: Who cares about that?

嘉宾：嗯，如果你能做到这一点，很可能就能发起某种缓冲区溢出攻击。你知道，缓冲区溢出攻击早就被广泛用于获取各种系统的访问权限了。事实上，我记得缓冲区溢出仍然不幸地位居安全漏洞榜首。嗯，对，所以有一些这样的规范。还有一些领域特定的规范，比如对于银行来说，我想他们会关心资金不能有任何损失之类的要求。所以，如果我执行一系列交易，那么资金总额应该保持不变。你可以想出一些这类通用要求。另外，事实证明，智能体其实很擅长提出规范。所以，嗯，我不知道你最近有没有用过 Cloud Code，但我经常发现，我会告诉它，我会说：“我想要这个。”Guest: Well, if you can do that, you can most likely run some kind of buffer overflow attack, which uh you know, is famously been used to gain access to all kinds of systems. In fact, I think the number was still sadly the number one security vulnerability is buffer overflow. Um yeah, so there are some specs like that. Uh there are also um sort of domain-specific specs like for a bank, I think they'd be interested in things like no loss of funds. So, if I run a sequence of uh transactions, then the total amount of money should stay the same. So, you can you can come up with some of those general uh things. Also, it turns out agents are actually quite good at coming up with specs. So, uh I don't know if you've done a cloud code session recently, but often what I find is, you know, I tell I say, "I want this."

然后它就会说：“哦，对。你大概还想要这个、这个，还有这个。”我就会说：“对，其实你说得没错。我确实想要那个。”所以我觉得，呃，智能体可以帮我们编写规格说明。我想象着这样一个世界：你有一个智能体助手，它会跟你交谈，带你梳理各种边界情况，并在这方面帮你。所以我觉得，在这个方向上能做的事情很多。And it's like, "Oh, yes. And you probably want this, this, and this, too." And I'm like, "Yeah, actually, you're right. I do want that." And so, I think uh agents can help us write specs, and I imagine a world where you have a a sort of agent assistant that's like talking to you and talking you through the different corner cases and helping you with that. So, I think there's a lot you can do in that direction.

主持人：所以，我的意思是，比如说，在开源模型中，假设你要对 VLLM 或 SGLang 之类的东西进行形式化验证。你可以在智能体的帮助下编写形式化规范。但你怎么知道智能体写出的规范，确实和开发者想要的一样，或者符合开发者的意图呢？Host: So, I mean, like for for example, you know, in the open-source model, like let's say, you know, you are formally verifying a VLLM or SGLang something like that. You could write, you know, formal spec um with assistance of agents. But how would you know that, you know, the even the the spec that agents, you know, write is, you know, the same as the developer wants or developer's intent?

嘉宾：是的，所以这里确实存在一个差距。我认为这是个有意思的研究领域，可以构建工具和智能体来帮助跨越这个差距。不过，即使你没有跨越这个差距，我也认为，如果你让智能体编写一大堆规范并证明它们正确，而且它成功做到了，那么你最终得到的代码很可能会比原本的更好。Guest: Yeah, so that there is a gap there, and you would have I think that's an interesting research area, which would be building uh tools and agents to help cross that gap. But but even if you don't cross that gap, I would argue that if you ask your agent to write a bunch of specs and prove them correct, and it succeeds, you most likely have better code than you would have had otherwise.

主持人：谢谢。再回到拥有更智能的模型这个话题，我觉得进展会更快。前沿模型越好——前提是它们确实表现出色、是优秀的模型——就越能为你提供严谨的规范。比如说：“等等，你没考虑到其他这些情况。社交工程攻击呢？有人打电话来，对方是个才入职一个月的人，什么都不太懂。他们不想被开除，不想犯错、惹恼客户；他们打来电话时，旁边还有个婴儿在哭，但那其实是假的。你一着急，就把那个东西给了他们。我看过一些视频，讲他们是怎么入侵的，还有……”Host: Thank you. And then going back to like having a smarter model, I'm going faster. The better the better better these frontier models, presuming that they're doing a good job and they're good models, the better they can give you tight specs. So, like, "Wait, you didn't think about all these other things. What about social attacks? When someone calls and there's a person who's been there for 1 month and they don't really know anything. They don't want to get fired. They don't want to make a mistake and have an angry customer and they're calling with their baby crying, but it's fake and like you rush it and then you give the thing I've seen these videos on how they hack and

嘉宾：[清了清嗓子]Guest: [clears throat]

主持人：然后你知道，社会工程攻击。嗯，你可以加一条规范，比如，如果某人在这里工作还不到 6 个月，而且还没有参加过模拟社会工程攻击的演练，也没有通过安全培训之类的，那么他们或许就不能把密码重置到新的电子邮件地址上。你知道，诸如此类的事情。你可以帮忙把这些情况都考虑一遍，不过总之，是的。好吧。不好意思，前面那位。Host: and then you know, social attack. Well, a spec you might put in there is if the person has been there for less than 6 months and they haven't been through a you know, a a fake you know, social hacking scenario and haven't passed safety training or whatever, then maybe they don't actually aren't can't give passwords to you know, resets to new email addresses. You know, some stuff like that. That you can help you can think through all those things scenarios, but anyway, yeah. All right. Excuse me. In the front here.

嘉宾：嗯，听起来你认为形式化验证是一种严格的审查流程，也许可以类比飞机防撞系统。嗯，工程领域通常会有一定程度的监管，因为一家公司的安全标准可能和另一家公司的不一样。那么，你认为监管会以某种方式参与 AI 安全吗？如果不会，你有什么办法激励企业采用你的形式化验证引擎吗？Guest: Um so it sounds like you see formal verification as some kind of rigorous review process and drawing analogies maybe aircraft collision avoidance. Well, um maybe in engineering there's generally some amount of regulation since the safety standards that one company might not match the safety standards of another. So do you see regulation being in any way or shape or form involved in AI safety? And if not, do you have some means of incentivizing companies to adopt your formal verification engine?

主持人：谢谢Host: Thank

嘉宾：是的。Guest: Yeah.

主持人：嗯，是的，我认为监管可以发挥作用。我想，哦，呃，问题是监管是否有作用？不同公司可能有不同的……我不知道，呃……Host: Um yeah, I think regulation can can play a role. I think Oh, uh the question was is there there a role for regulations? Different companies might have different I don't know, uh

客人：安全标准Guest: safety standards

主持人：安全标准Host: safety standards

主持人：如果不是这样，你会如何让所有人采用你的形式化验证引擎？Host: And if not, will how will you get everyone to adopt your formal verification engine?

嘉宾：哦，呃，我想最后那部分是关于那个……所以说到监管，呃，我这些年来的一位合作者是 Chris Gerdes。呃，他曾是斯坦福大学机械工程系的教授，现在在 Waymo 工作。嗯，不过他研究的是自动驾驶汽车，还曾前往华盛顿特区，帮助交通部制定自动驾驶汽车的法规。最后我想他和那里的所有人都意识到，现在就对该使用哪些技术作出过于具体的规定，还有点为时过早；更应该关注更高层面的最佳实践和标准，而不要规定得过于具体。因为这个领域，呃，你知道，一直有很多创新，而且今后也会继续如此。Guest: Ooh, uh I think the last part about that that the So in terms of regulation um uh one of my uh collaborators over the years has been Chris Gerdes. Uh he was a professor in mechanical engineering at at Stanford. He's now at Waymo. Um but he worked on automated vehicles and he was he went to Washington D.C. to help the Department of Transportation come up with um uh regulations for automated vehicles. In the end I think he and and everyone there kind of realized that it's a little bit premature to uh be too prescriptive in terms of what technologies to use but rather focus on higher-level best practices and um and standards at that level without being too prescriptive because this area is uh you know there's a lot of innovation that has been happening and and that will continue to happen.

我认为重要的是要认识到，各家前沿实验室，以及各种——我也说不准——自动驾驶公司，都不希望在安全方面相互竞争，对吧？Zoox 出事故并不符合 Waymo 的利益，反过来也一样。因此我认为，这是一个行业确实需要在各自领域携手合作的机会，对吧？自动驾驶领域的标准，显然会和语言模型或其他类型的 AI 应用标准有所不同。I think the important thing to realize is that um the various frontier labs, the various I don't know automated driving companies they don't want to compete on safety. Right? It's not in Waymo's interest for Zoox to have an accident and vice versa. And so I think this is an opportunity where um the industry really needs to work together in their particular domains, right? Automated driving, I mean those standards are just going to be different from language models or or other kinds of applications of AI.

主持人：是的，关于监管，我想说，嗯，我确实认为监管能发挥作用。我觉得，就像迈克尔说的，你得小心，别规定得太死；不过，可以想办法通过激励来推动一些有利于安全的一般原则。至于形式化方法这个具体领域，你知道，我做形式化已经30年了，一直在努力让大家采用它。试图告诉大家“你们必须换一种方式做这件事”，这不是个好主意。嗯，我觉得现在的不同之处在于，市场力量会形成激励。所以，如果我们能证明形式化方法可以自动化、能够大规模运行，而且能带来更高的安全性，并且有几家公司开始采用，那么其他每位 CISO 都会想：“哦，我们最好也这么做，不然你知道，我们就没有同样的优势了。”Host: Yeah, so I about regulation I would just say um I I do think there's a role for it. I think you have to be careful like Michael said not to be too prescriptive, uh, but to find ways to incentivize, um, general principles that would that would be good for safety. Uh, in the specific case of formal, you know, I've been doing formal for 30 years trying to get people to do it. It it's a bad idea to try to tell people you have to do this differently. Um, I think what's different now is I think there will be market forces that incentivize it. So, if we can show that uh, formal is automatable, work works at scale, and gives you higher security, and a few companies adopt it, then every other CISO is going to be like, oh, we better do that, too, or else, you know, we won't have that same, uh, advantage.

所以，我认为，呃，我们会看到，你知道，强大的市场力量会有所帮助，呃，我我认为实际上在整个 AI 安全领域都是如此。So, I think, uh, we will see, you know, strong market forces help, uh, I I think actually all across AI safety.

嘉宾：我认为形式化方法有一个好处值得特别强调，那就是现在你可以瞬间把东西 Lean 化，而以前这需要花费大量时间。你在某张幻灯片里提到了这一点，但这真的非常重要——现在这件事已经变得切实可行了。所以，人们之前听了你的话就走了，因为他们会说：“哦，你得雇 150 个 Lean 博士，去审查 Google 的所有代码，才能做到这一点。”现在你不必这么做了。没错，对吧？你只需要大概 100 美元、1,000 美元的 token，对吧？嗯，还有你提到的那个很有意思的观点，Michael，关于 Waymo 没有动力在安全性上竞争。我觉得前沿实验室的情况也一样。没人想看到更多攻击，也不想看到他们的模型被滥用之类的事情。Guest: And the one benefit that I think, um, I I would like to underscore on on formal methods is that you can leanify things instantaneously now. Where before it required so much time. You made that point on one of your slides, but like it's so important to really it's now tractable. So, you you you lost people because they said, oh, you just need to hire 150, you know, people who are, you know, PhDs in lean to like go through all the Google code and make this happen. Now you don't have to. That's right. Right? You need like, I don't know, $100, $1,000 in tokens, right? Um, and then on the on the it's really interesting point that you made, uh, Michael on, um, this the incentive for Waymo not to compete on safety. And I think the same thing is true for the frontiers. No one wants more attacks and and things like and misuse of their models.

这对所有人来说都是糟糕的营销。而且，呃，托马斯·布朗，汤姆·布朗刚刚在纳帕那边说了这件事。而且，呃，我觉得我们还应该说，他们刚刚都去了白宫，并签署了一份列有这四条内容的文件。所以，我其实很希望他们能在独立审计、一些安全防护措施以及其他所有这些事情上达成一致。他们都会去做这些事。六家实验室都会，包括英伟达，因为英伟达不制造 Megatron。他们不常被纳入讨论，但他们应该参与进来。嗯，所以，已经有了一个自律机构的框架，不需要政府监督，也不会采取惩罚性措施——这是你之前用的词。好。嗯，我们从后面这边开始。That's bad marketing for everyone. And um, and Thomas Brown Tom Brown just actually said that up in up in, uh, Napa. And um, and I think what, uh, we should also say is that they all just went to the White House and signed a document with these four four bullets. So, I'd actually like they are actually agreeing on independent audits, some of these safety guardrails, and all these other things. They they all are going to do those things. All All six of the labs, including Nvidia, cuz Nvidia doesn't make Megatron. They're not included in the conversation very often, but they should be. Um so, there are there are there is already a framework for a self-regulation body that doesn't need government oversight and isn't punitive is the word you used earlier. Okay. Um let's go from this side in the back there.

是的。Yeah.

主持人：谢谢。想问 Anthropic 一个问题。呃，我很好奇，你们首先瞄准哪些应用或市场？另外，你们如何衡量在现实世界中的成功？具体来说，就是你们正在瞄准的这些应用。Host: Thank you. Question for Anthropic. Uh curious, what what applications or markets are you targeting first? And, you know, how do you measure success in the real world? These specific applications you're you're targeting.

嘉宾：当然。嗯，这方面我不能说太多。我能说的是，我们的首要任务是构建一种能力，能够针对大规模代码自主、自动且高效地进行推理。嗯，我们觉得，如果你听说过那些实验室谈论的数学超级智能，那么这就像是代码超级智能——真正精准地对代码进行推理的能力。我们认为，一旦具备了这种能力，就有十万种事情可以用它来做。嗯，你可以想象用它来帮助企业、帮助开发者，也可以想象用它来协助安全工作。所以，嗯，对，这就是我们前进的方向。成功的标志是验证全世界所有的代码。Guest: Sure. Um so, I can't say too much about that. What I will say is our our very first priority is to build uh the capability to reason autonomously, automatically, efficiently, with a about code at scale. Uh we think it's sort of, you know, if you've heard of these uh labs talking about mathematical superintelligence, this is like code superintelligence. Like the ability to really reason precisely about code. We think once you have that, there's like 100,000 things you can do with it. Um you can imagine, you know, helping enterprise. You can imagine helping developers. You can imagine uh you know, helping with security. So, um So, yeah. That's the direction we're headed. Success is when all of the world's code is verified.

主持人：嗯，首先，谢谢。嗯，其次，呃，现在像 LLM 这样的系统，是人类通过代码——呃，我是说，通过界面与之交互的系统。我知道现在发生了很多提示注入攻击，也可能会通过智能体发生 XSS 攻击。你觉得形式化方法在应对这类攻击时能有什么帮助？我只是……Host: Um first of all, thank you. Um second, uh when you are like LLMs right now are an a system in which humans are interacting with the code uh with I mean the interface. And I know like there's a lot of prompt injection attacks that are happening and maybe XSS attacks that can happen through agents. Do you think these type like how would formal help in this sort of attack? I'm just

嘉宾：是的，所以，呃，如果我们说的是人类用自然语言与 LLM 交流，那确实会有一些困难，因为其中并没有什么代码部分是我们能够证明其性质的。不过，还是有一些可行的方法。亚马逊有一项名为“自动推理检查”的技术，他们会检查 LLM 的回答，并尝试通过自动形式化提取 LLM 想要传达的领域知识，然后再用严谨的领域模型对其进行验证。因此，即使整个过程都使用自然语言，也有一些技术可以用来提供一定的安全性和保障。Guest: Yeah, so uh again there there's some difficulty there if we're talking about natural language from a human to an LLM, then there's not really any part of that that's uh code that we can prove something about. Um but there are things that can be done. So Amazon has a technology called automated reasoning checks uh where they actually look at the responses of an LLM and they try to extract uh using auto formalization what the domain knowledge is that the LLM's trying to communicate and then they check that against uh rigorous domain model. So there are some techniques even when it's all natural language that can be leveraged to uh provide some security and safeguards.

主持人：我学计算机科学的时候，接触过 SQL 注入攻击，比如我记得经典的利用方式是 Johnny drop tables。有没有类似的模型，可以检查用户输入并 lint 出提示注入？Host: When I was learning CS there was like SQL injection attacks, you know, Johnny drop tables I think was the the classic uh exploit CD. Um is there no equivalent like a model to look at the um user input and lint out uh prompt injection?

嘉宾：没错，但这就是一场军备竞赛，对吧？所以你可以……Guest: Sure, but that's an arms race, right? So so you can

主持人：总是想方设法压过对方。Host: Always trying to outdo each other.

嘉宾：对。Guest: Right.

主持人：嗯，好吧，我想我们这边各有两位。我先请最后面那位。对。Host: Um okay, let's I think we have two and two. I'll go in the way back there. Yeah.

提问者：嗨，嗯，是这样，这个问题是问克拉克的。嗯，我很好奇，在你举的美国银行这个例子里，即使你把美国银行内部的所有软件都形式化了，这些软件也依赖很多长尾依赖项，甚至一直延伸到硬件层面。你可能还得形式化 x86 指令集，然后你还得……Guest: Hi, so um yeah, this question's for Clark. Um so I'm curious in your Bank of America example, uh even if you formalize all of the software within Bank of America, the software relies on a lot of a long tail dependencies even down to the hardware level. You'll have to maybe formalize the x86 instruction set and then you have to

主持人：这件事已经完成。x86 指令集已由多家公司正式标准化。Host: It's been done. The x86 instruction set has been formalized by several companies.

主持人：嗯，你怎么看待 Rowhammer 这类硬件级攻击？Host: Well, what do you think about things like hardware level attacks like rowhammer and that sort of thing?

嘉宾：是的，我是说，我觉得软件可能是比较容易入手的部分，硬件则要难一些。但我确实认为，最终的目标应该是验证所有软件、所有编译器以及所有硬件，然后就大功告成了，对吧？所以，我是说，为什么不呢？我觉得 AI 只会越来越强，而形式化工具和 AI 配合得很好。现在有不少初创公司正在借助 AI 来做硬件验证。我认为这项技术会越来越成熟。Guest: Yeah, I mean I I think probably software is low-hanging fruit, hardware is a bit more difficult, but I I do think that uh the eventual scope would be you verify all the software, you verify all the compilers, and you verify all the hardware, and then you call it a day, right? So, I mean, why not? I think AI is just going to get better, the formal tools work really well with AI. There's a bunch of startups doing hardware verification with AI's help. I think this technology is going to get better and better.

主持人：酷。是的。你。Host: Cool. Yeah. You.

嘉宾：是啊，我在 LinkedIn 上看到一位我认识的医生提到，如果 Waymo 是一家制药公司的药物，它早就能从美国政府那里获得一项出于人道主义考虑的用药豁免了，因为它挽救生命的效果实在太好了。所以我就有点好奇，网络安全领域有没有类似的东西。你知道，很多企业系统都有这么一个情况，对吧？会有一个管理员团队，对吧？然后，也许这些人并不是在做管理员工作——他们的密码就是 admin。不过，我听说过一件事：这些拥有管理员或开发者权限的人自己也会面临威胁。你知道，有加密货币高管被人砍断手指。嗯，我记得 Adobe 的 CEO 在九十年代还被绑架过。Guest: Yeah, so one thing I saw from a doctor I know on LinkedIn was talking about how if Waymo was like a pharma company's drug, it would have gotten a waiver from the US government for compassionate use cuz it's been so effective at saving lives. And so, I was kind of like you know, curious about if there's like some sort of like similar thing you can have for like cybersecurity. You know, one thing you have with a lot of like enterprise systems, right, is that you know, there's an admin team, right? And then, you know, maybe it's these guys aren't doing admin admin is their password, but um you know, one thing I've heard about is that you know, these folks with admin or developer access face threats themselves, you know, crypto execs have gotten their fingers cut off. Um the CEO of Adobe was kidnapped in the '90s, I remember.

嗯，我年纪还小，但我听说过这件事。我很好奇，能不能有一种足够值得信赖的 AI 系统，让它来担任你的管理员？这真的有可能吗？比如把它运行在某种机密虚拟机里。我只是有点好奇你对此有什么看法，以及我们能不能在一定程度上限制物理攻击面，打造出真正安全可靠的东西。And well, I'm I'm kind of young, but I I heard about it. Um And so, [clears throat] I was curious is like could you have an AI system that's like so trustworthy that it could be your admin? Is this even like possible? Like you run it in like some confidential virtual machine. Just kind of curious about what your thoughts are on this and like whether we can like kind of limit the sort of physical attack vector, you know, and have like something that's like truly safe um and and secure.

主持人：那我来回答吧，我想。Host: I'll take that one, I guess.

嘉宾：是的，我想，航空领域也会出现类似的问题，对吧？尤其是飞机辅助自杀，以及人们对人类飞行员心理健康状况的担忧。所以，问题是，为什么不把这也自动化呢？就像我想你是在建议把管理工作自动化一样。我认为，联邦航空管理局可能还要过一段时间才会考虑这个提议。目前的运作方式是，即使飞机没有飞行员，也会有一名飞行员受到美国联邦航空管理局（FAA）的监管并获得认证。如果出了什么问题，他们就要承担责任。所以我认为，我们需要非常仔细地考虑责任归属。这就是我对你这个建议的担忧。Guest: Yeah, I I think um a similar kind of question comes up in the aviation domain, right? Um especially with um uh aircraft-assisted suicides, right? Um and concerns over mental health the of um you know, human pilots. So, um yeah, the the question is, why don't you automate that? Just like how you I think you're suggesting automating the administration. Um So, I think it might be a little while until the Federal Aviation Administration will entertain that. The the way things are set up right now is that aircraft, even if it's unpiloted, um there's a pilot who is uh regulated and and certified by the the FAA. And if something goes wrong, they're responsible for it. So, I I think we need to think very carefully about responsibility. And that would be my concern with your suggestion.

主持人：是的，我觉得 Waymo 的对比挺有意思，对吧？Waymo 并不完美，但据他们所说，它确实在挽救生命。所以你可以想象，人们也会提出同样的论点。不过我觉得 Michael 提出的一个问题很有道理：如果事情进展不顺利，该怪谁？开发这个 AI 管理系统的公司，愿不愿意承担责——你知道，愿不愿意在出了问题时承担法律责任？如果愿意，那就说明他们的安全论证做得非常好。Host: Yeah, I think the the Waymo um comparison is interesting one, right? Like Waymo's not perfect, but it is according to them, it is saving lives. So, you could imagine making the same argument there, but I think Michael's point is a good one, like who who do you blame if it uh doesn't go well? And does the company that makes the AI admin, are they willing to take liab- you know, legal responsibility if something goes wrong? If they are, then that suggests they did a really good job with their safety case.

嘉宾：这实际上又回到了那个更智能、更出色的 AI 系统的话题。你看，在信息安全领域，有一种趋势是采用基于信任的架构。所以你要确保这些系统中的任何一个都不被信任：如果有人入侵了其中一个，也无法进一步入侵其他所有系统。嗯，你知道，如果我有一个非常聪明、始终在线的 AI 系统，监控流量、查看我的 Datadog，以及所有传入的内容，它发现有一大堆邮件从 CTO 那里发往某个外国账户之类的地方，或者刚生成了一大堆密钥，就被发到了一个非 @google.com 的地址，而是某个 Gmail 地址，你就会觉得：“什么情况？嗯……”所以，有些事情虽然没有明确而严格的规则，但只要上下文足够，你大概就能划出界限，说：“这可不太妙。”Guest: And this is actually um goes back to the point of like a a smarter and better AI system. If you like there's the the one system um trend in uh in in uh information security is your trust uh based architectures. And so like you want to make sure that there's zero trust in any one of these systems that if you infiltrate one, you can't infiltrate everything else. Um and you know, if I had a a really smart always-on AI system that's looking at traffic and looking at my data dog, looking at whatever is coming through and they see, you know, a bunch of wires going from the CTO, you know, to some foreign account or something like that or a bunch of keys just got generated and shipped to a non-at-google.com but to some Gmail, you'd be like, "What? Hmm." You know, and then so with enough like some things you don't have hard and fast rules, but with enough context, you can probably draw the line and be like, "This is not cool.

“我来标记一下。”然后就把它标记出来，提醒大家。经营过公司的人应该都遇到过这种 Sentry 告警。简直就是成千上万条垃圾告警，所以你很少会去看它们。Acast 也有这个问题，告警多到让人不堪其扰。所以你必须非常精准地筛选，我认为 AI 监控系统确实能做得好得多。那么，我们再来两个。我想我们来看看右边这位。Let me flag it." And just flag it to people. And so and and we've all had, you know, these century alerts for anyone that ran a company. And it's like it's just a thousand of these garbage alerts. And so you don't look at them very often. And it's like you know, the Acast has this issue as well where you like death by a thousand alerts. So you have to be really really targeted and I think AI uh watching the system can actually do a much better job with that. So. Um we'll take two more. I think we'll go here on the right here.

主持人：嗨。嗯，首先，我很感谢你们两位。我想听听关于形式化验证的看法，也想听听关于标准和安全的看法，尤其是物理系统方面的。嗯，有航空电子领域的专业人士或教授在这里，真是太好了。嗯，我特别想听听这方面的观点，因为你提到了基于动力系统的模型，比如扩散模型、归一化流。嗯，目前中国的实验室正在推动效率前沿，美国的实验室正在推动智能和能力前沿，但实际上，从一开始就没有人在推动可控性和可解释性前沿。Host: Hi. Um first, I'm really appreciative of both of like I wanted to hear on formal verification and then also like standards and safeties uh especially like in physical systems. Uh so having a avionics professional or professor here is great. Um I wanted to hear especially because you touched on uh dynamical systems based models like diffusion models, normalizing flows. Um right now we have the Chinese labs pushing the frontier of efficiency. We have the American labs pushing the frontiers of intelligence and capability, and we don't really have anyone pushing the frontiers of controllability and interpretability from the start.

确实有一些领域，比如发展性可解释性，人们会监测训练动态和涌现能力，并尝试用我们在各个领域中发现的数学来拟合我们观察到的现象。但我想问的是，你认为有没有可能对训练动态和智能加以约束，或者尝试描绘这样一条前沿：一端是可解释性与控制，另一端是智能与能力；同时研究方法从传统的统计机器学习方法、信号处理和控制理论，逐渐转向深度学习和神经网络。还有，我提到的很多术语可能用得不太对。我并不是想随便堆砌一堆流行词，只是……We do have some fields like developmental interpretability where people are monitoring training dynamics and emerging capabilities uh and trying to fit uh math that we have discovered throughout the fields like and try to try to fit it to what we're observing, but we I'm trying to uh basically ask like do you think there is room for constraining uh training dynamics and intelligence uh or trying to map this frontier of uh interpretability and control on one axis and intelligence and capability uh moving from traditional statistical machine learning methods uh and signal processing and control theory over into uh yeah, deep learning and neural networks. Also, I'm sure I have uh messed up a lot of the terms I mentioned. I don't mean to just add in a bunch of buzzwords, but

嘉宾：就像是以某种方式过滤梯度。Guest: Like uh filtering gradients in some way.

主持人：呃，好吧。是的。嗯，不，这个问题问得很好。我每年会给几个群体授课三次：通过斯坦福大学商学院为高管开设一个高管教育项目，另外还会通过 HAI 开设一个。嗯，他们是来自世界各地的高管，面临着很大压力，必须想办法制定 AI 战略，并将其应用到产品或流程中。我一开始就会提醒他们工程学的一项基本原则。工程学的基本原则与科学的基本原则非常相似，也就是奥卡姆剃刀：最简单的解释更有可能为真。在工程学中，嗯，更简单、可解释性更强的方法更有可能稳健可靠。因此，具体要看他们的应用场景；如果线性回归或决策树就能解决问题，那他们真的就应该用这些方法。Host: Uh okay. Yeah. Um No, the the this is a great question. So, I teach groups uh three times a year I offer an executive education program through the Stanford Graduate School of Business to executives, and I do another one um through HAI. And uh they're executives from you know, all around the world, and they're under a lot of pressure to somehow come up with an AI strategy and bring it into their products or processes. And what I remind them at the very beginning is of the fundamental principle of engineering. The fundamental principle of engineering is very similar to the fundamental principle of science, which is Occam's razor. You know, simplest explanation is more likely to be true. In engineering, the uh simpler, more interpretable method is more likely to be robust. And so, depending on their application, they should really be like if you can get away with linear regression or decision trees, you should you should be doing that.

现在有很多人很容易直接采用神经网络、Transformer 之类的方法。但这往往并不是正确的做法。因此，我鼓励大家先尝试最简单的方法，然后再试试稍微复杂一点的方法，看看性能提升是否足以证明增加的复杂性是值得的。如果不值得，那就继续使用可解释性更强的方法。不过我认为这是一个非常重要的话题。事实上，新的验证指南中有一章专门讨论可解释性，而这对于 AXI 获得国际标准的认可至关重要。There's a lot of temptation right now to go straight to neural networks and transformers and and all that. Uh but that's that's often not the right way to to go. Um and so, I uh I encourage everyone to try out the simplest method and then try something maybe a little bit more complicated and see if the performance lift justifies that additional complexity. If not, then stay with the more interpretable method. But I I think this is a a very important topic. In fact, one of the chapters in the new validation book is on explainability. And that that was critical in getting AXI accepted as an international standard.

嘉宾：呃，快速追问一下。你觉得有没有市场激励，或者足够的需求，能让人们去构建受限智能？这样一来，他们是否有可能与前沿实验室竞争？Guest: Uh really quick like follow on. Like, do you think that it there is like market uh incentive or like enough uh like demand like where we could people building like constrained intelligence uh like they would be able like it would be feasible uh to compete with like with the frontier labs.

主持人：所以，我想说，如果你能创造出在可衡量的意义上更安全的东西，那肯定会成为竞争优势。我也知道，外面有人正在思考该如何做到这一点。所以，希望他们能找到办法。Host: So, so I would say that if you um manage to create something that is measurably safer, then that would be a competitive edge, for sure. And And I know that there are people out there thinking about how to do that. So, you know, hopefully they can figure that out.

嘉宾：如果你，呃，呃，想创办一家公司的话，有一些创业加速器可以申请，他们会给你资金和指导。嗯，好吧。总之，后面那位。对。Guest: And if you, uh, uh, looking to start a company, there's these accelerators that you could apply to, and they give you money and guidance. Um, okay. Anyway, yeah, you in the back there. Yeah.

主持人：你好，非常感谢。那么，我的问题是，互联网时代教会了我们很多有关安全的知识。嗯，你觉得我们会从互联网时代借鉴些什么？或者说，我们会在这个生成式 AI 时代从互联网学到些什么新东西？还有，尤其是在真实安全方面。Host: Hi, thank you so much. So, my question is internet era taught us a lot about security. Uh, so what do you think will we, like, copy from the internet era, or what we will learn something new from the internet, uh, uh, this generative AI era? Or, uh, authentic security, especially.

客人：所以，这是给你的，也是给你们大家的。Guest: So, that's for you. And for you guys.

主持人：呃，那么，问题是，我们能从互联网时代学到什么，并将其应用到当下这个时代？Host: Uh, so, is the question what can we learn from the internet era that we could apply in the current era?

主持人：是的，还有，呃，你觉得互联网时代可能有哪些不同之处呢？Host: Yes, and, uh, what do you think could be different from the internet era, as well?

嘉宾：是的，我记得我还在纽约大学（NYU）当年轻教授时，听过一场关于安全的演讲。演讲大意是，问题只有两个：一个是人，另一个是计算机漏洞。Guest: Yeah, so I remember going to a talk when I was a young professor at NYU, uh, on security, and basically said there are only two problems. One is people, and the other is computer bugs.

主持人：是的。Host: Yes.

嘉宾：所以，我觉得我们……我觉得我们能修复电脑故障，但我不认为我们能改变人。Guest: So, I think we I think we can fix the computer bugs, but I don't think we can fix the people.

主持人：呃，我们……但但我觉得，不同之处在于，嗯，人工智能可以用各种各样不同的创造性方式来使用。所以，你知道，就像弗朗索瓦刚才说的，它可以充当一种监督者，或许能捕捉到一些社会工程攻击。呃，它当然也可以用来加快形式化方法之类的进程，从而保护系统。嗯，是啊，也许那个人工智能管理员的想法也不错，只要仍然有人参与其中。嗯，我一直很担心这一点。你们有人看过老电影《战争游戏》吗？很老的那种。但你知道，要是把一切都交给计算机，万一发生什么奇怪的事，导致事情失控，就没人能应对了。所以我觉得，我们确实需要有人参与其中。Host: Uh, we But, but what's different is, I think, um, AI can be used in all all sorts of different creative ways. So, it could be used, you know, as Francois was saying, as kind of a a watchdog to maybe like catch some of the social engineering. Uh, it can certainly be used to accelerate things like formal methods to, you know, secure the systems. Um, yeah, may maybe even the, uh, AI admin idea is a good one, as long as there's still some humans in the loop. Um I always worry, you know, I don't know if any of you are ever watched the movie WarGames, old old school, but but you know, you turn everything over to the computers and then there's nobody if if there's something weird happens like uh that can go off the rails. So, I think we do need humans in the loop.

嘉宾：嗯，有一篇著名的物理论文叫《多即不同》。嗯，它的前提大概是这样：“好，如果我有一个原子、两个原子，如果我有一大堆原子，很多很多原子，黑洞就开始形成了，光就逃不出去，光只是在里面绕一圈，然后又回来。”所以，会出现一些奇怪的现象。多即不同。我觉得，在这个世界里，我们曾经有60亿人，现在有70亿人，而如今有700万亿个智能体——姑且说它们的智能水平相当，或者各自有某种动机，而且我可以生成各种各样的智能体——数量一多，情况就完全不同了。所以，没错，CloudFlare 能够阻止 DDoS 攻击，但当你把……把无穷大应用到这个数字上时，一切都会崩溃。于是，就可能出现一些奇怪的情况，把问题暴露出来。Guest: Um there's a famous physics paper called More Is Different and um and it's kind of like the premise and like, "Okay, if I have, you know, one atom, and two atoms, if I have a bunch of atoms, I have a whole lot of atoms, black holes start to form, like light can't escape, light just does a loop and comes back." So, there's weird stuff. So, more is different. And I think in this world where we had 6 billion people and now we have 7 billion people and now we have 700 trillion agents that are let's just say at equal intelligence or have some motive and I can spawn all these different agents, more is just so different. And so, yeah, we had CloudFlare being able to stop DDoS's, but like everything breaks when you hit when you apply infinity to the to the number, everything breaks. And so, weird stuff can happen that exposes it.

我今天发的推文大致是这样写的：“我们刚刚在 Iclear 看到，很多系统都面临这种情况：一年内提交了 60,000 份申请，这个数量超过了历史上所有申请在一年内的累积总和。”所以，这就像一个很大的指数增长。上面那个 E，那个常数是个很大的数。因此，所有审核系统——比如我们在 Focal 有很多这样的系统——无论是查看 Century Alerts，还是查看客户支持工单，等等。假设是大学招生。比如说，对每一个高中生而言，最优策略就是申请美国的每一所学校——这就像一个纳什均衡。你为什么不这么做？其实，抱歉，应该是全世界的人都去申请全世界所有地方的学校。And I wrote the tweet today basically like, "There's a lot of systems that we just saw this with Iclear where 60,000 submissions submitted in 1 year, which is greater than the cumulus summation across all submissions in all history in 1 year." So, that that's like a big exponential. That E, the constant up there is a big number. And so, all review systems, which we we have many at uh Focal, for example, looking at the Century Alerts, looking at um customer, you know, support tickets, or whatever. If imagine college college admissions. Like a um you know, uh a Nash equilibrium, you know, optimal strategy for every single all all high school students is to apply to every single school in America. Why would you In fact, actually, sorry, the whole world should apply to all schools everywhere.

主持人：嗯。Host: Yeah.

嘉宾：对吧？这很贵。嗯，他们得收费。是啊，如果没有费用的话，那就只能这么办了。那么，你们实际上要怎么应对这类有人参与审核的系统？它们会遭到非常猛烈的 DDoS 攻击。嗯，最近讨论过的一个真实案例是小额索赔法庭。所以，如果你的智能体能替你向小额索赔法庭提起诉讼，你就不再需要律师了。Guest: Right? It's expensive. Well, it's they're going to have to charge money. Yeah, if there's if there's, you know, if there's no fee, then then that's kind of the what has to happen. And then so how do you actually handle these human review in the loop systems? They get DDoS really hard. Um a real one that that just got discussed was um small claims court. So if your agent can file a small claims uh on for you and you don't need a lawyer anymore.

主持人：是的。Host: Yeah.

嘉宾：司法司法系统会怎么样？它已经完全陷入瘫痪了。现在要走完司法程序就已经耗时太久，而接下来情况会变得荒唐到难以想象。所以所有这些系统都需要重新评估。因此，我认为，真正会有意义地发生变化的，是学习方式；这与互联网时代到现在相比，会有很大不同。我们以为自己知道什么叫大规模，但人类产生的流量将只占互联网流量的 0%。要知道，零可是个非常小的数字。Guest: What happens to the judicial judicial system? It's completely bogged down. It already takes too long to get through the judicial system, but now it's going to be insane and impossible. And so all these systems need to be reevaluated. And so the more is different is really the learning that is going to be meaningfully different, I think, from the internet era from to to to now. We thought we knew what big scale was, but like human traffic will be 0% of internet traffic. Like That's going to be a zero is a very small number.

主持人：谢谢。Host: Thank you.

嘉宾：好的，我们还有时间再回答一个问题。好，请讲。Guest: Okay, we have time for one more question. Yeah, please.

主持人：嗯，谢谢。这个问题是关于如何对基准进行基准测试。背景是，我在 LinkedIn 从事 AI 安全工作，而对危害的定义变化得非常快。即使只看有毒文本或偏见这样的小问题，每隔五年，新一代人就会为各种事物创造新的俚语。那么，你们如何确保这些俚语不会出现在招聘过程中，比如你收到的招聘人员发来的消息里？你们现在如何衡量这一点？目前用的是基准，但基准的更新速度很慢。公开基准，甚至内部基准，成本都很高，而且需要经过大量人工审核。你们认为，我们要如何从当前的技术水平——一些实验室发布基准、基准创建速度缓慢——迈向这样一种状态：基准能够动态演进，跟上术语变化的速度？Host: Um thank you. So this question is about benchmarking the benchmarks and the context is that I'm working in AI safety at LinkedIn and um the definitions of harms drift very fast. Uh even looking at something so small as toxic text or bias every 5 year the new generation has a new slang for everything. So uh how do you make sure that that slang doesn't show up in uh say hiring uh in the uh messages that you get from recruiters? Um how do you do how do you measure that right now is benchmarks, but benchmarks move very slowly. The public even in-house benchmarks have to be uh very costly and uh need to go through a lot of human review. What are your thoughts on how do we go uh from current uh state of the art? some labs publishing benchmarks and slow creation of benchmarks to a state where benchmarks are dynamic evolve as quickly as terms evolve?

嘉宾：是的，问得很好，我也很喜欢你举的例子。嗯，我想，正如我主张持续监控我们的 AI 系统一样，我们也应该持续监控我们的基准测试。好消息是，有一些定量方法可以识别分布偏移并监控语言变化，我认为我们只需要去做就行。Guest: Yeah, great question and I I like your example there. Um Yeah, I I think we just like how I advocated for a continuously monitoring our AI systems, we should continuously monitor our our benchmarks. And uh the good news is that there are some quantitative methods for identifying distribution shift and um monitoring shift in language I I think we we just need to do.

主持人：这里没什么要补充的。好。行，再来一个。这是最后一个。Host: Nothing to add there. Okay. All right, here's one more. Last one.

嘉宾：我想就改进基准测试再跟进一下。我觉得有件事我一直，呃，想就改进基准测试再跟进。我觉得研究人员总会遇到一个问题：一些常见的评测——我说的就是你，Math 500——里面有些部分是有问题的。呃，我觉得应该有人，也许是你们团队，跟 Hugging Face 或者其他地方协调一下，建立某种机制，让智能体能够集中发现这些资源存在的问题。我觉得就像我们发布报告，说不同的基准测试出了问题，或者不同的评测出了问题，然后报告就搁在那里一样。比如我有这篇论文，但有些……我只是在公开呼吁，希望有人能把这件事闭环处理一下。Guest: I'll just follow up with regard to better bench. I think one thing that I keep uh follow up with regard to better bench. I think one thing that I see researchers keep running into is that some common evals, I'm looking at you math 500, have broken pieces to them. Uh I feel like somebody and maybe it it's your group there needs to be some kind of coordination with hugging face or somewhere where agents will centrally find that these resources have these problems. I think that just like we put up you know, reports that different benchmarks are broken or different evals are broken and then it just sits there. Like I have this paper, but some I'm just open call for somebody to like close the loop here.

主持人：是啊，我想，嗯，我也见过这种情况。你知道，我有个以前的学生试着评估 SQL 查询，结果谁都做不到超过大概 70%，后来他发现其中大约 30% 实际上都是错的。所以，嗯，我觉得这只是大家推进得太快、有点粗心造成的。希望那些严谨的人最终能赶上来把问题修好，不过现在有点像一场军备竞赛，因为大家都在拼命加快速度。我也说不准。Host: Yeah, I think uh I've seen that as well. You know, I had former student who was trying to evaluate um uh SQL queries and nobody could get better than like 70% and then he showed that like 30% of them were actually wrong. So, uh I think it's just a matter of people moving too fast, being a little careless, and hopefully, you know, the people who are rigorous will eventually catch up and fix it, but it's a little bit of an arms race now cuz everyone's trying to move so fast. I don't know.

嘉宾：是的，我们需要版本控制、拉取请求、提交问题等等。绝对需要。Guest: Yeah, we we need version control and pull requests, issue filing, and and so forth. Absolutely.

主持人：我真的觉得，一个很棒的创业点子，是打造一个类似苹果 App Store 的基准测试平台，并对内容进行筛选，对吧？也就是说，不是谁都能随便把应用放上 App Store。他们会经过一套流程，判断你是否应该上架。Hugging Face，尽管我很尊重 Clem，也很喜欢他们，但那儿简直一团糟，真是一团糟。它就像……（嗤笑）简直像 GitHub，像狂野的西部。所以要找到合适的 GSMA K，其实并非易事，因为有 600 个不同的东西都叫 GSMA K。到底该用哪个？我也不知道。总之，请大家一起感谢 Clark 和 Michael 今晚来参加节目。Host: I actually think that a great idea for a startup is like a Apple App Store of benchmarks where there's curation, right? Like like that they don't just let anyone just throw an app onto the App Store. They go through a process. They they determine whether or not you should be on the App Store or not. Hugging Face, all due respect to Clem, I love them, but it's a mess. It's a mess. It's [snorts] like the wild It's like GitHub. It's like the wild west. And so like trying to find like the appropriate GSMA K, like it's actually non-trivial to find what is the actual right GSMA K cuz there's 600 different things called GSMA K. It's like which one do I use? I don't know. Anyway, please everyone help me thank Clark and Michael for joining us tonight.

嘉宾：非常感谢。Guest: Thank you so much.