UIUC 计算机科学副教授徐天音，聊 AI 智能体需要什么样的计算机系统，用 AI 给 ZooKeeper 建模，以及他为什么主张取消最佳论文奖。
徐天音是伊利诺伊大学香槟分校（UIUC）计算机科学副教授，研究云计算和数据中心的可靠性与安全性。2003 年至 2010 年，他在南京大学完成本科和硕士学业。第一次申请博士不顺，他去德国哥廷根大学交流了一年，第二次申请时进入加州大学圣迭戈分校（UCSD），师从 Yuanyuan Zhou。他的博士研究从配置错误入手，发表了《Do Not Blame Users for Misconfigurations》，并开发了 PCheck，希望在系统出事之前发现藏在配置里的问题。2017 年，他在 Facebook 工作了一年，2018 年博士毕业后加入 UIUC。
他曾 4 次在 OSDI、ASPLOS 获得最佳论文奖，但他一直反对用这些奖项引导研究。访谈时，他正利用学术休假在 UC Berkeley 的 Sky Computing Lab 访问，研究 AI 如何帮助改进系统，以及系统如何适应 AI 智能体。他的学生发起了 SREGym，为 SRE（Site Reliability Engineering）智能体提供排查和处理故障的评测环境。他们也在用 AI 为分布式系统建立数学模型，再借助形式化工具分析其中的问题。
在这期深度对话中，我们讨论了：
- 徐天音第一次申请博士接连被拒，放弃后来拿到的录取，一年后第二次申请进入 UCSD
- 配置写错后系统为何仍能正常运行，以及这个问题如何催生 PCheck
- 拿过 OSDI、ASPLOS 的 4 次最佳论文奖，为什么仍主张取消评奖
- AI 写出的证明，如何暴露 TLA+ 证明系统里人类没碰到过的漏洞
- AI 如何提高对系统研究贡献的要求，以及思考和写作为什么仍然重要
- SREGym 早期解题率为 11.4%，徐天音估计用新模型重跑可能接近 90%，以及小规模环境如何模拟真实生产故障
- 一位博士生曾花费约 5 年时间学习 TLA+、研究 ZooKeeper，并建立和维护相应模型；而 AI 帮助团队在约 5 小时内就为部分开源分布式系统完成了建模
- 另一次 ZooKeeper 证明任务为何跑了 5 天、花了约 2000 美元——系统需求又为何还得由人来定？
- 如何设计系统，让它在 AI 智能体操作出错后，通过撤销错误操作或只重启出问题的组件，尽快恢复正常
- 当代码由 AI 智能体来写，企业为何可能更愿意为可靠性与安全性投入资源
这期对话给我们的最大启示：
- 第二次申请，让导师看到了徐天音做系统研究所需的坚持。
主持人月球大叔提到，徐天音在 2010 年申请博士时曾被 24 所学校拒绝。他补充说，自己后来拿到过一个不错的录取，只是没有去。第一次接受 Zhou 的面试时，她问了 5 个关于目标、长处和研究兴趣的问题，他一个也没答上来。去哥廷根一年后，他重新申请 UCSD，认真准备了那些问题的答案。第二次通话，Zhou 却没有继续考他，而是问他为什么放弃之前的录取，随后开始劝他加入自己的组。在她看来，做系统研究需要不怕失败、愿意反复尝试的人，他已经通过了这个检验。徐天音对这一年的总结很克制：“我其实觉得自己没有太大的提高，只是又坚持了一年。”
- PCheck 的起点，是弄清楚配置错误究竟在什么时候变危险。
Zhou 教给他的研究方法，是先找到重要的问题，再把问题理解透，解决办法往往会随之变得简单。徐天音想弄明白，号称能够容错的系统，为什么遇到配置错误还是会出事。他向系统注入错误配置，发现有些错误并不会立刻造成异常：系统加载了配置，却还没有用到。等另一个故障发生，系统启动恢复流程，才第一次用到那个错误的值。原本应该救场的恢复机制，反而又制造了一个故障。他的第二篇博士论文 PCheck 就从这里长出来：提前找出这些暂时没被用到的错误配置，避免它们在系统已经出问题时才暴露。
- 徐天音反对最佳论文奖，因为追奖会把研究者的注意力带偏。
他参加过 SOSP 最佳论文奖的评选委员会，觉得评选高度主观。有人特别喜欢一篇论文、愿意提名，不等于它一定是质量最高的一篇，更不能保证它将来的影响力。他担心奖项反过来决定大家研究什么：“我觉得有了这种 paper awards 这个东西，反而让大家不好好做 research 了。” 他更希望研究者去做自己认为重要的问题，把工作做好，再向同行展示。他把自己的获奖归于运气，也说这两年获奖少了，并不觉得自己的论文质量就下降了很多。
- AI 写出的无效证明，暴露了证明工具过去没遇到过的漏洞。
在与 TLA+ Foundation 合作的评测项目中，团队让 AI 智能体使用 TLAPS，也就是 TLA+ 证明系统，证明协议的正确性。有些证明通过了工具检查，实际却不成立。徐天音把这种现象称为奖励投机：智能体找到了通过检查的办法，却没有完成真正要证明的事情，维护者因此开始修补一批此前没有预料到的漏洞。这也让他重新审视系统对用户行为的假设：“我觉得现在很多的系统它并不是为 AI agent 来设计的。如果你把 AI agent 当成一个用户的话，这个系统百分之百会出问题。”
- AI 智能体主导写代码，会让企业更难忽视可靠性与安全性。
徐天音认为，企业过去更愿意为功能和性能花钱，因为它们直接带来收入。可靠性与安全性主要防止损失，往往很难争取到同样的投入。多做测试、买保险，也常常比从根本上重新设计系统更容易获得支持。但如果越来越多的代码和系统操作交给 AI 智能体，可靠性与安全性就会成为必须解决的问题，而且不能只靠堆更多测试用例来应付。在他看来，这是相关领域研究者的机会：一些过去很难拿到资源、但本来就值得做的系统工作，现在有了更充分的投入理由。
- SREGym 的难点，是让小规模环境保留真实生产故障的关键特征。
主持人月球大叔提到一个包含 102 个场景、解题率为 11.4% 的早期评测。徐天音说，那已经是约一年前的结果，并估计：“如果你现在用最新的 model 来跑一遍，我觉得他们应该是能够到 90% 了都快。” 他希望评测持续给模型出难题，但也不是一道都解不了。理想状态是模型能完成约 30% 至 40% 的任务，剩下的仍有挑战。更难的是，怎样用 3 个或 5 个节点，模拟大型生产系统里的故障，同时让环境小到可以用于强化学习。团队让 UIUC 本科生参考 Cloudflare 等公司的公开故障复盘，在小环境中重现问题。他认为，这些更接近现实的故障，与最初那些基础故障相比，对智能体提出了不同的挑战。
- AI 帮助团队在数小时内为部分分布式系统建立数学模型。
徐天音的一名博士生花了约 5 年，学习形式化规约语言 TLA+，吃透 ZooKeeper 的 ZAB 协议与实现，并随着代码变化维护相应模型。有了这个模型，他们才得以借助形式化工具，解决系统中多年没有理清的问题。徐天音说，如今借助 AI，团队可以在约 5 小时内为部分开源分布式系统完成建模：前沿模型已经会写 TLA+，也能快速阅读代码。建模的难点仍是决定保留多少细节，太细会让后续分析难以完成，太粗又会漏掉故障。他们会引导智能体细致刻画容易出错的代码，约束奖励投机，再把建好的模型交给形式化工具分析。
- 形式化验证能检查代码是否符合规约，系统该做什么仍要人来定。
建好模型之后，构造证明还有自己的成本。徐天音提到另一次针对 ZooKeeper 系统规约的 AI 证明任务，跑了 5 天，花了约 2000 美元。因此，实验室当时做工具时选择了成本更低、反馈更快的模型检查，同时也把自动证明视为值得继续投入的方向。他看好先写形式化规约、再逐步验证 AI 所加代码的开发方式，但提醒：“即使你能够 formally verify，它只是告诉你，你的系统 code 跟你需要的 specification 是一致的，它其实就干了这件事情。” 有经验的人仍要想清楚系统的用途，以及规约需要覆盖哪些故障。现实中一旦出现规约没有描述的新故障，原来的保证也不能自动覆盖它。
- 让 AI 智能体使用系统，既要防错，也要让出错后的恢复更容易。
徐天音重新提起 David Patterson 在 2000 年前后推动的面向恢复的计算研究。既然系统终究会出故障，就应该投入资源，让它尽快恢复。项目尝试过系统级撤销，包括邮件服务器的案例，也研究过只重启一个组件、避免整个系统重启的办法。他认为，今天的微服务和无服务器架构中仍能看到后一种思路。他设想未来一些系统至少 80% 的用户是智能体，希望系统能够容忍它们的错误，给出有用的反馈，让它们再次尝试。现实的难题是，做一个系统可能要花一两年，而这期间智能体的能力还在不断变化。
- AI 提高了对研究贡献的要求，研究者仍得自己把问题想透。
徐天音认为，过去有些工作靠大量工程投入或少有人掌握的技能成立。AI 能做这些事之后，研究者就需要拿出更有价值的贡献。工具放大的是人的能力：“如果你的能力是 0，那你乘以 100 还是 0。” 他接受一种例外：如果贡献本身就是一个好用的软件或工具，一篇简短、围绕这个成果说明用法的论文可能就够了。但很多研究的价值在于理解问题，他不赞成普遍用一段与智能体的对话代替思考和写作。他认同 Leslie Lamport 的观点，写下来本身就在帮助人把问题想清楚。如果论文数量暴涨让评审吃不消，应该改进评审制度，让它承接这些工作，同时保留研究中的思考过程。