Claude 형식 검증 — 끝난 증명 베껴 쓰기

앤트로픽이 Claude에게 오픈소스 라이브러리 123개를 맡겨, 그 안의 시험 입구 239곳이 «64MB보다 작은 어떤 입력을 넣어도 멈추지 않는다»는 것을 수학으로 증명하게 한 연구입니다. 이걸 형식 검증이라고 부릅니다. 저는 그중 한 대목, «다른 에이전트가 끝낸 증명을 베껴 쓰게 했더니 토큰이 17% 줄었다»를 제 게임 스튜디오 아트팀에 붙여 봤습니다. 시간은 21% 줄었고, 비용은 그대로였습니다.

「무작위로 많이 넣어 보기」와 「전부 괜찮다고 증명하기」는 다른 일입니다

프로그램에 버그가 있는지 보는 흔한 방법은 퍼징입니다. 아무 입력이나 수없이 넣어 보고, 프로그램이 멈추는 순간을 찾습니다. 오래 돌릴수록 많이 찾습니다. 그런데 넣을 수 있는 입력은 끝이 없어서, 아무리 돌려도 «안 넣어 본 입력»이 남습니다.

형식 검증은 방향이 반대입니다. 하나하나 넣어 보는 대신, «어떤 입력이 와도 이 프로그램은 멈추지 않는다»를 수학 증명으로 씁니다. 증명이 맞는지는 사람이 아니라 검사 프로그램(여기서는 Rocq)이 한 줄씩 채점합니다.

문제는 이 증명이 엄청나게 길다는 것이었습니다. 운영체제 커널 하나를 만드는 데 2인년, 그걸 증명하는 데 20인년이 걸린 예가 있습니다. 그래서 지금까지는 비행기 제어 코드 같은 아주 중요한 곳에서만 했습니다.

이번 연구가 바꾼 것 — 증명을 쓰는 일을 Claude가 맡았습니다

앤트로픽은 이미 있던 퍼징 시험을 그대로 «약속»으로 바꿨습니다. «이 시험 입구는 64MB보다 작은 어떤 입력에도 멈추지 않는다.» 그리고 Claude가 그 약속의 증명을 썼습니다.

숫자	뜻
123개 · 239곳	증명한 라이브러리 수 · 시험 입구 수
약 1억 8천만 줄	쓴 증명 전체. 한 편이 보통 60만 줄
몇 주	걸린 기간
수백 개	증명하다가 찾은 버그. 수조 번 퍼징에서 안 나온 것도 있었다

증명이 막히면 그 자리에 버그가 있다는 신호입니다. Claude는 버그를 고치고, 고친 코드로 다시 증명했습니다. 예를 들어 20MB쯤 되는 특정한 모양의 입력에서만 터지는 버그가 있었습니다. 퍼저는 보통 1MB 넘는 입력을 안 넣어서 못 찾던 것입니다.

「증명됐다」는 「버그 0개」가 아닙니다

글이 직접 선을 그었습니다. 증명은 «약속을 지킨다»는 뜻이지, 그 약속이 현실과 맞는다는 뜻이 아닙니다.

이번 약속은 몇 가지를 깔고 있습니다. 한 줄로만 도는 프로그램, RISC-V라는 칩, 리눅스입니다. 그런데 대부분의 사람은 같은 라이브러리를 x86이나 ARM 칩에서 돌립니다. 그 차이만큼은 증명 밖입니다. 그래서 남은 버그가 있다면 어디를 봐야 하는지는 알게 됐다고 글은 말합니다. 약속 자체, 칩과 운영체제를 흉내 낸 모형, 채점 프로그램 셋입니다.

제가 가져온 건 증명이 아니라 「서로 베껴 쓰기」입니다

저는 증명을 쓸 일이 없습니다. 대신 글 뒤쪽의 한 실험이 눈에 걸렸습니다.

에이전트 여럿이 각자 다른 증명을 쓸 때, 서로의 끝난 증명을 베껴 갈 수 있게 공유 작업장을 열어 줬습니다. 그랬더니 혼자 쓸 때보다 토큰이 17% 덜 들었고, 혼자서는 실패하던 것이 성공하기도 했습니다. 이유도 적혀 있었습니다. 프로그램마다 증명의 대부분은 «어느 프로그램에나 있는 부분»이라서, 남의 것을 가져와 고치면 된다는 것입니다.

