Combining Mechanical and Agentic Specification Inference for Move
本文提出了一种面向 Move 证明器的规范推断工具，该工具将可靠的弱前置条件分析与代理式编码命令行界面协同结合，以自动生成并优化验证规范，在有效减少手动样板代码的同时，能够处理循环不变式和结构不变式等复杂属性。
原始论文采用 CC BY 4.0 许可（http://creativecommons.org/licenses/by/4.0/）。 这是对下方论文的AI生成解释。它不是由作者撰写或认可的。如需技术准确性，请参阅原始论文。 阅读完整免责声明
想象你正在建造一座复杂的房子（一个名为"Move 智能合约”的软件）。你希望确保这座房子是安全的：门只能用正确的钥匙打开，屋顶永远不会坍塌，房内的金库能妥善保管钱财。
为了证明房子是安全的，你需要编写一本详细的“规则手册”（称为规范），精确解释房子的每一部分应如何运作。手工编写这本规则手册极其繁琐、枯燥，且容易出错。这就像试图为房子里的每一块砖都写一份法律合同。
本文介绍了一种新工具，它像一个超级智能的建筑助手，帮助自动编写这本规则手册。它结合了两种截然不同的助手：一个刚性机器人和一个创造性人类。
两位助手
刚性机器人（机械分析）：
将其想象为一个超级精确的计算器。它查看蓝图（代码），并机械地计算出维持房子屹立所需的最小绝对规则。它擅长发现显而易见的事情，例如“如果你拉动这个杠杆，门就会打开”。然而，它在处理复杂的循环任务时会陷入困境（就像一名沿着巡逻路线行走的保安）。它不知道保安为什么绕圈行走，也不理解其中的模式；它只看到移动，因而感到困惑。创造性人类（AI 代理）：
这就是"Claude Code"人工智能。它擅长理解模式、习语和高层概念。它可以观察那名保安，然后说：“啊，我明白了！保安正在按顺序检查每一扇门，且已检查的门数量总是在增加。”它非常擅长编写“循环不变式”（针对重复动作的规则），而这些是机器人无法推断的。但是，AI 有时会过度发挥创意，编造出实际上与蓝图不符的规则。
它们如何协同工作
该工具将这两者置于一个循环中，利用“模型上下文协议”（MCP），这就像一套对讲机系统，将它们与施工现场连接起来。
- 机器人启动： 它扫描代码并写下基本的事实（“最弱前置条件”）。它说：“好的，我们知道如果你拥有钥匙，门就会打开。”
- 人类填补空白： AI 查看机器人的工作，然后说：“我注意到这里有一个循环。让我猜测一下模式：计数器每次增加一。”它添加这些高层规则。
- 裁判进行检查： "Move Prover"充当严格的建筑检查员。它接收合并后的规则手册，并尝试证明其正确性。
- 如果规则有效，那就太好了！
- 如果规则失败（例如，AI 猜错了模式），检查员会将一个“反例”发回给 AI。
- 修正： AI 阅读检查员的备注，意识到自己的错误，并重新编写规则。这一过程反复进行，直到检查员满意为止。
论文中的现实世界示例
作者在三种类型的“房子”上测试了该方法：
- 搜索引擎： 一个在列表中查找特定项目的函数。机器人理清了基本逻辑，但 AI 必须猜测“迄今为止已检查的项目数量总是小于总项目数”。
- 数学问题： 一个计算幂（如 ）的函数。机器人处理了数学运算，但循环部分很棘手。AI 必须发明一个“辅助函数”来解释乘法的模式，然后团队必须添加一个特殊的“证明提示”（就像给检查员的作弊小抄），以证明数学运算不会失控。
- 银行转账： 一个将资金分配给两个人的函数。这涉及更改“全局状态”（银行的账本）。AI 必须精确追踪资金如何从一个账户转移到另一个账户，确保在过程中没有资金被创造或销毁。
为什么这很重要
在此之前，编写这些规则手册是一个巨大的瓶颈。这就像雇佣一名律师为房子里的每一颗钉子都写一份合同。
- 机器人处理人类讨厌做的枯燥、机械的数学运算。
- AI处理机器人不擅长的模式识别。
- 检查员确保两者都不会撒谎。
结果是一个系统，开发者可以询问 AI：“为这段代码编写安全规则”，而在机器人的引导和检查员的核查下，AI 能够比人类单独完成时快得多地生成经过验证的安全规则手册。
核心结论
这并非一把能完美解决所有问题的魔法棒。AI 仍然需要特定的“技能”（关于如何行为的指令）来引导，以避免走捷径。但它代表了重大进步：一种伙伴关系，其中机器处理逻辑，AI 处理直觉，形式化验证器确保真实性，所有这些都协同工作在开发者自己的编码环境中。
您所在领域的论文太多了？
获取与您研究关键词匹配的最新论文每日摘要——附技术摘要，使用您的语言。