形式化验证3D CSG：93行规范胜过千行AI代码

在人工智能代码生成日益普及的当下，如何确保AI生成代码的正确性成为开发者面临的核心挑战。近日，一项名为“verified-3d-mesh-intersection”的开源项目在Hacker News上引发关注，它首次实现了3D构造实体几何（CSG）操作——网格相交的形式化验证，提供了一个令人耳目一新的可信度方案。

该项目使用Lean 4证明助手，对3D网格相交算法进行了形式化验证。其核心思路是：人类审查者只需阅读93行形式化规范，然后运行Lean检查器，即可认证内核的正确性，而完全跳过AI编写的1000多行实现代码。更令人印象深刻的是，AI自主编写了超过6万行Lean证明代码，这些证明同样无需人类检查——Lean检查器在编译时保证实现与规范一致，对任何大语言模型都不需要信任。

项目作者指出，这种做法允许将实现和证明视为黑盒，人类只需关注规范本身。通过引导AI代理完成一系列里程碑，最终得到了当前的结果。项目还提供了一个基于验证内核的网页演示，用户可以在浏览器中本地运行编译后的Lean代码，导入STL文件并执行网格相交操作，所有数据都不会发送到服务器。

从技术角度看，网格相交是3D CSG操作的基础。一个三角形网格通常被期望形成封闭且不自相交的表面。人类直观上将网格与“实体”关联起来——即空间中不在表面上但位于网格内部的点集。这种实体概念使得理解网格相交算法的输出变得直观：对于良好格式的输入网格，其实体集合的交集应等于输出网格的实体，且输出网格本身也是良好格式的。

然而，实际实现需要处理大量几何特殊情况，代码往往复杂且容易出错。传统上，开发者依赖测试来验证正确性，但测试无法覆盖所有边界情况。形式化验证则提供了一种数学上严格的保证：只要规范正确，实现就一定符合规范。

值得注意的是，该项目在性能上做出了明确取舍。目前，它计算两个各有7万个三角形的斯坦福兔子网格的精确相交需要24秒，远慢于最先进的网格相交实现。作者强调，这种性能差距并非形式化验证软件的固有局限——理论上，形式化验证软件可以达到与传统软件相当的速度。当前项目优先考虑最小化人类对正确性的审查工作量，而非性能优化。

输出网格虽然保证满足规范中描述的性质，但在其他未形式化的标准上可能并非最优。例如，它可能生成比必要更细的网格。这表明形式化验证需要明确界定需要保证的性质范围，而实际应用中的其他需求（如网格质量）可能需要额外的形式化工作。

这一项目为AI代码生成的可信度问题提供了一个有价值的参考。在AI编写代码越来越普遍的时代，如何确保这些代码的正确性成为关键挑战。形式化验证提供了一条路径：通过将人类审查聚焦于简洁的规范，而将复杂的实现和证明交给AI和自动检查器，可以在不牺牲可信度的前提下充分利用AI的生成能力。

项目在GitHub上开源，社区可以查看完整的规范、实现和证明代码。对于关注AI安全、形式化验证和3D图形学的开发者来说，这是一个值得深入研究的案例。