Show HN: 形式化验证的多边形相交算法——Opus 4.8 的一次突破

背景

在计算几何领域，多边形相交（Polygon Intersection）是一个基础但极其复杂的问题。许多矢量图形编辑器都具备处理“多边形”（Multipolygon）相交的功能。一个多边形由一组多边形组件和多边形孔洞组成，每个组件和孔洞都由顶点列表定义，从而描述了一个二维区域（即内部点的集合）。

从数学上讲，这个内部点集可以通过从平面上每一点发射射线，计算射线与多边形边界的交点数量的奇偶性来形式化定义。给定两个多边形，我们需要构建一个新的多边形，其内部点集是输入两个多边形内部点集的交集。

然而，由于输入多边形的配置有无穷多种，且每个多边形的内部点集也是无限的，传统的软件测试无法穷尽所有情况。更重要的是，在没有形式化验证的情况下，代码中的“内部点集”仅仅是一种解释，无法在代码层面被精确表示。因此，确保算法在所有极端配置下（如共线、重叠、微小差异导致的拓扑变化）都能正确工作，一直是工程上的巨大挑战。

核心内容

作者宣布实现了首个形式化验证（Formally Verified）的多边形相交算法实现，并展示了近期大语言模型（特别是 Claude Opus 4.8）在这一领域能力的巨大飞跃。

形式化验证与 Lean 4

该项目的核心在于使用 Lean 4 证明助手对相交算法的规范进行了形式化描述和完全验证。这意味着我们可以保证，对于任何配置的多边形输入，其生成的内部点集确实满足相交等式。

• 验证范围：验证不仅涵盖算法逻辑，还包括许多看似显而易见的几何事实。例如，证明上述“内部”定义不依赖于射线方向这一事实，就耗费了数千行 Lean 代码。
• 人类审查最小化：仓库的设计旨在最小化人类审查的工作量。人类审查者只需阅读三个核心文件（DataStructures.lean, Defs.lean, MultipolygonIntersectionAlgorithmWithPreconditionCheck.lean），共计 87 行代码，这些代码主要设置了基本的几何定义。相比之下，实现算法的代码（即使未优化）已经超过了这个长度的两倍，且更为复杂。
• AI 自主生成：实现代码及其正确性的形式化证明（在 ...Proofs.lean 和 ...Impl.lean 文件中）完全由 AI 代理自主编写，未经过人类审查。但由于有 Lean 检查器作为最终裁判，人类无需信任任何大语言模型（LLM）的输出。

模型能力的演进：从 Opus 4.5 到 4.8

作者详细回顾了使用 AI 代理完成此项目的历程，突显了模型能力的迭代：

1. Claude Opus 4.5/4.6：这是作者首次尝试。Opus 4.5 是第一个能处理非平凡 Lean 证明的模型，但能力有限。它要求人类提供完美严谨的证明草稿，并将其转化为 Lean 代码。例如，证明“内部集定义与射线方向无关”时，作者必须将其拆分为许多小步骤，导致项目陷入停滞。
2. Claude Opus 4.7：能力显著提升，能够采取更大的步骤。它证明了“对于任意两个多边形，存在一个交集”，但仍需要人类提供使用欧拉回路（Eulerian circuits）的思路，并分步提示如何处理棘手的特殊情况。随后，它能从定理中自主提取出形式化验证的算法。
3. Claude Opus 4.8（突破）：
   • 一次性完成：在 Opus 4.8 发布后的第二天，作者在 ultracode 模式下进行了两项并行测试：
     • 从零开始重新证明主要多边形相交定理（无提示，隔离环境）。
     • 扩展算法以处理重叠线段的特殊情况（此前 Opus 4.7 在此失败）。
   • 结果：两个会话均在几小时的自主工作后成功。
   • 策略优化：Opus 4.8 能够制定并执行大型证明策略。它更准确地处理了“错误中间定理”的风险。当之前的模型因尝试证明错误的中间定理而卡住时，Opus 4.8 会表现出“怀疑”，自主切换到不同策略，或在必要时运行并行子代理尝试多种策略。

技术细节与局限性

• 构建要求：需要 elan 和 lean-toolchain（当前锁定为 leanprover/lean4:v4.15.0 以简化 WebAssembly 构建）。
• 检查证明：通过 lake build 运行所有证明。
• 公理检查：必须检查定理依赖的公理，以防 AI 引入不需要的公理。目前仅依赖可信公理 [propext, Classical.choice, Quot.sound]。
• 性能权衡：作者指出，强制 AI 代理进行形式化验证的一个缺点是，生成的代码可能较慢或忽略其他未在规范中捕获的实际考量。这可能是因为形式化验证的难度迫使代码更简单，且训练数据中缺乏经过形式化验证的实际软件案例。

关键要点

• 首创性：据作者所知，这是首个经过形式化验证的多边形相交算法实现。
• AI 能力跃迁：Claude Opus 4.8 能够“一次性”（one-shot）提供带有形式化证明的算法实现，而之前的模型需要多步策略指导。
• 信任机制转移：正确性的信任完全来自 Lean 检查器和人类对少量规范（87行）的审查，而非来自 LLM 本身。
• 验证复杂性：形式化验证的篇幅主要不在于算法本身，而在于证明许多看似简单的几何事实（如射线法定义的独立性）需要数千行代码。
• 人类审查极简：人类只需审查定义几何基础的少量核心文件，复杂的实现和证明由 AI 自主完成并接受机器验证。
• 潜在缺陷：形式化验证约束可能导致生成的代码牺牲性能或实用性，以换取证明的简洁性。
• 智能策略调整：Opus 4.8 展现了处理证明失败和策略切换的高级能力，如并行子代理和自动回退机制。

意义与影响

1. 软件可靠性的新范式

该项目展示了形式化验证在解决计算几何等复杂算法问题上的潜力。传统测试无法覆盖无穷的配置空间，而形式化验证提供了数学上的确定性。通过将 AI 代理作为“工人”，人类作为“架构师”和“规范制定者”，可以大幅降低形式化验证的人力门槛。

2. AI 代理能力的里程碑

Opus 4.8 的表现标志着 AI 在长程推理、复杂代码生成和形式化数学证明方面的重大进步。它不再仅仅是一个代码补全工具，而是能够独立规划、执行复杂证明策略并自我纠错的智能体。这为未来自动化开发高可靠性系统（如操作系统内核、密码学协议、金融核心系统）铺平了道路。

3. 人机协作模式的演变

该项目确立了一种新的协作模式：人类定义规范与核心逻辑，AI 负责实现与证明，机器负责验证。这种模式将人类从繁琐的、易错的细节证明中解放出来，专注于更高层级的逻辑设计和规范制定。

4. 对计算几何领域的贡献

多边形相交是计算机图形学、GIS（地理信息系统）和 CAD 软件的核心功能。提供一个经过形式化验证的实现，可以为这些领域提供“黄金标准”参考，有助于发现现有开源库中可能存在的边缘情况 Bug。

5. 挑战与反思

作者指出的性能损失问题提醒我们，形式化验证与工程优化之间存在张力。未来的研究方向可能包括如何在保持形式化验证正确性的同时，引入性能约束，或开发更智能的 AI 代理以平衡正确性与效率。此外，如何确保 AI 不引入隐藏公理，也是形式化验证自动化过程中必须严格把控的安全环节。