1000줄 AI 코드 대신 93줄 명세 신뢰하기: 형식 검증된 3D CSG

Formally verified 3D mesh intersection - trust 93 lines of spec, not 1000+ lines of AI-written code To my knowledge, this is the first formally verified implementation of a 3D constructive solid geometry (CSG) operation: mesh intersection, implemented in Lean 4 and verified against a concise specification that pins down the surface of the resulting mesh exactly and guarantees practical well-formedness conditions on the triangulation. (See also related work .) This project is also an experiment in avoiding having to trust AI-generated code. A human reviewer only needs to read 93 lines of formal specification and run the Lean checker as described below to certify the correctness of the kernel, skipping the intricate 1000+ lines of AI-written implementation. To prove correctness, AI autonomously wrote over 60,000 lines of Lean proofs, which also never have to be inspected by a human. The Lean checker guarantees conformance to the specification at compile time, with zero trust placed in any LLM. This allows us to treat the implementation and proofs as a black box. I guided the agent through the milestones described below to arrive at the result presented here. Web demo Try out the web demo built around the verified kernel, where you can intersect example meshes or import and intersect meshes from STL files. The compiled Lean code runs locally in your browser; no data is ever sent to a server. Note that while the kernel is formally verified, the UI and glue code are not. Our implementation is far slower than state-of-the-art mesh intersection implementations: it takes 24 seconds to compute the exact intersection of two 70k-triangle Stanford bunnies. In this project we prioritize minimizing the effort of human review of correctness over performance. Note that this performance gap is not a fundamental limitation of formally verified software, which can in principle be as fast as conventional software. See details . The output meshes are guaranteed to satisfy the properties described below, but the meshing may be suboptimal with respect to other criteria that we did not yet formalize; for example, it may produce a mesh that is finer than necessary. Background and formalization A triangle mesh is a set of triangles, usually expected to form a closed surface that does not penetrate itself, among other well-formedness conditions we will discuss below. Humans intuitively associate triangle meshes with a "solid", i.e. a volume in 3D space: the set of all points not on the surface but "inside" the mesh. ("Inside" can be described mathematically by signed ray intersection counting.) This concept of solids allows us to understand what the output of algorithms such as a mesh intersection algorithm should look like, even when the implementation that works on the actual mesh data structure is intricate and has to treat many geometrical special cases with dedicated code. From a mesh intersection algorithm, we expect that the set intersection of the solids of well-formed input meshes is the solid of the output mesh and that the output is a well-formed mesh again. (We also expect that the algorithm detects and reports correctly if the inputs are not well-formed.) solid (meshIntersect M₁ M₂) = solid M₁ ∩ solid M₂ This pins down the surface of the resulting mesh exactly as the boundary of the intersected solids. Algorithms working on triangle meshes can efficiently compute meshes representing solids we have in mind, but conventional programming languages cannot express "solids" explicitly or make statements about them, since these are infinite sets. In Lean this is possible and we can for example intersect such infinite sets or prove that two infinite sets are equal. Moreover, Lean allows us to prove that a function satisfies a condition for all possible input meshes, whereas conventional programming languages only allow us to test that the function satisfies a condition for specific inputs. We define well-formedness of meshes to capture the conditions commonly expected by real-world mesh processing tools - watertight surface, bounding a solid with multiplicity one with coherent outward orientation, no degenerate triangles, no self-intersections - with one relaxation: the surface may touch itself, not at the interiors of faces but along edges and vertices. So strict 2-manifoldness is not required. See why an intersection algorithm that always produces manifold meshes is not possible . Minimal human review without trusting AI In order to certify correctness of the kernel, which checks the well-formedness preconditions of the inputs and computes the mesh intersection, a reviewer only needs to read 93 lines of formal specification and run the Lean checker as described below . The reviewer can skip the intricate 1000+ lines of AI-written implementation of the algorithm. The Lean checker guarantees conformance to the specification at compile time, with zero trust assumptions on any LLM. It suffices to read the files CSG/DataStructures.lean , CSG/Def.lean , CSG/MeshIntersectWithPreconditionCheck.lean and CSG/WellFormedCheckMsg.lean and run the Lean checker as described below. These are just 93 lines of code, excluding comments. Other files do not need to be read, since the theorem statements that specify meshIntersectWithPreconditionCheck (in the file with the same name) only rest on definitions stated in these 4 files. A reviewer can skip the implementation of meshIntersectWithPreconditionCheck that reaches over 1000 lines of code in 4 files in CSG/Impl/ , since it is guaranteed by the deterministic Lean checker to conform to the human-reviewed specification. This works thanks to 60,000 lines of AI-written formal proofs in CSG/Proof/ , which also never have to be inspected by a human. This compression and simplification from the implementation to the specification is possible because many things the implementation has to deal with can be completely decoupled from the specification: The implementation has to handle special geometrical cases , which make up much of the complexity of the algorithm, whereas the formal specification is short because the math can be formulated generally. The Lean checker guarantees that all special cases are handled in accordance with the specification without the specification enumerating the special cases. The implementation uses accelerating data structures in order to avoid quadratic runtime complexity and other optimizations. While we did not formalize runtime complexity, the Lean checker guarantees that with all these optimizations we still produce results according to the specification. If in a future commit we for example further improve the runtime performance or the quality of the output mesh, the reviewed specification stays the same and we get correctness with respect to it, without any re-review. Also see how I developed this project only through shaping this specification. Development During development, I controlled only a small specification, leaving the proofs and detailed implementation as a black box to agents. I started with a specification that I estimated was relatively easy to implement and formally prove correct and then grew the requirements. In each of the steps listed below, I had the agent implement and formally prove the specification. This stepwise refinement allowed me to delegate large pieces of work to agents, while getting feedback that my specification is satisfiable and verifying the progress of the agents toward my end goal at each milestone. I instructed agents to first write informal proofs before formalizing. I started by having an agent formalize a paper that provides a mathematical framework for describing solids based on simplicial chains. This gave me a formal existence result without concrete implementation (see CSG/Legacy/ChainIntersectionExistence.lean ). F. R. Feito and M. Rivero, "Geometric modelling based on simplicial chains," Computers & Graphics 22 (5), 611–619 (1998). doi:10.1016/S0097-8493(98)00