verified-3d-mesh-intersection: 形式化验证的3D网格相交工具
Show HN: Formally verified 3D CSG: Trust 93 lines spec, not 1000 lines AI code
这是一个基于Lean 4实现的3D构造实体几何（CSG）网格相交项目，据我所知是首个经过形式化验证的同类实现。它通过93行精简的规范定义，确保输出网格的几何正确性，而无需人工审查AI生成的1000多行复杂代码或6万行证明。虽然性能暂未优化，但项目核心在于将人类审查成本降至最低，让开发者能完全信任由LLM生成的代码逻辑。用户可在本地浏览器中体验Web Demo，直接处理STL文件进行网格相交运算。
只需阅读93行形式化规范并运行Lean检查器，即可完全信任由AI生成的1000多行复杂代码，无需对任何大语言模型抱有任何信任假设。
HN 评论区
48- permute
注意，这里的声明是针对计算网格相交的内核（kernel），而非 Web 演示：虽然内核经过了形式化验证，但 UI 和调用内核的胶水代码（glue code）并没有。我曾遇到过一个问题，看起来像是生成的网格上有破洞：后来发现是胶水代码中的一个溢出 bug（现已修复），该代码负责将输出网格的精确有理数坐标（我们已证明其符合规范）转换为浮点数，再发送给 GPU。所有几何运算都在内核内部进行，而我们知道内核的规范是成立的。
- bob1029
这真的很酷。我认为 CSG（构造实体几何）是构建 3D 环境（尤其是“室内”场景）最直观的方式之一。在正确的 CSG 工作流中，几何体永远不会被破坏。通过构建刷（brush）的层级结构，可以快速迭代参数，比如走廊的长度，或者从一个目标点到另一个目标点所需的时间。通常，你只需要对单个刷应用一个变换，就能实现那些在非 CSG 工作流中需要耗费整个下午才能恢复的效果。
目前商业游戏引擎中 CSG 的情况相当糟糕。Unity 有一些第三方方案效果不错，但它们也充满 bug，且与生态系统的其他部分集成不佳。有一段时间我曾考虑自己编写 CSG 实现，但阻碍我的正是本项目所解决的那些难题。EditorWindow 的集成部分对我来说没那么可怕（尽管也挺痛苦）。真正让我望而却步的是高级几何和集合运算。看来，这条“恶龙”至少已经被（部分）斩杀了。
- brandonpelfrey
这看起来是非常酷的工作。如果我漏掉了什么，请见谅：我仍然不太确定，我们如何从形式化证明（很棒！）过渡到一个实现（无论是 LLM 还是人类编写的），并且能确信该实现确实符合证明？我们如何知道实现与证明中的描述精确对应？
- agentultra
> 人类审查员只需阅读 93 行形式化规范并运行 Lean 检查器，即可认证内核的正确性，而无需检查那 1000 多行由 AI 编写的复杂实现代码。为了证明正确性，AI 自主编写了超过 60,000 行 Lean 证明，这些证明也永远不需要人类检查。
我对这种方法很好奇，因为这类声明让我很难相信。证明内核（proof kernel）背后有一个理论：它们必须很小，因为需要由人类信任和验证。否则整个系统就会崩溃。
我们如何信任一个由 LLM 生成的内核确实证明了正确的事情？
- swiftcoder
好吧，这非常酷。我还没完全搞懂它是如何处理数值稳定性问题的——这是基于网格的 CSG 操作真正的死敌。