에이전트 세계의 정확성§

에이전트가 우리가 배포하는 코드의 대부분을 쓰게 될 것이다. 손으로 코드를 짜는 시절은 내가 준비된 것보다 더 빨리 끝나가고 있다.

모든 패러다임 전환이 그렇듯, 이건 많은 부정, 불안, 불확실성, 자기성찰, 오만, 그리고 전반적인 괴리감을 낳는다. 혼돈이 지배할 때, 나는 지금 일어나는 일을 이해할 만한 신뢰할 수 있는 유사 사례와 프레임워크를 찾는 게 도움이 된다.

이 글에서, 나는 한때 이국적이고, 과잉이며, "쓸데없는 디테일에 너무 오래 매달리는 부류가 쓰는 것"으로 여겨졌던 기법들이 곧 기본기가 될 것이라고 주장한다. 어셈블리에서 고수준 언어로의 전환과 평행선을 그어 보고, 우리가 지금 구조적으로 같은 문제에, 단지 압축된 일정으로 직면해 있다고 주장하겠다.

마지막으로, 정형 기법, 속성 기반 테스팅, 기계적으로 검증된 명세가 지금 우리가 손에 잡아야 할 도구가 되어야 한다고 말하는 진영에 합류하겠다. 경제학이 그쪽으로 뒤집혔고, 솔직히 말해서: 에이전트의 결과물에 대한 통제력을 확실하게 유지하기 위해 우리가 집중하기 시작해야 할 추상화 수준은 아마 그 정도일 것이다.

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

고수준 언어가 등장했을 때, 사람들에게 어셈블리 작성을 멈추라는 말이 떨어졌다. 전환에는 시간이 걸렸다. 컴파일러에는 잘못된 코드를 생성하는 버그가 있었다. 손으로 짠 어셈블리는 컴파일러가 내놓는 것보다 빨랐고 — 종종 지금도 그렇다. 그래도 전환은 일어났다, 수십 년에 걸쳐, 장인들이 어셈블리 기술을 유지하면서 고수준 언어를 채택하는 식으로 줄타기하며. 컴파일러가 좋아지면서, 결국 거의 모든 사람이 바꿨다. 고수준 언어는 자체적인 묘수들을 개발하기 시작했다 — JIT 컴파일, 가비지 컬렉션, 세대별 힙 — 기술적으로는 어셈블리에서도 가능했지만 더 높은 추상화 수준에서만 실용적이 된 것들이다. 패턴은 대략 이랬다:

• Phase 0: 모두가 어셈블리를 쓴다. 몇몇 괴짜들이 고수준 언어를 쓰며, 다양한 런타임을 가지고 논다 - Prolog, 심볼릭 시스템, 변두리로 여겨지는 것들.
• Phase 1: 사람들이 고수준 언어를 쓰기 시작하고, 다른 이들은 진지하지 않게 본다. 고참들은 신참들이 코딩할 줄 모르게 될까 걱정한다. 그들은 컴파일러 출력의 정확성을 점검해야 하고, 우리 모두가 어셈블리 기술을 유지해야 한다고 주장한다.
• Phase 2: 컴파일러가 생성한 코드가 정확함을, 또는 적어도 대부분의 경우에 합리적으로 정확함을 증명하는 데 많은 프로그래밍 언어 연구 노력이 들어간다.
• Phase 3: 사람들은 대부분 고수준 언어를 쓴다. 컴파일러와 인터프리터는 대체로 정확하다. 고수준 언어로 쓰는 것이 이상한 선택이라고 더 이상 아무도 믿지 않는다. 어셈블리를 모르고도 엔지니어로 능숙한 것은 완전히 괜찮다.

이건 대략 오십 년이 걸렸고, 프로그래밍 언어 연구자의 공급, 그 작업에 투자할 상업적 식욕, 그리고 이런 것들을 증명하는 일이 실제로 어렵고 느리다는 사실에 의해 속도가 제한되었다. 미래에 대한 거친 생각을 밀어붙이는 정신 나간 몽상가¹의 세대마다, 동시대 실무자들은 다소 무시하는 듯한, 회의적인 태도로 머리를 긁적였다. 그리고 대부분의 경우, 몽상가들은 (생존자 편향이지, 안다) 결국 옳다고 증명되었다. 고수준 언어, 거의-영어에 가까운 표현, 그리고 아무도-어셈블리를-읽지-않는-것이 표준이 되었다.

나는 우리가 지금 같은 평행 지점에 있다고 주장한다. 오십 년의 궤적이, 몇 달로 압축되어 있다.

