에이전틱 세상에서의 정확성
에이전트가 우리가 배포하는 코드 대부분을 쓰게 될 것이다. 손으로 코드를 쓰는 시대는 끝나가고 있다. 우리 대부분이 마음의 준비를 끝내기도 전에.
나는 우리가 역사적으로 이단적으로 취급해 온 기법들 — 정형 기법, 속성 기반 테스트, 기계적으로 검사되는 스펙 — 이 이제 테이블 스테이크가 되어야 한다고 주장한다. 경제 논리가 그쪽으로 뒤집혔기 때문이다.
어셈블리에서 고급 언어로
고급 언어가 등장했을 때 사람들은 어셈블리를 그만 쓰라는 말을 들었다. 전환에는 시간이 걸렸다. 컴파일러에는 잘못된 코드를 생성하는 버그가 있었다. 손으로 짠 어셈블리는 — 그리고 종종 지금도 — 컴파일러가 내놓는 것보다 빨랐다. 그래도 전환은 일어났다. 수십 년에 걸쳐, 어셈블리 기술을 유지한 채 고급 언어를 받아들인 장인들이 조심스럽게 줄타기를 해 가며. 컴파일러가 좋아지면서 결국 거의 모두가 갈아탔다. 고급 언어는 자기만의 기법들 — JIT 컴파일, 가비지 컬렉션, 세대별 힙 — 을 개발하기 시작했는데, 기술적으로는 어셈블리에서도 가능했지만 더 높은 추상화 계층에서만 실용적이 되었다. 패턴은 대략 이러했다:
- Phase 0: 모두가 어셈블리를 쓴다. 별난 사람들 몇몇이 고급 언어를 쓰고, 여러 런타임 — Prolog, 심볼릭 시스템들, 비주류로 여겨지는 것들 — 을 가지고 논다.
- Phase 1: 사람들이 고급 언어를 쓰기 시작하고, 다른 이들은 그것을 진지하지 못한 것으로 본다. 고참들은 신참들이 코딩할 줄 모르게 될까 걱정한다. 그들은 우리가 정확성을 위해 컴파일러 출력을 표본 검사해야 하며, 모두가 어셈블리 기술을 유지해야 한다고 주장한다.
- Phase 2: 프로그래밍 언어 연구의 많은 노력이 컴파일러가 생성하는 코드가 맞다는 것을, 또는 적어도 대부분의 경우에는 적당히 맞다는 것을 증명하는 데 들어간다.
- Phase 3: 사람들은 대부분 고급 언어를 쓴다. 컴파일러와 인터프리터는 대체로 맞다. 고급 언어로 쓰는 것이 이상한 선택이라고 더 이상 아무도 믿지 않는다. 어셈블리를 모르고도 유능한 엔지니어가 되는 데 아무 문제가 없다.
이건 대략 50년이 걸렸고, 프로그래밍 언어 연구자의 공급, 그 일에 투자할 상업적 의지, 그리고 이런 것들을 증명하는 일이 진짜로 어렵고 느리다는 사실이 병목이었다. 각 세대는 이전 세대의 이단자들을 흡수했다1.
나는 우리가 지금 비슷한 지점에 와 있다고 주장한다, 압축된 채로. 50년의 궤적이 몇 달로 압축된 채.
자연어
우리는 한 단계 더 올라섰다. 우리는 이제 EHL(even-higher-level) 언어로 쓴다: 자연어. 우리는 LLM 에이전트가 EHL을 HL(Go, Rust, Python, TypeScript)로 번역해 주기를 기대한다. 그리고 우리는 그 출력을 진정으로 신뢰하지는 않는다.
장인으로서, 우리는 지난번 10배 도약 때와 같은 방식으로 행동한다:
- 우리는 사람들에게 LLM 에이전트의 출력을 검증할 것을 요구한다
- 우리는 기본적으로 출력을 신뢰하지 않는다
- 우리는 (HL 언어로) 코딩하는 법을 배울 기회를 갖지 못할 어린 세대를 걱정한다
- "LLM에게 코드를 쓰게 하자"라는 개념이 비주류에서 어느 정도 받아들여지는 쪽으로 옮겨가고 있다
- 최전선의 EHL 원리주의자들이 별짓을 다 하고, 나머지는 그게 뭔지 모른다2
좋은 소식은, 어셈블리에서 HL로 간 것이 우리에게 새 개념(JIT, GC, 세대별 힙)을 만들 머릿속 여유를 내준 것처럼, HL에서 EHL로 가는 것도 우리에게 여유 사이클 — 그리고 부수적으로, 더 많은 인력 — 을 주어 정확성의 기준선을 올린다. 문제는 이것이다: EHL이 유효한 HL로 컴파일된다는 것을 우리는 어떻게 신뢰하는가? 에이전틱 코딩에서 오는 정확성 우려를 어떻게 해결하는가?
소프트웨어 엔지니어링 기법
지난 20~30년 동안, TDD와 그 주변의 규율은 — 서로 다른 어조로 — 테스트가 소프트웨어 생성의 일급 산출물이라고 주장해 왔다.3 광신도들이 도를 넘었고 시계추가 되돌아왔다. 새삼 다시 옳은 말이 된다. 에이전트를 진짜 테스트 하네스로 단단히 붙들어두지 않으면, 그들은 그럴듯한 헛소리를 써놓고 휘파람 불며 떠나기 때문이다.
하지만 TDD가 테스트의 종착점이었던 적은 없다. 1940년대부터 우리는 프로그램의 속성이 증명될 수 있다는 것을 알고 있었다. Tony Hoare는 1969년에 "An Axiomatic Basis for Computer Programming"을 출판했다. "실제 소프트웨어에는 비현실적", 사람들은 수십 년 동안 그렇게 말했다.
전형적인 단위 테스트는 프로그램 상태를 통과하는 하나의 경로를 걷는다.4 골든 테스트, 테이블 테스트, 단위 테스트, 통합 테스트 — 같은 발상의 변종들. 알려진 것이 알려져 있음을 증명할 뿐, 모르는 것에 대해서는 아무것도 증명하지 못한다.
속성 기반 테스트5(PBT)는 상태 공간을 무작위 보행으로 누빈다 — 그럴듯한 범위의 입력값을 생성하고 프로그램이 특정 속성을 절대 위반하지 않음을 검증한다. Go(rapid), Rust(proptest), TypeScript(fast-check)에서 본질적으로 동일하게 표현 가능하다.6 각각이 수백 또는 수천 개의 무작위 벡터를 뽑고, 실패를 최소 반례로 줄인다. 단위 테스트보다 엄밀하게 더 강하다.
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)
})
}불변식: 정렬은 멱등이다.
이미 정렬된 슬라이스를 정렬해도 바뀌지 않는다: . 이 테스트는 다양한 입력으로 수천 번 실행되며 불변식이 항상 참임을 보장한다. 실패하면, 불변식 위반을 재현하는 최소 범위로 입력 도메인을 줄인다.
PBT에는 그 나름의 이단의 역사가 있다7. John Hughes와 Koen Claessen은 ICFP 2000에서 "QuickCheck: A Lightweight Tool for Random Testing of Haskell Programs"를 출판했다. 수년 동안 "Haskell 쓰는 사람들은 좀 이상하다"는 식으로 취급되다가, 모든 주류 언어로 퍼져나갔다.
정확성에 대한 진짜 증명을 원한다면, 정형 기법이 필요하다. 역사적으로 가장 중요한 시스템에만 한정되어 왔다. 부담스러운 비용 때문이다. 하지만 스펙으로 명시된 것에 대해서는, "프로그램이 아마도 맞겠지, 정도."보다 훨씬 더 강한 보장을 얻는다. TLA+ 스펙8은 상태 기계이고, 불변식이며, 모델 검사기가 모든 도달 가능한 상태에 대해 검증하는 정리다 — 하나의 경로가 아니라, 모든 경로. 그게 테스트와 증명의 차이다.
TLA+에는 그 나름의 이단자들의 역사가 있다. Leslie Lamport가 1990년대 초에 개발했다. 20년 동안 틈새 학계 연습이었다 — Newcombe et al., 2015가 AWS가 DynamoDB, S3, EBS를 배포하기 전에 버그를 찾기 위해 TLA+를 어떻게 사용했는지 문서화하기까지는. 출판에서 산업적 돌파까지 20년의 간극. 패턴은 계속 반복된다.9
패턴은 "이단자들은 언제나 옳다고 인정받는다"가 아니다. 더 좁고 더 유용한 것이다: 처음에는 낭비적이거나, 틈새이거나, 부조리해 보이는 기법들이, 주변의 추상화 수준과 경제가 움직이고 나면 종종 합리적이 된다. PDP-1에서는 GC가 낭비였다; 64GB RAM의 서버에서는 질문조차 되지 않는다. 기법이 바뀐 게 아니다. 그것을 쓰지 않는 비용이 바뀐 것이다.
압축된 시간이 새로운 변수다. Hoare의 1969년 논문에서 AWS-on-TLA+까지의 궤적은 대략 45년이 걸렸다. 다음 궤적은 45년 — 또는 20년, 또는 5년조차 — 걸려서는 안 된다. 에이전트는 지금 이 순간 HL 코드 안에서 마구 날뛰고 있다. 스펙이 다음 피난처이고10, 우리는 그곳을 향해 스피드런해야 한다.
셈법이 막 뒤집혔다
세 가지가 동시에 일어났다.
1. 생산성이 한 단계 올라섰다. 에이전트는 코드가 작성되는 속도에서 10배 도약이다. 좋은 에이전트 루프와 일주일을 일해 봤다면, 이걸 직접 느꼈을 것이다.
2. 품질 리스크도 함께 올라갔다. 에이전트는 환각을 일으키고, 점점 벗어나며, 그럴듯하지만 미묘하게 틀린 코드를 쓴다. 보정 없이는, 에이전트가 코딩의 더 많은 부분을 가져갈수록 코드 품질은 퇴보한다.
3. #2를 보정하는 기법들이 막 싸졌다.
정형 기법은 컴퓨팅에서 비쌌던 적이 없다11. 그것들은 인간의 주의력에서 비쌌다. Anvil 논문은 약 4.5배의 증명 대 코드 비율을 보고한다 — 인간이 증명을 쓰고 마무리될 때까지 반복할 때. 그래서 "모든 것에 TLA+를 쓰라"가 원칙적으로는 30년 동안 옳았음에도 산업적으로 채택되지 못한 것이다.
그 부담은 이제 다른 일꾼이 진다. 검증기는 결정론적이고, 기계로 검사되며, 모호함 없이 통과 아니면 실패다. 증명이 닫히지 않으면, 어떤 추측이 어떤 상태에서 실패하는지 검증기가 정확히 짚어 준다. 이것이 에이전트가 가장 잘하는 워크플로다: 짧은 피드백 루프, 명확한 신호, 수렴할 때까지 반복한다.
그리고 에이전트는 지루해하지 않는다.
이전에는 인간의 인내심에 막혀 있던 기법들이 이제는 컴퓨팅에 막혀 있고, 컴퓨팅은 싸다.
그래서 셈법이 뒤집힌다. 생산성으로 얻은 이익의 일부를 정확성에 과하게 재투자해도, 결과적으로는 순이익이 남는다 — 더 큰 도달 범위, 이전보다 더 높은 품질. 정확성은 이제 테이블 스테이크가 되어야 한다, 우리가 원리주의자여서가 아니라, 우리가 그것을 할 때 계산이 맞아떨어지고, 안 하면 어긋나기 때문이다.
에이전틱 코드를 신뢰하기
우리가 필요한 기법들은 이미 존재한다 — 그저 비용 모델의 변화를 기다리고 있었을 뿐이고, 그 변화가 막 일어났다.12 그래서 나는 주장한다, 지금:
- 사소하지 않은 프로그램의 핵심 로직 — 상태 기계, 반드시 성립해야 하는 불변식, "거의 맞는 것"이 맞는 것이 아닌 대목 — 에는 정형 기법을 사용하라. LLM 지원 소프트웨어 수준 증명에는: Dafny, Verus, 또는 Lean (Creusot과 Kani는 상호 보완적인 Rust 선택지다). 분산 시스템 설계에는: P 또는 TLA+.
- 나머지 대부분 — 의미 있는 입력 공간이 있는 모든 곳 — 에는 속성 기반 테스트를 기본으로 사용하라.
- 회귀 및 해피 패스 페르소나 커버리지에는 — 전통적인 테스트를 유지하되, 솔직해져라: 그것들은 정확성에 대한 테스트가 아니다. 표현에 대한 테스트다.
- 스펙 주도 개발에는 — 하중을 지탱하는 부분에 대해 TLA+ 스펙도 함께 작성하라. 한계비용은 작고, 보상은 크다.
이건 더 이상 선택사항이 아니다. 기법은 존재한다. 비용은 막 떨어졌다. 에이전트가 가져다 주는 생산성 이익이 그 투자 비용을 감당해 주는 동시에, 그것을 요구하기도 한다.
우리의 피난처 — 지금으로서는
HL 왕국은 에이전트에 의해 식민지화되고 있다. 우리는 그들의 마당에서 그것과 싸우지 않는다 — 우리는 한 단계 위로 후퇴한다, 코드 위의 계층으로: 자연어, 제품 스펙, 정형 스펙, 불변식, 도메인 모델, 페르소나. 한때 빈약했던 것들(비공식 제품 스펙, 사용자 스토리)과 한때 비쌌던 것들(정형 기법, 고급 테스팅 패턴)이 이제 둘 다 하중을 지탱하고 있다, 같은 이유로 — 그것들은 우리가 스스로에게 명료한 상태를 유지하고 에이전트가 HL 영역에서 하고 있는 일에 대해 규율을 강제할 수 있는 지렛대를 유지하는 방법이다.
중요한 기술은 그 층위를 다루는 것을 가능하게 하는 기술들이다: 실제로 제약이 될 만큼 사용자 스토리를 잘 쓰는 것, 도메인 모델을 도출하는 것, 불변식을 식별하는 것, 어디서 테스트할지 검증할지 증명할지 결정하는 것, 에이전트가 교묘하게 빠져나갈 수 없도록 스펙을 충분히 엄격하게 설계하는 것. 이런 것들 중 어떤 것도 할 줄 모른다면 — 사용자 스토리를 쓰고, 도메인 모델을 도출하고, 불변식을 찾고, 그 한 묶음으로 모아 테스트할 만한 추상화 계층으로 쌓아 올리는 것 — 점심시간은 끝났고, 누가 당신 샌드위치까지 먹어치웠다.
- 1Grace Hopper는 FLOW-MATIC(1955-59)을 설계했고, "컴퓨터는 영어를 이해할 수 없다"는 통념에 맞서 영어 형태의 문장을 읽는 컴파일러를 출시했다. John Backus는 IBM의 FORTRAN(1957)을 이끌었다; 어셈블리 사제 계급은 컴파일된 코드가 손으로 쓴 성능을 따라잡을 수 없다고 말했지만, 704가 그렇지 않음을 보여주었다. John McCarthy는 LISP(1958)를 설계했고 가비지 컬렉션을 프로덕션에서 처음으로 출시했다; GC는 수십 년 동안 "진짜" 작업에는 비실용적이라고 일축되었다. Dijkstra, "Go To Considered Harmful"(1968) — 구조적 프로그래밍은 테이블 스테이크가 되기 전에 비주류였다. Robin Milner는 타입 추론과 함께 ML(1973)을 설계했고, "타입이 잘 잡힌 프로그램은 잘못될 수 없다" — 그때는 학계의 진귀품이었지만, 지금은 오늘날 모든 타입 언어의 설계상 조상이다. 그 궤적 — FORTRAN('57)에서 C('72), C++('85), Java('95), Go('09), Rust('10) — 은 연구자 공급, 상업적 의지, 그리고 이런 것들을 증명하는 일이 어렵다는 사실이 병목이었다.
- 2Steve Yegge(Gas Town, Gas City), Geoffrey Huntley(ralph loops), Simon Willison의 실황 중계.
- 3Kent Beck, TDD: By Example(2002); Fowler, Refactoring(1999); McConnell, Code Complete(2판 2004); Dan North, "Introducing BDD"(2006); Gojko Adzic, Specification by Example(2011).
- 4
- 5일족: 변성 테스팅 — 관련된 입력의 출력 사이의 관계(ML, 과학 코드); 차분 테스팅 — 두 구현, 같은 입력, 비교(컴파일러, 리팩터, 포트); 상태 기반 / 모델 기반 PBT — 모델에 대한 연산 시퀀스(
rapid.StateMachine,proptest-state-machine,quickcheck-state-machine); 콘콜릭 실행(KLEE, SAGE); 변이 테스팅 — 테스트의 *강도(strength)*를 측정한다. 퍼징은 적대적 입력 생성 변종이다. 그중 어느 것도 가장 사소한 경우를 제외하고는 프로그램이 맞다는 것을 증명할 수 없다 — 조합 폭발이 금방 일어난다. - 6에이전틱 코딩이 자리잡는 곳. TypeScript: 구조적 타입은 인간-에이전트 경계에서 컴파일 타임 검증을 정확성을 가장 싸게 사는 방법으로 만든다. Rust: Verus와 타입 시스템이 proof-carrying code를 실현 가능하게 만든다; 인간을 늦췄던 작성 편의 부담을 에이전트는 쉽게 지불한다. Go: 빠른 컴파일/vet/테스트 루프는 에이전트를 부릴 때 중요하다;
vet/staticcheck/레이스 디텍터/퍼징이 성숙해 있다. - 7John Hughes와 Koen Claessen, "QuickCheck"(ICFP 2000). 수년 동안 "Haskell 쓰는 사람들은 좀 이상하다"는 식으로 취급되다가, 모든 주류 언어로 퍼져나갔다:
rapid(Go),proptest(Rust),fast-check(JS/TS),hypothesis(Python). - 8작은 TLA+ 스펙:
---- MODULE Counter ---- VARIABLES count Init == count = 0 Next == count' = count + 1 Spec == Init /\ [][Next]_count NonNegative == count >= 0 THEOREM Spec => []NonNegative ==== - 9Xavier Leroy / CompCert, 2000년대 중반 — 정형 검증된 C 컴파일러, 오늘날 항공우주와 암호 분야에서 사용된다. L4.verified / seL4(2009) — 최초의 정형 검증된 OS 마이크로커널. RustBelt(POPL 2018) — Rust의 타입 시스템이 건전함이 증명되었다. Verus와 Anvil(OSDI '24, Best Paper) — Rust로 작성된 정형 검증된 쿠버네티스 컨트롤러, 현재 "학계의 호기심" 단계다.
- 10이 피난처도 영원히 가지는 않는다. HL을 먹어치운 같은 압축이 스펙 계층에 다가올 것이다 — 에이전트가 목표로부터 스펙을 도출하고, 서로에 대해 검증한다. 그때쯤이면 우리는 오늘날의 소프트웨어 산업보다는 Iain M. Banks의 컬처에 더 가까워져 있고, 질문은 "AI가 묵묵히 일하는 동안, 인간은 어떻게 가장 잘 살 것인가"이다.
- 11실행당 비용은 사소하지 않을 수 있다 — TLC 실행, Verus 증명 검사, 퍼징 캠페인은 CPU를 잡아먹는다. 그래도 경제는 성립한다: 소프트웨어는 compile/verify once, ship many times이다 — 한계 배포 비용은 0에 가깝다, Andreessen의 "Why Software Is Eating the World"에 따르면. 검증에는 하드웨어를 들이부어라, 희소 자원(인간의 주의력)에 맞춰 최적화하라.
- 12다음 10배 도약은 2030년 안에 오는 게 아니다; 23년 안에 온다. 월계관에 너무 오래 기대지 마라. 그 곡선 위에서 살아가는 법을 익혀라.