schildep/verified-3d-mesh-intersection 来源：https://github.com/schildep/verified-3d-mesh-intersection

形式化验证的3D网格相交 - 信任93行规约，而非1000+行AI编写代码

据我所知，这是首个形式化验证的3D构造实体几何（CSG）操作实现：网格相交（mesh intersection）。该实现使用 Lean 4 编写，并已根据一份简洁的规约进行了验证，该规约精确地确定了结果网格的表面，并保证三角剖分满足实用的良构条件。（另见相关工作。）

本项目也是一次实验，旨在避免必须信任AI生成的代码。人类审阅者只需阅读93行形式化规约，然后按下文所述运行 Lean 检查器，即可验证内核的正确性，而无需查看复杂的1000+行AI编写实现。为了证明正确性，AI自主编写了超过60000行 Lean 证明，这些证明同样无需人工审阅。Lean 检查器在编译时保证实现符合规约，对任何大语言模型（LLM）都不需要信任。这使得我们可以将实现和证明视为黑盒。我通过下文描述的里程碑指导智能体，最终得到这里呈现的结果。

在线演示

尝试基于已验证内核构建的在线演示（https://schildep.github.io/verified-3d-mesh-intersection），您可以相交示例网格或从STL文件导入并相交网格。编译后的 Lean 代码在您的浏览器本地运行；数据不会发送到任何服务器。注意，虽然内核是形式化验证的，但UI和胶水代码并未验证。

我们的实现远慢于最先进的网格相交实现：计算两个7万三角形的斯坦福兔（Stanford bunny）的精确相交需要24秒。在本项目中，我们优先最小化正确性的人工审阅工作量，而非性能。注意，这种性能差距并不是形式化验证软件的根本限制——原则上它可以达到与传统软件相同的速度。详见性能。

斯坦福兔与斯坦福兔的相交

输出网格保证满足下文描述的性质，但网格划分可能在其它尚未形式化的标准上不是最优的；例如，它可能产生比必要更精细的网格。

背景与形式化

三角形网格是一组三角形的集合，通常期望形成一个封闭的、自身不穿透的表面，此外还有下文将讨论的其他良构条件。人们直观地将三角形网格与“实体“关联起来，即三维空间中的一个体积：所有不在表面上但位于网格“内部“的点的集合。（“内部“可以通过带符号的射线相交计数数学描述。）

网格内部的点集。截面可视化及带符号射线相交测试，用于确定给定点是否在实体内部。

这种实体的概念使我们能够理解诸如网格相交算法等算法的输出应该是什么样子，即使处理实际网格数据结构的实现很复杂，并且必须用专门的代码处理许多几何特殊情形。对于网格相交算法，我们期望：良构输入网格的实体的集合交集等于输出网格的实体，并且输出再次是良构的网格。（我们还期望算法能正确检测并报告输入是否不是良构的。）

lean solid (meshIntersect M1 M2) = solid M1 ∩ solid M2

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

带孔立方体与近似球体的网格相交。2D截面可视化。

在三角形网格上工作的算法能够高效地计算代表我们心目中实体的网格，但传统编程语言无法显式表达“实体“或对其做出陈述，因为这些是无限集合。在 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 检查器保证它符合人工审阅的规约。
• 这得益于AI编写的60000行形式化证明（位于 CSG/Proof/），这些证明同样不需要人工检查。

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

• 实现必须处理特殊的几何情形，这些构成了算法的大部分复杂性；而形式化规约很简短，因为数学上可以一般化地表述。Lean 检查器保证所有特殊情形都按照规约处理，而无需规约枚举特殊情形。
• 实现使用加速数据结构以避免平方级的运行时复杂度以及其他优化。虽然我们没有形式化运行时复杂度，但 Lean 检查器保证，经过所有这些优化，我们仍然产生符合规约的结果。如果未来的提交进一步改进运行时性能或输出网格质量，已审阅的规约保持不变，我们无需重新审阅即可保证正确性。

另见我是如何通过塑造这个规约来开发本项目的。

开发

在开发过程中，我只控制一个小型规约，将证明和详细实现作为黑盒留给智能体。我首先制定一个我认为相对容易实现并形式化证明正确的规约，然后逐步增加需求。在下面列出的每一步中，我都让智能体实现并形式化证明该规约。这种逐步精化的方式使我能够将大量工作委托给智能体，同时获得关于我的规约是否可满足的反馈，并在每个里程碑验证智能体朝最终目标的进展。我指示智能体在形式化之前先写非形式化证明。

