图灵奖得主迪菲智源大会：形式化方法成研发重点

在2026北京智源大会开幕式上，图灵奖得主、美国国家工程院院士惠特菲尔德·迪菲（Whitfield Diffie）发表了一场极具深度的主题演讲。他直截了当地将议题定为《护AI智能体之安，御AI智能体之险》（Security For AI Agents, Security Against AI Agents）。这个方向正是当前AI安全领域最棘手的核心挑战之一。

迪菲的核心洞见在于：当前主流的“控制论”安全策略——即程序出错后再修补的被动响应模式——本质上是事后补救。他提出，未来应全力推进形式化方法（formal methods）的研究与落地，让程序从设计之初就能按照预期可靠执行，而非依赖反复打补丁。关键在于对比：密码系统由于规模极小，可以进行完整的形式化验证；然而典型的计算机程序——编译器、操作系统、应用乃至智能体——规模庞大，远超人工手动验证的极限。过去业界指望AI未来能自动完成验证，但迪菲尖锐指出，当前编程实践中对智能体的“限制”（Confinement）——确保智能体仅能访问授权资源——远未达标。这才是当前AI安全体系真正的薄弱环节。