에이전트 시대의 정확성§

우리가 배포하는 코드는 대부분 에이전트가 쓰게 될 것이다. 손으로 코드를 쓰던 시절은 내가 마음의 준비를 하기도 전에 끝나 가고 있다.

모든 패러다임 전환이 그렇듯, 이번 전환도 부정, 불안, 불확실함, 고뇌, 오만, 그리고 설 자리를 잃은 듯한 감각을 잔뜩 불러일으킨다. 모든 게 혼란스러울 때, 지금 무슨 일이 벌어지고 있는지 이해하려면 설득력 있는 비유나 틀을 찾는 게 도움이 된다.

이 글에서 나는 한때 이색적이거나, 과하거나, "쓸데없이 완벽에 집착하는 사람들이나 쓰는 것"처럼 보였던 기법들이 곧 기본이 될 것이라고 주장하려 한다. 먼저 지금 상황을 어셈블리에서 고수준 언어로 넘어가던 시절과 비교하겠다. 그리고 지금 우리가 구조적으로 똑같은 문제를 겪고 있고, 다른 점은 그 일이 훨씬 짧은 기간에 벌어진다는 것뿐이라고 주장할 것이다.

마지막으로, 나는 정형 기법, 속성 기반 테스트, 기계적으로 검사되는 명세를 지금 도입해야 한다고 말하는 사람들 편에 서려 한다. 셈법이 이 도구들에 유리하게 뒤집혔다. 솔직히 말하면, 에이전트의 결과물을 확실히 통제하려면 우리는 아마 이 수준의 추상화에 집중하기 시작해야 할 것이다.

어셈블리에서 고수준 언어로§

고수준 언어가 등장했을 때, 사람들은 어셈블리를 그만 쓰라는 말을 들었다. 전환에는 시간이 걸렸다. 컴파일러에는 잘못된 코드를 생성하는 버그가 있었다. 손으로 짠 어셈블리는 — 지금도 종종 그렇듯 — 컴파일러가 내놓는 코드보다 빨랐다. 그래도 전환은 수십 년에 걸쳐 일어났고, 개발자들은 어셈블리 실력을 놓지 않은 채 고수준 언어도 받아들이며 균형을 잡았다. 컴파일러가 좋아지면서 결국 거의 모두가 넘어갔다. 고수준 언어는 JIT 컴파일, 가비지 컬렉션, 세대별 힙 같은 자기만의 기법을 발전시키기 시작했다. 이런 기법은 어셈블리로도 기술적으로는 가능했지만, 고수준 추상화에서야 비로소 실용적이 되었다. 패턴은 대략 이랬다:

• 0단계: 모두가 어셈블리를 썼다. 별난 사람 몇몇이 고수준 언어를 쓰고, 여러 런타임을 가지고 놀았다. Prolog나 기호 처리 시스템처럼 비주류로 여겨지던 것들이었다.
• 1단계: 사람들이 고수준 언어를 쓰기 시작했고, 다른 사람들은 이를 진지하게 받아들이지 않았다. 고참들은 신참들이 코딩할 줄 모르게 될까 봐 걱정했다. 그들은 컴파일러 출력이 올바른지 가끔 직접 확인해야 하고, 모두가 어셈블리 실력을 유지해야 한다고 주장했다.
• 2단계: 프로그래밍 언어 연구자들은 컴파일러가 생성하는 코드가 올바르다는 것, 적어도 대부분은 그럭저럭 올바르다는 것을 증명하는 데 많은 노력을 쏟았다.
• 3단계: 사람들은 주로 고수준 언어를 썼다. 컴파일러와 인터프리터는 대체로 올바르게 동작했다. 고수준 언어로 쓰는 게 이상한 선택이라고 믿는 사람은 더 이상 없었다. 어셈블리를 몰라도 얼마든지 유능한 엔지니어가 될 수 있게 되었다.

