AI4Math · 开场主旨 · Dawn Song

来源： 开场主旨 · Dawn Song 播客： ICML 2026 · AI4Math 分类： AI 研究 原文发表： 2026-07-11 纪要生成： 2026-07-13

基本信息

• Workshop：3rd AI for Math Workshop — Toward Self-Evolving Scientific Agents
• 类型：Opening Keynote（开场主旨，列于 Opening Remarks 内；由组织者 Haocheng Wang 主持并做 workshop 概况介绍后，邀请 Dawn Song 做开场）
• 题目：Building Provably Secure Systems with Frontier AI（用前沿 AI 构建可证明安全的系统）
• 讲者：Dawn Song（UC Berkeley 计算机科学教授；Berkeley Center for Responsible Decentralized Intelligence 主任；MacArthur / Guggenheim Fellow，ACM/IEEE Fellow）
• 真实时段：约 08:22–08:40（KST，7/11）

一句话概括

从网络安全视角论证前沿 AI 是双刃剑、短期内更利于攻击方；主张走 "secure by construction / by design" 路线，用形式化验证 + AI 自动定理证明 + 程序合成来生成可证明安全的代码，把 AI 的天平扳回防守方。这是 AI for Math（尤其定理证明）在安全领域的重大应用动机。

开场：本届 workshop 概况（主持人 Haocheng Wang）

Dawn Song 之前，组织者 Haocheng Wang 先做了开场并介绍 workshop 数据（这些数字对了解本届会议规模有价值，一并记录）：

• 投稿量 346 篇，是去年两倍多；且投稿量逐年翻倍（30 → 172 → 346），社区动能明显。
• 接收 210 篇，接收率维持约 2/3。为在投稿翻倍下守住标准，采用 reciprocal reviewing（互惠评审）政策：投稿作者须担任审稿人。配 6 位 program chair、42 位 area chair、3355 位审稿人；每篇至少 2 审、超 82% 得 3 审以上。
• 颁 10 篇 paper award（史上最多）。
• 主题分布（按作者关键词）：自动定理证明约占 1/4（最大），数学应用约 20%；把形式化相关（定理证明、自动形式化、形式验证）合并则超 40%——是社区"重心"。
• 4 条 challenge track：Track 1（FormalRx，评自动形式化是否忠实保留数学含义，是主持人本人的工作，已有两支队伍在复现中即超基线）；Track 2（TCS proving in Lean，已有非平凡算法题被多队证出，如 splay tree 的更强界、搜索算法运行时间界）；Track 3（SeePhys Pro，依赖视觉输入含手绘图的物理推理，投稿最多、超 860）；Track 4（端到端自动形式化 + Lean 证明生成，SNU 提供）。挑战总计 506 名参赛者、2300+ 次提交，是史上最大 challenge 规模；四赛道冠军将于下午首场展示。

随后主持人介绍全天日程，并邀请 Dawn Song（UC Berkeley，可信 AI 与 AI for science 先驱）做开场主旨。

背景与动机

Dawn Song 先致歉迟到（在另一 workshop 演讲）。她说开场目的是"搭台"、说明为何 AI for math 重要：后续多数报告聚焦数学领域，而她要讲一个很重要的方向——用 AI 定理证明帮助构建可证明安全的系统。

大背景：继"agent 元年"后，今年 agent 继续爆发式增长。她认为在享受 AI/Agentic AI 红利的同时，必须关注广谱 AI 风险；并个人坚信网络安全是最大的 AI 风险域之一，理由：攻击动机本就多样、今天已造成巨大损失，而 AI 能显著降低攻击成本、扩大攻击规模。核心问题：前沿 LLM 作为双用途（dual-use）技术，会更利于攻击方还是防守方？要回答，须逐阶段分析"攻击杀伤链"与"防御链"。团队为此建了业界领先的 benchmark 来评测前沿 AI 在各阶段的能力。

主要内容

AI 攻击能力正快速抬升（benchmark 证据）

• CyberGym：团队近期工作，被多数前沿实验室采用，用于评测前沿 AI 发现漏洞和生成 PoC（proof-of-concept，即能触发漏洞的输入）的能力。曲线显示能力快速上升：较早的 Claude 模型曾登顶 leaderboard（并在每个主流 OS 和 web 浏览器中发现 0-day）；更近期 GPT-5 cyber 拿下 CyberGym 榜首，显示能力进一步提升。
• ExploitGym：CyberGym 只测"找漏洞 + 生成 PoC"，还缺关键一步——给定已找到的漏洞和 PoC，AI 能否自动生成可用的 exploit（真正转化为攻击，如任意代码执行）。ExploitGym 与多个前沿实验室及合作者共建，含三类真实程序：用户态程序、浏览器 VA 引擎、Linux 内核。结果显示：即使这剩下的关键一步，前沿 AI 现在也很能干——能在 ExploitGym 上自动生成 exploit，更令人担忧的是这些 exploit 能绕过标准防御。
• 鉴于重要性，团队近期发起 Frontier AI Cyber Security Observatory，联合社区对前沿 AI 网络安全能力做持续监测。

