AI 생성 코드 검증

AI는 코드를 기계 속도로 쏟아내지만, 그게 맞는지 확인하는 일은 아직 사람 속도에 묶여 있습니다. 그 간극을 메우는 다층 검증 구조를 정리합니다.

검증이 새 병목이 된 이유

생성이 빨라지면서 개발의 병목은 작성에서 검증으로 옮겨 갔습니다. 키보드를 두드리는 시간보다, 결과물이 옳은지 따지는 시간이 더 길어졌습니다.

Stack Overflow가 2025년 발표한 개발자 설문에서 응답자의 84% 이상이 AI 도구를 쓴다고 답했습니다. 반면 결과물을 전적으로 신뢰한다는 비율은 29%에 그쳤습니다. 도구는 퍼졌지만 신뢰는 따라오지 못한 셈입니다.

생산성 수치도 한 방향이 아닙니다. METR가 2025년 7월 발표한 무작위 대조 시험(RCT, randomized controlled trial)에서는 정반대 결과가 나왔습니다. 숙련 오픈소스 개발자가 AI를 쓸 때 오히려 19% 느려졌습니다. 작성은 빨라져도 검토·수정이 그 이득을 잠식했다는 해석입니다.

AWS 최고기술책임자(CTO) Werner Vogels는 이 현상을 검증 부채(Verification Debt)라고 불렀습니다. 코드는 기계 속도로 쌓이는데, 옳음을 확인하는 일은 사람 속도에 묶여 누적되는 보이지 않는 빚입니다. 이 빚은 결함이 당장 드러나지 않아 모이다가 한꺼번에 터지고, AI가 갚는 속도보다 더 빨리 쌓입니다.

컴파일되는데 틀린 코드

AI 코드의 까다로운 점은 그럴듯하게 구성된다는 데 있습니다. 컴파일도 되고 기본 단위 테스트도 통과하지만, 그것이 의도대로 동작한다는 보장은 아닙니다. 이를 영어로는 plausible by construction(그럴듯하게 구성됨)과 correct by construction(올바르게 구성됨)의 차이로 구분합니다.

실증 수치는 이 간극을 뒷받침합니다.

수치가 가리키는 결론은 분명합니다. AI 코드의 문제는 처음에 안 잡히면 오래 남고, 한 가지 검사만으로는 걸러지지 않습니다.

여기에 함정이 하나 더 있습니다. 같은 모델에게 코드와 테스트를 함께 시키면, 둘이 같은 맹점을 공유합니다. 코드가 틀린 가정을 깔면 테스트도 같은 가정을 깔아 통과시켜 버립니다. 이를 동어반복 테스트(tautological test) 함정이라고 부릅니다.

검증의 4축

자율화 정도와 무관하게, 모든 검증 활동은 네 개의 축 위에 놓입니다. 각 축이 묻는 질문이 다르므로, 한 축을 통과해도 다른 축은 그대로 비어 있습니다.

위 표에서 자동화가 쉬운 쪽은 구문·동작 축입니다. 의미 축은 의도를 알아야 하므로 부분 자동에 머물고, 정형 축은 스펙이 있어야만 완전 자동이 됩니다. 검증 설계란 결국 이 네 축을 어떤 도구로 어디까지 채울지 정하는 일입니다.

결정론에서 정형 검증까지

실무에서는 위 4축을 생성부터 운영까지 이어지는 여러 레이어로 펼칩니다. 싸고 빠르게 거를 것을 앞에 두고, 비싼 검증은 뒤로 미루는 순서입니다.

L1 결정론 레이어는 무료에 가까운 1차 필터입니다. 컴파일러·타입체커가 컴파일은 되는데 의미가 틀린 코드를 먼저 거릅니다. 정적 분석 보안 테스트(SAST)인 ESLint·Semgrep·CodeQL을 모든 AI 커밋에 차단형으로 거는 것이 2026년의 표준입니다. 여기에 추상 구문 트리(AST) 교차검증을 더하면 환각된 호출까지 걸러집니다. 생성된 코드의 AST를 파싱해, 사용된 API 시그니처를 라이브러리 원본과 대조하는 방식입니다.

L2 실행 레이어는 돌려봐야 아는 것을 담당합니다. 핵심 기법은 다음과 같습니다.

