형식 검증된 3D 메시 교차 (3D mesh intersection) - 1,000줄 이상의 AI 작성 코드가 아닌 93줄의 명세를 신뢰하세요

제가 알기로, 이것은 Lean 4로 구현된 최초의 형식 검증된 3D 구성적 고체 기하학 (CSG, constructive solid geometry) 연산인 메시 교차 (mesh intersection) 구현입니다. 이 구현은 결과 메시의 표면을 정확하게 고정하고 삼각측량 (triangulation)에 대한 실질적인 형태 적합성 (well-formedness) 조건을 보장하는 간결한 명세를 통해 검증되었습니다. (관련 연구도 참조하세요.)

이 프로젝트는 또한 AI가 생성한 코드를 신뢰해야 하는 상황을 피하기 위한 실험이기도 합니다. 인간 검토자는 93줄의 형식 명세를 읽고 아래에 설명된 대로 Lean 체커를 실행함으로써 커널의 정확성을 인증할 수 있으며, 복잡한 1,000줄 이상의 AI 작성 구현 코드는 건너뛸 수 있습니다. 정확성을 증명하기 위해 AI는 60,000줄 이상의 Lean 증명 코드를 자율적으로 작성했으며, 이 또한 인간이 검사할 필요가 없습니다. Lean 체커는 LLM에 대한 신뢰 없이 컴파일 타임에 명세와의 일치성을 보장합니다. 이를 통해 우리는 구현과 증명을 블랙박스 (black box)로 취급할 수 있습니다. 저는 아래에 설명된 마일스톤을 통해 에이전트를 안내하여 여기에 제시된 결과에 도달했습니다.

웹 데모

검증된 커널을 기반으로 구축된 웹 데모를 사용해 보세요. 여기서 예시 메시를 교차하거나 STL 파일에서 메시를 가져와 교차시킬 수 있습니다. 컴파일된 Lean 코드는 브라우저에서 로컬로 실행되므로 데이터가 서버로 전송되지 않습니다. 커널은 형식 검증되었지만, UI와 글루 코드 (glue code)는 검증되지 않았음을 유의하십시오.

우리의 구현은 최첨단 (state-of-the-art) 메시 교차 (mesh intersection) 구현체들보다 훨씬 느립니다. 7만 개의 삼각형으로 구성된 두 개의 Stanford bunny의 정확한 교차를 계산하는 데 24초가 소요됩니다. 이 프로젝트에서 우리는 성능보다 정확성에 대한 인간의 검토 노력을 최소화하는 것을 우선시합니다. 이러한 성능 격차는 형식 검증된 (formally verified) 소프트웨어의 근본적인 한계가 아니며, 원칙적으로는 기존 소프트웨어만큼 빠를 수 있음에 유의하십시오. 상세 내용을 참조하십시오.

Intersection of Stanford bunny with Stanford bunny

출력 메시 (output meshes)는 아래에 설명된 속성을 충족함을 보장하지만, 우리가 아직 형식화 (formalize)하지 않은 다른 기준들에 대해서는 메시 구성 (meshing)이 최적이 아닐 수 있습니다. 예를 들어, 필요 이상으로 더 세밀한 메시를 생성할 수 있습니다.

배경 및 형식화 (Background and formalization)

삼각형 메시 (triangle mesh)는 삼각형들의 집합이며, 일반적으로 아래에서 논의할 여러 형태적 건전성 (well-formedness) 조건들 외에도 자기 자신을 관통하지 않는 닫힌 표면을 형성할 것으로 기대됩니다.

인간은 직관적으로 삼각형 메시를

삼각형 메시 (triangle meshes) 상에서 작동하는 알고리즘은 우리가 의도하는 입체 (solids)를 나타내는 메시를 효율적으로 계산할 수 있지만, 기존의 프로그래밍 언어는 이러한 입체들이 무한 집합 (infinite sets)이기 때문에 이를 명시적으로 표현하거나 그에 대한 진술을 할 수 없습니다. Lean에서는 이것이 가능하며, 예를 들어 이러한 무한 집합 간의 교차 (intersect)를 구하거나 두 무한 집합이 동일함을 증명할 수 있습니다. 더욱이, 기존 프로그래밍 언어는 특정 입력에 대해 함수가 조건을 만족하는지 테스트하는 것만 허용하는 반면, Lean을 사용하면 가능한 모든 입력 메시에 대해 함수가 조건을 만족함을 증명할 수 있습니다.