자연어§

우리는 한 단계 더 위로 올라갔다. 우리는 이제 EHL(even-higher-level, 더 높은 수준의) 언어로 쓴다: 자연어. 우리는 LLM 에이전트가 EHL을 HL(Go, Rust, Python, TypeScript)로 번역해 주기를 기대한다. 그리고 우리는 그 출력을 정말로 신뢰하지 않는다.

장인으로서, 우리는 지난번 한 자릿수 도약 때와 똑같이 행동한다:

• 우리는 LLM 에이전트의 출력을 사람들이 검증하도록 요구한다
• 우리는 출력을 기본적으로 신뢰하지 않는다
• 우리는 (HL 언어로) 코딩을 배울 기회를 갖지 못할 젊은이들을 걱정한다
• "LLM이 코드를 쓰게 하자"는 개념이 변두리에서 합리적으로 받아들여지는 쪽으로 이행하고 있다
• 프런티어 EHL 순수주의자들은 다른 모두가 어리둥절해하는 이상한 짓을 한다²

좋은 소식은, 어셈블리에서 HL로 가는 것이 새로운 개념(JIT, GC, 세대별 힙)을 개발할 여분의 정신적 사이클을 우리에게 준 것과 똑같이, HL에서 EHL로 가는 것이 우리에게 여분의 사이클을 — 그리고 부수적으로, 더 많은 인력을 — 정확성의 기준을 올리는 데 준다는 것이다. 질문은 이거다: EHL이 유효한 HL로 컴파일되는 것을 어떻게 신뢰할 것인가? 에이전트형 코딩의 정확성에 대한 우려를 어떻게 풀 것인가?

소프트웨어 엔지니어링 방법론§

지난 이삼십 년 동안, TDD와 그 주변 규율은 - 서로 다른 어조로 - 테스트는 소프트웨어 생성의 1급 산출물이라고 주장했다.³ 어떤 영역에서는 이게 너무 멀리 갔지만("테스트 없이는 코드 한 줄도 쓰지 마라!") 시계추가 다시 반대로 돌아오고 있다고 생각한다. 다시 갑자기 적절해졌는데, 만약 에이전트를 제대로 된 테스트 하니스로 옭아매지 않으면, 그들은 그럴듯한 헛소리를 써놓고 휘파람 불며 떠나기 때문이다. 1년 전, 나는 "테스트 먼저 없이는 코드를 쓰지 마라"를 스스로에게 요구하지 않았지만, 오늘 나는 내 에이전트들에게는 절대적으로 그 기준을 요구한다.

하지만 TDD가 테스팅의 종착점이었던 적은 없다. 1940년대 이래로, 우리는 프로그램의 속성이 증명될 수 있음을 알고 있었다. Tony Hoare는 1969년에 "An Axiomatic Basis for Computer Programming"를 출판했다. 수십 년 동안, 사람들은 그게 "실제 소프트웨어에는 비실용적"이라고 말했다. 학계의 헛된 꿈이라고.

전형적인 단위 테스트는 프로그램 상태를 통한 하나의 경로를 걷는다.⁴ 골든 테스트, 테이블 테스트, 단위 테스트, 통합 테스트 - 같은 아이디어의 변주들. 그들은 알려진 것이 알려져 있음을 증명한다. 그들은 미지의 것에 대해서는 결코 아무것도 증명하지 못한다.

속성 기반 테스팅⁵(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)
    })
}

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

이미 정렬된 슬라이스를 정렬해도 바뀌지 않는다: . 이 테스트는 다양한 입력으로 수천 번 실행되며 불변식이 항상 참임을 보장한다. 실패할 때, 입력 도메인을 불변식 위반을 재현하는 최소 범위로 줄인다.

PBT는 변두리에서 시작한 자기 나름의 역사가 있다⁷. John Hughes와 Koen Claessen은 ICFP 2000에서 "QuickCheck: A Lightweight Tool for Random Testing of Haskell Programs"를 출판했다. 수년간 하스켈 쓰는 사람들은 좀 이상하다는 식으로 다뤄지다가, 모든 주류 언어로 퍼졌다.

정확성에 대한 진짜 증명을 위해서는, 정형 기법이 필요하다. 비싼 비용 때문에 역사적으로 가장 중요한 시스템에만 한정되었다. 하지만 명세된 것에 대해서는, "프로그램이 아마 정확할 것 같다"보다 훨씬 강한 보장을 갖는다. TLA+ 명세⁸는 상태 머신, 불변식, 그리고 모델 검사기가 도달 가능한 모든 상태에 걸쳐 검증하는 정리다 - 한 번의 보행이 아니라, 모든 보행. 그게 테스트와 증명의 차이다.