이 과정은 대략 50년이 걸렸다. 병목은 세 가지였다. 프로그래밍 언어 연구자가 부족했고, 그 연구에 투자하려는 상업적 의욕이 부족했고, 이런 것을 증명하는 일 자체가 실제로 어렵고 느렸다. 미래에 대한 엉뚱한 아이디어를 밀어붙이는 정신 나간 몽상가들¹이 세대마다 있었고, 그때마다 동시대 실무자들은 고개를 갸웃거리며 그들을 살짝 무시하고 의심했다. 그리고 결국 대부분은 몽상가들이 옳았다(생존자 편향인 건 나도 안다). 고수준 언어, 거의 영어에 가까운 표현, 그리고 '이제 아무도 어셈블리를 읽지 않는다'는 상태가 표준이 되었다.

나는 지금 우리가 그때와 같은 지점에 있다고 본다. 50년에 걸친 흐름이 몇 달로 압축되었다.

자연어§

우리는 한 단계 더 위로 올라왔다. 이제 EHL(초고수준) 언어, 곧 자연어로 쓴다. LLM 에이전트가 EHL을 HL(고수준 언어: Go, Rust, Python, TypeScript)로 번역해 주기를 기대한다. 그리고 우리는 그 결과물을 그다지 믿지 않는다.

개발자로서 우리는 지난번 큰 도약 때와 똑같이 행동하고 있다:

• 사람들에게 LLM 에이전트의 결과물을 검증하라고 요구한다
• 기본적으로 결과물을 믿지 않는다
• (HL 언어로) 코딩을 배울 기회를 얻지 못할 젊은 세대를 걱정한다
• "LLM에게 코드를 쓰게 하자"는 생각이 비주류에서 점점 받아들여지는 쪽으로 옮겨 가고 있다
• 앞서 나간 EHL 순수파는 남들이 보기엔 영문 모를 기이한 짓을 한다²

좋은 소식도 있다. 어셈블리에서 HL로 넘어가면서 남은 머릿속 여력으로 JIT, GC, 세대별 힙 같은 새로운 개념을 발전시킬 수 있었다. 마찬가지로 HL에서 EHL로 넘어가면 정확성 수준을 끌어올릴 여력이 생기고, 덤으로 일손도 더 생긴다. 문제는 이것이다. EHL이 올바른 HL로 컴파일된다는 걸 어떻게 믿을 수 있을까? 에이전틱 코딩에서 오는 정확성 걱정을 어떻게 해결할까?

소프트웨어 공학 방법론§

지난 20~30년 동안, TDD와 그 주변의 방법론들은 저마다 다른 어조로 테스트는 소프트웨어 개발의 일급 산출물이라고 주장해 왔다.³ 어떤 분야에서는 이게 지나쳤지만("테스트 없이는 코드를 한 줄도 쓰지 마라!"), 나는 흐름이 다시 테스트 쪽으로 돌아오고 있다고 생각한다. 이게 갑자기 다시 중요해진 이유는 간단하다. 제대로 된 테스트 하네스로 꽉 묶어 두지 않으면, 에이전트는 그럴듯한 헛소리를 늘어놓고는 아무 일 없다는 듯 휘파람을 불며 가 버린다. 1년 전만 해도 나는 스스로에게 "테스트 없이 코드부터 쓰지 마라"를 요구하지 않았지만, 지금은 내 에이전트들에게 그 기준을 철저히 요구한다.

하지만 TDD가 테스트의 전부였던 적은 없다. 1940년대부터 우리는 프로그램의 속성을 증명할 수 있다는 것을 알고 있었다. Tony Hoare는 1969년에 "An Axiomatic Basis for Computer Programming"을 발표했다. 수십 년 동안 사람들은 그게 "실제 소프트웨어에는 비현실적"이라고 했다. 학계의 헛된 꿈이라는 것이었다.