우리는 실제 메시 처리 도구에서 흔히 기대되는 조건들 — 수밀 표면 (watertight surface), 일관된 외부 방향 (coherent outward orientation)을 가지며 중복도 1 (multiplicity one)로 입체를 둘러싸는 것, 퇴화된 삼각형 (degenerate triangles)이 없는 것, 자기 교차 (self-intersections)가 없는 것 — 을 포착하기 위해 메시의 적절성 (well-formedness)을 정의하되, 한 가지 완화된 조건을 둡니다. 즉, 표면이 자기 자신과 접할 수 있지만, 면의 내부 (interiors of faces)가 아닌 모서리 (edges)와 정점 (vertices)을 따라서만 접해야 합니다. 따라서 엄격한 2-매니폴드성 (2-manifoldness)은 요구되지 않습니다. 항상 매니폴드 메시를 생성하는 교차 알고리즘이 불가능한 이유를 참조하십시오.

AI를 신뢰하지 않는 최소한의 인간 검토

입력값의 정형성(well-formedness) 전제 조건을 확인하고 메시 교차(mesh intersection)를 계산하는 커널의 정확성을 인증하기 위해, 검토자는 단 93줄의 형식 명세(formal specification)를 읽고 아래에 설명된 대로 Lean 체커(Lean checker)를 실행하기만 하면 됩니다. 검토자는 알고리즘을 구현하기 위해 AI가 작성한 1,000줄 이상의 복잡한 코드는 건너뛸 수 있습니다. Lean 체커는 어떠한 LLM(Large Language Model)에 대해서도 신뢰 가정을 하지 않으며, 컴파일 타임에 명세와의 일치성을 보장합니다.

• CSG/DataStructures.lean, CS/Def.lean, CSG/MeshIntersectWithPreconditionCheck.lean, CSG/WellFormedCheckMsg.lean 파일을 읽고 아래에 설명된 대로 Lean 체커를 실행하는 것으로 충분합니다. 주석을 제외하면 이 파일들은 단 93줄의 코드에 불과합니다. meshIntersectWithPreconditionCheck를 명시하는 정리(theorem) 문구들(동일한 이름의 파일에 있음)은 오직 이 4개 파일에 기술된 정의들에만 의존하므로, 다른 파일들은 읽을 필요가 없습니다.
• 검토자는 CSG/Impl/ 내 4개 파일에 걸쳐 1,000줄이 넘는 meshIntersectWithPreconditionCheck의 구현부를 건너뛸 수 있습니다. 이는 결정론적인(deterministic) Lean 체커에 의해 인간이 검토한 명세를 준수함이 보장되기 때문입니다.
• 이것이 가능한 이유는 CSG/Proof/에 있는 60,000줄의 AI 작성 형식 증명(formal proofs) 덕분이며, 이 역시 인간이 검사할 필요가 전혀 없습니다.

구현(implementation)에서 명세(specification)로의 이러한 압축과 단순화는, 구현이 처리해야 하는 많은 요소들이 명세로부터 완전히 분리(decoupled)될 수 있기 때문에 가능합니다:

• 구현은 알고리즘 복잡성의 상당 부분을 차지하는 특수한 기하학적 사례들을 처리해야 하지만, 수학적 공식을 일반화하여 표현할 수 있기 때문에 형식 명세는 짧습니다. Lean 검사기(checker)는 명세가 특수한 사례들을 일일이 열거하지 않더라도, 모든 특수 사례가 명세에 따라 처리되었음을 보장합니다.
• 구현은 이차 시간 복잡도(quadratic runtime complexity) 등을 피하기 위해 가속 데이터 구조(accelerating data structures)와 기타 최적화 기법을 사용합니다. 런타임 복잡도(runtime complexity)를 형식화(formalize)하지는 않았지만, Lean 검사기는 이러한 모든 최적화가 이루어진 상태에서도 여전히 명세에 부합하는 결과를 생성함을 보장합니다.

예를 들어, 향후 커밋에서 런타임 성능이나 출력 메시(mesh)의 품질을 더욱 개선하더라도, 검토된 명세는 동일하게 유지되며 재검토 없이도 명세에 대한 정확성(correctness)을 확보할 수 있습니다. 제가 어떻게 이 명세를 형성(shaping)하는 것만으로 이 프로젝트를 개발했는지도 확인해 보세요.

개발 (Development)

