를 이용해 최초로 정형 검증된 3D CSG(구성적 고체

93줄의 정형 명세로 1,000줄 이상의 AI 구현체 무결성을 인증하며 3D CSG(구성적 고체 기하학) 메쉬 교차의 첫 번째 정형 검증 구현체가 개발됐다. Lean 4(정형 검증 언어)를 활용해 간결한 사양을 바탕으로 검증을 수행했다. 구현물은 결과 메쉬의 표면을 정확하게 정의하는 데 집중했다. 삼각형 분할의 실질적인 웰폼드니스(well-formedness, 구조적 적합성) 조건을 보장해 구현의 정확성을 확보했다.

7만 개의 삼각형으로 구성된 Stanford bunnies(3D 모델 데이터셋) 두 개의 정확한 교차를 계산하는 데 24초가 소요된다. 최신 메쉬 교차 구현체와 비교해 처리 속도가 현저히 느린 수치다. 이러한 성능 저하는 정형 검증 소프트웨어가 가진 근본적인 한계로 인한 현상이 아니다. 인간이 정확성을 검토하는 데 드는 노력을 최소화하기 위해 의도적으로 성능을 희생한 결과다.

정확성 검토의 효율성을 성능보다 우선순위에 뒀다. 최신 구현체의 속도를 추종하기보다 인간이 검증 가능한 코드를 작성하는 것에 집중했다. 결과적으로 처리 속도를 낮추는 대신 인간 리뷰어의 검토 비용을 줄이는 설계 방향을 택하며 수학적 무결성 증명을 우선했다.

AI가 생성한 복잡한 코드 대신 93줄의 정형 사양과 Lean

인간 검토자는 1,000줄 이상의 AI 작성 구현 코드를 읽는 대신 93줄의 정형 사양만 확인한다. 정형 사양은 시스템이 만족해야 할 조건을 수학적으로 정의한 명세서다. 이후 Lean checker(정형 검증 도구)를 실행하면 컴파일 타임에 사양 준수 여부가 보장된다. 복잡한 구현 코드를 일일이 분석하는 과정을 생략하고도 커널의 정확성을 인증할 수 있다. LLM(대규모 언어 모델)에 대한 신뢰를 전혀 두지 않고 수학적 증명만으로 무결성을 확보한 구조다.

AI는 1,000줄 이상의 구현 코드와 60,000줄 이상의 Lean 증명을 자율적으로 작성했다. Lean은 수학적 정리를 증명하는 대화형 정리 증명기다. 60,000줄이 넘는 방대한 분량의 증명 역시 인간이 일일이 검토할 필요가 없다. 구현체와 증명 과정을 블랙박스로 처리해 검토자의 분석 부담을 완전히 제거했다. AI가 스스로 생성한 구현과 증명을 Lean checker가 기계적으로 검증하며, 인간은 최종적으로 93줄의 사양만 검토해 전체 시스템의 정확성을 확정한다. 이 과정에서 AI가 작성한 증명은 인간의 개입 없이 Lean checker의 인증만으로 유효성을 인정받는다.

확인해야 할 핵심 지점

정형 검증된 Lean(린, 정형 검증 언어) 커널과 동일 명세의 C++ 구현체를 비교해 블랙박스 테스트로 잡지 못한 3가지 고유 버그를 발견했다. AI 에이전트에게 구현과 증명을 위임하며 사양을 단계적으로 구체화하는 방식을 통해 이를 검증했다. 구현과 증명이 쉬운 작은 사양에서 시작해 요구사항을 점진적으로 확장하며 사양의 충족 가능성과 진행 상황을 확인했다.

출력 메쉬는 수밀 표면(watertight surface) 및 자기 교차 없음 등 웰폼드니스(well-formedness) 조건을 만족해야 한다. 일관된 외부 방향을 가진 단일 고체 경계와 퇴화 삼각형 없음 등이 여기에 포함된다. 표면이 면의 내부가 아닌 모서리와 정점을 따라 서로 닿는 것은 허용한다.

UI 및 글루 코드, 런타임 성능, 출력 메쉬의 삼각형 분할 품질은 정형 검증 범위에서 제외된다. AI 생성 코드를 신뢰하는 기준을 구현체 리뷰에서 정형 명세 리뷰로 전환해 검토 비용을 낮추고 무결성을 확보해야 한다.