Lean 4 中经过正式验证的 3D CSG 网格交集

Overview

该项目提供了一个用于 3D 构造实体几何（CSG）网格交集的经过正式验证的内核。该内核使用 Lean 4 编写，其正确性由一个 93 行的规范保证，该规范定义了两个格式良好的输入网格相交后得到的确实体。实现本身处理了所有特殊的几何情况，超过 1000 行的 AI 生成代码，对应的证明超过 60 000 行，全部由 AI 代理自主生成。人类审查者只需阅读规范并运行 Lean 检查器来认证内核；实现和证明可以被视为黑箱。

Specification and Trust

审查者的任务仅限于四个 Lean 文件：CSG/DataStructures.lean、CSG/Def.lean、CSG/MeshIntersectWithPreconditionCheck.lean 和 CSG/WellFormedCheckMsg.lean。它们共计 93 行代码（不含注释），陈述了定理 meshIntersectWithPreconditionCheck_ok_spec 及相关的正确性条件。由于 Lean 检查器在编译时验证 AI 生成的实现符合这些定理，因此不会将信任放在生成代码或 60 000 行证明的大型语言模型上。规范捕捉了数学期望：solid (meshIntersect M₁ M₂) = solid M₁ ∩ solid M₂，并强制执行格式良好的前置条件，以及对格式错误输入的正确错误报告。

Development Process

开发通过在将实现和证明工作委托给 AI 代理的同时，对规范进行逐步细化来进行。作者最初基于单纯链提出了一个形式存在结果，然后请求带有正确性证明的实现，并逐步收紧需求（例如，移除一般位置假设，添加格式良好约束，并引入包围体积层次结构优化）。在每个里程碑，代理生成了满足当前规范的代码和证明；作者只需验证规范仍然可满足。大多数步骤使用 Claude Opus 4.8，偶尔使用 Fable 5 进行非正式证明策略。最终规范位于顶级 CSG/ 目录中，证明位于 CSG/Proof/，实现位于 CSG/Impl/。

Performance

经过验证的内核故意比最先进的网格交集工具慢，因为该项目优先考虑最小化人工审查工作而非速度。在 M4 Pro 处理器上，交叉两个斯坦福兔子的无孔版本（每个约 70k 三角形）单线程大约需要 24 秒。减速主要源于两个因素：内核使用精确的有理数运算而不是硬件加速的浮点数，并且它在运行时验证输入的格式良好性，这占据了总执行时间的相当大比例。作者指出，这种性能差距并不是正式验证软件的根本限制；如果对这些因素进行优化，经过验证的实现在原则上可以达到与传统工具相当的速度。

Limitations and Design Choices

• 内核的输出网格满足正式规范，但可能比必要的更细；项目未正式化诸如最小三角形数量之类的标准。
• 由于规范不要求流形输出，当相交的实体仅在边或顶点处相接时，算法可能生成非流形表面。施加流形条件会使得对于某些输入，规范变得不可满足。
• 网页演示及其关联的胶水代码（例如，用于 GPU 渲染的转换为浮点数）未经过正式验证；胶水代码中的过去错误被追溯为在将精确有理数坐标转换为浮点数时发生的溢出。
• 项目未正式化运行时复杂度或超出良好形成性的特定三角化策略。

Related Work

• Di Vito 和 Hocking（NASA Formal Methods 2021）在 PVS 中验证了一个多边形合并算法。
• 作者之前的 verified-polygon-intersection 仓库在 Lean 4 中使用类似的 AI 生成实现和证明方法执行了 2D 多重多边形交集。
• 存在未经验证的精确 3D 网格布尔库，例如 CGAL 的 Nef 多面体，它们依赖于测试和非正式推理，而不是机器检查的证明。

Community Discussion

Hacker News 帖子的评论指出了几点：

• 作者澄清验证仅适用于内核；UI 和胶水代码仍未验证（参见 @permute 的评论）。
• 有关与 Manifold 库的性能和零腐蚀比较的问题被提出（@iFire）。
• 对于信任 LLM 生成的证明的担忧被提出，强调了小证明内核的重要性（@agentultra）。
• 批评指出，除非使用硬件浮点数，否则精确有理数运算限制了实际实用性（@CyLith）。
• 对于将工作集成到 FreeCAD 的兴趣被表达（@bartvk）。

Conclusion

通过将简洁、可读的人类规范与大型 AI 生成的实现和证明基础分离，该项目展示了正式验证如何减少正确性审查的负担。Lean 检查器提供编译时保证，确保 AI 生成的代码符合规范，从而使内核可以在不检查其内部的情况下被信任，同时承认在性能和某些实际方面的权衡，这些方面仍然超出验证范围。