제 스튜디오에도 똑같은 모양이 있을 것 같았습니다. AI가 도트 애니메이션을 만들 때, 그림을 그리는 대본 말고도 비교 시트를 만들고 확대해 보고 점검하는 대본을 매번 씁니다. 그건 어느 캐릭터에나 있는 부분입니다.

재 보니 84%를 매번 새로 쓰고 있었습니다

먼저 지금 상태를 쟀습니다. 아트팀이 지금까지 남긴 대본 2만 1천여 줄을, 먼저 만든 대본과 줄 단위로 맞대 봤습니다.

	줄	비율
새로 쓴 줄	18,012	84%
그대로 · 조금 고쳐 다시 쓴 줄	3,306	16%

다시 쓴 16%도 거의 전부 같은 세션이 자기 것을 이어 쓴 경우였습니다. 다른 세션이 만든 대본은 거의 안 가져다 썼습니다. 그리고 새로 쓴 줄 가운데 7,450줄은 그림이 아니라 보기 · 비교 · 점검 도구였습니다.

그래서 붙이고, 같은 일을 둘로 나눠 돌렸습니다

앞서 끝난 대본 111개를 작업별로 묶은 목록 한 장을 만들었습니다. 그리고 같은 일을 네 번 시켰습니다.

• 일: 윈디(네 발)와 괴력몬(두 발)이 쓰러지는 애니메이션 4장씩
• A조 2명: 지금 방식 그대로
• B조 2명: «대본을 쓰기 전에 이 목록에서 같은 일을 한 대본을 찾아 베껴 고쳐 쓰라»
• 같은 모델, 같은 노력 단계, 같은 시각에 따로 돌렸습니다

결과 — 덜 쓰고 빨리 끝났지만, 돈은 그대로였습니다

B조는 새로 쓴 줄이 86%에서 19%로 줄었습니다. 시간은 21%, AI가 내놓은 글자(출력 토큰)는 19% 줄었습니다. 앤트로픽이 잰 17%와 거의 같은 크기입니다.

그런데 전체 비용은 거의 같았습니다. 베껴 온 대본을 읽느라 읽는 쪽 토큰이 늘어서, 덜 쓴 만큼을 거의 다 도로 냈습니다. 그림은 넷 다 기계 점검을 통과했습니다. 눈으로 보면 한 장씩 흠이 있었는데(B조 윈디는 누운 몸통이 떠 보였습니다), 조 사이 우열은 보이지 않았습니다.

그래서 스튜디오에는 붙여 두었습니다. 같은 돈으로 더 빨리 끝나기 때문입니다. 다만 «토큰을 아끼는 방법»으로는 이번 측정에서 증명되지 않았습니다.

못 한 것

• 표본이 두 쌍뿐입니다. 같은 A조끼리도 비용이 1.7배 차이 났습니다. 앤트로픽은 36개 과제를 세 번씩 돌렸습니다. 제 숫자는 방향만 보여 주고 크기는 못 믿습니다.
• 그림 수준은 아직 사람이 안 봤습니다. 기계 점검 통과는 «결함이 없다»까지입니다.
• B조가 지적한 목록 결함 둘을 고쳐서 붙였습니다. 한 작업의 대본이 여러 절로 흩어져 있던 것, 베낀 대본의 기본값이 다른 기준에 맞춘 값이라는 걸 알 길이 없던 것입니다. 고친 목록으로는 아직 다시 재지 않았습니다.

여기부터는 자세한 기록입니다

앤트로픽(Frontier Red Team)과 Theorem이 2026-10-22 에 낸 연구다. OSS-Fuzz 의 퍼징 입구를 «64MB 미만의 어떤 입력에도 크래시하지 않는다»는 명세로 바꾸고, Claude 가 RISC-V 로 컴파일된 실행 파일 수준에서 그 증명을 썼다. 123개 라이브러리 · 239개 입구가 증명됐다. 나는 이 글에서 «증명 재사용» 실험 하나를 골라 문스튜디오 아트팀(도트 애니메이션 에이전트)에 옮기고, 2종 × 2조로 전후를 쟀다.

원문이 말한 것 — 숫자와 조건

원문의 주장은 «LLM 이 형식 검증을 훨씬 큰 규모에서 할 수 있게 만들고 있다»이다. 근거로 든 수치를 그대로 옮긴다.

