首个形式化验证的 3D CSG 几何计算实现

Show HN：形式化验证的 3D CSG：相信 93 行规范，不相信 1000 行 AI 代码

据我所知，这是首个形式化验证的三维构造立体几何（CSG）操作实现：网格交集，用 Lean 4 实现，并针对一份简洁的规范进行了验证，该规范精确确定了结果网格的表面，并保证了三角剖分的实用良好成形性条件。（另见相关工作。）

这个项目也是一个实验，目的是避免必须相信 AI 生成代码。人工审查者只需要读 93 行形式化规范，并运行如下所述的 Lean 检查器来认证核心的正确性，跳过复杂的 1000+ 行 AI 编写的实现。为了证明正确性，AI 自主编写了 60,000+ 行 Lean 证明，这些也不需要人工检查。Lean 检查器在编译时保证符合规范，完全不相信任何 LLM。这使我们能够将实现和证明视为黑盒。我通过下述里程碑指导智能体最终得到了这里呈现的结果。

尝试围绕验证核心构建的网页演示，你可以在其中交集示例网格，或导入并交集来自 STL 文件的网格。编译后的 Lean 代码在你的浏览器中本地运行；数据永远不会发送到服务器。需要注意的是，虽然核心是形式化验证的，但 UI 和粘合代码不是。

我们的实现远慢于最先进的网格交集实现：计算两个 70k 三角形的斯坦福兔子的精确交集需要 24 秒。在这个项目中，我们优先考虑最小化人工审查正确性的工作量，而不是性能。注意这个性能差距不是形式化验证软件的基本限制，形式化验证软件原则上可以和传统软件一样快。见详细信息。

输出网格保证满足下述性质，但网格划分对于我们尚未形式化的其他标准可能不是最优的；例如，它可能生成比必要更细的网格。

背景和形式化

三角网格是三角形的集合，通常预期形成不穿透自身的闭合表面，以及其他我们将讨论的良好成形性条件。

人类直观地将三角网格与一个"实体"相关联，即三维空间中的一个体积：所有不在表面上但"内部"的点的集合。（"内部"可以通过有符号光线交集计数在数学上描述。）

这种实体的概念使我们能够理解网格交集算法等算法的输出应该是什么样子，即使处理实际网格数据结构的实现很复杂，必须用专门代码处理许多几何特殊情况。

从网格交集算法，我们期望良好成形的输入网格的实体的集合交集就是输出网格的实体，且输出再次是良好成形的网格。（我们也期望该算法能正确检测并报告输入是否不良好成形。）

solid (meshIntersect M₁ M₂) = solid M₁ ∩ solid M₂

这精确地将结果网格的表面定为交集实体的边界。

处理三角网格的算法可以高效地计算代表我们心目中的实体的网格，但传统编程语言无法明确表达"实体"或对其做陈述，因为这些是无限集。在 Lean 中这是可能的，例如我们可以交集这样的无限集或证明两个无限集相等。而且，Lean 允许我们证明一个函数对所有可能的输入网格满足某个条件，而传统编程语言只允许我们测试该函数对特定输入满足条件。

我们定义网格的良好成形性以捕捉真实网格处理工具普遍期望的条件 —— 水密表面，以重数 1 界定实体、具有一致的向外方向、无退化三角形、无自交集 —— 有一个放松：表面可以相切，但不在面的内部而是沿着边和顶点。所以严格的 2-流形性不是必需的。见为什么总是生成流形网格的交集算法是不可能的。

最小人工审查，不相信 AI

为了认证核心的正确性（核心检查输入的良好成形性前置条件并计算网格交集），审查者只需要读 93 行形式化规范并运行如下所述的 Lean 检查器。审查者可以跳过复杂的 1000+ 行 AI 编写的算法实现。Lean 检查器在编译时保证符合规范，对任何 LLM 完全零信任。

只需读文件 CSG/DataStructures.lean、CSG/Def.lean、CSG/MeshIntersectWithPreconditionCheck.lean 和 CSG/WellFormedCheckMsg.lean，并运行如下所述的 Lean 检查器。不计注释，这些只有 93 行代码。其他文件无需读，因为指定 meshIntersectWithPreconditionCheck 的定理陈述（在同名文件中）只依赖于这 4 个文件中陈述的定义。