攻防不对称：短期内 AI 更利于攻击方

作为 dual-use 技术，前沿 LLM 影响巨大，网络安全域已到"拐点"。不幸的是：

• 等价类（equivalence classes）问题：同一套防御能力，因 dual-use 本质也能助攻。
• 攻防天然不对称：团队近期分析表明，短期内 AI 利于攻击方多于防守方——攻击者只需找到一个漏洞、一次成功 exploit 即得手，防守者却要在攻击者之前发现并修补所有漏洞。

由此的大问题：社区能否共同发展新机制，把 AI 扭转为"助防多于助攻"？

三代防御范式

过去数十年（含她自己与安全社区的工作），防御范式历经三代：

1. 反应式防御（reactive）：攻击发生后检测→阻断→事件响应。但防守者总在追赶，攻击者借 AI 可更快、更隐蔽、更大规模发动攻击——仍是攻击方受益更多。
2. 主动式的 bug finding（proactive）：仍存结构性不对称，偏向攻击方（攻击者只需一个洞，防守者要补所有洞）。
3. secure by construction / secure by design（本讲主张）：不做 bug 检测/反应式防御，而是从设计上构建可证明安全的程序与系统，用形式化验证给出可证明的安全保证——这能提供有利于防守方的结构性不对称。

已进入"形式化验证系统"时代，但受限于证明工程

已有一批系统被完整形式化验证：微内核、文件系统、编译器、密码库等。但这些系统未被广泛使用，主因是证明工程极其耗人力——如 seL4 花了数十"证明工程师·年"，且一旦改代码就得改证明。希望借 AI 自动化证明工程。她指出：早在 7–8 年前，她的组（与 OpenAI 的 Ilya 等合作）就是最早用深度学习自动化定理证明的团队之一，当时已能自动化某些证明步骤；随着 LLM 与前沿 AI 发展，她坚信已到用前沿 AI 自动化定理证明（用于形式数学推理和程序验证）的拐点。团队有一篇 overview 论文，给出了推进前沿 AI 自动化定理证明的路线图——目标是让 AI agent 不只是下棋，而是能帮助自动化定理证明、结合程序合成来生成不含大量漏洞的"可证明安全代码"。

可验证代码生成：Verina 与 Vero

• 任务定义（verifiable code generation）：给定任务描述，不只生成代码，还要生成规范（specification）并生成"代码满足规范"的证明。
• Verina：团队构建的综合基准。一年前刚建时，前沿模型整体表现很差；但随后（尤其众多做自动定理证明的创业公司推动）进展飞快，如今 Verina 已被完全饱和。
• Vero：为进一步度量并推进领域，团队近期推出更难的 repo 级可验证代码生成基准。核心问题："AI agent 能否构建经过形式化验证的软件仓库？"可评测两种设定：生成"代码 + 证明"，或给定代码"只生成证明"。评测显示：对这类更有挑战的任务，前沿 agent 在 repo 级仍很吃力，仍有大量提升空间。她欢迎大家试用 Vero 并合作推进。

结语与邀约

希望社区共同快速推进，发展出能自动化定理证明与程序验证的强 agent，结合程序合成生成可证明安全的代码。鉴于前沿 AI 在网络安全上的能力快速上升且 dual-use，这件事更紧迫、更关键。演讲末尾她邀请大家参加 AgentX Summit（UC Berkeley，8/1–8/2；去年首届 2000+ 现场、40000+ 线上，今年预计 5000+ 现场、数十万线上），其中有 AI for Math 专场，可现场或线上参加。

关键结论 / Takeaways

• 网络安全是最大 AI 风险域之一；前沿 AI 作为 dual-use 技术，因等价类问题与攻防不对称，短期内更利于攻击方，形势紧迫。
• 破局方向是 secure by construction：形式化验证 + AI 自动定理证明 + 程序合成 → 生成可证明安全的代码，提供有利防守方的结构性不对称。
• 度量基准是关键抓手：CyberGym / ExploitGym（攻击能力）、Verina（已饱和）、Vero（repo 级，仍是硬骨头）。这正是 AI for Math / 定理证明的重大应用动机。

Q&A / 讨论亮点

开场主旨，无独立 Q&A 环节；结束后主持人衔接第一场 invited talk（Junqi Liu）。

名词 / 引用

• CyberGym：评测漏洞发现 + PoC 生成能力的基准（Claude 曾登顶，GPT-5 cyber 刷新）。
• ExploitGym：评测自动生成可用 exploit 的基准（用户态/浏览器 VA 引擎/Linux 内核；exploit 可绕过标准防御）。
• Frontier AI Cyber Security Observatory：前沿 AI 安全能力持续监测计划。
• Verina：可验证代码生成基准（已饱和）。
• Vero：repo 级可验证代码生成基准（前沿 agent 仍吃力）。
• secure by construction / by design：以形式化验证从设计上保证安全的第三代防御范式。
• seL4：形式化验证微内核，证明工程耗"数十工程师·年"的典型。
• AgentX Summit：UC Berkeley 8/1–8/2，含 AI for Math 专场。

原文发表：2026-07-11  ·  纪要生成：2026-07-13