AI가 만든 코드를 리뷰할 때 “테스트는 통과했습니다”라는 말과 “검증됐습니다”라는 말은 같은 뜻이 아닙니다. 전자는 시도한 입력에서 문제가 없었다는 뜻이고, 후자는 어떤 명세에 대해 모든 입력에서 성립한다는 주장입니다. 그런데 그 명세가 틀렸다면 증명은 아무리 정확해도 원하는 동작을 보장하지 못합니다.
Lean의 창시자 Leonardo de Moura는 The Data Exchange 인터뷰에서 이 간극을 여러 각도로 설명합니다. 인터뷰 페이지는 10월 29일과 10월 21일을 함께 표기하고 있어, 발행일 하나로 단정하지 않고 “10월 하순 공개된 대담”으로 읽었습니다. 이 글은 인터뷰 전문과 Lean 프로젝트의 공개 자료를 바탕으로, AI 코드 검증 주장을 실무에서 어떻게 확인할지 정리한 해설입니다. Lean을 설치해 예제를 컴파일하지는 않았습니다.
테스트와 증명은 경쟁 관계가 아니다
de Moura의 구분은 단순합니다. 테스트는 버그의 존재를 보여주지만 부재를 보여주지는 못합니다. 반대로 형식 증명은 명세를 만족한다는 것을 모든 입력에 대해 보일 수 있습니다. 다만 증명은 명세가 실제 요구를 담고 있을 때만 의미가 있습니다.
그는 테스트가 먼저라는 점도 인정합니다. 테스트를 작성하면 시스템을 이해하게 되고, 증명하기 전에 틀린 가정을 발견할 수 있습니다. 이미 거짓인 명세는 토큰을 아무리 써도 증명할 수 없습니다.
인터뷰에서 나온 zlib 사례가 이 차이를 잘 보여줍니다. 압축한 데이터를 다시 풀면 원본이 나온다는 성질을 Lean 정리로 표현하고, 범용 AI가 그 증명을 작성했다는 것입니다. 여기서 핵심은 “압축 라이브러리를 테스트했다”가 아니라 “압축·해제 왕복이 특정 전제 아래 항상 원본을 복원한다”는 명세를 세웠다는 점입니다.
AI가 코드를 이해하는 것처럼 보일 때 생기는 세 가지 빈칸
인터뷰에는 AI가 다른 언어로 작성된 코드를 Lean 모델로 옮기고, 그 모델로 버그를 찾는 사례가 나옵니다. Claude Code 개발자가 AI에게 Lean으로 코드를 모델링해 버그를 찾아보라고 했고, 실제 수정으로 이어졌다는 일화도 언급됩니다. 이는 “버그 찾기”에는 유용하지만 “버그 없음”을 보장하는 단계와는 다릅니다.
| 빈칸 | 질문 | 실패 방식 |
|---|---|---|
| 요구사항 간극 | 우리가 원하는 것을 명세에 정확히 적었는가 | 명세는 만족하지만 사용자는 원하지 않는 동작 |
| 모델 충실성 | Lean 모델이 실제 코드와 같은 동작을 하는가 | 모델에서 증명했지만 구현은 다른 언어·다른 경로 |
| 커널·신뢰 기반 | 어떤 검사기와 전제를 신뢰하는가 | 증명 검사기 버그, 라이브러리 가정, 잘못된 공리 |
de Moura는 Navier-Stokes 사례에서 비슷한 문제를 언급합니다. 자연어로 쓴 비형식 증명과 Lean 증명 사이에 미세한 불일치가 있었고, 미분 차수 같은 가정이 달라졌다는 것입니다. 수학적으로는 큰 차이를 만들 수 있지만, 겉으로 보기에는 같은 정리처럼 보입니다.
에이전트 시대에는 이 빈칸이 더 중요해집니다. 코드 생성이 쉬워질수록 “무엇을 만족해야 하는가”와 “그 만족을 누가 어떤 도구로 확인했는가”가 남습니다.
약한 명세는 증명해도 의미가 없다
Lean 4 스타일로 두 명세를 비교해 보겠습니다. 아래 코드는 개념 설명용이며, Lean 컴파일러로 실행해 검증한 예제가 아닙니다. 두 번째 정리의 sorry는 증명 대신 넣은 자리표시자이며, 그 자체로는 검증된 증명이 아닙니다.
def clamp (x lo hi : Int) : Int := max lo (min hi x)
-- 약한 명세: 어떤 정수 하나를 반환한다는 사실만 말한다.
theorem clamp_returns_a_value (x lo hi : Int) :
∃ y, clamp x lo hi = y := ⟨_, rfl⟩
-- 의미 있는 명세: lo ≤ hi일 때 결과가 두 경계 사이에 있다.
theorem clamp_bounded (x lo hi : Int) (h : lo ≤ hi) :
lo ≤ clamp x lo hi ∧ clamp x lo hi ≤ hi := by
sorry
첫 번째 정리는 참이지만 거의 아무것도 보장하지 않습니다. 함수가 정수를 반환한다는 것은 타입이 이미 말해 줍니다. 이런 명세를 증명한 뒤 “형식 검증됐다”고 말하면, de Moura가 지적한 “명세가 사실상 없는 것과 같은” 상황이 됩니다.
두 번째 명세는 경계 조건을 실제로 제한합니다. 물론 lo ≤ hi라는 전제가 빠지면 명세가 거짓이 될 수 있으므로, 전제도 요구사항의 일부입니다. 좋은 명세는 “무엇을 보장하지 않는지”까지 드러냅니다.
“검증됐다”는 주장을 확인하는 질문
de Moura는 검증을 주장하는 공급자에게 명세를 보여 달라고 하라고 말합니다. 어떤 속성을 검증했는지, 어떤 검사기를 썼는지, 신뢰 기반이 무엇인지도 물어야 합니다. 이를 실무 체크리스트로 바꾸면 다음과 같습니다.
| 질문 | 좋은 답의 형태 | 피해야 할 답 |
|---|---|---|
| 어떤 속성을 증명했는가 | 정리·불변식·전제·예외 조건이 공개됨 | “코드는 검증됐습니다”만 있음 |
| 명세가 요구사항과 어떻게 연결되는가 | 요구사항 추적표, 리뷰 기록 | 테스트 이름만 나열 |
| 구현과 모델이 같다는 근거는 무엇인가 | 추출·번역 도구, 차등 테스트, 수동 리뷰 | “AI가 모델을 만들었으니 같다” |
| 어떤 커널과 신뢰 기반을 쓰는가 | 독립 커널, 작은 trusted base, 버전 | 검사기 세부를 공개하지 않음 |
| 실패·예외 경로도 명세에 포함됐는가 | 오류 반환, 자원 고갈, 동시성 조건 | 정상 경로만 증명 |
| 유지보수 비용은 얼마인가 | 명세 변경 절차, 재검증 시간 | 한 번 증명하면 끝이라는 설명 |
Lean 생태계는 이 질문에 답할 도구를 제공합니다. 증명을 여러 커널로 다시 검사하는 기능이나 Rust 코드를 Lean으로 옮겨 검증하는 Aeneas 같은 도구가 그 예입니다. 그러나 도구가 있다고 해서 명세의 의미까지 자동으로 맞는 것은 아닙니다. 모델과 구현의 동기화는 별도의 작업입니다.
AI 코드에 바로 적용할 수 있는 순서
모든 프로젝트에 형식 증명을 도입할 필요는 없습니다. de Moura도 모든 소프트웨어가 같은 수준의 검증을 필요로 하지는 않는다고 말합니다. 비용과 실패 영향이 큰 부분부터 시작하는 편이 현실적입니다.
- 핵심 불변식 하나를 고릅니다. 예: “재시도해도 결제가 두 번 되지 않는다”, “권한 없는 사용자는 데이터를 읽을 수 없다”.
- 실행 가능한 속성 테스트로 먼저 표현합니다. 입력 생성기와 실패 시 최소 재현 사례를 남깁니다.
- 모델과 구현의 차이를 확인합니다. 같은 입력을 양쪽에 넣는 차등 테스트나 추출 과정을 마련합니다.
- 명세가 안정되고 실패 비용이 큰 경우에만 증명으로 확장합니다. 프로토타입 UI나 빠르게 바뀌는 제품 요구사항은 테스트와 리뷰가 더 경제적일 수 있습니다.
- 검증 주장을 문서화합니다. 어떤 명세를, 어떤 도구로, 어떤 전제 아래 확인했는지 저장소에 남깁니다.
AI는 이 과정을 단축할 수 있습니다. 코드를 읽고 Lean 모델 초안을 만들거나, 반례를 찾거나, 명세를 더 명확히 쓰도록 도울 수 있습니다. 하지만 “이 모델이 내 코드와 같다”는 판단과 “이 명세가 우리가 원하는 것이다”라는 판단은 여전히 사람의 몫입니다.
인터뷰의 결론은 코드 작성 능력의 종말이 아니라 책임의 이동에 가깝습니다. AI가 코드를 대신 써도, 무엇을 보장할지 정하고 그 보장을 검사 가능한 형태로 남기는 일은 사라지지 않습니다. 오히려 코드가 싸질수록 명세를 소유하는 능력이 차이를 만듭니다.
이 글은 특정 제품의 성능이나 Lean의 도입 효과를 측정한 결과가 아닙니다. 인터뷰에서 제시된 개념과 공개 도구를 바탕으로 한 실무 해석이며, Lean 예제는 컴파일하지 않았습니다.