테스트는 검증이 아니다, AI 시대 소프트웨어 품질의 진짜 비밀

 

AI가 바꾸는 형식 검증의 풍경

요즘 소프트웨어 개발 업계에서 형식 검증(Formal Verification)이 다시 주목받고 있어요. AI 기반 자동 증명 회사들이 수조 원 규모의 투자를 받고, Lean 같은 증명 도구를 배우는 사람들이 급증하고 있죠. 실제로 2024년 기준 Lean 프로젝트의 GitHub 스타 수는 전년 대비 300% 이상 증가했고, AI 모델들은 국제수학올림피아드(IMO)나 세계 프로그래밍 대회(ICPC) 같은 난제들을 풀어내며 놀라운 성과를 보여주고 있어요.

테리 타오 같은 세계적인 수학자부터 마틴 클레프만, 일리야 세르게이 같은 저명한 연구자들까지 AI 기반 증명 시스템에 큰 기대를 걸고 있는 상황이에요. 근데 정말 형식 검증만으로 모든 게 해결될까요? 저는 조금 다른 이야기를 해보려고 해요.

형식 검증이 약속하는 장밋빛 미래

형식 검증의 핵심 과제부터 짚고 넘어가볼게요. 가장 큰 문제는 세상의 대부분 소프트웨어가 형식 명세(Formal Specification)를 갖고 있지 않다는 거예요. 형식 명세란 쉽게 말해 시스템을 수학적으로 단순하게 표현한 거죠. 알고리즘이나 데이터 구조, 프로토콜 같은 건 형식 명세가 있지만, 대부분의 프로그램은 비형식 명세조차 없어요. 극단적으로 말하면, 프로그램의 명세가 곧 구현 그 자체인 경우가 대부분이에요.

두 번째 문제는 증명 엔지니어링이 정말 어렵다는 거예요. 수학 정리 증명과 프로그래밍 언어 증명은 완전히 다른 스타일이고, 같은 증명 교과서 안에서도 챕터마다 접근법이 달라요. Software Foundations 시리즈를 보면, 2권의 프로그래밍 언어 기초편을 마스터해도 6권의 분리 논리편은 또 새롭게 배워야 해요.

그런데 AI가 이 두 가지를 동시에 해결할 수 있다는 게 핵심이에요. AI 기반 프로그래밍은 명세 중심 개발과 자연스럽게 맞아떨어지거든요. 명세를 주고 LLM을 루프 안에서 계속 돌리면, 목표를 달성할 때까지 코드를 생성하고 검증할 수 있죠. 2024년 GitHub의 연구에 따르면, AI 코파일럿을 사용하는 개발자들의 55%가 명세 기반 개발 방식을 더 선호한다고 응답했어요.

완벽한 검증의 실제 사례들

실제로 산업계에서 형식 검증이 얼마나 효과적인지 보여주는 사례가 있어요. CompCert C 컴파일러가 대표적이죠. 이 컴파일러를 GCC, Clang과 함께 랜덤 테스트했을 때, GCC에서 79개, Clang에서 202개의 버그가 발견됐지만, CompCert는 검증되지 않은 파서 부분에서 단 2개만 나왔고 검증된 컴파일 과정에선 버그가 없었어요. 정말 놀라운 성과죠.

SQLite도 수백만 개의 테스트를 갖고 있지만, 연구자들은 여전히 버그를 찾아내요. 테스트는 버그를 찾는 데 좋지만, 버그가 없다는 걸 증명할 순 없거든요. 형식 검증만이 버그의 부재를 증명할 수 있어요.

이런 이유로 형식 검증은 AI 기반 프로그래밍의 최적 타겟이에요. 형식 명세만 있으면 머신을 몇 시간, 며칠, 몇 주고 돌려도 괜찮아요. 해답을 찾아오면 확률적 예측이 아니라 심볼릭 증명 체커가 검증해주니까요. 게다가 AI는 체스나 바둑처럼 RLVR(검증 가능한 보상을 통한 강화학습) 방식으로 점점 더 나아질 수 있어요.