항목	값
대상	OSS-Fuzz 라이브러리 123개 · 퍼징 입구 239개
명세	64MB 미만 모든 입력 · 모형화한 모든 리눅스 응답과 메모리 배치에서 크래시 없음
전제	단일 스레드 정적 바이너리 · 고정 메모리 예산 · RISC-V · 리눅스 · musl libc
증명 규모	Rocq 약 1억 8천만 줄 · 한 편 약 60만 줄 · 바이너리 중앙값 1만 8천 명령
기간	몇 주
믿어야 하는 것	RISC-V · 리눅스 프로세스 형식 모형 · 증명한 정리 문장 · Rocq 검사기

크래시는 잘못된 메모리 접근, 실패한 assert, 모형에 없는 동작 셋을 뜻한다. 퍼징 시험을 Rocq 로 옮겨 적지 않고 컴파일된 바이너리를 그대로 해석했는데, 옮겨 적다가 생기는 오류를 피하려는 선택이었다.

버그가 증명 «과정»에서 나왔다

증명이 막힐 때마다 Claude 가 코드를 고치고 명세를 다시 만든 뒤 다시 증명했다. 수백 개가 나왔다. 원문이 든 예는 넷이다. 20MB 안팎의 드문 배치에서만 나는 압축 해제기의 카운터 언더플로, 64MB 입력과 2GB 넘는 메모리가 있어야 나는 이미지 디코더의 범위 밖 읽기, 한 파일에 대한 두 핸들을 특정 순서로 불러야 나는 읽기, 깊게 중첩된 입력이 필요한 libexpat 의 알려진 취약점 재발견. 퍼저는 보통 1MB 까지만 넣는다.

보상 해킹을 원문이 먼저 짚었다

«고치고 다시 증명»에는 구멍이 있다. 프로그램을 «아무것도 안 하는» 코드로 바꾸면 무엇이든 증명된다. 원문은 패치마다 감점을 주고, 바뀌는 입력이 얼마나 적은지 증명하면 가산점을 줬으며, 패치를 기록해 감사했다고 적었다. 내 게이트 운영에서도 같은 모양을 여러 번 겪었다 — 「통과」가 목표가 되면 통과하기 쉬운 쪽으로 대상이 바뀐다.

효율 두 가지 — 새 모델, 그리고 재사용

• 실제 OSS-Fuzz 코드로 만든 작은 검증 과제 36개에서, Opus 5.5 는 절반을 Opus 5 보다 약 40% 적은 토큰으로 증명했다(과제당 단일 에이전트 3회 · 500만 토큰 예산).
• 에이전트가 서로의 증명을 복사할 수 있는 공유 작업장에서는 혼자일 때보다 토큰이 17% 덜 들었다. 끝난 34편 중 30편이 혼자 평균보다 쌌고, 혼자서는 못 끝낸 두 편이 끝났다.
• 재사용이 통한 이유도 적혀 있다. 증명의 대부분이 C 런타임 초기화와 AddressSanitizer 처럼 모든 프로그램에 있는 부분이었다.

내 환경에 대봤다 — 아트팀 대본의 재사용률

문스튜디오 아트팀은 도트 애니메이션을 Python 대본으로 만든다. 작업마다 _scripts 폴더에 대본을 남기고, 규칙에도 «다음 종이 다시 쓴다»고 적혀 있었다. 실제로 다시 쓰는지 쟀다.

재는 법. 대본 파일마다, 그보다 먼저 만든 «다른 작업 폴더»의 대본들과 줄 단위로 맞대 가장 비슷한 값을 쓴다. 분류는 원문 그림 6 의 칸을 따랐다 — 같음(99% 이상) · 조금 고침(8099%) · 많이 고침(4080%) · 새로 씀(40% 미만).

분류	줄	비율
새로 씀	18,012	84%
많이 고침	1,599	8%
같음	1,024	5%
조금 고침	683	3%

대본 115개 · 2만 1,318줄. «같음»은 전부 같은 세션의 다음 판이었다(이펙트 공용 도구 한 벌이 1→2→4→5판으로 이어짐). 몸 애니메이션과 이펙트 사이, 다른 세션 사이의 재사용은 2~10% 수준으로 사실상 없었다. 새로 쓴 줄을 파일 이름으로 가르면 보기 · 비교 · 점검 · 측정 도구가 7,450줄이었다 — 원문이 말한 «모든 프로그램에 있는 부분»에 해당한다.

