1000줄 중 93줄만 읽으면 된다는 주장
3D 메시의 불리언 연산(두 입체가 겹치는 부분만 남기거나, 하나에서 다른 하나를 빼내는 연산)을 구현한 라이브러리가 공개됐는데요, 코드 자체보다 저자가 내세운 주장이 더 흥미로워요. 구현 코드 1000줄 가까이는 AI가 썼고, 사람이 읽고 신뢰해야 하는 건 93줄짜리 명세뿐이라는 거예요. 그 1000줄이 93줄의 명세를 절대 위반하지 않는다는 건 기계가 증명해준다는 구조죠.
CSG가 뭐고, 왜 그렇게 자주 터지냐면
CSG는 Constructive Solid Geometry의 줄임말인데요, 이게 뭐냐면 단순한 도형들을 합치고 빼고 겹쳐서 복잡한 형태를 만드는 방식이에요. 육면체에서 원기둥을 빼면 구멍 뚫린 블록이 되죠. OpenSCAD로 3D 프린팅 모델을 만들어본 분, Blender에서 불리언 모디파이어를 써본 분이라면 이미 매일 쓰고 있는 기능이에요.
문제는 이게 이론적으로는 초등학교 집합 문제인데 실제 구현은 악명 높게 어렵다는 점이에요. 삼각형 메시의 좌표는 부동소수점이에요. 그런데 실무 모델에는 축퇴(degenerate) 상황이 넘쳐나요. 두 면이 정확히 같은 평면에 놓이거나, 한쪽 꼭짓점이 상대편 삼각형 위에 딱 얹히거나, 모서리가 모서리를 스치듯 지나가거나요. 이럴 때 '이 점이 안쪽이냐 바깥쪽이냐'를 판정하는 계산이 소수점 열여섯째 자리 오차로 뒤집혀요. 한 삼각형에서는 안쪽이라 하고 옆 삼각형에서는 바깥쪽이라 하면 결과는 구멍 난 표면, 뒤집힌 법선, 모서리 하나에 면이 셋 붙은 비다양체 메시가 돼요. 슬라이서에 넣으면 프린트가 실패하고, 물리 엔진에 넣으면 물체가 벽을 통과해요.
그래서 진지한 구현들은 그냥 float로 계산하지 않아요. 유리수 기반의 정확 산술을 쓰거나, 부호만은 절대 틀리지 않게 보장하는 강건 술어(robust predicates)를 쓰거나, 좌표를 격자에 붙이는 스냅 라운딩을 써요. CGAL, libigl, Cork, 그리고 최근 Blender와 OpenSCAD가 채택한 Manifold 같은 엔진들이 다 이 문제와 씨름한 결과물이에요. 요컨대 이 분야는 '테스트를 아무리 돌려도 언젠가 이상한 모델이 들어와 깨지는' 영역이라, 형식 검증을 붙일 이유가 충분해요.
명세를 믿는다는 게 무슨 뜻이냐면
일반적인 테스트는 내가 상상한 입력만 확인해요. 형식 검증은 반대로 '모든 가능한 입력에 대해 이 성질이 성립한다'를 수학적으로 증명해요. 증명 보조 도구가 논리적 빈틈을 하나하나 따지고, 빠뜨린 경우가 있으면 증명이 끝나지 않아요.
그러면 사람이 할 일이 코드 검토에서 명세 검토로 바뀌어요. 결과 메시가 감싸는 모든 점은 입력 A와 B 양쪽 내부에 있어야 한다, 결과는 닫힌 표면이어야 한다, 원래 두 도형 밖의 공간은 결과에도 포함되지 않아야 한다 같은 성질을 적어두는 게 명세예요. 93줄이면 커피 한 잔 마시면서 정독할 수 있는 양이죠. 1000줄짜리 기하 알고리즘을 따라가며 오차 처리까지 검토하는 것과는 난이도가 완전히 달라요.
물론 공짜는 아니에요. 명세가 틀리면 증명도 의미가 없어요. 조건을 너무 약하게 써서 아무 구현이나 통과하는 공허한 명세를 쓰는 실수도 흔해요. 그리고 신뢰의 뿌리에는 명세 말고도 증명기의 커널과 컴파일러가 남아요. 이걸 신뢰 기반(TCB)이라고 부르는데, 검증은 신뢰를 없애는 게 아니라 신뢰해야 할 것의 크기를 줄이는 작업이에요. 이 프로젝트가 어떤 증명 도구를 쓰고 어디까지 증명을 걸었는지는 저장소를 직접 열어 확인해보시는 걸 권해요. 검증 프로젝트는 '무엇을 증명했고 무엇은 가정했는가'가 진짜 핵심이거든요.
AI 시대의 진짜 병목은 리뷰 대역폭
이 프로젝트가 던지는 더 넓은 메시지는 이거예요. LLM은 코드 생산량을 몇 배로 늘려줬는데, 사람이 코드를 읽고 판단하는 속도는 그대로예요. 그래서 앞으로 레버리지는 '코드를 잘 쓰는 능력'보다 '무엇이 옳은지를 검증 가능한 형태로 적는 능력'에 있어요.
형식 증명까지 안 가도 계단은 여러 단계가 있어요. 타입으로 잘못된 상태를 아예 표현 불가능하게 만들기, 불변식과 단정문 심기, 속성 기반 테스트(입력을 무작위로 수천 개 만들어 성질이 깨지는지 보는 방식, 파이썬 Hypothesis나 JS의 fast-check, 러스트 proptest 같은 도구)로 성질을 검사하기, 이미 신뢰받는 구현과 같은 입력으로 결과를 비교하는 차분 테스트, 그리고 퍼징까지요. 불리언 연산이라면 이런 성질을 걸 수 있어요. 같은 연산을 두 번 해도 결과가 같은가, 교집합의 부피가 두 입력의 부피보다 크지 않은가, 인자 순서를 바꿔도 같은 결과인가, 결과가 항상 닫힌 표면인가. 이 정도만 걸어도 AI가 만든 코드의 사고 대부분은 걸러져요.
한국 개발자에게 주는 시사점
CAD, 3D 프린팅, 게임 엔진, 로보틱스 시뮬레이션, 건축 BIM 쪽이라면 이 라이브러리 자체가 바로 관심 대상이에요. 불리언 연산이 깨져서 며칠 날려본 경험이 있다면 더요.
그 외 대부분의 팀에는 방법론이 남는 시사점이에요. AI에게 일을 시키는 순서를 뒤집어보세요. 지금은 보통 '이 기능 구현해줘, 테스트도 같이'라고 하는데, 그러면 구현과 테스트가 같은 오해를 공유해요. 대신 사람이 먼저 성질과 불변식을 정하고, 그걸 만족하는 구현을 AI가 채우게 하는 순서가 훨씬 안전해요. PR 템플릿에 '이 변경이 지켜야 하는 성질' 칸을 만들어두는 것만으로도 팀 문화가 달라져요. 배워둘 가치로 보면 Lean이나 Dafny 같은 도구는 주말에 맛만 봐도 사고방식이 남고, 속성 기반 테스트는 오늘 당장 도입할 수 있어요.
마무리
한 줄로 정리하면, AI가 코드를 쓰는 시대의 신뢰는 코드 리뷰의 꼼꼼함이 아니라 명세의 작음에서 나와요.
여러분 팀은 AI가 만든 코드를 어떻게 믿고 있나요? 리뷰로 버티고 있다면 그게 얼마나 더 버틸 수 있을까요? 그리고 여러분의 도메인에서 93줄로 적어낼 수 있는 핵심 성질은 무엇일까요?
🔗 출처: Hacker News