Show HN: Formally verified 3D CSG: Trust 93 lines spec, not 1000 lines AI code

개요

Formally verified 3D CSG(Constructive Solid Geometry) 구현체는 93줄의 간결한 명세에 대한 신뢰를 바탕으로 1000줄 이상의 AI 생성 코드를 검증하며, 이는 3D 메쉬 교차 연산에 대한 최초의 형식 검증 사례입니다.

주요 내용

* 형식 검증된 3D CSG 구현: Lean 4를 사용하여 3D 메쉬 교차 연산을 형식 검증했으며, 결과 메쉬 표면을 정확하게 정의하고 실제적인 잘-구성됨(well-formedness) 조건을 보장하는 간결한 명세와 비교 검증되었습니다.
* AI 코드의 형식 검증: AI가 60,000줄 이상의 Lean 증명을 자율적으로 작성했으며, 인간 검토자는 93줄의 형식 명세만 읽고 Lean 검증기를 실행하여 커널의 정확성을 인증할 수 있습니다. LLM에 대한 신뢰 없이 컴파일 시점에 명세와의 일관성을 보장합니다.
* 개발 과정: 개발자는 작은 명세를 제어하고 증명 및 상세 구현은 에이전트에게 위임하는 단계적 정제 방식을 사용했습니다. 이를 통해 에이전트 작업 위임, 명세 만족성 피드백 획득, 진행 상황 검증을 수행했습니다.
* 성능 및 실무적 고려사항: 현재 구현은 최첨단 메쉬 교차 구현체보다 훨씬 느리며, 70k 삼각형 메쉬의 정확한 교차 계산에 24초가 소요됩니다. 본 프로젝트는 성능보다 인간 검토의 노력을 최소화하는 데 중점을 두었습니다.
* 웹 데모: 검증된 커널을 기반으로 로컬 브라우저에서 실행되는 웹 데모를 제공하며, 서버로 데이터를 전송하지 않습니다. UI 및 글루 코드는 형식 검증되지 않았습니다.
* 명세와 구현의 분리: 형식 명세는 수학적 개념을 일반화하여 간결하게 표현하며, 구현은 복잡한 기하학적 특수 사례를 처리합니다. Lean 검증기는 명세가 모든 특수 사례를 처리함을 보장합니다.
* C++ 구현과의 비교: 비형식적 명세로 AI가 작성한 C++ 구현에서는 3가지 버그가 발견되었으나, 형식 검증된 Lean 구현에서는 이러한 버그가 없습니다.
* 구축 및 검사: Elan을 사용하며, Lean 버전은 lean-toolchain 파일에 고정되어 있습니다. WebAssembly 빌드를 위해 emscripten, zstd, node/npm 등이 필요합니다.
* 일반적으로 매니폴드하지 않은 출력 메쉬: 특정 입력에 대해 교차 연산 결과가 매니폴드하지 않은 표면을 가질 수 있으며, 이는 모든 알고리즘이 매니폴드 출력을 보장하는 것이 불가능하기 때문입니다.

시사점

AI와 형식 검증을 결합하면 모든 입력에 대해 엄격한 정확성 보장을 제공하며, 코드 수정 시에도 지속적으로 유지됩니다. 이는 복잡한 기하학적 연산에서 인간의 검토 부담을 줄이고 코드의 신뢰성을 높이는 데 기여합니다.