전형적인 단위 테스트는 프로그램 상태 속에서 경로 하나를 따라간다.⁴ 골든 테스트, 테이블 테스트, 단위 테스트, 통합 테스트 - 모두 같은 아이디어의 변형이다. 이런 테스트는 이미 아는 것을 다시 확인해 줄 뿐이다. 모르는 것에 대해서는 아무것도 증명하지 못한다.

속성 기반 테스트⁵ (PBT)는 상태 공간에서 무작위 경로 탐색을 한다 - 그럴듯한 범위의 입력값을 생성하고, 프로그램이 특정 속성을 절대 위반하지 않는지 검증한다. PBT는 Go(rapid), Rust(proptest), TypeScript(fast-check)에서 거의 똑같은 모양으로 쓸 수 있다.⁶ 각각 수백, 수천 개의 무작위 입력 벡터를 뽑고, 실패하면 최소한의 반례로 축소한다. 단위 테스트보다 엄밀하게 더 강력하다.

Go에서는 이렇게 생겼다:

func TestSortIsIdempotent(t *testing.T) {
    rapid.Check(t, func(t *rapid.T) {
        v := rapid.SliceOf(rapid.Int()).Draw(t, "v")
        once := append([]int(nil), v...)
        sort.Ints(once)
        twice := append([]int(nil), once...)
        sort.Ints(twice)
        require.Equal(t, once, twice)
    })
}

불변식: 정렬은 멱등적이다.

f(f(x)) = f(x)

이미 정렬된 슬라이스를 다시 정렬해도 바뀌지 않는다: sort(x) = sort(sort(x)). 이 테스트는 다양한 입력으로 수천 번 실행되며 불변식이 항상 참인지 확인한다. 실패하면, 불변식 위반을 재현하는 가장 작은 입력으로 줄여 준다.

PBT 역시 비주류에서 시작한 나름의 역사가 있다⁷. John Hughes와 Koen Claessen은 ICFP 2000에서 "QuickCheck: A Lightweight Tool for Random Testing of Haskell Programs"를 발표했다. 몇 년 동안 이건 "Haskell 하는 사람들은 이상해" 취급을 받다가, 결국 모든 주류 언어로 퍼졌다.

진짜 정확성 증명을 하려면 정형 기법이 필요하다. 정형 기법은 예전부터 비용이 너무 커서 가장 중요한 시스템에만 쓰였다. 하지만 명세된 부분에 대해서는, "프로그램이 아마 맞을 거야, 아마도"보다 훨씬 강한 보장을 얻는다. TLA+ 명세⁸는 상태 머신, 불변식, 정리로 이루어지고, 모델 검사기는 이를 도달 가능한 모든 상태에 걸쳐 검증한다 - 경로 하나가 아니라 모든 경로다. 그게 테스트와 증명의 차이다.

PBT처럼 TLA+도 나름의 기묘한 길을 걸었다. Leslie Lamport가 1990년대 초에 이것을 개발했다. 20년 동안은 학계의 틈새 연구 정도로 여겨졌다 - 그러다 Newcombe et al., 2015가 나왔다. AWS가 TLA+로 DynamoDB, S3, EBS의 버그를 배포하기 전에 찾아낸 과정을 기록한 논문이다. 발표된 뒤 산업계에서 빛을 보기까지 20년이 걸렸다.⁹

처음 등장했을 때 낭비이거나, 비주류이거나, 터무니없어 보이던 기법도 주변의 추상화 수준과 셈법이 바뀌고 나면 합리적인 선택이 되는 경우가 많다. PDP-1에서 GC는 낭비였다. 64 GB RAM 서버에서는 고민할 거리도 아니다. 기법은 바뀌지 않았다. 바뀐 건 그걸 쓰지 않는 비용이었다.