PBT처럼, TLA+도 자기만의 이상한 길을 걸었다. Leslie Lamport는 1990년대 초에 이를 개발했다. 이십 년 동안 틈새 학술 활동이었다 - Newcombe et al., 2015가 AWS가 DynamoDB, S3, EBS의 버그를 배포 전에 찾기 위해 TLA+를 어떻게 사용했는지 문서화하기 전까지는. 출판에서 산업적 돌파구까지 이십 년의 간극이었다.⁹

영점에서 낭비적이고, 틈새이고, 부조리해 보이는 기법들은 주변 추상화 수준과 경제학이 움직이고 나면 종종 합리적이 된다. GC는 PDP-1에서는 낭비였다; 64 GB RAM이 있는 서버에서는 질문거리도 아니다. 기법은 바뀌지 않았다. 그것을 쓰지 않는 비용이 바뀌었다.

시간 압축이 새 변수다. Hoare의 1969년 논문에서 AWS-on-TLA+까지의 궤적은 대략 사십오 년이 걸렸다. 다음 궤적은 사십오 년이 - 또는 이십 년, 심지어 오 년도 - 걸려선 안 된다. 에이전트는 지금 HL 코드에서 날뛰고 있다. 명세가 다음 피난처이고¹⁰, 우리는 그쪽으로 스피드런해야 한다. 사람들은 마크다운으로 견고한 제품 명세를 쓰는 것이 에이전트 성공으로 가는 프롬프트 엔지니어링이라는 데 대체로 동의했다. 그리고 새로운 변두리는 그것을 넘어서고 있다.

그렇다, 견고한 제품 명세는 시작이다. 하지만 산업적 프로그래밍은 그것과 "그냥 믿어봐" 식의 분위기보다 더 많은 것을 요구한다. 우리는 HL 실무자들이 했던 작업, 즉 우리가 관심 갖는 범위에 대해 출력이 정확함을 보장하는 작업을, 검토할 수 없는 코드의 바다에 빠지지 않으면서 사람의 감독을 유지하는 방식으로 해야 한다. 우리는 이 모든 코드를 검토할 수 없을 것이다. 우리는 이 모든 코드를 생산하지 않을 여유가 없을 것이다. 이게 긴장이다. 그러니 우리는 위로 후퇴해서 _제품 명세_만이 아니라 그것을 정형 증명, 불변식 기반 PBT, 기계적으로 검증 가능한 모델, 그 모든 다채로움과 결합하는 데 집중하기 시작해야 한다. 우리는 HL 코드를 작성하고 검토하는 일에서 물러나 이런 보험 계약을 작성하는 쪽으로 가야 한다: 더 높은 수준의(EHL) 코드를 작성하는 쪽으로.

경제학이 막 뒤집혔다§

세 가지가 동시에 막 일어났다.

1. 생산성이 한 단계 올라갔다. 에이전트는 코드가 쓰이는 속도에서 한 자릿수의 변화다. 좋은 에이전트 루프로 일주일을 일해 봤다면, 직접 느꼈을 것이다.

2. 품질 위험도 함께 올라갔다. 에이전트는 환각을 일으키고, 표류하고, 그럴듯하지만 미묘하게 틀린 코드를 쓴다. 보상 없이는, 에이전트가 키보드를 더 많이 차지하면서 코드 품질은 퇴화한다.

3. #2를 보상하는 방법들이 막 싸졌다.

정형 기법은 계산 비용 면에서는 결코 비싸지 않았다¹¹. 그들은 사람의 주의력 면에서 비쌌다. 내 영역에 가까운 곳에서(쿠버네티스 오퍼레이터 작성), Anvil 논문은 사람이 증명을 작성하고 마무리까지 반복하는 데 약 4.5배의 증명-대-코드 비율을 보고했다. 그건 많은 증명이다. 그게 "TLA+를 모든 것에 쓰자"가 삼십 년 동안 원리적으로 작동했음에도 업계 채택을 얻지 못한 이유다.

하지만 그 세금은 이제 다른 일꾼이 낸다. 검증기는 결정론적이고, 기계적으로 검사되며, 모호하지 않게 녹색이거나 빨간색이다. 증명이 닫히지 않으면, 검증기는 어떤 추측이 어떤 상태에서 실패하는지 정확히 말해준다. 이건 에이전트가 가장 잘하는 워크플로다: 빡빡한 피드백 루프, 명확한 신호, 수렴할 때까지 반복.

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

