想象一下，你正在用一套神奇的、具有自我修复能力的砖块来盖房子。这些砖块被称为“Rust”，它们之所以出名，是因为内置了一位安全检查员，拒绝让你建造任何不稳定的结构。如果你试图把窗户放在墙壁该在的位置，检查员就会大喊“不！”，并在你铺下第一块石头之前阻止你。这使得 Rust 在构建软件方面极其安全，能在崩溃和安全漏洞发生前就将其阻止。然而，有时一位大师级建筑师需要做一些检查员无法理解的事情——比如使用一种特殊的、危险的工具快速移动一根沉重的横梁。在 Rust 的世界里，这被称为“不安全代码”（unsafe code）。这就像是一个特许通行证，让你绕过检查员，但代价沉重：如果你犯了一个错误，整个房子都可能坍塌。为了保证房屋屹立不倒，你需要编写一本非常严格的数学“规则书”（称为规范），来证明如何安全地使用这些危险工具。但是，手工编写这些规则书非常困难、缓慢，且容易出现人为错误。

这就是 KaPilot 故事开始的地方。研究人员提出了一个简单的问题：我们能否教一个超级聪明的计算机大脑（AI）来为我们编写这些安全规则书？挑战在于，这些 AI 擅长写代码，但它们往往会模仿所见代码中的错误，而不是理解其背后的“意图”。它们可能会写出一本看起来很完美但遗漏了微小致命细节的规则书。这篇论文介绍了 KaPilot，这是一个协同解决这个难题的多智能体团队。它不仅仅是要求 AI “写一条规则”，而是让 KaPilot 扮演侦探、作家和严厉编辑的多重角色。它阅读建筑师的笔记（文档）、提取真正的安全规则、撰写草案、检查漏洞，然后通过严格的测试以确保其确实有效。其结果是一个能够自动为危险代码生成高质量安全规则的系统，使得无需人类专家亲手编写每一条规则即可更轻松地构建安全软件。

侦探、作家与编辑

把验证不安全 Rust 代码的过程想象成尝试为一辆没有刹车的高速赛车编写一份完美的说明书。如果说明书错了，赛车就会坠毁；如果说明书太模糊，驾驶员就不知道如何驾驶；如果说明书太严格，驾驶员就无法行动。

KaPilot 是一个多智能体框架，这只是一个高级说法，意思是一个由专门的 AI 角色组成的团队在协作。以下是他们各自的角色：

1. 侦探 (SafetyReq)： 在动笔之前，团队需要知道规则“应该是”什么样的。通常，这些规则隐藏在随代码附带的杂乱的人类编写笔记（文档）中。“SafetyReq”智能体充当侦探的角色。它阅读这些笔记，忽略废话，并提取出一份清晰、简洁的规则清单。这就像是将一段关于“不要按红按钮”的啰嗦故事转化为清晰的编号列表：“1. 不要按红按钮。2. 不要站在红按钮 5 英尺范围内。”这一步至关重要，因为它防止了 AI 仅仅是复制代码中的错误。
2. 作家 (SpecGenerate)： 一旦侦探有了清单，“SpecGenerate”智能体就会介入。它是负责将清单转化为计算机能理解的正式数学语言（具体来说是一种名为 Kani 的语言）的作家。它并不靠猜测，而是严格以侦探的清单为指南。
3. 编辑 (SpecPrecheck)： 在作家的草案交给最终负责人之前，“SpecPrecheck”智能体会对其进行审查。它是一位严厉的编辑，会询问：“你是否涵盖了侦探发现的所有要点？你的句子是否太弱了？或者太强了？”如果草案很粗糙，编辑会带着具体的修改意见将它退回给作家。这个过程会循环进行，直到草案变得稳固。
4. 测试司机 (SpecVerify)： 最后，“SpecVerify”智能体接过草案并将其投入现实世界的测试。它使用一个名为 Kani 的工具来模拟数百万种不同的驾驶场景，以观察赛车是否会坠毁。如果赛车坠毁了（验证失败），测试司机会准确告诉作家究竟为什么会坠毁，然后循环重新开始。

“洗牌与混合”策略

这是该团队真正聪明的地方。有时，AI 会生成几个不同版本的规则书。一个版本可能有一个完美的“起始”条件（前置条件）但“结束”条件（后置条件）较弱；另一个版本可能起始条件较弱但结束条件完美。如果你只是简单地选择其中一个，你可能会错过最佳组合。

KaPilot 使用了一种称为**“洗牌与蕴含”（shuffle-and-implication）*的策略。想象你有一副扑克牌，每张牌都是规则书的不同部分。团队会将这些牌进行洗牌，将一个版本中最好的“起始”部分与另一个版本中最好的“结束”部分混合在一起。然后，他们测试这些新的组合，看看它们是否比原始草案效果更好。这就像是从一辆车中取出最好的引擎，再从另一辆车中取出最好的轮胎，从而组装出一辆终极赛车。这确保了他们不仅仅是满足于一个“足够好”的规则书，而是寻找最好*的一个。

研究发现

研究人员在 124 段不同的不安全 Rust 代码上测试了 KaPilot。他们将其分为两组：

• 金牌集 (Gold Set，54 个函数)： 这些函数拥有由人类专家编写的“地面真值”规则书，因此团队可以检查 KaPilot 的工作是否正确。
• 极限集 (Ultra Set，70 个函数)： 这些函数没有人类规则书，因此团队只需检查 KaPilot 是否能生成任何可行的规则书。

结果令人印象深刻。对于金牌集，KaPilot 成功为 88.9% 的函数生成了可运行的规则书。更重要的是，在 57.4% 的情况下，它编写的规则书与人类专家的规则书一样好，甚至更好。对于极限集，它成功为 71.4% 的函数创建了可运行的规则书。

当他们将 KaPilot 与另一个名为 AutoSpec 的 AI 工具（已适配此新系统）进行比较时，KaPilot 完胜。它产生的通过测试的规则书多了 14.8%，且在语义等价或优于人类编写的规则书方面也提升了 25.9%。

为什么这很重要

论文指出，仅仅要求 AI “根据这段代码写一条安全规则”效果并不理想。AI 倾向于复制代码的缺陷或被复杂性搞混。通过将任务分解为专门的团队——一个读笔记，一个写，一个改，一个测——KaPilot 避开了这些陷阱。

研究人员还发现，人类笔记（文档）的质量非常重要。如果笔记含糊不清，AI 就会挣扎；但当笔记清晰时，KaPilot 就会大放异彩。他们还发现，他们的“洗牌”策略是关键要素；如果没有它，系统往往会停留在平庸的解决方案上，而不是寻找完美的组合。

简而言之，KaPilot 表明我们不需要在人类专业知识和 AI 速度之间做选择。通过将 AI 作为遵循严格逻辑过程的专业助手团队，我们可以自动化地为软件中最危险的部分创建安全规则，让数字世界变得更加安全。该论文并不声称解决了所有问题（一些复杂的循环仍需要人类帮助），但它证明了这种多智能体方法是实现自动化、可靠的软件验证迈出的巨大一步。