以太坊联合创始人维塔利克·布特林并不认为人工智能的进步最终会让网络安全变得本质上无法取胜。
布特林相信，相反的情况最终可能会发生：人工智能或许能为防御者提供所需的工具，让他们构建出从一开始就更难被利用的软件。
“一种越来越普遍的观点是，人工智能黑客意味着网络安全注定要失败。我不同意，”布特林周三在X社交媒体网络上发表了一篇篇幅很长、一如既往内容充实的帖子，其中写道。
据这位以太坊联合创始人称，一旦开发者开始充分利用形式化验证，网络安全自然会偏向防御者。
布特林还将这一信念直接与他自身在加密货币中的敞口联系起来，透露他大约90%的净资产仍留在加密货币中。
他主张，任何继续持有大量加密货币的人，实际上都在押注：尽管攻击者日益老练，仍然可以构建出足够安全的数字系统。
“如果人工智能能证明纳维-斯托克斯方程和费马大定理，那么人工智能就能把‘这个程序是安全的’这一陈述作为数学定理来证明，”布特林写道，他指的是纳维-斯托克斯问题和费马大定理。
他的论点基于形式化验证，这是一种用数学方法证明软件满足特定性质的方法。
布特林在5月的一篇文章中广泛探讨了同样的想法，他在文中将人工智能辅助的形式化验证描述为对安全关键型软件具有巨大变革意义的工具。然而，证明此类软件是安全的可能会被证明颇具挑战性。
定义问题
布特林以加密消息应用Signal为例，说明为什么这可能很困难。
攻击者可能会试图伪造消息、阻止消息到达、重放旧消息、攻陷服务器、操纵用于发现另一用户公钥的过程，或利用操作系统中的漏洞。
其他问题可能来自被破坏的数据库、恶意库、编译器，甚至硬件层面的信息泄露。
即使对话内容保持加密，攻击者仍可能得知谁在通信。因此，“安全”究竟意味着什么，其数学定义本身就可能变得极其复杂。
“所以……即便是定义也可能超过一千行代码，并且需要深入细致的思考才能弄清楚，”布特林写道。
攻击者与防御者
毫无疑问，能力更强的人工智能系统可以让发现漏洞变得更容易。
然而，机器推理能力的同样提升，也可能大幅降低形式化证明软件按照精心构建的安全规范运行的成本。
双方都会拥有人工智能。