이전에 사람의 인내심으로 막혀 있던 기법들은 이제 계산 자원으로 막혀 있고, 그건 싸다. 문제에 하드웨어를 던지는 것이 여기서 이야기의 전부다.

그래서 셈법이 뒤집힌다. 우리는 정확성에 과잉 투자하기 위해 생산성 이득의 일부를 지불하고, 그 결과 순이익으로 나온다 - 더 큰 도달 범위, 이전보다 더 높은 품질. 정확성은 지금 기본기가 되어야 하는데, 우리가 순수주의자라서가 아니라, 그렇게 하면 수지가 맞고 안 하면 안 맞기 때문이다.

에이전트형 코드 신뢰하기§

우리에게 필요한 기법들은 이미 존재한다 - 그저 비용 모델의 변화를 기다리고 있었을 뿐이고, 그 변화가 막 일어났다.¹² 그러니 나는 지금 다음을 주장한다:

• 사소하지 않은 모든 프로그램의 핵심 로직 - 상태 머신, 유지되어야 하는 불변식, "거의 맞는" 것이 맞지 않은 부분들 - 에 대해서는 정형 기법을 쓰라, 또는 시도하라. LLM 보조 소프트웨어 수준 증명을 위해서는: Dafny, Verus, 또는 Lean (Creusot과 Kani는 보완적인 Rust 선택지다). 분산 시스템 설계를 위해서는: P 또는 TLA+.
• 나머지 대부분 - 의미 있는 입력 공간이 있는 곳이라면 어디든 - 에 대해서는 속성 기반 테스팅을 기본값으로 쓰라. 에이전트가 쓸모없고 오해를 부르는 테스트를 쓰지 않도록 변이 테스팅 도구에 아마 투자해야 한다.
• 회귀 및 정상 경로 페르소나 커버리지를 위해서는 - 전통적인 테스트를 유지하되, 솔직해지자: 그것들은 정확성의 테스트가 아니다. 그것들은 표현의 테스트다. "이 테스트가 말하는 그대로 한다".
• 명세 주도 개발을 위해서는 - 부담을 견디는 부분에 대해서는 정형 명세도 작성하라. 한계 비용은 작고, 보상은 크다.

이건 오래 선택사항으로 남지 않을 것이다. 방법은 존재한다. 비용은 막 떨어졌다. 에이전트로 인한 생산성 이득은 그 투자 비용을 대주는 동시에 그 투자를 요구한다.

우리의 피난처 - 지금은§

HL 왕국이 에이전트에 의해 식민지가 되고 있다. 우리는 그것을 그들의 영역에서 싸우지 않는다 - 우리는 위로, 코드 위의 층으로 후퇴한다: 자연어, 제품 명세, 정형 명세, 불변식, 도메인 모델, 페르소나. 한때 허약했던 것들(비공식 제품 명세, 사용자 스토리)과 한때 비쌌던 것들(정형 기법, 고급 테스팅 패턴)은 지금 둘 다 부담을 견디는 것들이다, 같은 이유로 - 그것들은 우리가 우리 자신에게 읽힐 수 있는 상태를 유지하고 HL 땅 아래에서 에이전트가 하는 일에 대한 강제력을 유지하는 방식이다.

중요한 기술은 그 층을 운영하게 해주는 것들이다: 실제로 제약을 가할 만큼 사용자 스토리를 잘 쓰기, 도메인 모델 도출하기, 불변식 식별하기, 어디를 테스트하고 어디를 검증하고 어디를 증명할지 결정하기, 에이전트가 빠져나갈 수 없을 만큼 명세를 빡빡하게 설계하기. 만약 이 중 어느 것도 - 사용자 스토리 쓰기, 도메인 모델 도출, 불변식 찾기, 그 모든 것을 테스트할 가치가 있는 추상화 층으로 조립하기 - 할 줄 모른다면, 점심시간은 끝났고, 누군가 당신의 샌드위치를 먹어치웠다.

1. 1
   Grace 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)까지 - 는 연구자 공급, 상업적 식욕, 그리고 이런 것들을 증명하는 일이 어렵다는 사실에 의해 속도가 제한되었다.
2. 2
   Steve Yegge (Gas Town, Gas City), Geoffrey Huntley (ralph loops), Simon Willison의 running commentary.
