Show HN：形式化验证的3D CSG——信任93行规范，而非1000行AI代码
当形式化验证遇上AI生成代码：3D网格交集实现的新范式
近日，一个名为“Formally verified 3D CSG”的项目在Hacker News上引发关注。该项目号称是首个经过形式化验证的3D构造实体几何（CSG）操作实现——具体来说，是一个在Lean 4中实现的网格交集算法。其核心亮点在于：人类审查者只需阅读93行形式化规范，并运行Lean检查器，即可认证内核的正确性，而无需信任由AI编写的1000多行实现代码。
信任的转移：从AI代码到规范
在AI辅助编程日益普及的今天，生成的代码是否可靠始终是悬在开发者头上的“达摩克利斯之剑”。该项目通过一种巧妙的方式规避了这一问题：AI不仅编写了实现代码，还自主撰写了超过60,000行的Lean证明，但这些证明同样无需人工审查。Lean检查器在编译时确保实现与规范一致，零信任被置于任何大语言模型（LLM）之上。开发者只需聚焦于那93行简洁的规范——它精确描述了结果网格的表面，并保证了三角剖分的实际良构性条件。
性能的权衡：正确性优先
当然，这种严格的形式化验证并非没有代价。根据项目披露，其内核计算两个各含7万个三角形的斯坦福兔子网格的交集需要24秒，远慢于当前最先进的网格交集实现。项目明确表示，其优先目标是最小化人类审查正确性的工作量，而非追求极致性能。不过，作者指出这种性能差距并非形式化验证的根本局限——原则上，形式化验证软件可以达到与传统软件相同的速度。
背景与形式化
三角网格通常被视为3D空间中实体的边界表示，但实际应用中往往存在自交、非流形等问题。该项目的形式化规范不仅定义了精确的表面，还保证了实用的良构性条件，如闭合性、无自交等。这意味着输出网格在数学上是可靠的，尽管在网格细化程度等其他未形式化的标准上可能并非最优。
行业意义
这一项目为AI代码的可信性提供了新思路：将AI作为黑盒生成器，而将信任锚定在形式化规范和证明检查器上。对于需要高安全性的领域（如CAD、医疗影像、机器人仿真），这种方法可能比依赖代码审查或测试更为可靠。同时，它也展示了Lean 4在复杂几何计算验证中的潜力。
结语
虽然当前性能尚不实用，但该项目无疑为形式化验证与AI生成代码的结合树立了一个里程碑。它提醒我们：在追求AI效率的同时，形式化方法仍然是确保关键系统正确性的“黄金标准”。随着形式化验证工具链的成熟和AI证明能力的提升，未来或许会出现更多“规范可信、实现黑盒”的可靠系统。
