schildep/verified-3d-mesh-intersection

# 经过形式化验证的 3D 网格相交 —— 信任 93 行规范，而不是 1000 多行 AI 编写的代码 据我所知，这是首个经过形式化验证的 3D 构造实体几何（CSG）操作的实现：网格相交，使用 Lean 4 实现，并针对[简明的规范](#background-and-formalization)进行了验证，该规范精确限定了生成网格的表面，并保证了三角剖分的实用良好格式条件。（另请参阅[相关工作](#related-work)。） 本项目也是一项避免必须信任 AI 生成代码的实验。人类审查者只需阅读[93 行形式化规范](#minimal-human-review-without-trusting-ai)并按[如下所述](#building-and-checking)运行 Lean 检查器，即可证明核心逻辑的正确性，从而跳过[复杂的](#special-cases)1000 多行 AI 编写的实现。为了证明正确性，AI 自主编写了超过 60,000 行的 Lean 证明，这些证明同样永远不需要人类进行检查。Lean 检查器在编译时保证了对规范的一致性，对任何 LLM 保持零信任。这使得我们可以将实现和证明视为一个黑盒。我引导智能体完成了[下文描述的](#development)各个里程碑，最终得出了此处展示的结果。 ## Web 演示 试用围绕已验证核心构建的 [Web demo](https://schildep.github.io/verified-3d-mesh-intersection)，你可以在其中对示例网格进行相交操作，或者从 STL 文件导入并相交网格。编译后的 Lean 代码在你的浏览器中本地运行；永远不会向服务器发送任何数据。请注意，虽然核心逻辑经过了形式化验证，但 UI 和胶水代码并未经验证。 我们的实现远慢于最先进的网格相交实现：计算两个包含 7 万个三角形的 Stanford bunny 的精确相交需要 24 秒。在本项目中，我们将尽量减少正确性方面的人工审查工作量置于性能之上。请注意，这种性能差距并非形式化验证软件的根本限制，原则上它完全可以和传统软件一样快。详见[详情](#performance)。  输出的网格保证满足下文描述的属性，但在我们尚未形式化的其他标准（例如，生成了比必要情况更精细的网格）方面，其网格化可能并非最优。 ## 背景与形式化 三角网格是一组三角形的集合，通常期望它们能构成一个不发生自相交的封闭表面，此外还有我们将在下文讨论的其他良好格式条件。 人类在直觉上会将三角网格与“实体”（即 3D 空间中的一个体积）联系在一起：即所有不在表面上但处于网格“内部”的点的集合。（“内部”可以通过带符号的射线相交计数来进行数学描述。）  这种关于实体的概念使我们能够理解诸如网格相交算法等操作的输出应该是什么样子，尽管基于实际网格数据结构工作的实现极其复杂，并且必须使用专门的代码来处理[许多几何特殊情况](#special-cases)。 对于网格相交算法，我们期望良好格式的输入网格的实体集合的交集即为输出网格的实体，并且输出再次成为良好格式的网格。（我们还期望算法能够正确检测并报告输入是否并非良好格式。） ``` solid (meshIntersect M₁ M₂) = solid M₁ ∩ solid M₂ ``` 这[精确限定了](CSG/Example.lean)生成网格的表面，使其完全等同于相交实体的边界。   处理三角网格的算法能够高效地计算出代表我们心目中实体的网格，但传统的编程语言无法显式地表达“实体”或对其做出声明，因为它们是无限集合。在 Lean 中这是可能的，例如，我们可以对这样的无限集合求交集，或者证明两个无限集合是相等的。此外，Lean 允许我们证明某个函数对于所有可能的输入网格都满足特定条件，而传统编程语言仅允许我们测试该函数对于特定输入是否满足条件。 我们将网格的良好格式定义为涵盖现实世界网格处理工具通常期望的条件——水密表面、以一致的外向方向包围重数为 1 的实体、无退化三角形、无自相交——但有一处放宽：表面可以自接触，但不是在面的内部，而是沿着边和顶点。因此，并不要求严格满足 2-manifold 性质。请参阅[为什么不可能存在总是生成 manifold 网格的相交算法](#why-we-cannot-have-manifold-output-meshes-in-general)。 ## 无需信任 AI 的最小化人工审查 为了证明核心逻辑（用于检查输入的良好格式前置条件并计算网格相交）的正确性，审查者只需阅读 93 行形式化规范并按[如下所述](#building-and-checking)运行 Lean 检查器。审查者可以跳过极其复杂的、1000 多行由 AI 编写的算法实现。Lean 检查器在编译时保证了对规范的一致性，对任何 LLM 保持零信任假设。 - 只需阅读文件 [`CSG/DataStructures.lean`](CSG/DataStructures.lean)、[`CSG/Def.lean`](CSG/Def.lean)、[`CSG/MeshIntersectWithPreconditionCheck.lean`](CSG/MeshIntersectWithPreconditionCheck.lean) 和 [`CSG/WellFormedCheckMsg.lean`](CSG/WellFormedCheckMsg.lean)，并按如下所述运行 Lean 检查器即可。不计注释，这些仅仅是 93 行代码。其他文件无需阅读，因为指定 `meshIntersectWithPreconditionCheck`（位于同名文件中）的定理声明仅仅依赖于这 4 个文件中陈述的定义。 - 审查者可以跳过位于 [`CSG/Impl/`](CSG/Impl/) 中 4 个文件内超过 1000 行代码的 `meshIntersectWithPreconditionCheck` 实现，因为确定性的 Lean 检查器已保证其符合经过人工审查的规范。 - 这得益于 [`CSG/Proof/`](CSG/Proof/) 中 60,000 行由 AI 编写的形式化证明，这些证明同样永远不需要人工进行检查。 这种从实现到规范的压缩与简化之所以可能，是因为实现必须处理的许多事情可以与规范完全解耦： - 实现必须处理[几何特殊情况](#special-cases)，这构成了该算法的大部分复杂性；而形式化规范之所以简短，是因为数学可以被概括性地表达。Lean 检查器保证所有特殊情况都按照规范进行处理，而无需规范去逐一枚举这些特殊情况。 - 实现使用了加速数据结构以避免二次方的时间复杂度并进行了其他优化。虽然我们没有对运行时复杂度进行形式化，但 Lean 检查器保证，在应用所有这些优化的情况下，我们依然能够得出符合规范的结果。 如果在未来的某次提交中，我们例如进一步改善了运行时性能或输出网格的质量，经过审查的规范将保持不变，而我们依然能获得相对于它的正确性，无需进行任何重新审查。另请参阅我是如何仅通过塑造该规范来[开发本项目的](#development)。 ## 开发 在开发过程中，我只控制了一个小型的规范，将证明和详细的实现作为黑盒留给智能体。我从我估计相对容易实现和进行形式化证明正确的规范开始，然后逐步增加需求。在下面列出的每一个步骤中，我都让智能体去实现并进行形式化证明该规范。这种循序渐进的完善让我能够将大块的工作委派给智能体，同时获得关于我的规范是可满足的反馈，并在每个里程碑验证智能体向着我最终目标的进展。我指示智能体在形式化之前先编写非正式证明。 - 我首先让一个智能体对一篇论文进行形式化，该论文提供了一个基于单纯链来描述实体的数学框架。这给了我一个没有具体实现的形式化存在性结果（见 [`CSG/Legacy/ChainIntersectionExistence.lean`](CSG/Legacy/ChainIntersectionExistence.lean)）。 - 然后我要求提供一个带有正确性证明的实现（[`CSG/Legacy/ChainIntersectionAlgorithm.lean`](CSG/Legacy/ChainIntersectionAlgorithm.lean)）。这已经满足了一个类似于我最终目标的形式化规范。但当时仍然允许并确实出现了三角形重叠等问题。 - 接着我指定了对输出网格的限制（类似于当前 `WellFormedMesh` 的状态），以禁止第一次实现中出现的那类问题。我还对输入引入了后续被移除的一般位置限制，以避免实现在这一步中必须考虑大量特殊情况。更严格的要求迫使进行完全的重新实现，但部分形式化框架可以重用。 - 然后我移除了对输入的一般位置限制，这迫使智能体正确处理所有几何特殊情况。 - 接着我让智能体利用层次包围盒及其他优化手段优化实现。我没有对运行时间进行形式化要求，但 Lean 验证了优化后依然满足相同的形式化规范。因此，在这一步中，我无需重新审查任何内容即可确保正确性。 - 最后，我进一步加强了规范，使其更易于审查。 这一过程产生了你可以在 [`CSG/`](CSG/) 文件夹顶层看到的规范，位于 [`CSG/Proof/`](CSG/Proof/) 的证明，以及位于 [`CSG/Impl/`](CSG/Impl/) 的实现。 在上述大多数步骤中，我使用了 Claude Opus 4.8。对于某些步骤，我使用了 Fable 5 来创建初始的非正式证明策略，然后让 Opus 编写形式化证明和实现。上述某些步骤花费了超过 24 小时的自主智能体工作时间。 ## 与使用非正式规范的 vibecoding 的比较 与常规的 vibecoding 相比，将 AI 与形式化验证结合使用产生了严格的保证：我们知道这些保证对于所有输入都成立，并且在对程序进行后续的每次修改时都会持续强制执行。但与常规的 vibecoding 一样，在每一个步骤中，开发过程都可能积累一些技术债：我最终得到的实现和证明远谈不上简洁，也没有遵循一个具有凝聚力的设计；而如果是由一个掌控全局的人类来控制的话，本应如此。此外，还有一些我们在此未进行形式化的约束，例如运行时性能，或者除了良好格式条件之外，输出实体表面的三角剖分方式。因此，这些约束与常规的 vibecoding 一样难以控制。 作为对比，我给了 Opus 4.8 一份关于规范的非正式描述，并要求它用 C++ 实现。不包括测试、胶水代码等在内的实现长度与 Lean 实现处于相同的 1000 多行的范围内。尽管它编写了单元测试并迭代修复了自己的实现，但在由一个独立的智能体将其与经过形式化验证的 Lean 实现进行对比检查后，在 C++ 几何核心中发现了 3 个不同的 bug，并在特定输入上进行了重现。所有这些 bug 都很罕见，几乎不可能通过黑盒测试来捕捉。由其他智能体针对非正式规范对代码进行的迭代对抗性审查也许能捕捉到这些 bug。但如果没有形式化验证，是不可能确定实现中不再有更多 bug 的。（该 C++ 核心至少有 3 个被重现的不同 bug：1. 在某些配置中，良好格式网格的某个顶点既位于网格另一部分的边上，又位于另一个良好格式网格的面上。2. 在良好格式的输入网格上，当内部计算中的级联射线相交测试碰巧都击中了三角形的边时。3. 在某些配置中，一个大面被几个小特征切割。）