• 프로퍼티 기반 테스트(PBT): '모든 입력에 대해 결과는 0 이상' 같은 불변식을 무작위 입력으로 반복 검증합니다.
• 차분 테스트: 기존 구현과 AI 구현에 같은 입력을 넣어 출력을 비교합니다. 마이그레이션·리팩터링에서 핵심입니다.
• 퍼저(libFuzzer, AFL++)와 샌드박스: AI 코드를 적대적 코드로 가정하고, 네트워크를 끊은 격리 환경에서 돌립니다.

Meta가 2026년 2월 공개한 JiTTests(Just-in-Time Tests)는 변경된 diff 전용 테스트를 즉석에서 생성하는 방식입니다. 기존 hardening 테스트보다 약 4배 많은 회귀를 잡았다고 보고했습니다(Meta 발표 기준).

차분 테스트는 정답을 일일이 적지 않아도 검증이 됩니다. 기존 구현을 오라클로 삼아 출력 일치만 보면 되기 때문입니다. 아래는 표준 라이브러리만으로 구성한 최소 예시이며, 2만 건 입력을 통과합니다.

import random
 
# 검증 대상: AI가 새로 작성한 구현
def new_impl(xs):
    return sum(x for x in xs if x > 0)
 
# 기준(oracle): 기존에 신뢰하는 구현
def old_impl(xs):
    total = 0
    for x in xs:
        if x > 0:
            total += x
    return total
 
def test_differential_and_property():
    rng = random.Random(0)
    for _ in range(20000):
        xs = [rng.randint(-50, 50) for _ in range(rng.randint(0, 20))]
        assert new_impl(xs) == old_impl(xs)   # 차분: 두 구현이 같은가
        assert new_impl(xs) >= 0              # 프로퍼티: 항상 0 이상인가
 
if __name__ == "__main__":
    test_differential_and_property()
    print("OK")

L3 LLM 심사 레이어는 다른 LLM에게 코드를 채점시키는 LLM-as-Judge 방식입니다. 다만 코드를 쓴 모델과 채점 모델이 같으면 동어반복 함정에 빠집니다. 그래서 자동 병합 정책은 다른 벤더 모델의 승인을 조건으로 두는 경우가 많습니다.

L4 정형 검증 레이어는 스펙 충족을 수학적으로 증명합니다. Dafny·Lean·Verus로 작성한 명세를 SMT 솔버가 백그라운드에서 증명하는 방식입니다. 비용이 크므로 항공우주·의료·금융 코어·자율주행 같은 안전 필수(safety-critical) 모듈에만 적용하는 것이 현실적입니다.

사람이 남는 자리

자동 검증을 아무리 쌓아도 사람을 완전히 빼기는 어렵습니다. Macroscope 2025 벤치마크에 따르면, 선도 AI 리뷰 도구도 실제 버그의 약 50%만 잡습니다. 그래서 인간 게이트(L5)는 변경의 영향 범위(blast radius), 즉 사고가 났을 때 번지는 범위에 따라 리뷰 강도를 조절합니다.

자동 병합을 허용하더라도 조건은 까다롭습니다. 모든 CI 검사가 통과하고, 다른 벤더 모델의 심사를 거치며, diff 커버리지와 CodeQL·Snyk를 충족하고, diff 크기가 상한 안에 들어야 합니다. 이 정책은 Mergify·Kodiak·OPA 같은 엔진으로 강제합니다.

게이트를 통과한 코드도 끝이 아닙니다. 배포 가드(L6)는 카나리로 트래픽을 1%에서 점진적으로 올리고, 에러율이 임계치를 넘으면 자동 롤백합니다. 운영 모니터링(L7)은 변경 실패율과 평균 복구 시간(MTTR)을 추적해, AI 유발 이슈의 생존율을 별도 지표로 관리합니다.

정리

AI가 작성한 코드의 검증은 한 가지 기법으로 끝나지 않고, 생성에서 CI·배포·운영까지 이어지는 다층 방어선으로 자리 잡았습니다. 구문·동작·의미·정형의 4축을 결정론·실행·LLM 심사·정형 검증·인간 게이트·배포 가드·모니터링 레이어로 펼칩니다. 싼 검사를 앞에 두고 비싼 검사를 뒤로 미루는 순서가 표준입니다. 같은 모델에게 코드와 테스트를 함께 맡기면 맹점이 공유되므로, 차분 테스트처럼 외부 오라클을 두거나 다른 벤더 모델로 채점하는 장치가 중요합니다. 결국 핵심은 변경의 영향 범위에 맞춰 자동화와 인간 리뷰의 비중을 조절하고, 배포 후에도 AI 유발 이슈의 생존율을 계속 측정하는 데 있습니다.