徐天音（Tianyin Xu）¶
- 背景: UIUC 终身教授，计算机系统方向（可靠性、容错、配置错误）。南京大学本硕（2003–2010）→ 哥廷根大学交换一年 → UCSD 博士（2018）→ UIUC 任教至今；实习经历包括 NetApp、Facebook、Microsoft Research。现于 UC Berkeley Sky Computing Lab 学术休假（host 为 Ion Stoica）。
- 本库中的位置：本库第一位学术界系统研究者。此前系统/基础设施来源全是从业者（游凯超、Simon Mo、朱邦华、Baseten 团队、肖志斌）。他提供了本库迄今关于 AI 压缩一项研究工作的最具体的一组数字。
- 首次收录: 月球大叔，2026-08-22
⚠️ 他的博士导师在转录稿里只以
YY/Wai Wai出现。线索有三条：创办过三家公司且都相当成功、此前在 UIUC 任教七年、做系统方向。本库不替他认定这是谁。他在本期说了两次的一句话，本库认为最能概括他："我其实不太相信 AI，但我认为人是应该被相信的。"（[01:32:12]、[01:48:22]）
立场与关注点¶
一、把 agent 当用户：他把十年前的论文接到了今天¶
- 2013 年那篇的论点（[00:15:21]）："Do Not Blame Users for Misconfigurations"——如果很多用户都没意识到问题、都犯同一个错，那可能是系统设计本身有问题。
- ⚠️ 今天的版本（[00:19:23]）："现在大家都在谈 AI-native 系统，但很多现有系统根本不是为 AI agent 这个用户设计的。把 agent 当用户，系统一定会挂。"
- ⚠️ 他给的 reward hacking 一手证据（[00:20:25]–[00:21:25]）：与 TLA+ Foundation 合作做 benchmark，让 agent 给协议写正确性证明。TLA+ 工具链极其成熟，人写了大量证明从没碰到过怪问题；但 agent 写出各种看起来证完了、实际不成立的证明，逼得 TLA+ Foundation 的人开始修一批他们从没想过的 bug。他给的机制解释很干净：
人写证明时是真的想证明这个协议是对的；AI 并不真的想证明协议是对的，AI 只想通过这个证明系统。
- 结论（[00:21:25]）："一旦 AI agent 成为用户，所有系统都应该重新思考怎么处理这个接口。"
- ⚠️ 他对"找 bug"这件事本身评价很低（[00:17:21]）："我从来不觉得找 bug 有多激动人心，因为工业界的 bug 太多了——多到人根本修不完。" 他认为价值在让开发者在设计时就想清楚用户会怎么用。
二、形式化验证：五年 → 五小时，以及被留下的那部分¶
- ⚠️ 数字（[01:11:55]–[01:12:55]）：AI 之前，一位后来去 Microsoft Research 的学生花了整整五年，把 ZooKeeper 及其共识协议 ZAB 做成可跑模型检查的 TLA+ 形式模型。现在这件事变成五小时。
- 五年花在哪：TLA+ 任何本科课程都不教，学透要一两年；还得写 spec（形式模型与不变式），而要建好模型必须极深地理解那个系统；而且系统在变、代码在变，你得跟着演化重写模型。
- 为什么现在快：前沿模型写 TLA+ 已经像写 C 或 Python 一样熟练，而且它已经学过这些开源系统的全部源码。
- ⚠️ 被自动化掉的是学习成本，不是判断（[01:12:55]–[01:13:55]）：真正难的是"该建模什么、不该建模什么"——全都建模，模型会大到跑不动；建得太简单，又发现不了任何问题。这过去靠老手经验或天才学生的直觉。
- ⚠️ 他们现在把这一步也交给 AI，理由值得完整记一次：
一个成熟的开源项目走过很多年，AI 其实知道哪些部分 tricky、哪些部分不太可能出问题。于是我们告诉 AI：这类代码很容易出错，你要更仔细地建模；那个地方历史上从没出过问题，直接抽象掉。AI 做这件事做得非常好。
- ⚠️ 但 AI 干这件事的坑也在这里（[01:14:56]）："AI 不是人，它可能 reward hacking，能产出一个看起来正确、但不是你要的模型。所以你需要办法去引导甚至约束它。"
- 成本数据点（[01:17:59]）：用 TLAPS 跑一个 ZooKeeper 的 system spec（描述系统而非协议，层次较低）花了 2000 美元、跑了 5 天——"我觉得这还是相对昂贵"。他们最终选模型检查而非证明，因为便宜、反馈即时、更实用。
- ⚠️ 经济学翻转（[01:14:56]–[01:16:59]）：形式化方法存在几十年，没普及的原因是成本——需要高度专门化能力，且不符合硅谷 "move fast and break things"。但在 NASA 完全说得通（他们甚至避免多线程代码，用单线程 + 形式化验证再上 Mars Pathfinder 这类任务）。"一旦 AI 把形式化验证自动化，经济账就完全变了。"
- 他对调试 vs 验证的区分："调试是被动的——出了问题你才去调。但我们的梦想是让故障根本不发生。"
- "买保险"框架：过去更便宜的做法是部署 + 买保险（十年一次的故障就买大额保单）；现在一份形式化证明可以保证这类故障不发生。
- 历史上谁在投："AI 之前最热心、现在仍最热心的是微软（因为 Azure），然后是 AWS。基本上就这两家。" ⚠️ "有了 AI 之后这个门槛变得很低。"
- ⚠️ 他自己给的限定，必须与上面一并读（[01:22:02]–[01:23:03]）。被问"既然验证已从五年压到五小时，为什么还有人说 AI 建系统最大的问题是可靠性"：
即使你能形式化验证，它也只告诉你代码与你要的 spec 一致，仅此而已。但"你到底需要什么样的系统、想要什么样的 spec"——这件事很难完全靠 AI 解决，需要有经验的人。
他举的例子是 fault model：你设想故障长什么样再建容错系统，"但明天你发现基础设施里有些不在你故障模型里的故障怎么办？定义这个 spec 其实没那么容易。"
- SDD（specification-driven development）（[01:20:00]）：先写形式 spec，之后每次让 AI 写东西都能验证它满足 spec——"这样不论 AI 做了什么，最终产出都是可验证的"。
三、SREGym 与 benchmark 方法论¶
- 数字（[01:02:52]–[01:03:52]）：102 个真实运维场景，一年前 agent 只解出 11.4%；他说用今天的模型重跑"会接近 90%"。⚠️ 他主动说明这是学生主导的项目。
- 能力跃迁的时间点（[01:03:52]）：2025 年底到 2026 年初有一次本质性飞跃；今年又有一波。此前的限制是推理幻觉高、上下文不够大。
- ⚠️ benchmark 方法论（[01:04:52]）：
好的 benchmark 是能度量 AI 边界的。AI 很弱时做一个极难的、一个都做不出来，这个 benchmark 不好；AI 能做 90% 的，也基本没用了。最好的是 AI 能做 30%–40%。
- ⚠️ 真正的挑战是保真度（[01:04:52]–[01:06:53]）：benchmark 只能是小环境（三五个节点），与 Meta 那种超大规模差别很大。从大系统做成小系统必然要扔东西——扔掉的如果重要，模拟器就没用了；什么都想留，就没法变小。而你必须要小的，因为要做 RL。
- ⚠️ 与 coding benchmark 的对照："coding benchmark 是离线的，你不停生成代码就行。SRE 太实时了——你解决之后它真的修好了线上 bug 吗？整个反馈过程是在线的。"
- 他们的做法（[01:06:53]）：让本科生（REU 项目）读 Cloudflare 一类公司公开的故障 postmortem，在小模拟环境里复现，再测 AI。发现是相比最基础的故障，真实故障对 AI 构成的挑战完全不同。
四、AI 当 SRE：能力不是问题，"谁来指导"才是¶
- 他对前沿模型评价很高（[00:58:50]）："基本上任何系统任务，如果你告诉 AI 怎么做，AI 基本都能做。关键问题是你怎么去做，以及成本是多少。"
- 人的角色（[00:59:50]）："AI 就像一个很聪明的人。假设你公司有极多的人、个个勤奋，你仍然需要告诉他们什么才是对的事。" 落到操作上就是给初级工程师示范什么叫好的工作：怎么权衡、怎么拆解任务，然后让 AI 做重复的部分。
- ⚠️ 由此推出的教育问题，以及他自己承认无解的那一半（[01:00:51]–[01:02:52]）：既然是有经验、有品味的人去指导 agent，那么——
一个应届生怎么成为这样的人？这个训练与指导的过程没有了，我认为这对当前的 CS 教育是巨大的冲击。
- 他的乐观答案：学生用 AI 练学习、练研究，自然能到这个水平。
- ⚠️ 他自己拆掉了它：① 你太 junior，品味和指导不够，AI 的输出可能给你一些不高水平的东西；② 这些岗位越来越少——原本人是通过一个个小岗位慢慢爬上去的。
- 结论的两半："人仍然是非常重要的一环，建议与导师这类东西不会被 AI 取代"；但对市场萎缩——"这是一个非常真实的问题，但我其实不知道怎么解决。"
五、终局设想，以及把 ROC 整个翻出来¶
- ⚠️ 他对"理想的系统"的定义是从可靠性出发的（[01:23:03]）：
一个可靠的系统，是在未来至少 80% 的用户是 agent 的情况下仍然可靠的系统。而 agent 会出错、会幻觉、会跑偏——你的系统怎么容忍这些，并且给出反馈？因为 agent 也很聪明，只要你给它反馈，它第二轮就会做得更好。
- ROC（Recovery-Oriented Computing）（[01:24:06]–[01:29:06]）：约 2000 年 David Patterson 牵头的斯坦福—伯克利项目。
- 核心前提：系统必然会挂——"即使你把全部资源都投到测试和形式化验证上"。所以应该在恢复上大量投入。
- ⚠️ 实证发现：故障中占比最大的一块来自人为错误——操作员失误，不是硬件。 Jim Gray 在 Tandem Computers（产品线 NonStop，目标是造一个永不停机的系统）做的实证研究得出同样结论。
- 两个想法：system-wide undo（难以泛化，最后只做了一个可撤销的邮件服务器，论文发在 USENIX ATC）与 microreboot（"70% 的恢复机制就是重启"，但工业系统重启昂贵——缓存、TLB 全没了；所以只重启那一个组件）。
- ⚠️ 今昔对照："今天这个想法体现在微服务和 serverless 里——你可以 microreboot 单个微服务。这个想法其实已经活在实践里了。"
- ⚠️ 他的主张：在 agent 时代把这些经典原则重新拿出来直接复用，问哪些仍有价值、哪些不再需要，"这样就不必为每一条旧约束做优化，而能为 AI agent 设计一个好得多的系统"。被问"agent 的每一个操作都能被撤销"是否可行，他答"完全可以做到，这在理论上并不难，只是有没有人愿意做"。
- ⚠️ 他给的现实约束："现在 AI 系统的一大挑战是发展太快，很少有人愿意专注一两年去建一个系统。"
六、为什么可靠性与安全终于能拿到资源¶
- ⚠️ 历史解释（[01:31:10]）：
二三十年前，可靠性和安全从来不是 first-class 原则，因为它们不挣钱——只有性能挣钱。可靠性你只是担心别亏钱，所以可以靠别的办法达到：买保险，或者写一大堆（永远不完备的）测试用例给自己信心。
- ⚠️ 翻转的原因是 agent："如果你让 agent 主导做很多事情、包括写代码，那可靠性和安全就是最大的问题，而这不是靠把测试用例规模堆上去就能解决的。所以这是一个很好的机会，可靠性与安全的研究者可以拿到很多资源。"
- ⚠️ 他认为这对系统研究是结构性机会的另外两条（[00:21:25]–[00:23:26]）：
- 重设计的成本终于有人愿意付——"过去你想从根本上重新设计一个系统，成本很高，不是所有人都愿意投"。
- 评价标准变了——"过去你做一个系统只能处理一类 workload，评委一定会以'不够通用'拒掉你的论文。现在我就做一个 IO 性能特别好的系统，很多人就会很兴奋，它的经济市场特别大。"
七、对研究与学术生态的看法¶
- ⚠️ 他主张取消最佳论文奖（[00:13:21]–[00:15:21]）：他自己拿过、也当过 SOSP 最佳论文评审委员。"最佳论文这件事非常随机、非常主观，对我来说完全不能代表一篇论文的质量。" 机制是：拿到提名通常只意味着某一位评审特别喜欢你的论文并提名了它。
- 核心论点："有这些论文奖，实际上让大家不去好好做研究。如果把最佳论文去掉，大家就会去做自己最喜欢的研究，那是最好的状态。"
- 被问会不会得罪人，他答"我真的不担心"，并说已在会议上向很多人表达过。
- ⚠️ 他反对"先读 100 篇论文"（[00:35:34]）：转述导师的激进观点——"每篇论文都非常有偏见，只是作者自己的视角"；顶会评审严格，所以"大家写论文时用了很多技巧，不一定那么诚实"。他自己的比喻是："很多论文就像 feed，你消费太多 feed，大脑就麻木了，然后就没法创新了。" 替代方案是从真实问题出发，而不是读人家的 limitations 一节然后写下一篇。
- ⚠️ 反对把论文简化成"摘要 + 引言 + 与 agent 的对话"（[00:41:37]–[00:44:41]）：他承认如果贡献是一个好用的 artifact，也许摘要就够了；但"很多研究其实是一个思考的过程，因为研究的本质是理解世界"。他引 Leslie Lamport——"如果你不把东西写下来，你其实没法把它想透"。
- ⚠️ 他对"为什么现在有人提这个"的诊断：AI 让生产力提高、投稿暴增（系统圈"过去一年可能只有 200 篇投稿，现在变成 1000 篇"），而原有的评审组织方式不可扩展。"我们该反思的是怎么让这个系统 scale 到当前投稿量，而不是把它简化成另一个系统——把写作那部分、思考那部分去掉，研究的本质就被破坏了。"
- ⚠️ AI 时代研究的门槛变了，本质没变（[00:43:41]–[00:45:42]）："过去那种想法不算特别有意思、但涉及大量工程工作的研究，现在相对困难了，因为 AI 能帮你做这些。" 但——"研究的本质没变。好的研究者仍然是好的研究者。陶哲轩仍然是陶哲轩。"
- ⚠️ 对"AI 提升 100 倍"的反问："问题是你的 baseline 是多少？如果你的能力是 0，乘 100 还是 0。"
- ⚠️ "fight dragons, not windmills"（他主页上的话，[00:49:45]–[00:51:47]）：龙是真问题，风车是假问题。
- 他的配套观点："没有小问题，只有没被深挖的问题。" 系统领域的根本问题就那么几个——怎么推理并发、怎么推理异步、怎么推理非确定性行为——"解决了这些，上层的问题都解决了"。
- 给学生的操作建议：从一个相对具体的小问题开始，不要 boiling the ocean；尽量往深挖，挖到哪算哪，再做下一个项目。
- ⚠️ agent 取代不了导师（[00:38:36]）："agent 是一个相当冷的东西……不是那种体贴或者周全的东西。" 它能提升编码与系统构建的生产力、也能帮你想点子，"但最后你仍然要自己搞清楚哪些能做、哪些不能做"。
- ⚠️ 对 AGI 讨论的态度（[00:39:37]）："想 AGI 实现之后会发生什么，对我来说是相当浪费时间的事。对我来说就像在想世界末日之后该做什么——想想挺好玩，但别太当真。"
八、教学、职业与个人方法论¶
- ⚠️ 他的操作系统课（[00:52:47]–[00:56:50]）：UIUC 把它拆成两门——系统编程（除 kernel 外的一切：并发、进程控制、内存控制；作业是写 malloc、写 shell）与 kernel 编程（他教的这门）。
- ⚠️ 他对这门课价值的判断很反常识：上这门课的学生毕业后真去做 Linux 开发的"不到 10%、可能不到 5%"；95% 之后是去 hack Kubernetes 或建 AI 基础设施。
- 那教了什么："kernel hacking 只是一个媒介，他们获得的技能是怎么管理这种复杂度。" 此前所有课的大作业都是从零写小东西（小数据结构、小算法、小 malloc、小 shell）；而这门课要你去 hack Linux——一个非常复杂、非常脏的东西，一个学期根本不可能完全搞懂。那在这个过程里你怎么往前推进？
- 他把它接到自己在 Facebook 的经历上：面对一个巨大代码库，要在一个月内推进并建出东西，就必须做大量抽象、理解复杂度、并仍然能往前推进——而且文档没有、代码很 hacky。
- ⚠️ 落点："如果一个学生上完这门课，能获得面对一条凶龙、或者面对一个并不完美的世界的信心，我认为这就是这门课教给他们的最大技能。我不是想把 100 个人都训练成 kernel hacker。"
- ⚠️ 对"还要不要学 CS"（[00:56:50]）：他同意市场会萎缩——"过去一些非常简单的任务也需要雇一个 CS 本科生，现在 AI 能做"。但"如果你说 OS 会消失，我不认为有这个可能……整个现代社会都在构建大规模计算机系统"。
- 学术界 vs 工业界（[01:38:18]–[01:48:22]）：
- ⚠️ "学术界的工作是推进前沿。你今天推进它，AI 明天可能就学会了。但除非我们持续推进那个前沿，AI 就没有新东西可学。" 且资源变少（部分因政府干预）意味着更要追真正根本的问题。
- ⚠️ "学术界已经不是 70 年代的学术界了。当年美国可能只有五台计算机、都在学校，学校做什么工业界立刻跟。现在工业界常常完全领先学术界——我读博时 Google 已经做出 MapReduce 和 Bigtable 才发论文，然后成千上万篇论文去优化它们。"
- 实习：强烈建议，但"去了实习还按学校那套做，显然不是好做法"。他学生 Xudong 在沃尔玛实习的头两周逮人就问"你们公司最重要的问题是什么"，拿到十几个答案——"很多人没法把它组织成一个研究问题，但每个人都会诚实地告诉你他认为最重要或最难的问题是什么"。
- ⚠️ 选工作的唯一标准："如果我在这个岗位做五年，我能学到什么技能、培养出什么能力？回答了这个问题，下一步就非常清楚了。" 以及"我该和谁一起工作"。
- ⚠️ "学术界是一个非常标准化的地方——美国最好的学校和一所普通学校其实差别不大，教职就做三件事：教学、研究、带学生。但工业界不同公司不同团队差别极大。"
- ⚠️ 他导师的那句话："在计算领域，你的第一份工作不是你永远的工作。别为第一份工作纠结，把它当成一个学习过程。如果你真的学到了，下一份工作会更好；如果没有，再高的薪酬包也挡不住你两年后被裁。"
- ⚠️ "工业界最大的危险是拿到一个岗位然后停止学习。学术界的好处是它逼着你学——你得带学生、申经费、承担各种责任、还要教课。"
- 学术界真实的缺点："大家都很穷，所以如果你真的需要钱、家里需要钱，这可能不是特别好的选择。"
- 给博士生的三条建议（他自称"所有建议都是坏建议"，[01:49:23]–[01:51:24]）：
- 找到一个你真正在意的问题——"每天早上刷牙时照镜子：你是兴奋地想继续做这个问题，还是想'糟糕，我又得回办公室搞这个'？" 他说这件事真的很难，可能要一两年甚至三年。
- 发展出一套靠谱的研究方法——"研究不同于工程，往往没有捷径。速度本身不重要，速度可以用时间补。但方法对了，你最终会到。"
- 持续打磨技能栈——"时间精力有限，你不可能什么都做。知道要做什么之后，就有意识地培养做好它所需要的技能。"
- ⚠️ "系统研究不是纯理论，不需要非凡的天才。把这三件事做对，任何人都能做系统研究。"
- 学术休假为什么去伯克利（[01:33:13]–[01:38:18]）：休假制度的用意是"每个机构都有自己的约束与偏见，待太久就很难跳出框架思考，你会把一切当作理所当然"。
- ⚠️ 他去年推迟了一年："去年特朗普政府大幅削减 NSF 经费。UIUC 是全美最大的公立大学之一，联邦经费的陡降给学校带来巨大压力……系里有相当程度的焦虑，而我感到那种焦虑蔓延到了很多博士生身上——他们看到经费削减，再加上 AI 的冲击，大家都很紧张。我觉得在那个当口离开不合适。"
- 为什么是伯克利："伯克利的研究文化与 UIUC 截然不同，某些方面甚至是相反的。" —— "我本可以去一所更像 UIUC 的学校，它也许很出色，但如果文化太相似，去那儿的意义是什么？"
- ⚠️ "研究是一件美的事，而美的事没有单一标准。伯克利的风格与 UIUC 不同，UIUC 的风格与 MIT 也不同。这是好事，这些路子都应该能共存。"
- 他给其他教授的实际建议：学术休假的访问者不会给接待机构带来什么负担，反而是一个可以交流的同事，"多数大学非常欢迎，机会比你以为的多"。