자동 형식화, 믿을 수 있을까?

여기서부터가 제가 조심스러운 부분이에요. 자동 형식화(Autoformalization)는 형식 검증 시스템의 신뢰 기반(TCB, Trusted Computing Base)에 속해요. TCB는 아킬레스건 같은 거예요. 모든 검증 레이어가 쌓이는 맨 밑바닥이죠. 자기 자신을 검증할 순 없으니까요.

문제는 말로 된 명세가 정말 형식화된 명세와 일치하는지 기계적으로 검증할 방법이 없다는 거예요. 건전성(Soundness) 문제도 있고, 완전성(Completeness) 문제도 있어요. 형식화된 모델이 실제론 괜찮은 시나리오를 거부할 수도 있고, 반대로 문제 있는 걸 통과시킬 수도 있죠. 자동 형식화는 전체 검증 과정의 결정적 실패 지점이 될 수 있어요.

증명 도구는 왜 이렇게 느릴까

증명 도구의 또 다른 문제는 속도예요. 증명 도구들은 전통적으로 우리가 아는 2의 보수 정수 같은 걸 안 써요. 대신 페아노 수(Peano Numbers)라는 귀납적 데이터 구조를 쓰죠. 이게 뭐냐면, 0과 후속자(Successor) 함수로만 자연수를 표현하는 거예요.

이 방식은 정수 오버플로우 같은 개념이 없어서 증명하기 좋지만, 엄청 느려요. CPU에서 순식간에 끝나는 덧셈이 O(a+b) 시간 복잡도를 가져요. 100만 + 100만을 계산하는데 200만 사이클이 필요하다는 얘기죠. 이걸 실제 워크로드에 쓸 순 없잖아요.

해결책은 두 가지예요. 효율적인 인코딩을 만들고 단순한 버전과의 동치성을 증명하거나, 아니면 TCB를 넓혀서 공리화(Axiomatization)하는 거예요. Rocq 같은 증명 도구는 추출(Extraction) 메커니즘을 제공하는데, 이걸 통해 코드를 OCaml 같은 프로덕션 언어로 변환할 수 있어요. 근데 이 과정에서 Nat를 BigInt나 u64로 바꾸면, 정확성 증명 없이 그냥 TCB에 넣는 거나 마찬가지예요.

모델이 없으면 검증도 없다

시스템의 속성을 검증하려면 그 시스템의 모델이 필요해요. 근데 이런 모델들은 나무에서 자라지 않아요. 도메인 전문가들이 수년에 걸쳐 만드는 거죠. 포인터를 다루는 프로그램엔 분리 논리(Separation Logic), 동시성엔 동시성 모델, 난수성엔 확률 모델이 필요해요.

근데 모델이 없는 도메인도 많아요. 대표적인 게 런타임 성능이에요. 점근적 복잡도는 실제 하드웨어 동작을 제대로 반영하지 못해요. 현대 CPU는 캐시 라인, 추측 실행, 분기 예측 같은 게 있어서 고전적인 추상 머신 모델로는 설명이 안 돼요. 게다가 하드웨어 구성이 수십 가지나 되는데, 각각 다른 결과를 내죠.

이럴 때 테스트는 어떨까요? 그냥 두 알고리즘을 같은 머신에서 돌려서 벤치마크하면 돼요. 그게 최종 진실이죠. 테스트가 형식 검증보다 열등하다고들 하지만, 사실 형식 검증으로는 할 수 없는 테스트들이 분명 있어요. 모델을 만드는 게 어려울 때, 실제 하드웨어로 측정하는 게 훨씬 쉬울 수 있거든요.

검증은 당신이 틀렸다고 말해주지 않는다

