Show HN: 93줄 스펙만 믿으면 되는 형식 검증된 3D CSG (AI 코드 1000줄은 안 읽어도 됨)

TL;DR Highlight

93줄 스펙만 읽고 Lean 검증기를 돌리면 AI가 쓴 1000줄+ 구현의 정확성이 보장된다

Who Should Read

AI가 쓴 코드를 어떻게 믿고 배포할지 고민하는 백엔드·에이전트 개발자

Core Mechanics

스펙 93줄만 읽으면 된다
- Lean 4로 3D 메시 교집합(CSG)을 구현하고 검증했다.
- 사람은 스펙 4개 파일(93줄, 주석 제외)만 읽고 Lean 검증기를 돌리면 된다.
- AI가 쓴 구현 1000줄+와 증명 6만 줄+는 읽지 않아도 된다.
검증기가 LLM을 대신 믿어준다
- 구현이 스펙에 맞는지는 컴파일 시점에 Lean 검증기(결정적 프로그램)가 확인한다.
- LLM에 대한 신뢰는 필요 없다고 저자는 말한다.
- 스펙은 solid(meshIntersect M₁ M₂) = solid M₁ ∩ solid M₂ 형태로 짧게 쓸 수 있었다.
스펙을 조금씩 키우며 에이전트에게 맡겼다
- 쉬운 스펙에서 시작해 요구사항을 단계별로 늘렸다.
- 단계마다 에이전트가 구현과 증명을 다시 썼다.
- 마지막에 BVH(경계 볼륨 계층) 같은 최적화를 넣어도 스펙은 그대로라 재검토가 필요 없었다.
같은 스펙을 C++로 vibecoding하니 버그 3개
- Opus 4.8에 비형식 스펙을 주고 C++로 구현시켰고 길이는 비슷한 1000줄+였다.
- 단위 테스트를 직접 썼는데도 독립 에이전트 검토에서 서로 다른 버그 3개가 재현됐다.
- 저자는 블랙박스 테스트로는 잡기 거의 불가능한 드문 버그라고 한다.

Community Reactions

스펙이 정말 맞는지 묻는 의견
- 증명 커널은 작아야 신뢰할 수 있다는 이론이 있는데 LLM이 만든 증명을 어떻게 믿느냐는 의문이 나왔다.
- 검증된 증명이 실제 구현과 어떻게 정확히 이어지는지 모르겠다는 질문도 있었다.
웹 데모 버그는 커널이 아니었다는 저자 설명
- 결과 메시에 구멍이 보였는데 정확한 유리수 좌표를 GPU용 float로 바꾸는 글루 코드의 오버플로 때문이었다(수정됨).
- 검증 대상은 커널이고 UI와 글루 코드는 검증 대상이 아니라고 저자가 덧붙였다.
실용성에 대한 반론
- 하드웨어 가속 float로 구현되지 않으면 성능이 부족해 실무에서 쓰기 어렵다는 의견이 있었다.
- 수치 안정성 처리와 float로 확장했을 때 동일 평면 면 처리 가능 여부를 궁금해하는 댓글도 있었다.
기존 라이브러리와 비교 요청
- elalish/manifold와 성능·무손상 면에서 비교해 달라는 요청이 있었다.
- manifold의 Apache2 단위 테스트를 써 보라는 제안도 있었다.
- union, difference 확장과 퍼즈 테스트 여부를 묻는 댓글도 있었다.
AI 코드는 읽기보다 검사기가 낫다는 경험
- Claude와 함께 만든 코드는 읽기보다 끝까지 돌려 보며 신뢰를 쌓았다는 경험이 있었다.

How to Apply

AI 코드에 대한 스펙 먼저 짧게 써 보기
- 오늘 AI가 짜는 함수 하나를 골라 입출력 관계를 한 줄 속성으로 적어라.
- 예를 들어 정렬 결과는 입력의 순열이며 오름차순이라고 쓴다.
- 구현을 읽기 전에 이 속성부터 테스트로 옮겨라.
property-based 테스트로 AI 구현 검증하기
- 핵심 로직에 Hypothesis나 fast-check로 속성 테스트를 붙여라.
- 단위 테스트 통과 후에도 무작위 입력으로 AI 구현을 한 번 더 돌려라.
스펙을 단계별로 키우며 에이전트에 위임하기
- 쉬운 요구사항부터 시작해 마일스톤마다 에이전트에게 구현과 검증을 시켜라.
- 각 단계에서 스펙이 만족 가능한지 확인한 뒤 다음 요구사항을 추가하라.
다른 에이전트로 교차 검토 돌리기
- 구현을 쓴 에이전트와 다른 에이전트에게 비형식 스펙과 코드를 비교해 버그를 재현하게 하라.
- 재현된 입력은 회귀 테스트로 저장하라.

Try It

복사해서 바로 해보기

# Claude 또는 ChatGPT에 붙여넣기 (논문 방법의 간이 버전: 스펙 먼저, 구현은 블랙박스)

아래 함수에 대해 구현은 보지 말고 스펙부터 작성해줘.
함수 설명: {{함수 설명}}

1. 입력과 출력 사이에 항상 성립해야 하는 속성을 5줄 이내로 써줘.
2. 그 속성을 Hypothesis(Python) property-based 테스트로 바꿔줘.
3. 구현은 다른 관점에서 따로 작성해줘.

이어서 해 볼 것: 구현 코드 {{구현}}을 붙여넣고 테스트가 깨지는 반례를 찾아달라고 요청해 보세요.

Terminology

Lean 4코드와 수학 증명을 함께 쓸 수 있는 언어다. 컴파일러가 증명이 맞는지 기계적으로 확인해 준다.

CSGConstructive Solid Geometry의 약자다. 교집합·합집합·차집합으로 도형을 조립하는 3D 모델링 방식이다.

형식 검증코드가 스펙을 모든 입력에서 만족함을 수학적으로 증명하는 일이다. 테스트가 일부 입력만 확인하는 것과 다르다.

BVH경계 볼륨 계층이다. 삼각형을 상자로 묶어 계층화해 충돌 검사 횟수를 줄이는 자료구조다.

watertight구멍 없이 닫힌 표면을 말한다. 물을 담아도 새지 않는 그릇 같은 메시다.