AI 생성 코드 검증

AI 생성 코드는 컴파일과 테스트의 통과 범위를 구분하고, 변경의 영향에 맞춰 검토해야 합니다.

검증이 새 병목이 된 이유

코드 생성 시간이 줄어도 전체 개발 시간이 같은 비율로 줄지는 않습니다. 생성 결과를 이해하고 요구사항과 대조하는 작업이 남기 때문입니다.

Stack Overflow의 2025년 개발자 설문에서 응답자의 84%는 AI 도구를 사용 중이거나 사용할 계획이라고 답했습니다. 정확성 문항에서 신뢰한다는 응답은 33%였으며, 전체 응답 중 '매우 신뢰'는 3%였습니다. 사용 의향과 결과 신뢰도 사이에 큰 차이가 있습니다.

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

AWS 최고기술책임자(CTO) Werner Vogels는 확인하지 않은 코드가 누적되는 문제를 검증 부채(Verification Debt)라고 설명했습니다. 검토를 미루면 이후 변경에서 기존 코드의 가정까지 다시 확인해야 하므로, 생성량과 검증 처리량을 함께 관리할 필요가 있습니다.

컴파일되는데 틀린 코드

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

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

AI 코드의 문제는 처음에 안 잡히면 오래 남고, 한 가지 검사만으로는 걸러지지 않습니다.

여기에 함정이 하나 더 있습니다. 같은 모델에게 코드와 테스트를 함께 시키면, 둘이 같은 맹점을 공유할 수 있습니다. 코드가 잘못된 가정에 기반하면 테스트도 같은 가정을 사용해 오류를 놓칩니다. 이를 동어반복 테스트(tautological test) 함정이라고 부릅니다.

검증의 4축

이 글은 검증 활동을 구문·동작·의미·정형의 네 축으로 나눕니다. 각 축의 질문은 일부 겹치지만, 한 종류의 검사만 통과했다고 전체 요구사항이 검증되지는 않습니다.

위 표에서 자동화가 쉬운 쪽은 구문·동작 축입니다. 다만 통과 결과는 도구가 검사한 범위만 보장합니다. 정형 검증도 명세만 주면 끝나는 과정이 아니며, 루프 불변식과 보조정리를 사람이 보충해야 할 수 있습니다. 검증 설계는 네 축을 어떤 도구로 어디까지 채울지 정하는 일입니다.

결정론에서 정형 검증까지

다음은 위 4축을 생성부터 운영까지 연결하는 구성 예시입니다. 싸고 빠르게 거를 것을 앞에 두고, 비싼 검증은 뒤로 미루는 순서입니다.

flowchart LR
    G["AI 코드 생성<br/>자연어 의도 → 변경 diff"] --> L1["L1 결정론<br/>컴파일·타입·정적분석"]
    L1 --> L2["L2 실행 테스트<br/>단위·프로퍼티·차분·퍼저"]
    L2 --> L3["L3 LLM 심사<br/>다른 벤더 모델이 채점"]
    L3 --> L4["L4 정형 검증<br/>안전 필수만 수학적 증명"]
    L4 --> L5["L5 인간 게이트<br/>영향 범위별 리뷰"]
    L5 --> L6["L6 배포 가드<br/>카나리·자동 롤백"]
    L6 --> L7["L7 운영 모니터링<br/>지표·인시던트 대응"]

L1 결정론 레이어는 비용이 낮은 1차 필터입니다. 컴파일러와 타입체커는 구문·타입 오류를 잡지만, 컴파일되는 의미 오류까지 판정하지는 못합니다. ESLint·Semgrep·CodeQL 같은 정적 분석을 AI 변경의 차단형 검사로 두는 방식을 권장할 수 있습니다. 추상 구문 트리(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와 Verus는 SMT 기반 자동화를 제공하고, Lean은 사용자가 증명 항목과 전술을 구성하는 대화형 정리 증명기입니다. 자동화가 막히면 루프 불변식이나 보조정리를 추가해야 하므로, 실패 비용이 큰 모듈부터 적용 범위를 정하는 편이 현실적입니다.

사람이 남는 자리

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

아래 표는 리뷰 정책을 설계하는 예시입니다. 인원과 변경 크기 기준은 조직의 위험 허용 범위로 조정해야 합니다.

자동 병합은 필수 CI 검사와 검토 조건을 충족한 변경에 한해 적용합니다. 모델 심사나 정적 분석은 조직이 선택한 정책에 포함할 수 있으며, 서로 다른 모델도 같은 오류를 놓칠 수 있습니다. 정책 엔진과 저장소의 병합 규칙으로 선택한 조건을 적용합니다.

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

정리

AI 생성 코드의 검증은 구문·동작·의미·정형 검사의 범위를 구분하는 데서 시작합니다. 빠른 자동 검사로 걸러낸 뒤 영향이 큰 변경에 실행 테스트와 리뷰를 집중할 수 있습니다.

코드와 테스트가 같은 잘못된 가정을 공유하지 않도록 독립적인 기준을 마련해야 합니다. 배포 이후의 오류도 추적해 검증 과정에서 놓친 조건을 다음 검사에 반영합니다.