AI-Assisted Completion of CertiGC Proofs: An Experience Report
本经验报告详细阐述了如何利用 AI 辅助工具（Codex）通过围绕一个新的记录后向边不变性（recorded-backward-edge invariant）来重构验证过程以处理可变更新，从而在 Rocq 中稳定并完成了 CertiGC 已验证的分代垃圾回收器证明，在此过程中，人类专家专注于判定不变性并审计证明路径以确保正确性。
原始论文采用 CC BY 4.0 许可（http://creativecommons.org/licenses/by/4.0/）。 这是对下方论文的AI生成解释。它不是由作者撰写或认可的。如需技术准确性，请参阅原始论文。 阅读完整免责声明
想象一下，你是一位名为 CertiGC 的宏大、充满魔力的图书馆的总建筑师。这座图书馆不仅仅是存储书籍，它还是一个活生生的、呼吸着的系统，能够自动清理旧的、不再使用的书籍，以为新书腾出空间。多年来，图书馆一直遵循着一个简单的规则：“一旦一本书被放在书架上，就再也没有人会移动它，也不会有人写下指向新书的笔记。”这个规则让清洁人员的工作变得非常轻松。他们可以扫过书架，因为他们知道没有任何旧书会突然指向一本全新的书。
但随后，图书馆决定变得更加有趣。他们想要允许**可变（mutable）**更新：允许图书管理员在旧书中写下新的笔记，从而指向新到的书籍。突然间，旧的规则（“旧书不得指向新书”）被打破了。清洁人员的地图失效了。如果他们继续根据旧地图进行清扫，就会漏掉那些由新笔记所指向的新书，导致这些书被误扔掉！
这是一个关于一个团队如何使用一个超级智能的 AI 助手——名叫 Codex——来修复图书馆清洁地图的故事。但这里有一个转折：Codex 并不是凭空变出了一个新地图。相反，Codges 扮演了一个不知疲倦、极度有条理的实习生角色，它能够阅读成千上万页的内容，尝试新的想法，并一遍又一遍地运行“清洁模拟”。而一名人类专家则在一旁监督，说：“是的，这个想法可行，”或者“不，这违反了规则。”
核心问题：破碎的地图
原始地图依赖于一个“无后向边（No-Backward-Edge）”规则。把它想象成一个单行道系统，你只能在时间轴上向前行驶。但随着新的“可变”更新，你突然可以从一个旧社区向新社区进行“后向行驶”。旧地图说：“这是不可能的！”而新的现实说：“这种情况经常发生！”
如果团队试图强行让旧地图继续工作，他们就必须假装那些后向行驶从未发生过。这意味着图书馆只能是它那个“无聊版本”的正确体现，而无法实现那些酷炫新功能的版本。这不是目标。他们需要一个新的规则，承认后向行驶是可能的，但前提是必须将其记录在一个特殊的日志本中。
AI 的角色：不知疲倦的实习生
人类专家知道他们需要一条新规则：“每当一本旧书指向一本新书时，必须将其记录在‘被记住集合（Remembered Set）’日志本中。”
他们请求 Codex 协助构建证明，以确保这条新规则能保证图书馆的安全。Codex 不仅仅是写出了最终答案。它扮演了一个侦探的角色：
- 阅读代码： 它扫描了图书馆的蓝图。
- 提出规则： 它提出了“记录后向边（Recorded-Backward-Edge）”的概念（即日志本的想法）。
- 测试规则： 它将图书馆的清洁模拟（“Rocq 内核”）运行了数千次。
- 修复漏洞： 当模拟崩溃时，Codex 会调整其证明脚本，尝试不同的角度，然后再次运行。
人类专家的工作是最关键的部分：法官。Codex 可以提出一个规则，但必须由人类来决定这个规则是否真的符合图书馆的现实行为。例如，Codex 可能会建议：“让我们在最终报告中假装这个日志本不存在。”人类则会说：“不！日志本是真实存在的。我们不能隐瞒它。”
结果：一座整洁的图书馆
经过大量的努力，团队成功了。
- 修复方案： 他们用新的“记录后向边”规则取代了破碎的“无后向边”规则。
- 证明过程： 图书馆的清洁过程被证明是安全的，即使有了这些新的更新。最终的定理（“大证书/Grand Certificate”）对外界而言看起来仍然一样：“图书馆是整洁且有序的。”但在底层，其逻辑要聪明得多。
- 清理工作： 即使在主证明被接受之后，团队也没有停止工作。他们额外花费了时间（5 月 1 日至 5 月 3 日）审计规则，以确保没有旧的、错误的假设隐藏在代码中。他们移除了一个从图书馆旧的、无聊的版本中遗留下来的“陈旧（stale）”条件。
这告诉了我们什么
这篇论文表明，像 Codex 这样的 AI 工具在维护与修复方面表现卓越。当任务涉及以下内容时，它们可以成为人类专家的完美搭档：
- 传播不变性（Propagating Invariants）： 将一条新规则应用到庞大的代码库中，并确保它在每一个角落都有效。
- 清理工作： 修复混乱的证明脚本并移除旧的、无用的代码。
- 测试： 反复运行“模拟”（编译器），以观察微小的改动是否会破坏任何东西。
然而，论文非常明确地指出了 AI 无法独立完成的事情。
- 它并没有发现整个解决方案： 人类必须理解图书馆的语义，并决定应该采用什么样的规则。
- 它并没有取代人类法官： AI 可以提议一个规则，但必须由人类来验证该规则是否会意外削弱图书馆的安全保障。
- 它不是“魔杖”： AI 并不是一次性写出整个证明。它是一个“受监督的、由检查器驱动的”过程。人类始终在循环之中，引导着 AI，拒绝糟糕的想法，并确保最终结果确实是正确的。
数据统计
团队为此工作了一段时间。在“Codex 辅助阶段”（即 AI 进行繁重工作阶段），时间是在 2026 年 4 月 22 日至 5 月 3 日 之间。
- 在此期间，共有 51 次 git 提交（代码更新）。
- AI 进行了 13,305 次工具调用（如读取文件、运行测试或编辑代码等操作）。
- 人类给出了 415 条提示词（对 AI 的指令）。
- AI 在这个问题上花费了 59.3 个活跃小时。
论文强调，这并不是一个 AI 独自解决的“已解决问题”。相反，这是一次成功的协作：AI 处理了那些乏味、重复的检查与修复工作，而人类则提供了深刻的理解以及对真理的最终裁定权。最终的结果是一座安全、经过验证且准备好迎接未来的图书馆。
您所在领域的论文太多了？
获取与您研究关键词匹配的最新论文每日摘要——附技术摘要，使用您的语言。