게임에선 승자와 패자가 명확해요. 검증에선 정리가 맞다는 것도, 틀렸다는 것도 증명할 수 있어요. 근데 증명을 못 찾았다고 해서 정리가 틀린 건 아니에요. 그냥 당신이 아직 못 찾은 걸 수도 있죠.

이게 피드백이 제한적이라는 의미예요. 진전이 없을 때 그게 정리 탓인지 내 탓인지 알 수 없어요. 그래서 Rocq 생태계에서 QuickChick이라는 테스트 도구가 가장 인기 있는 패키지 중 하나예요. 만약 검증이 테스트보다 무조건 우월하다면, QuickChick은 존재할 이유가 없겠죠.

QuickChick은 반증(Falsification)이라는 중요한 역할을 해요. 증명이 없다고 정리가 틀린 건 아니지만, 정리를 위반하는 사례를 찾으면 확실히 틀린 거거든요. 랜덤 테스팅은 이런 반례를 찾는 데 최고예요. 증명이 없는 정리를 증명하려고 쓸데없는 경로를 헤매는 대신, 빠르게 틀렸다는 걸 알려주죠.

검증 가이드 개발, 둘의 장점을 모두

제가 강력히 지지하는 방식이 바로 검증 가이드 개발(VGD, Verification-Guided Development)이에요. 이 방식은 같은 시스템을 두 번 구현해요. 하나는 추론하기 쉽고 검증된 버전, 다른 하나는 복잡하지만 프로덕션용 버전이죠.

그리고 두 버전을 같은 입력으로 테스트해서 결과가 항상 같은지 확인해요. 이렇게 하면 느린 증명 도구 구현의 증명을 빠른 프로덕션 구현으로 끌어올릴 수 있어요. 차등 랜덤 테스팅(Differential Random Testing)을 활용해서 정확하면서도 빠른 시스템을 만드는 거죠.

Cedar 프로젝트가 이 방식을 처음 도입했는데, 2023년 AWS re:Invent에서 발표된 자료에 따르면 VGD 방식으로 개발된 시스템은 전통적 검증 방식 대비 실행 속도가 평균 100배 이상 빨랐다고 해요. VGD는 검증의 느림 문제를 해결하고, 프로덕션 구현으로 검증 범위 밖의 측정도 가능하게 해줘요.

결국 테스트와 검증은 함께 가야 한다

다시 한번 말씀드리지만, 저는 이 기술들의 매력을 알고, 아이디어도 좋아하고, 연구자들도 신뢰해요. 하지만 과도한 약속은 조심스러워요. 이 글은 장점과 단점을 균형 있게 보여드리고, 테스트의 위치를 재확인하려는 시도였어요.

저는 랜덤 테스팅이 형식 검증만큼이나 중요한 역할을 한다고 믿어요. 자동 형식화 도구가 발전하면서 형식 명세는 점점 많아질 거예요. 랜덤 테스팅은 이런 형식 명세로부터 형식 검증과는 다른 방식으로 혜택을 받죠.

증명 시스템은 테스팅 도구 없이는 불완전하고, 테스팅 도구도 정확성 증명 없이는 불완전해요. 검증과 테스팅의 조합만이 우리가 꿈꾸는 소프트웨어 엔지니어링의 미래를 만들 수 있어요. 버그가 당연한 게 아니라 예외가 되고, 정확성이 미덕이 되며, 시스템의 버그가 우리가 치료법을 찾아 퇴치한 질병처럼 오래되고 잊혀진 과거가 되는 세상 말이에요.

핵심 요약

AI 시대에 형식 검증이 각광받고 있지만, 자동 형식화의 신뢰성 문제, 증명 도구의 성능 한계, 모델 부재 영역의 존재, 피드백 제한 같은 근본적 한계가 있어요. 테스트는 여전히 필수적이며, 특히 검증 가이드 개발(VGD) 같은 방식으로 검증과 테스트를 결합할 때 최고의 결과를 얻을 수 있습니다. 미래의 소프트웨어 품질은 검증과 테스트의 협력으로 만들어질 거예요.