以太坊网络团队发布了一系列由化名为 big_tech_sux 的 Vyper 核心开发者撰写的客座文章，探讨在人工智能飞速发展的时代，形式化验证所扮演的角色。
作者认为，大语言模型的进步，使得对程序正确性进行数学证明变得更为可行。而对于管理着数十亿美元资金的智能合约而言，形式化验证正逐渐成为一种必需品。
人工智能正在改变软件验证方式
该系列文章解释说，形式化验证是一种数学方法，它能够证明程序在所有可能执行场景下的正确性，而不仅仅局限于测试覆盖的那些场景。
作者以函数 f(x) = x/2 为例，指出可以数学证明其结果永远不会超过输入值。
他表示，这种方法能够发现极其罕见的、几乎不可能通过常规测试检测出的错误。
“形式化验证可以发现千万亿分之一概率的事件，这种事件在测试期间永远不会出现，但却可能导致灾难性的故障。”作者指出。
同时他也承认，直到最近，运用这种方法仍需要庞大的专家团队来创建程序的数学模型并进行复杂的证明。
在这位开发者看来，随着现代大语言模型日益接近通用人工智能，这一过程已得到显著简化。
然而，作者也强调，即使借助人工智能，形式化验证仍然是一个复杂且耗费资源的过程。特别是，将程序代码转换为形式化模型时可能包含不精确之处，这会影响到结果的可信度。
人工智能的发展正在改变攻防平衡
文章中指出，人工智能的发展同时提高了防御者和攻击者的效率。
作者提到了一个案例：尚未发布的 OpenAI 模型曾发现了可以绕过多层防护的零日漏洞。
在此背景下，作者表示，形式化验证能让优势向防御方倾斜。
“虽然攻击者只需找到一种输入序列来攻破系统，但防御者可以利用形式化验证来证明系统对所有可能的输入都具有稳定性。”他强调道。
正因如此，对于像管理着用户数十亿美元资金的智能合约这样的关键软件来说，形式化验证正成为“一种必要前提，而非可选项”。
值得注意的是，这延续了以太坊联合创始人维塔利克·布特林先前关于使用人工智能进行代码形式化验证的讨论。
end-content