3. 3
   Kent Beck, TDD: By Example (2002); Fowler, Refactoring (1999); McConnell, Code Complete (2nd ed 2004); Dan North, "Introducing BDD" (2006); Gojko Adzic, Specification by Example (2011).
4. 4
   예제 기반 테스팅은 입력 공간을 한 고정 지점에서 표본 추출한다. 커버리지 지표는 무엇이 정확한가가 아니라 무엇이 걸어졌는가를 측정한다. Dijkstra의 1969년 NATO 발언은 고전이다: "프로그램 테스팅은 버그의 존재를 보이는 데는 쓸 수 있지만, 그 부재를 보이는 데는 결코 쓸 수 없다!" (report, EWD249에서 부연). "모든 보행" 보장은 모델 검사에서 온다 - 경계까지의 도달 가능 상태 전수 탐색.
5. 5
   가족 구성원: 변형 테스팅 - 관련된 입력의 출력 간 관계(ML, 과학 코드); 차등 테스팅 - 두 구현, 같은 입력, 비교(컴파일러, 리팩토링, 포팅); 상태 기반/모델 기반 PBT - 모델에 대한 연산의 시퀀스(rapid.StateMachine, proptest-state-machine, quickcheck-state-machine); 콘콜릭 실행(KLEE, SAGE); 변이 테스팅 - 테스트 강도 측정. 퍼징은 적대적-생성기 변형이다. 가장 자명한 것들을 제외하면 어느 것도 프로그램의 정확함을 증명할 수 없다 - 조합론이 빠르게 폭발한다.
6. 6
   내가 생각하기에 에이전트형 코딩이 수렴하는 곳. TypeScript: 구조적 타입은 인간-에이전트 경계에서 컴파일 시간 검증을 가장 싼 정확성 구매로 만든다. Rust: Verus와 타입 시스템은 증명 동반 코드를 가능하게 한다; 사람을 늦췄던 사용성 세금은 에이전트가 쉽게 낸다. Go: 에이전트를 굴릴 때 빠른 컴파일/vet/테스트 루프가 중요하다; vet/staticcheck/race-detector/퍼징이 성숙해 있다.
7. 7
   John Hughes와 Koen Claessen, "QuickCheck" (ICFP 2000). 수년간 하스켈 쓰는 사람들은 좀 이상하다는 식으로 다뤄지다가, 모든 주류 언어로 퍼졌다: rapid(Go), proptest(Rust), fast-check(JS/TS), hypothesis(Python).
8. 8
   작은 TLA+ 명세:

   ---- MODULE Counter ----
   VARIABLES count
   
   Init == count = 0
   Next == count' = count + 1
   
   Spec == Init /\ [][Next]_count
   
   NonNegative == count >= 0
   THEOREM Spec => []NonNegative
   ====
   

9. 9
   Xavier Leroy / CompCert, 2000년대 중반 - 정형 검증된 C 컴파일러, 오늘날 항공우주와 암호학에서 사용된다. L4.verified / seL4 (2009) - 최초의 정형 검증된 OS 마이크로커널. RustBelt (POPL 2018) - Rust의 타입 시스템이 건전함이 증명되었다. Verus와 Anvil (OSDI '24, 최우수 논문) - Rust로 된 정형 검증된 쿠버네티스 컨트롤러, 현재 "학술적 호기심" 단계.
10. 10
    이 피난처도 영원하지 않다. HL을 먹어 치운 같은 압축이 명세 층에도 올 것이다 - 에이전트가 목표에서 명세를 도출하고, 서로 검증한다. 그때쯤이면 우리는 오늘의 소프트웨어 산업보다 Iain M. Banks의 컬처에 더 가까워져 있고, 질문은 "사람이 AI가 일하는 동안 어떻게 최고의 삶을 사는가"가 된다.
11. 11
    실행당 비용은 사소하지 않을 수 있다 - TLC 실행, Verus 증명 검사, 퍼징 캠페인이 CPU를 갉아먹는다. 그래도 경제학은 작동한다: 소프트웨어는 "한 번 컴파일/검증, 여러 번 출하"다 - 한계 배포 비용이 0에 가깝다, Andreessen의 "Why Software Is Eating the World"대로. 검증에 하드웨어를 던지고, 희소한 자원(사람의 주의력)에 맞춰 최적화하라.
12. 12
    다음 한 자릿수의 변화는 20-30년 안에 오는 게 아니다; 2-3년 안에 온다. 안주하지 마라. 곡선 위에서 사는 법을 배워라.