形式化验证的3D CSG：信任93行规范而非1000行AI代码

据我所知，这是3D构造性实体几何（CSG）操作——网格相交——的首个形式化验证实现，在Lean 4中实现，并针对一个简洁的规范进行了验证，该规范精确确定了结果网格的表面，并保证了三角剖分上的实际良构条件。

（另见相关工作。）该项目也是一项避免信任AI生成代码的实验。人类审查者只需阅读93行形式化规范，并运行下面描述的Lean检查器，即可验证内核的正确性，跳过复杂的1000多行AI编写的实现。

为了证明正确性，AI自主编写了超过60000行的Lean证明，这些证明也无需人工检查。Lean检查器在编译时保证符合规范，对任何LLM都不予信任。这使我们能够将实现和证明视为黑盒。我通过下面描述的里程碑指导智能体，最终得到了此处呈现的结果。

试试围绕已验证内核构建的Web演示，你可以相交示例网格或从STL文件导入并相交网格。编译后的Lean代码在浏览器本地运行；没有数据发送到服务器。请注意，虽然内核是形式化验证的，但UI和胶水代码并未验证。

我们的实现比最先进的网格相交实现慢得多：计算两个7万三角形的斯坦福兔子的精确相交需要24秒。在这个项目中，我们优先考虑最小化人类对正确性的审查工作，而非性能。请注意，这种性能差距并非形式化验证软件的根本限制，原则上形式化验证软件可以与传统软件一样快。

详见细节。输出网格保证满足下面描述的属性，但网格化可能在我们尚未形式化的其他标准上不是最优的；例如，它可能产生比必要更细的网格。三角形网格是一组三角形，通常期望形成一个不穿透自身的封闭表面，以及我们将在下面讨论的其他良构条件。

人类凭直觉将三角形网格与“实体”联系起来，即3D空间中的一个体积：所有不在表面上但位于网格“内部”的点的集合。（“内部”可以通过有符号射线相交计数进行数学描述。

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

从网格相交算法，我们期望良构输入网格的实体的集合交集是输出网格的实体，并且输出再次是一个良构网格。（我们还期望如果输入不是良构的，算法能正确检测并报告。

）solid (meshIntersect M₁ M₂) = solid M₁ ∩ solid M₂这精确地将结果网格的表面固定为相交实体的边界。

在三角形网格上工作的算法可以高效地计算表示我们心中实体的网格，但传统编程语言无法显式表达“实体”或对其做出陈述，因为这些是无限集合。在Lean中这是可能的，例如我们可以相交这样的无限集合或证明两个无限集合相等。

此外，Lean允许我们证明一个函数对所有可能的输入网格都满足条件，而传统编程语言只允许我们测试函数对特定输入满足条件。

我们定义了网格的良构性，以捕捉现实世界网格处理工具通常期望的条件——水密表面、以一致外向法向包围多重性为1的实体、无退化三角形、无自相交——但有一个放宽：表面可能接触自身，不是在面的内部，而是沿着边和顶点。

因此不要求严格的2-流形性。

了解为什么一个始终产生流形网格的相交算法是不可能的。为了验证内核的正确性——该内核检查输入的良构前置条件并计算网格相交——审查者只需阅读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/中60000行AI编写的形式化证明，这些证明也无需人工检查。

这种从实现到规范的压缩和简化之所以可能，是因为实现必须处理的许多事情可以完全与规范解耦：- 实现必须处理特殊的几何情况，这构成了算法的大部分复杂性，而形式化规范很短，因为数学可以一般性地表述。

Lean检查器保证所有特殊情况都按照规范处理，而无需规范列举特殊情况。- 实现使用加速数据结构以避免二次运行时复杂度和其他优化。虽然我们没有形式化运行时复杂度，但Lean检查器保证，通过所有这些优化，我们仍然根据规范产生结果。

如果未来提交中我们进一步改进运行时性能或输出网格质量，审查过的规范保持不变，我们就能获得相对于它的正确性，无需任何重新审查。另请参见我如何仅通过塑造这个规范来开发该项目。在开发过程中，我只控制一个小的规范，将证明和详细实现作为黑盒留给智能体。

我从一个我认为相对容易实现并形式化证明正确的规范开始，然后逐步扩展需求。

在下面列出的每个步骤中，我让智能体实现并形式化证明规范。这种逐步细化使我能够将大量工作委托给智能体，同时获得我的规范可满足的反馈，并在每个里程碑验证智能体朝着最终目标的进展。我指示智能体在形式化之前先写非形式化证明。

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

F. R. Feito和M. Rivero，“基于单纯链的几何建模”，《计算机与图形》22(5)，611–619 (1998)。

doi:10.1016/S0097-8493(98)00067-3-然后我要求一个带有正确性证明的实现（CSG/Legacy/ChainIntersectionAlgorithm.lean）。

这已经满足了一个类似于我最终目标的正式规范。但