• 我首先让智能体形式化一篇论文，该论文提供了一种基于单纯链描述实体的数学框架。这给了我一个形式化的存在性结果，但没有具体实现（参见 CSG/Legacy/ChainIntersectionExistence.lean）。

  F. R. Feito and M. Rivero, “Geometric modelling based on simplicial chains,” Computers & Graphics 22(5), 611–619 (1998). doi:10.1016/S0097-8493(98)00067-3 (https://doi.org/10.1016/S0097-8493(98)00067-3)

• 然后我要求提供一个带正确性证明的实现（CSG/Legacy/ChainIntersectionAlgorithm.lean）。这已经满足了一个类似于最终目标的正式规约。但重叠三角形和其他问题仍然被允许并确实发生了。
• 然后我为输出网格指定了限制（类似于当前 WellFormedMesh 的状态），以禁止第一个实现中的那种问题。我还引入了一个对输入的一般位置限制，后来我移除了它，以避免在这一步中实现要考虑大量特殊情形。更严格的要求迫使完全重新实现，但部分形式化框架可以被重用。
• 然后我移除了输入的一般位置限制，这迫使智能体正确处理所有特殊的几何情形。
• 然后我让智能体使用包围体层次结构和其他优化来优化实现。我没有形式化运行时要求，但 Lean 验证了优化后的实现仍然满足相同的正式规约。因此在这一步，我不需要重新审阅任何内容来确保正确性。
• 最后，我进一步强化了规约，使其更易于审阅。

这个过程产生了您现在在 CSG/ 文件夹顶层看到的规约，在 CSG/Proof/ 中的证明，以及在 CSG/Impl/ 中的实现。

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

与非正式规范下的“氛围编程“对比

与常规的氛围编程（vibecoding）不同，将AI与形式化验证相结合，可以产生严格的保证：我们知道这些保证对所有输入都成立，并且在程序的后续每次修改中都会得到维护。但与常规的氛围编程一样，每步开发都可能积累债务：我最终得到的实现和证明远非整洁，也没有遵循一个一致的设计，不像由保持整体概览的人类控制时那样。此外，我们在这里没有形式化一些约束，例如运行时性能或输出实体面部的三角剖分方式（除了良构性条件）。因此这些约束与常规氛围编程一样难以控制。

为了比较，我给了 Opus 4.8 一个非正式规约描述，并要求它在 C++ 中实现。实现（不包括测试、胶水代码等）的长度与 Lean 实现相当，也在1000+行范围内。尽管它编写了单元测试并迭代式修复了自己的实现，但由独立智能体将其与形式化验证的 Lean 实现进行比较后，在 C++ 几何内核中发现了3个不同的错误，并针对特定输入复现了。所有这些错误都很罕见，几乎不可能通过黑盒测试捕获。由其他智能体根据非正式规约对代码进行迭代对抗性审阅可能会捕获这些错误。但如果没有形式化验证，就无法确定实现中是否还有更多错误。（C++ 内核至少有3个不同的错误已被复现：1. 在某些配置下，良构网格的一个顶点同时落在同一网格另一部分的边上以及另一个良构网格的一个面上；2. 在良构输入网格上，内部计算中一系列射线相交测试恰好都命中三角形边；3. 在某些配置下，一个大面被若干小特征切割。）

与非正式氛围编程的对比，点击展开用于产生替代 C++ 实现的提示词

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

该函数应检查输入是否为下面意义上的良构网格，如果不是，则产生错误消息。仅在输入良构时运行相交。

我们对“良构网格“的定义捕捉了现实世界网格处理工具通常预期的条件——水密表面、包围一个多重数为1且具有一致外法向的实体、无退化三角形、无自交——但有一个放宽：表面可以自我接触，但不能在面的内部，而只能沿边和顶点（因此不需要严格的2-流形性）。这个放宽是必需的，以便任何两个良构网格的相交再次是良构的。

所有计算应使用有理数。它应正确所有特殊情形。如果输入是良构的，则总是产生一个良构的网格作为输出。您可以成对相交三角形（使用BVH优化），生成多边形并使用Steiner扇进行三角剖分。

将形式化验证与氛围编程结合的缺点：

• 它往往产生更慢的代码，或者忽视规约中未捕获的其他实际考虑。这源于形式化验证的困难推动代码简化，以及训练数据中缺少形式化验证的实用软件。
• 智能体自主开发形式化证明所需的 token 和时间可能比非形式化推理其实现多出几个数量级。
• 许多实际问题不容许简单的形式化规约。

在我写这段话时，AI智能体处理大型明确定义任务的能力正随着每个模型发布而迅速提升。人类审阅其输出并对此推理的能力却没有。我希望我们能够利用形式化验证等方法作为杠杆来保持控制。

构建与检查

需要 elan (https://github.com/leanprover/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 (https://github.com/leanprover/lean4/pull/6063))