与非正式 vibecoding 的对比，点击展开用于生成 C++ 替代实现的 prompt

将形式化验证与 vibecoding 结合的缺点： - 它往往会产生运行较慢的代码，或者无视规范中未捕获的其他实际考量。这源于形式化验证的难度推动了对更简单代码的需求，以及训练数据中缺乏经过形式化验证的实际软件。 - 智能体自主开发形式化证明所需的 token 数量和时间，可能比对实现进行非正式推理要多出几个数量级。 - 许多实际问题并不具备简单的形式化规范。 在我写下这篇文章时，AI 智能体处理大型定义明确任务的能力正随着每次模型的发布而迅速提升。而人类审查其输出并对其进行推理的能力却并非如此。我希望我们能够将形式化验证及其他方法作为一种杠杆来保持掌控力。 ## 构建与检查 需要 [elan](https://github.com/leanprover/elan)。Lean 版本被锁定在 [`lean-toolchain`](lean-toolchain)（当前为 `leanprover/lean4:v4.15.0`）以简化 WebAssembly 构建；elan 会在首次使用时自动安装它。 首先从社区缓存下载预构建的 Mathlib（如果没有这一步， 下一步将从源码编译 Mathlib，这需要很长时间）： ``` lake exe cache get ``` 检查所有证明： ``` lake build ``` 检查所关注的定理所依赖的公理（在以下示例中， 即 demo 中调用的网格相交实现的正确性定理）。这很重要，因为智能体 可能在证明中引入了不需要的公理。本仓库中的所有定理仅 依赖于受信任的公理 `[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 bundle（需要 `emscripten`、`zstd` 和 `node`/`npm`；`wasm-opt` 为可选项）： ``` ./build_web_demo.sh ``` ## 性能 该算法拒绝了[原始的 Stanford bunny](https://graphics.stanford.edu/data/3Dscanrep/)，因为该网格不是水密的，所以我封闭了底部的孔。在 M4 Pro 上进行单线程计算时，该实现需要 24 秒才能计算出两个 7 万三角形网格的精确相交。 该实现远远慢于最先进的网格相交实现。在本项目中，我们将尽量减少正确性人工审查的工作量置于性能之上。 - 大多数其他实现使用硬件加速的浮点计算。（即使是像 CGAL 这样的精确实现，在浮点精度足够的情况下，也会使用浮点数进行判定。）我们没有这样做。这不是 Lean 的根本限制，但使用硬件加速的浮点数将需要人工审查者信任的额外公理。 - 我们在运行时根据我们的良好格式定义检查所有输入，这占据了总运行时间的很大一部分。  ## 为什么我们通常无法得到 manifold 的输出网格 在以下示例中，对带孔立方体的精确旋转会导致一个表面为非 manifold 的实体。（请看输出前方实体两个部分相接触的那个点。）在 Web demo 中，将两个网格的移动网格大小都设置为 1/3，并将旋转位数设置为 1，即可排列出这种情况。如果你重置旋转并移动带孔立方体，你也可以排列出输出实体的表面沿着一条边呈现非 manifold 的情况。  如果我们强加一个 manifold 的条件，将没有算法能够满足我们的规范。 ## 特殊情况 规范虽然简短，但算法必须使用专门的代码来处理几何特殊情况，才能满足规范。 在这里，两个四面体的右侧面以相同的法线方向发生共面重叠。规范隐式地强制算法在这些共面面的相交部分生成一个面。不遵循形式化规范的程序可能会忽略这种情况，并在表面上产生一个孔或双重面。  在这个示例中，四面体恰好接触，它们之间的体积为零——即法线方向相反的面的共面重叠。我们的规范强制输出为空。许多生产应用在这样的情况下会随机产生双层膜伪影。在[上面带孔立方体的示例中](#why-we-cannot-have-manifold-output-meshes-in-general)，你可以看到一个具有相反法线方向的共面重叠的复杂示例。  算法还必须处理许多其他的特殊情况。得益于形式化验证，我们不需要为任何情况编写单元测试来确保正确性。 - 一个网格的顶点落在另一个网格上。算法必须确保考虑到此类顶点，以便在切口的两侧都创建面。 - 一个或两个输入网格不满足 4 个良好格式条件之一，并且必须被正确报告。 - 我们上面讨论过的共面重叠本身也有子特殊情况，例如重叠面的边是共线的。 - ... 还有一些特殊情况是实现必须处理正确的，它们从输入中是不可见的，而是在算法内部的几何构造中产生的。如果不阅读实现，我们绝不会想到要测试这些情况。我们的规范确保了所有这些都得到了正确处理，而我们无需对此进行思考。 - 实现中为了在子程序中确定内部/外部而发射的射线，恰好击中了三角形的边或顶点，甚至共面地穿过一个面。 - 某个面恰好位于层次包围盒加速结构的边界框边界上，这要求我们在实现中放入正确的不等式。 - 以上几点不仅适用于相交，也适用于良好格式检查。在该部分代码中处理不当可能会导致网格被错误地归类为非良好格式。 - 算法的子程序会创建 T-junction，必须再次修复它们才能生成良好格式的输出网格。 - ... ## 相关工作 - [Di Vito 和 Hocking (NASA Formal Methods 2021)](https://doi.org/10.1007/978-3-030-76384-8_6) 在 PVS 中验证了一种多边形合并算法，该算法将两个重叠的简单多边形合并为一个没有孔的单一外边界。 - 我早期的 [verified-polygon-intersection](https://github.com/schildep/verified-polygon-intersection) 项目在 Lean 4 中验证了 2D 多多边形相交，正如我们在此所做的那样，依赖于 AI 编写的实现和证明。 - 当然，存在未经形式化验证的精确 3D 网格布尔运算，例如 [CGAL 的 Nef polyhedra](https://doc.cgal.org/latest/Nef_3/)。在实践中它们是精确且健壮的，但其正确性依赖于测试和非正式推理，而不是经过机器检查的证明。

标签：3D几何计算, AI代码生成, AI工具, Lean 4, 定理证明, 形式化验证, 数据可视化, 构造实体几何(CSG), 网格相交