审查者可以跳过 meshIntersectWithPreconditionCheck 的实现，该实现在 CSG/Impl/ 中的 4 个文件中超过 1000 行代码，因为确定性 Lean 检查器保证它符合人工审查的规范。

这得益于 CSG/Proof/ 中 60,000 行 AI 编写的形式化证明，这些也不需要人工检查。

从实现到规范的这种压缩和简化之所以可能，是因为实现必须处理的许多事情可以完全与规范解耦：

实现必须处理特殊几何情况，这构成了算法复杂性的大部分，而形式化规范很简洁，因为数学可以用通用方式表述。Lean 检查器保证所有特殊情况都按照规范处理，而不需要规范枚举特殊情况。

实现使用加速数据结构以避免二次运行时复杂性和其他优化。虽然我们没有形式化运行时复杂性，但 Lean 检查器保证，即使有所有这些优化，我们仍然按规范生成结果。

如果在将来的提交中我们例如进一步改进运行时性能或输出网格的质量，审查过的规范保持不变，我们获得关于它的正确性，无需任何重新审查。另见我如何仅通过塑造这个规范开发这个项目。

在开发过程中，我只控制一个小规范，将证明和详细实现留给智能体作为黑盒。我从一个我认为相对容易实现和形式化证明为正确的规范开始，然后扩展需求。在下面列出的每个步骤中，我让智能体实现和形式化证明该规范。这种逐步细化使我能够将大部分工作委托给智能体，同时获得反馈说我的规范是可满足的，并在每个里程碑验证智能体朝向我最终目标的进展。我指示智能体先写非形式化证明再形式化。

我首先让智能体形式化了一篇提供基于单纯链描述实体的数学框架的论文。这给了我一个形式化的存在性结果，没有具体实现（见 CSG/Legacy/ChainIntersectionExistence.lean）。F. R. Feito 和 M. Rivero，"Geometric modelling based on simplicial chains"，计算机图形学 22(5)，611–619（1998）。doi:10.1016/S0097-8493(98)00067-3

然后我要求一个带有正确性证明的实现（CSG/Legacy/ChainIntersectionAlgorithm.lean）。这已经满足了类似于我最终目标的形式化规范。但重叠三角形和其他问题仍然被允许并确实发生了。

我随后为输出网格指定了限制条件（类似于 WellFormedMesh 的当前状态），以禁止第一个实现中出现的各类问题。我还对输入引入了一般位置限制，之后将其移除，以避免实现在这一步骤中不得不考虑大量特殊情况。更严格的需求强制进行了完整的重新实现，但部分正式框架可以被重用。

我随后为输出网格指定了限制条件（类似于 WellFormedMesh 的当前状态），以禁止第一个实现中出现的各类问题。我还对输入引入了一般位置限制，之后将其移除，以避免实现在这一步骤中不得不考虑大量特殊情况。更严格的需求强制进行了完整的重新实现，但部分正式框架可以被重用。

我随后移除了对输入的通用位置限制，这强制智能体正确处理所有特殊的几何情况。

我随后移除了对输入的通用位置限制，这强制智能体正确处理所有特殊的几何情况。

随后我让智能体用包围体层次结构和其他优化来优化实现。我没有对运行时进行形式化需求的定义，但 Lean 验证了优化后的代码仍然满足相同的形式化规范。因此在这一步骤中，我不必重新审查任何内容来保证正确性。

随后我让智能体用包围体层次结构和其他优化来优化实现。我没有对运行时进行形式化需求的定义，但 Lean 验证了优化后的代码仍然满足相同的形式化规范。因此在这一步骤中，我不必重新审查任何内容来保证正确性。

最后我进一步强化了规范并使其更容易审查。

最后我进一步强化了规范并使其更容易审查。

这个过程产生了你在 CSG/ 文件夹顶层看到的规范、CSG/Proof/ 中的证明和 CSG/Impl/ 中的实现。

大部分上述步骤我使用了 Claude Opus 4.8。部分步骤我使用 Fable 5 来创建初始的非正式证明策略，然后让 Opus 编写正式证明和实现。上述某些步骤花费了超过 24 小时的自主智能体工作。

与凭感觉编程和非正式规范的对比