개발 과정에서 저는 아주 작은 명세만을 제어하였고, 증명(proofs)과 상세 구현은 에이전트(agents)에게 블랙박스(black box)로 남겨두었습니다. 저는 구현과 형식적 증명이 상대적으로 쉬울 것으로 예상되는 명세부터 시작하여 점진적으로 요구 사항을 늘려 나갔습니다. 아래 나열된 각 단계에서 저는 에이전트가 명세를 구현하고 이를 형식적으로 증명하도록 했습니다. 이러한 단계적 정교화(stepwise refinement)를 통해 저는 에이전트에게 방대한 작업량을 위임하는 동시에, 제 명세가 충족 가능한지(satisfiable)에 대한 피드백을 받고 각 마일스톤(milestone)마다 최종 목표를 향한 에이전트의 진행 상황을 확인할 수 있었습니다. 저는 에이전트들에게 형식화(formalizing)를 하기 전에 먼저 비형식적 증명(informal proofs)을 작성하도록 지시했습니다.

• 저는 먼저 에이전트에게 심플리셜 체인 (simplicial chains)을 기반으로 입체를 기술하기 위한 수학적 프레임워크를 제공하는 논문을 형식화 (formalize)하도록 시켰습니다. 이를 통해 구체적인 구현 없이도 형식적인 존재성 결과 (formal existence result)를 얻을 수 있었습니다 (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)00067-3

• 그 다음, 정당성 증명 (proof of correctness)을 포함한 구현을 요청했습니다 (CSG/Legacy/ChainIntersectionAlgorithm.lean). 이는 이미 저의 최종 목표와 유사한 형식적 명세 (formal specification)를 충족했습니다. 하지만 삼각형의 중첩(overlapping triangles) 및 기타 문제들이 여전히 허용되었고 실제로 발생하기도 했습니다.

• 이후 저는 첫 번째 구현에서 발생했던 종류의 문제들을 금지하기 위해, 출력 메시 (output mesh)에 대한 제한 사항을 지정했습니다 (현재의 WellFormedMesh 상태와 유사함). 또한, 구현 단계에서 너무 많은 특수 사례 (special cases)를 고려하지 않도록 하기 위해 입력값에 대한 일반 위치 (general position) 제한을 도입했다가 나중에 제거했습니다. 더 엄격해진 요구 사항으로 인해 전체 재구현이 필요했지만, 형식적 프레임워크 (formal framework)의 일부는 재사용할 수 있었습니다.

• 그 다음 입력값에 대한 일반 위치 제한을 제거하였고, 이로 인해 에이전트는 모든 특수한 기하학적 사례들을 올바르게 처리해야만 했습니다.

• 이어서 에이전트들에게 경계 볼륨 계층 구조 (bounding volume hierarchies) 및 기타 최적화 기법을 사용하여 구현을 최적화하도록 했습니다. 실행 시간 (runtime)에 대한 요구 사항을 형식화하지는 않았지만, Lean은 최적화된 결과가 여전히 동일한 형식적 명세를 만족함을 검증했습니다. 따라서 이 단계에서는 정당성을 보장하기 위해 아무것도 다시 검토할 필요가 없었습니다.

• 마지막으로 명세를 더욱 강화하고 검토하기 더 쉽게 만들었습니다.

이 과정을 통해 CSG/ 폴더 최상위에서 볼 수 있는 명세, CSG/Proof/의 증명, 그리고 CSG/Impl/의 구현이 완성되었습니다.

위 단계들의 대부분은 Claude Opus 4.8을 사용하여 진행했습니다. 일부 단계에서는 Fable 5를 사용하여 초기 비형식적 증명 전략 (informal proof strategy)을 수립한 다음, Opus가 형식적 증명 (formal proofs)과 구현을 작성하도록 했습니다. 위 단계 중 일부는 자율 에이전트 (autonomous agent)가 24시간 이상 작업해야 했습니다.

비형식적 명세 (informal specification)를 사용한 바이브코딩 (vibecoding)과의 비교

일반적인 바이브코딩 (vibecoding)과 대조적으로, AI와 형식 검증 (formal verification)을 결합하면 모든 입력에 대해 유효함이 보장되며, 프로그램의 후속 수정이 이루어질 때마다 해당 보장이 계속 강제되는 엄격한 보증을 얻을 수 있습니다. 하지만 일반적인 바이브코딩과 마찬가지로, 각 단계를 거치면서 개발 과정에서 일종의 부채가 쌓일 수 있습니다. 최종적으로 얻은 구현과 증명 모두, 전체적인 개요를 파악하고 있는 인간이 제어했을 때처럼 깔끔하거나 응집력 있는 설계 (cohesive design)를 따르지는 못합니다. 또한, 런타임 성능 (runtime performance)이나 출력된 솔리드 (solid)의 면(face)이 적절한 형태 조건 (well-formedness condition)을 넘어 삼각측량 (triangulated)되는 방식과 같이, 여기서 형식화하지 않은 몇 가지 제약 조건들이 존재합니다. 따라서 이러한 제약 조건들은 일반적인 바이브코딩과 마찬가지로 제어하기 어렵습니다.