Lean 4를 이용한 형식 검증된 3D CSG 메쉬 교차

개요

이 프로젝트는 3D 구성적 입체 기하학(CSG) 메쉬 교차를 위한 형식 검증된 커널을 제공합니다. 커널은 Lean 4로 작성되었으며, 두 개의 잘 형성된(well-formed) 입력 메쉬를 교차했을 때 발생하는 정확한 입체를 정의하는 93줄의 명세(specification)에 의해 정확성이 보장됩니다. 모든 특수한 기하학적 사례를 처리하는 구현부 자체는 1000줄 이상의 AI 생성 코드이며, 이에 대응하는 증명은 60,000줄이 넘으며 모두 AI 에이전트에 의해 자율적으로 생성되었습니다. 인간 검토자는 명세를 읽고 Lean 체커를 실행하여 커널을 인증하기만 하면 되며, 구현과 증명은 블랙박스로 취급될 수 있습니다.

명세 및 신뢰성

검토자의 작업은 CSG/DataStructures.lean, CSG/Def.lean, CSG/MeshIntersectWithPreconditionCheck.lean, CSG/WellFormedCheckMsg.lean라는 네 개의 Lean 파일로 제한됩니다. 이 파일들은 meshIntersectWithPreconditionCheck_ok_spec 정리와 관련 정확성 조건을 기술하는 93줄의 코드(주석 제외)를 포함하고 있습니다. Lean 체커가 컴파일 시점에 AI가 생성한 구현이 이 정리들과 일치하는지 검증하므로, 코드를 생성한 대규모 언어 모델이나 60,000줄의 증명에 신뢰를 둘 필요가 없습니다. 명세는 수학적 기대치인 solid (meshIntersect M₁ M₂) = solid M₁ ∩ solid M₂를 포착하며, 잘 형성된 상태에 대한 전제 조건을 강제하고 잘못된 입력에 대한 정확한 오류 보고를 수행합니다.

개발 프로세스

개발은 구현 및 증명 작업을 AI 에이전트에게 위임하면서 명세를 단계적으로 정교화하는 방식으로 진행되었습니다. 저자는 심플리셜 체인(simplicial chains)에 기반한 형식적 존재성 결과에서 시작하여, 정확성 증명을 포함한 구현을 요청하고, 요구 사항을 점진적으로 강화했습니다(예: 일반 위치(general-position) 가정 제거, 잘 형성된 상태 제약 조건 추가, 경계 볼륨 계층 구조(bounding-volume-hierarchy) 최적화 통합). 각 마일스톤에서 에이전트는 현재 명세를 충족하는 코드와 증명을 생성했으며, 저자는 명세가 여전히 충족 가능한 상태인지만 확인하면 되었습니다. 대부분의 단계에서는 Claude Opus 4.8을 사용했으며, 비형식적 증명 전략을 위해 가끔 Fable 5를 사용했습니다. 최종 명세는 최상위 CSG/ 디렉토리에 위치하며, 증명은 CSG/Proof/, 구현은 CSG/Impl/에 있습니다.

성능

검증된 커널은 속도보다 인간의 검토 노력을 최소화하는 것을 우선시하기 때문에 의도적으로 최첨단 메쉬 교차 도구보다 느립니다. M4 Pro 프로세서에서 Stanford bunny의 watertight 버전 두 개(각 약 70k 삼각형)를 교차하는 데 단일 스레드 기준으로 약 24초가 소요됩니다. 이러한 속도 저하는 두 가지 주요 요인에서 기인합니다. 커널이 하드웨어 가속 부동 소수점 대신 정확한 유리수 산술을 사용한다는 점과, 실행 시간의 상당 부분을 차지하는 입력의 잘 형성된 상태 검증을 런타임에 수행한다는 점입니다. 저자들은 이러한 성능 격차가 형식 검증 소프트웨어의 근본적인 한계가 아니라고 언급합니다. 이러한 요소들이 최적화된다면 검증된 구현도 이론적으로는 기존 방식만큼 빠를 수 있습니다.

한계 및 설계 선택

• 커널의 출력 메쉬는 형식 명세를 충족하지만 필요 이상으로 세밀할 수 있습니다. 프로젝트는 최소 삼각형 개수와 같은 기준을 형식화하지 않았습니다.
• 명세가 매니폴드(manifold) 출력을 요구하지 않기 때문에, 교차하는 입체가 가장자리나 정점에서 단순히 맞닿는 경우 알고리즘이 비매니폴드 표면을 생성할 수 있습니다. 매니폴드 조건을 강제하면 일부 입력에 대해 명세를 충족할 수 없게 됩니다.
• 웹 데모 및 관련 글루 코드(예: GPU 렌더링을 위한 부동 소수점 변환)는 형식 검증되지 않았습니다. 과거 글루 코드의 버그는 정확한 유리수 좌표를 부동 소수점으로 변환할 때 발생하는 오버플로로 인해 발생한 것으로 밝혀졌습니다.
• 프로젝트는 잘 형성된 상태 외에 런타임 복잡도나 특정 삼각측량 전략을 형식화하지 않습니다.

관련 연구

• Di Vito와 Hocking (NASA Formal Methods 2021)은 PVS에서 폴리곤 병합 알고리즘을 검증했습니다.
• 저자의 이전 verified-polygon-intersection 저장소는 유사한 AI 생성 구현 및 증명 방식을 사용하여 Lean 4에서 2D 다중 폴리곤 교차를 수행했습니다.
• CGAL의 Nef polyhedra와 같이 기계 검증된 증명 대신 테스트와 비형식적 추론에 의존하는 검증되지 않은 정확한 3D 메쉬 불리언 라이브러리들이 존재합니다.

커뮤니티 토론

Hacker News 게시물에 대한 댓글에서 몇 가지 사항이 강조되었습니다:

• 저자는 검증이 커널에만 적용된다고 명확히 했습니다. UI 및 글루 코드는 검증되지 않은 상태로 남습니다 (@permute의 댓글 참조).
• 성능 및 Manifold 라이브러리와의 데이터 손상 제로 비교에 대한 질문이 제기되었습니다 (@iFire).
• LLM이 생성한 증명을 신뢰하는 것에 대한 우려가 제기되었으며, 작은 증명 커널의 중요성이 언급되었습니다 (@agentultra).
• 정확한 유리수 산술이 하드웨어 부동 소수점을 사용하지 않는 한 실용적인 유용성을 제한한다는 비판이 있었습니다 (@CyLith).
• 이 작업을 FreeCAD에 통합하는 것에 대한 관심이 표명되었습니다 (@bartvk).

결론

간결하고 사람이 읽을 수 있는 명세를 대규모 AI 생성 구현 및 증명 기반과 분리함으로써, 이 프로젝트는 형식 검증이 정확성 검토의 부담을 어떻게 줄일 수 있는지 보여줍니다. Lean 체커는 AI가 생성한 코드가 명세를 준수한다는 컴파일 타임 보증을 제공하여, 내부를 조사하지 않고도 커널을 신뢰할 수 있게 해주는 동시에, 성능 및 검증 범위 밖에 있는 특정 실용적 측면에서의 트레이드오프를 인정합니다.