与常规凭感觉编程相比，将 AI 与形式化验证相结合能够产生严格的保证，我们知道这些保证对所有输入都成立，并且随着程序的每一次后续修改都能被持续执行。但与常规凭感觉编程一样，随着每一步骤的进行，开发可能会积累一些债务：我最终得到的实现和证明都远非像一个保持全局视图的人类控制下那样干净和遵循一致的设计。此外，还有一些约束条件我们没有在这里形式化，比如运行时性能或输出实体面的三角化方式（除了格式正确条件之外）。因此这些约束与常规凭感觉编程一样难以控制。

作为对比，我给 Opus 4.8 一个非正式的规范描述，并要求它用 C++ 实现。不包括测试、粘合代码等的实现长度在与 Lean 实现相同的 1000+ 行范围内。虽然它编写了单元测试并迭代修复了自己的实现，但当一个独立智能体检查它与形式化验证的 Lean 实现的对比时，发现了 C++ 几何内核中的 3 个不同的错误，并在特定输入上重现了这些错误。所有这些错误都很罕见，几乎不可能通过黑盒测试捕获。针对非正式规范的其他智能体的迭代对抗性代码审查可能已经捕获了这些错误。但没有形式化验证，不可能确定实现中没有更多的错误。（C++ 内核至少有 3 个不同的错误被重现：1. 在某些配置中，一个格式正确的网格的顶点既位于另一部分网格的边上，又位于另一个格式正确的网格的面上。2. 在格式正确的输入网格上，当内部计算中的连级射线相交测试恰好都击中三角形边时。3. 在某些配置中，当一个大的面被几个小的特征切割时。）

实现一个精确的 3D 网格相交算法。用 C++ 编写，编译为 wasm，产生一个我可以交互的工件。重要的是内核（一个简单的函数）位于一个自包含的独立文件中，几何内核与所有粘合代码分离。（此文件仅依赖于一个独立的 bignum/精确有理实现，单独的文件）。此函数应该只将网格作为具有精确坐标的三角形数组作为输入/输出。

此函数应该检查输入是否为下面所定义意义的格式正确的网格，否则产生一个错误消息。仅在输入格式正确时运行相交。

我们对"格式正确的网格"的定义捕捉了实际世界网格处理工具通常期望的条件 - 水密表面，以重数一限制一个实体，一致的向外方向，没有退化三角形，没有自相交 - 有一个放松：表面可能接触自己，不在面的内部而是沿着边和顶点（因此严格的 2-流形性不是必需的）。这个放松是必要的，使得任何两个格式正确的网格的相交都再次是格式正确的。

所有内容应该用有理数计算。它应该正确处理所有特殊情况。如果输入是格式正确的，总是产生一个格式正确的网格作为输出。你可以成对相交三角形（使用 bvh 优化）发出多边形并用 Steiner 扇三角化。

将形式化验证与凭感觉编程相结合的缺点：

它倾向于产生较慢的代码或忽视规范中未捕捉到的其他实际考虑。这源于形式化验证的难度推向更简单的代码，以及训练数据中形式化验证的实际软件的缺乏。

对于智能体来说，自主开发形式化证明可能需要比非正式推理其实现多几个数量级的 token 和时间。

许多实际问题不允许一个简单的形式化规范。

如我撰写本文时，AI 智能体处理大型明确定义的任务的能力正随着每个模型版本的发布而迅速增加。人类审查其输出并对其进行推理的能力没有。我希望我们能使用形式化验证以及其他方法作为杠杆来保持控制。

构建和检查

需要 elan。Lean 版本在 lean-toolchain 中被固定（当前 leanprover/lean4:v4.15.0）以简化 WebAssembly 构建；elan 在首次使用时自动安装它。

首先从社区缓存下载预构建的 Mathlib（没有这个，下一步将从源代码编译 Mathlib，这需要很长时间）：

lake exe cache get

如果这在 dyld 错误中中止，提及 SG_READ_ONLY（最近的 macOS）：此处固定的 Lean 版本捆绑了一个有已知问题的链接器，在较新的 Lean 版本中已修复（lean4#6063）。用 Apple 的编译器重新链接缓存工具有效：

rm -rf .lake/packages/mathlib/.lake/build/bin
SDKROOT="$(xcrun --show-sdk-path)" LIBRARY_PATH="$(lean --print-prefix)/lib" LEAN_CC="$(xcrun -f clang)" lake exe cache get

lake build

检查定理所依赖的公理（在以下示例中，在演示中调用的网格相交实现的正确性定理）。这很重要，因为智能体可能已向证明中引入了不需要的公理。此存储库中的所有定理仅依赖于受信任的公理 [propext, Classical.choice, Quot.sound]：

