MIT 11月17日办形式化验证论坛 防超智能黑客

时间：2026 年 11 月 3 日 21:48（北京时间，美国东部时间同日 9:48）。麻省理工学院教授 Adam Chlipala 在自己的博客 Structure and Guarantees 上发出公告，并在 LessWrong 同步转载；论坛本身安排在 11 月 17 日 16:30 至 18:30（美东时间），17:30 起是招待会。 地点：美国马萨诸塞州剑桥市，麻省理工学院 32-155 教室（MIT Campus, 32-155, Cambridge, MA）。 人物：主持人 Adam Chlipala，麻省理工学院计算机科学教授（Arthur J. Conner 1888 届教授），Nectry 联合创始人，MIT CSAIL 主页上写着他的背景在编程语言与形式化方法，研究涉及对象能力系统、proof-carrying code、类型系统与整体程序优化编译器。嘉宾三人：Byron Cook，亚马逊云科技副总裁兼杰出科学家，2016 年创立 AWS 自动推理团队（Automated Reasoning Group）；Noah Evans，Draper 实验室首席技术专家，此前在桑迪亚国家实验室带形式化方法团队；Armando Solar-Lezama，麻省理工学院计算杰出教授、CSAIL 副总监兼首席运营官，领导计算机辅助编程组。 事件详情：麻省理工学院 Schwarzman 计算学院下属的 SERC（Social and Ethical Responsibilities of Computing，计算的社会与伦理责任）项目主办一场名为 Provably Secure: Math Against Superintelligent Hackers 的论坛。官方活动页给出的设问是：形式化验证能不能保证 AI 智能体被约束住、找出全部某类安全漏洞、并对更强的 LLM 做到前瞻防御。Chlipala 在公告里把动机写得更直接：围绕 AI 智能体逃出约束、按构建者利益之外行事的担忧正在升温，而最新一批 LLM 在重要软件里找出安全漏洞的速度令人警觉。论坛想复盘的核心是形式化验证这项老技术的新前景，用数学证明程序行为，看它能不能用在关键计算基础设施上。Chlipala 还提出一个更硬的问题：当智能体写出的代码可能比我们更懂计算时，人们如何对用来核验它的规格本身建立信心。三位嘉宾的履历正好覆盖三个不同场景：Cook 的博士工作是把 CPU 与软件之间的接口形式化，此后长期做模型检验，2014 年加入 AWS 主导形式化验证落地，2016 年创立 AWS 自动推理团队，是目前把形式化方法用到企业规模最大的一股力量；Evans 从 IBM 与贝尔实验室的系统软件起步，加入桑迪亚国家实验室新组建的形式化方法团队，参与核武库相关硬件与软件的正确性和安全性证明，近期转到 MIT 附近的 Draper 实验室，继续做面向国防的密码与安全工程；Solar-Lezama 博士期间做形式化方法，提出的 program sketching 技术让自动化工具按数学要求自动补全代码空缺，之后进入 MIT CSAIL 教职，近年致力于把机器学习方法与逻辑方法结合起来做下一代工具。Chlipala 自己还写过几篇相关论证，包括对复杂系统做形式化验证能带来即插即用的安全收益、但仍要面对选对规格这一老问题，以及 AI 攻击者强到不能再依赖漏洞保密、应当习惯把所有代码反复重写；他也提到当前 AI 智能体的思考方式与人类相对接近，处在所谓简单模式，这种状态不会持续太久。注册免费、仅限线下参与、没有直播，会后录制视频稍后公开。 背景：形式化验证不是新东西，用数学证明程序行为在计算机科学里已有数十年历史，过去主要用在硬件、编译器与航空核电等高保证领域，近十多年才被推入大规模软件工程。AWS 自 2014 年起把形式化方法全面引入自身研发与运维体系，美国桑迪亚国家实验室等形式化团队则把国家实验室的软硬件正确性证明做到规模化。Solar-Lezama 的程序综合工作让程序生成第一次有了可验证的规格作为前提，Chlipala 的研究则一直围绕让程序更易证明正确展开。这条脉络此前主要在专业圈内讨论，2026 年以来 AI 智能体逃逸与 AI 自动找漏洞两类问题同时升温，把形式化验证重新推到公共议题前台——它提供的不是保证模型不作恶，而是保证程序在给定规格下不会跑偏。 影响：这场论坛的价值在于把一个长期偏哲学的争论拉到可工程化的层面。约束智能体、证明系统行为、清零某类缺陷，都是能写成规格并逐条验证的命题；反过来，它也把难度暴露出来——规格写错，证得再漂亮也只是给错误行为背书，Chlipala 把这称作形式化验证的经典坑。对开发者与安全团队，如果这类方法规模化，靠漏洞保密的安全模型将站不住脚，重写与证明会成为常态开销，Amazon、Sandia、Draper 这三类机构的存在说明这已不是纯学术议题。对 AI 安全政策讨论，多一个把数学证明当作工具的务实选项，与只谈模型行为评测的路线形成补充。 总结：麻省理工 11 月 17 日将举办一场把形式化验证与超级智能黑客放在一起谈的公开论坛，由 Adam Chlipala 主持，Byron Cook、Noah Evans、Armando Solar-Lezama 分别代表企业、政府实验室和 MIT 的三种实践路径。它承认了一个现实前提——最新的 LLM 已经在以惊人速度找出真实软件里的漏洞，因此安全不能再依赖漏洞保密。真正值得看的是它提出的工程问题：能不能用数学证明来保证智能体被约束住，以及当智能体写的代码比我们更懂计算时，如何相信我们写下的规格。论坛免费线下开放，不直播，视频会后上线。 常见问题： 问：形式化验证 AI安全吗？ 答：它保证的是程序符合你写下的规格，规格选错就等于给错误行为背书，这是形式化验证的经典坑。 问：形式化验证在AI中验证的目的是什么？ 答：本次论坛聚焦两点：保证 AI 智能体被约束在预期行为内，以及找出全部某类安全漏洞，扛住更强的模型。 参考来源： Adam Chlipala 在 LessWrong 发布的论坛公告原文，含三位嘉宾履历与议题设问 https://www.lesswrong.com/posts/wHgj3oPxqoDbdTvyK/mit-panel-provably-secure-math-against-superintelligent Chlipala 个人博客 Structure and Guarantees 的首发原文（Substack） https://stng.substack.com/p/mit-panel-provably-secure-math-against 麻省理工学院 Schwarzman 计算学院在 Eventbrite 上的官方活动页，含时间、地点、嘉宾头衔与活动说明 https://www.eventbrite.com/e/provably-secure-math-against-superintelligent-hackers-tickets-2004252101990 MIT CSAIL 的 Adam Chlipala 个人主页，载明其研究方向与形式化方法背景 https://www.csail.mit.edu/person/adam-chlipala MIT CSAIL 的 Armando Solar-Lezama 个人主页，载明其任 CSAIL 副总监兼首席运营官并领导计算机辅助编程组 https://www.csail.mit.edu/person/armando-solar-lezama Amazon Science 自动推理研究团队页面，对应 Byron Cook 创立的 AWS Automated Reasoning Group https://www.amazon.science/research-areas/automated-reasoning