적용 — 공유 작업장 목록 한 장

끝난 대본의 머리말 첫 줄과 «쓰는 법» 줄을 손대지 않고 옮겨 목록 한 장을 만드는 대본을 썼다. 손으로 요약하지 않은 이유는, 요약하는 순간 목록이 대본과 어긋나기 시작하기 때문이다. 처음 판은 대본 111개를 쓰임새(비교 · 보기 · 측정 · 납품 · 뼈대 · 본체)로 묶었다.

실험 설계

과제	쓰러짐 애니메이션 · 오른쪽 · 4장 안팎 · 부위 움직이기 · 끝 장 유지
대상	윈디(네 발) · 괴력몬(두 발 · 팔 넷) — 둘 다 원작 쓰러짐이 없다
기준	리자몽 원작 쓰러짐 · 기계 점검 · 숫자 거름 다섯 · 비교 시트
A조	지금 방식 그대로
B조	지시문 맨 앞에 «목록에서 같은 일을 한 대본을 찾아 베껴 고쳐 쓰라» 한 단락
통제	같은 에이전트 정의 · 같은 모델 · 같은 노력 단계 · 같은 시각 · 서로의 폴더는 열지 않게 함

토큰은 각 에이전트 기록의 호출별 사용량을 더했다. 비용은 입력 1 · 캐시 쓰기 1.25 · 캐시 읽기 0.1 · 출력 5 의 상대 가중으로 셌다.

결과

	A 윈디	A 괴력몬	B 윈디	B 괴력몬
새로 쓴 줄	86%	86%	17%	21%
시간	9분 25초	11분 36초	8분 50초	7분 37초
출력 토큰	54,385	62,494	50,544	44,622
캐시 쓰기	123,167	149,208	161,935	147,529
상대 비용	698k	1,168k	1,001k	816k
기계 점검	통과	통과	통과	통과

조 평균으로 B 는 시간 −21% · 출력 −19% · 상대 비용 −3% 였다. 캐시 쓰기는 +13% 였다. 이 증가가 베낀 대본을 읽어 들인 몫이고, 출력에서 아낀 만큼을 거의 상쇄했다. 두 B 가 베껴 온 곳은 같았다 — 같은 동작 · 같은 길 · 같은 기준을 먼저 한 거북왕 쓰러짐 작업 한 벌이었다.

B조가 짚은 목록 결함 둘

• 한 작업의 대본 한 벌이 쓰임새별로 다섯 절에 흩어져 있었다. 둘 다 결국 «작업 한 벌을 통째로» 베꼈으니, 목록의 단위가 틀렸던 것이다. → 작업 단위로 다시 묶었다.
• 베낀 대본의 허용 기본값이 이전 작업 기준(다른 정답지의 4px)에 맞춘 값이었다. 그대로 뒀으면 이번 기준(2px)에서 점검이 떨어질 뻔했다. 대본 안에 그 값의 출처가 없었다. → 목록 머리에 «베낀 기본값은 이번 기준으로 다시 잰다»를 적었다.

판정 — 붙였다, 이유는 시간이다

에이전트 정의와 작업 안내에 «대본을 새로 쓰기 전에 목록에서 작업 한 벌을 찾아 베낀다» 한 줄을 넣고, 목록 생성 대본을 같은 폴더에 두었다. 비용이 같고 시간이 줄었으며 품질이 떨어진 증거가 없어서다.

수확은 하나지만 값을 치르고 배운 것이 하나 더 있다. «덜 쓴다»와 «덜 낸다»는 다른 숫자다. 출력만 봤으면 «19% 절감»이라고 보고했을 것이다. 읽는 쪽을 같이 더하자 그 절감은 잡음 안으로 사라졌다. 원문의 17% 도 토큰 총량이라, 내 조건에서 그대로 재현됐다고 말할 수 없다. 내 과제는 증명보다 훨씬 짧아서 «읽는 비용»의 비중이 크다는 차이도 있다.

남은 일은 셋이다. 고친 목록으로 다시 재기, 표본을 늘리기, 그림 수준을 사람 눈으로 보기.