printf 'import CSG.MeshIntersectWithPreconditionCheck\n#print axioms CSG.meshIntersectWithPreconditionCheck_ok_spec\n#print axioms CSG.meshIntersectWithPreconditionCheck_ok_of_wellFormed\n#print axioms CSG.meshIntersectWithPreconditionCheck_error_sound\n#print axioms CSG.meshIntersectWithPreconditionCheck_error_of_not_wellFormed\n' | lake env lean --stdin

同时确保定理实际上对编译的函数成立，即实现没有通过以下任何关键字被其他东西覆盖。此搜索应该没有匹配项：

rg -n 'implemented_by|extern|csimp|skipKernelTC|unsafe|partial|opaque' CSG/

构建由 web 应用提供的 WebAssembly 包（需要 emscripten、zstd 和 node/npm；wasm-opt 是可选的）：

./build_web_demo.sh

该算法拒绝了原始斯坦福兔模型，因为网格不是水密的，所以我关闭了底部的孔。该实现在 M4 Pro 上以单线程方式计算两个 70k 三角形网格的精确相交需要 24 秒。

该实现速度远低于最先进的网格交集实现。在这个项目中，我们优先考虑最小化人工审查正确性所需的工作量，而不是性能。

大多数其他实现使用硬件加速的浮点运算。（即使像 CGAL 这样的精确实现也在浮点精度足够的决策中使用浮点数。）我们没有。这不是 Lean 的根本限制，但使用硬件加速浮点会引入额外的公理，需要人工审查者予以信任。

我们在运行时根据良定义规范检查所有输入，这占了总运行时间的相当大一部分。

为什么通常无法获得流形的输出网格

在下面的示例中，对带孔立方体的精确旋转会产生一个曲面非流形的实体。（见输出前方的点，实体的两个分量在此处接触。）将两个网格的移动网格大小都设置为 1/3，旋转精度设置为 1，可在网络演示中重现此情况。如果重置旋转并在周围移动带孔的立方体，还可以安排输出实体的曲面沿边非流形的情况。

如果我们施加流形性约束，就没有算法能够满足我们的规范。

规范很简洁，但算法必须用专用代码处理特殊的几何情况才能满足规范。

这里两个四面体的右面共面重叠且法向相同。规范隐式要求算法在这些共面面的交集处发出一个面。不遵循形式规范的程序可能会忽略这种情况，在曲面上产生孔洞或双面。

在此示例中，四面体完全相接，它们之间体积为零——这是法向相反的共面面的重叠。我们的规范强制输出为空。许多生产应用在这类情况下会随机产生双膜工件。在上面的带孔立方体示例中，可以看到法向相反的共面重叠的非平凡示例。

算法需要处理许多其他特殊情况。由于形式验证的存在，我们无需为任何情况编写单元测试来确保正确性。

一个网格的顶点可能位于另一个网格上。算法必须确保考虑这些顶点，以在切割的两侧创建面。

一个或两个输入网格可能不满足 4 个良定义条件之一，这必须被正确报告。

共面重叠本身存在子情况，如重叠面的边共线。

还有一些特殊情况实现必须正确处理，这些情况在输入中不可见，但在算法的几何构造过程中出现。不阅读实现代码，我们永远想不到测试这些。我们的规范确保所有这些都得到正确处理，而无需我们主动思考。

在实现中射出的射线用于确定内外时，可能精确击中三角形的边或顶点，甚至共面穿过一个面。

一个面可能完全位于边界体积层次加速结构中的边界框边界上，要求实现中的不等式设置正确。

上述要点不仅适用于交集，也适用于良定义检查。在该部分代码中出错可能导致网格被误判为不满足良定义。

算法的子例程可能创建 T 型接点，必须再次修复才能产生良定义的输出网格。

Di Vito 和 Hocking（NASA Formal Methods 2021）在 PVS 中验证了多边形合并算法，将两个重叠的简单多边形合并成单个外边界且无孔。

我之前的 verified-polygon-intersection 项目在 Lean 4 中验证了二维多边形交集，依赖 AI 编写的实现和证明，就如同我们在此处所做的那样。

未验证的精确三维网格布尔运算当然存在，例如 CGAL 的 Nef 多面体。它们在实践中精确且稳健，但其正确性基于测试和非正式推理，而非机器检查的证明。