시간의 압축이 새로운 변수다. Hoare의 1969년 논문에서 AWS의 TLA+ 도입까지의 흐름은 대략 45년이 걸렸다. 다음 흐름은 45년이 걸려서는 안 된다 - 20년도, 아니 5년도 안 된다. 에이전트가 지금 이 순간 HL 코드 속에서 날뛰고 있다. 스펙은 다음 안전지대¹⁰이고, 우리는 그곳을 향해 스피드런을 해야 한다. 에이전트를 잘 부리는 프롬프트 엔지니어링의 핵심이 Markdown으로 탄탄한 제품 스펙을 쓰는 것이라는 데에는 대체로 다들 동의한다. 그리고 새로운 최전선은 이걸 넘어서고 있다.

그렇다, 탄탄한 제품 스펙이 출발점이다. 하지만 산업 현장의 프로그래밍에는 이것과 "나만 믿어" 식의 바이브만으로는 부족하다. 우리는 HL 실무자들이 했던 일을 해야 한다. 결과물이 우리가 신경 쓰는 범위에서 올바르다는 것을 보장해야 한다. 그것도 사람이 감독을 놓지 않으면서, 다 리뷰할 수도 없는 코드 더미에 파묻히지 않는 방식으로 해야 한다. 우리는 이 코드를 전부 리뷰할 수 없을 것이다. 그렇다고 이 코드를 만들지 않을 여유도 없을 것이다. 바로 여기서 긴장이 생긴다. 그러니 우리는 한 단계 위로 물러나야 한다. 제품 스펙에만 집중할 게 아니라, 거기에 정형 증명, 불변식 기반 PBT, 기계적으로 검증할 수 있는 모델 같은 온갖 것을 함께 갖춰 나가기 시작해야 한다. 우리는 HL 코드를 쓰고 리뷰하는 일에서 물러나, 이런 보험 증서를 쓰는 쪽으로 가야 한다. 그게 곧 초고수준(EHL) 코드를 쓰는 일이다.

셈법이 뒤집혔다§

방금 세 가지 일이 한꺼번에 일어났다.

1. 생산성이 한 단계 올라갔다. 에이전트 덕분에 코드 작성 속도가 열 배 단위로 빨라졌다. 좋은 에이전트 루프로 일주일만 일해 봤다면 이걸 직접 느꼈을 것이다.

2. 품질 위험도 함께 올라갔다. 에이전트는 환각을 일으키고, 엇나가고, 그럴듯하지만 미묘하게 틀린 코드를 쓴다. 보완책이 없으면, 에이전트가 키보드를 더 많이 차지할수록 코드 품질은 떨어진다.

3. 2번을 보완하는 방법들이 막 싸졌다.

정형 기법에서 연산¹¹이 비쌌던 적은 없었다. 비싼 건 사람의 주의력이었다. 내 분야와 가까운 영역(Kubernetes 오퍼레이터 작성)을 다룬 Anvil 논문에 따르면, 사람이 증명을 직접 쓰고 완결될 때까지 다듬어 나가자, 증명 분량이 코드의 약 4.5배가 되었다. 엄청난 양의 증명이다. "모든 것에 TLA+를 쓰자"는 생각이 원리상으로는 30년 동안 통했는데도 산업계에서 채택되지 못한 이유가 이것이다.

하지만 이제 그 비용은 다른 일꾼이 치른다. 검증은 결정론적이고 기계가 검사하며, 결과는 초록 아니면 빨강으로 분명하게 갈린다. 증명이 완결되지 않으면, 검증기는 어떤 명제가 어떤 상태에서 실패하는지 정확히 알려 준다. 이게 바로 에이전트가 가장 잘하는 작업 방식이다: 촘촘한 피드백 루프, 분명한 신호, 수렴할 때까지의 반복.

그리고 에이전트는 지루해하지 않는다.

예전에는 사람의 인내심에 막혀 있던 기법들이 이제는 연산량에만 묶여 있고, 연산은 싸다. 문제에 하드웨어를 들이부으면 끝이다.

그러니 셈법이 뒤집힌다. 생산성 향상분의 일부를 치러서 정확성에 과하게 투자하고도, 우리는 순이익을 본다. 범위는 더 넓어지고, 품질은 예전보다 더 높아진다. 정확성은 지금 기본이 되어야 한다. 우리가 순수주의자여서가 아니다. 그렇게 하면 계산이 우리에게 유리하게 돌아가고, 안 하면 불리하게 돌아가기 때문이다.

에이전트가 쓴 코드를 믿으려면§

우리에게 필요한 기법들은 이미 존재한다 - 비용 모델이 바뀌기만을 기다리고 있었을 뿐이고, 그 변화가 막 일어났다.¹² 그래서 나는 지금 이렇게 주장한다:

• 사소하지 않은 프로그램의 핵심 로직(상태 머신, 반드시 성립해야 하는 불변식, "거의 맞는" 건 틀린 것과 다름없는 부분)에는 정형 기법을 쓰거나 적어도 시도해라. LLM의 도움을 받는 소프트웨어 수준의 증명에는 Dafny, Verus, 또는 Lean을 써라(Creusot과 Kani는 보완적인 Rust 선택지다). 분산 시스템 설계에는 P나 TLA+를 써라.
• 나머지 대부분에는 - 의미 있는 입력 공간이 있는 곳이라면 어디든 - 기본으로 속성 기반 테스트를 써라. 에이전트가 쓸모없고 오해를 부르는 테스트를 쓰지 않도록, 우리는 아마 변이 테스트 도구에 투자해야 할 것이다.
• 회귀 테스트와 사용자 페르소나별 정상 경로 커버리지에는 - 기존 테스트를 유지하되, 솔직해져라: 그건 정확성을 검사하는 테스트가 아니다. "이 테스트에 적힌 대로 동작한다"는 걸 기록해 두는 테스트다.
• 스펙 주도 개발에는 - 전체를 떠받치는 부분에 대해 정형 명세도 작성해라. 한계 비용은 작고, 보상은 크다.

이게 선택 사항으로 남아 있을 시간은 얼마 남지 않았다. 방법은 있다. 비용은 막 떨어졌다. 에이전트가 가져온 생산성 향상은 그 투자 비용을 치러 주는 동시에, 그 투자를 요구한다.

우리의 안전지대 - 당분간은§

HL 왕국을 에이전트들이 점령해 가고 있다. 우리는 그들의 텃밭에서 싸우지 않는다 - 위로, 코드 위의 계층으로 물러난다: 자연어, 제품 스펙, 정형 명세, 불변식, 도메인 모델, 페르소나. 예전에 허술했던 것들(비공식 제품 스펙, 사용자 스토리)과 예전에 비쌌던 것들(정형 기법, 고급 테스트 패턴)이 이제 둘 다 같은 이유로 핵심이 되었다. 이것들이 있어야 우리가 무슨 일이 벌어지는지 스스로 파악할 수 있고, 저 아래 HL 세계에서 일하는 에이전트에게 규칙을 지키게 할 힘을 잃지 않는다.

중요한 기술은 그 계층을 다루게 해 주는 기술이다: 실제로 제약이 될 만큼 사용자 스토리를 잘 쓰는 것, 도메인 모델을 도출하는 것, 불변식을 찾아내는 것, 어디를 테스트하고 어디를 검증하고 어디를 증명할지 정하는 것, 에이전트가 요리조리 빠져나가지 못할 만큼 스펙을 촘촘하게 설계하는 것. 사용자 스토리를 쓰고, 도메인 모델을 도출하고, 불변식을 찾고, 이 모든 걸 엮어 테스트할 가치가 있는 추상화 계층으로 만드는 일 말이다. 이 중 어느 것도 할 줄 모른다면, 점심시간은 끝났고 누군가 이미 당신 밥그릇을 챙겨 갔다.