요약
AI가 코드와 증명을 쏟아내는 시대에는 기계로 확인하는 검증이 새로운 병목이 된다고 레오 드 모라는 말합니다.
Lean(프로그래밍 언어이자 증명 보조 도구)을 만든 레오 드 모라가 팟캐스트 The Data Exchange에 나와 한 이야기입니다. 그는 AWS 부사장이자 Lean을 개발하는 비영리 조직의 수석 설계자이기도 합니다.
왜 중요한가
- 개발자가 할 일의 중심이 코드 작성에서 명세(소프트웨어가 지켜야 할 성질을 정해 둔 것) 작성으로 옮겨 간다는 전망입니다.
- 코드는 다시 생성하면 되고, 버전 관리로 지킬 기준은 명세가 된다고 봤습니다.
- "형식 검증을 마쳤다"는 업체의 말만으로는 믿을 수 없으니, 도입 담당자가 확인할 항목을 제시했습니다.
핵심 내용
- 테스트는 시험한 입력만 확인하지만, 증명은 모든 입력을 다룹니다.
- 어떤 성질을 증명해 두면 AI가 과감하게 최적화해도 결과가 그대로인지 증명으로 확인할 수 있습니다.
- 그의 말에 따르면 Claude Code 개발 책임자는 Lean을 모르는데도 Claude에게 Lean으로 버그를 찾게 해 실제 버그를 고쳤습니다.
- AI가 만든 모델이 실제 코드와 다를 위험이 남아 있어, 둘의 결과를 비교하는 차등 테스트로 버그를 찾는 사례가 나오고 있습니다.
- 업체에는 명세, 검증한 성질, 쓴 증명 검사기, 믿어야 하는 코드의 크기를 물어보라고 권했습니다.
HN 반응
- AI가 만든 검증의 성질이 맞는지는 어떻게 아느냐는 물음이 나왔고, 명세로 일이 옮겨 갈 뿐이며 완벽한 명세는 없다는 회의론도 있었습니다.
- 라이브러리만 붙이면 되는 속성 기반 테스트(무작위 입력으로 성질을 확인하는 방식)가 더 실용적이라는 의견과, 반례 찾기와 증명은 목적이 다르다는 반론이 맞섰습니다.
최고의 조합은 Lean 4/TLA+ 같은 도구에 AI, 그리고 결정론적 생성기를 더하는 것이라고 생각합니다. 대규모 시스템에서는 형식 기법의 단언(assertion)을 사람이 이해할 수 있는 크기로 압축해야 합니다. 단언이 모델과 거기에 딸린 코드 생성기가 정확한지를 확인하는 방식이면 이게 가능합니다. 생성기가 생성된 코드의 증명을 만들어 내고, 사람은 그 생성기가 올바른 대규모 단언을 만들어 낸다는 점만 증명 가능하게 확인하면 됩니다.
형식 기법이 대규모 시스템에서 AI를 제어하는 방법이 바로 이겁니다.
저희는 Open Markets Initiative에서 이 방식을 쓰고 있습니다. 오픈소스 전자 거래 프로토콜 코드가 정확한지 보장하려고 Lean 4, TLA+, Rocq 코드를 수백만 줄 생성했습니다. 예상하지 못했는데, Lean 증명기가 실제로 잘못된 단계를 몇 군데 찾아냈습니다. https://github.com/Open-Markets-Initiative
TLA+의 요점은 설계의 여러 측면을 아주 높은 수준에서 모델링하는 것이라서, 결정론적 생성은 원칙적으로 현실성이 없는 것 아닌가요? TLA+ 모델은 LLM에게 유용할 수는 있겠죠(진짜 버그를 찾는 데 도움이 되니까요).
정말 흥미롭네요!
이 내용을 자세히 정리한 논문이나 글이 있나요?
이 부분이 완전히 이해되지는 않습니다. 조금 더 자세히 설명해 주실 수 있습니까?
속성 기반 테스트(PBT)는 어떻게 생각하세요? 속성 기반 테스트를 몇 개 만들어 봤는데 거의 형식 검증 같은 느낌이더라고요.
같은 게 아니라는 건 알지만, PBT는 제가 생각도 못 했을 온갖 황당한 버그를 잡아냅니다. 상태가 있는 코드나 서비스 사이에 걸친 문제 같은 것들이요. PBT의 유일한 불만은 설정이 번거롭다는 건데, 그건 LLM이 해결해 줬어요.
요즘은 PBT 얘기가 별로 안 보이는데, LLM 시대에는 들인 노력 대비 얻는 게 엄청나게 큽니다.
저는 PBT와 퍼징이 기본적으로 같은 거라고 생각해요.
웃긴 건, 어떤 샘플링이 충분히 포괄적이라고 말하려면 필요한 추론이 오히려 증명에 가까워진다는 거예요! 커버리지 기반 퍼징인 AFL이 여기서 원조 혁신가였죠. 그런데 인터프리터를 생각해 보세요. 인터프리터 자체의 코드 커버리지는 별 의미가 없고, 인터프리터가 실행하는 프로그램까지 탐색해야 하잖아요!
그래서 "내 테스트가 충분히 포괄적인가?"는 사실 끝이 없는 문제이고, 극한에서는 형식 검증만큼 어렵습니다.
결국 둘이 수렴할 거라고 봐요. 무작위 테스트를 "몬테카를로 형식 검증"이라고 불러도 되겠네요, 헤헤.
정말 맞는 말씀이에요! 저도 애초에 PBT를 알게 된 게 FoundationDB 이야기를 언급하는 발표를 봐서였어요. 정말 흥미로운 이야기죠. 링크가 필요하신 분이 있으면 찾아서 드릴게요.
저도 속성 기반 테스트가 훌륭하다고 생각합니다.
다만 제 생각에 둘은 초점이 매우 달라서, 소프트웨어가 정해진 상태와 매개변수 안에서 해야 할 일을 하는지 따질 때 서로 다른 자리를 차지합니다.
이 모든 논의에서 가장 중요한 요소가 빠져 있다고 생각합니다. 바로 밸리데이션(validation)입니다.
베리피케이션(verification)은 소프트웨어가 해야 할 일을 하는지 증명하거나 테스트하거나 확인하는 것이고, 밸리데이션은 소프트웨어가 사용자의 필요를 해결하고 있는지 증명하거나 테스트하거나 확인하는 것입니다.
속성 기반 테스트가 좋은 이유는 많은 언어에서 라이브러리로 구현되어 있기 때문입니다. 코드베이스를 Lean으로 다시 쓸 필요가 없죠.
형식 검증을 위한 모델링을 배울 수 있는 자료를 아시는 분 있나요? (꼭 Lean이 아니어도 됩니다)
Lamport의 책이나 Hillel Wayne의 책이 둘 다 좋습니다. 명세 언어로서의 상태 기계는 예전부터 꽤 접근하기 쉬우면서도 깊이가 있었습니다. 증명 보조기를 본격적으로 해 보고 싶다면 Software Foundations가 훌륭하고, Rocq를 알면 Lean을 이해하기까지의 차이는 꽤 작습니다.
https://lamport.azurewebsites.net/tla/book.html https://logicforprogrammers.com/ https://softwarefoundations.cis.upenn.edu/
필수 배경지식입니다.
실전용입니다.
Daniel Jackson의 Software Abstractions: Logic, Language, and Analysis - "Alloy" 언어로 구조(즉 데이터) 모델링을 가르칩니다.
Leslie Lamport의 Specifying Systems: The TLA+ Language and Tools for Hardware and Software Engineers - "TLA+" 언어로 행동(즉 상태 기계) 모델링을 가르칩니다.
위 두 권은 "시스템 모델링", 즉 완전한 시스템을 형식적으로 구축하는 데 필요한 모든 것을 다룹니다.
PS: Event-B 방법론 같은 것도 몇 가지 더 있지만, 필요해지면 그때 보셔도 됩니다.
여기서 시작하세요: https://github.com/bendlang/bend
이건 바이브 코딩으로 만든 프로젝트이지, 형식 검증 모델링을 배우는 자료가 아닙니다.
에이전트로 형식 검증을 생성한다면, 검증되는 속성이 올바른 속성인지 어떻게 알 수 있나요?
제가 보기에 AI는 현재 검증을 주로 사람이 만든 도구에 의존합니다. AI가 강화학습(RL) 알고리즘을 일부 활용해 사람이 각 단계에서 밟아 온 경로를 찾아내긴 했지만, 그 경로는 본질적으로 여전히 사람의 수학 도구를 기반으로 하고 있고 인간 전문가의 확인이 필요합니다. 수학을 다루는 AI에게 새로운 방법과 검증 경로를 제공할 수 있는, 더 혁명적인 틀이 필요합니다.
실수하지 마세요, 하면 되죠
거의 농담이고요, 다만 에이전트 스스로도 형식 명세가 자연어 명세에 충실한지 점점 더 잘 가려내고 있긴 해요.
알 수 없죠. 기계 신을 흔들림 없이 믿는 수밖에요.
그래서 형식 기법이 정말 다음 단계가 되려면, 결정론적인 소스에서 CoC 언어로 가는 컴파일러가 필요하고 우리는 다시 돌아가야 해요.
Lean은 C로만 컴파일되기 때문에 좀 아쉬운, 사이비 종교 같은 선택이에요. 소프트웨어에는 Dafny처럼 타깃이 훨씬 많은 증명기를 써야 합니다. Rocq(예전 이름 Coq)조차 여러 함수형 언어로 컴파일할 수 있는데, Lean은 그렇지 못하죠.
늘 그렇듯 AI 쪽 사람들은 제일 먼저 떠오른 해법에 달라붙었고, 최근 수학 응용 분야에서 두각을 나타낸 덕에 이제 아무것도 제대로 이해하지 못한 채, 장단점도 따져 보지 않고 게으르게 컴퓨팅에 적용해 보기 시작했어요. 물론 모델들이 Lean으로 집중 훈련되었을 테니 우리는 이제 사실상 Lean에 묶였죠. 그래도 CoC 언어이긴 하지만, 이게 제대로 돌아가려면 이제 그 주변에 컴파일 체계를 잔뜩 더 만들어야 해요.
대부분 질문과는 상당히 거리가 먼 얘기네요. 그리고 Lean을 선택한 이유는 꽤 단순합니다. 프로그래밍에도 쓰도록 설계되었고, 실제로 성공했기 때문입니다. C로 컴파일하는 건 분명히 나쁜 선택입니다(아니, 분명하진 않은가 보네요, 다들 왜 그런지 계속 그런 식으로 언어를 구현하니까요). 하지만 어떤 증명기를 쓸지 정할 때 가장 덜 중요한 요소 중 하나라고 할 수 있습니다. Lean의 대안은 Idris(건전하지 않고 인기도 없습니다), ATS(인기가 없습니다), Rocq(더 합리적이지만 여전히 대부분 학술 프로젝트입니다) 정도입니다.
C로 컴파일하는 건 언어를 컴파일할 때 분명히 아주 훌륭한 선택으로 보입니다. 타깃 언어로 좋은 선택이고, 기존 도구를 많이 활용할 수 있고, 표준이 안정적이고, 상호 운용성이 좋고, 지원 플랫폼도 넓습니다. 게다가 정밀하게 모델링할 수 있을 만큼 단순하기도 합니다.
현재 mathlib의 기초 이론은 형식 증명에 비용이 많이 든다는 가정 아래 만들어져 있습니다. 증명을 최대한 공유하려고 개념들을 잘게 쪼개 놓았죠. LLM이 있으면 이 가정은 더는 맞지 않습니다. 개념과 증명은 가능한 한 사람의 사고방식에 맞게 만들고, 증명은 LLM이 이론 사이에서 옮겨 주면 됩니다. 번역이 올바른지는 Lean이 보장할 겁니다.
사람이 읽고 쓰기 어려운 검증 방식을 왜 쓰는지 모르겠어요.
제가 뭔가 놓치고 있는 것 같긴 한데, 이게 결국 다음 두 가지에 불과한 게 아닌지 모르겠습니다.
완벽한 명세 같은 건 없습니다. AI가 앗아 가는 것 중 하나가 글자 하나하나마다 오가는 피드백 주기입니다. 소프트웨어를 짜다가 return 문을 쓰는 도중에 "어, 이건 내가 하려던 게 아닌 것 같은데" 하고 깨달은 적이 셀 수 없이 많아요. 명세를 쓰면서 그런 경험을 어떻게 재현할 수 있을지 모르겠습니다... 명세를 쓰기 전에 몇 시간씩 앉아서 곰곰이 생각하는 사람은 없을 테니까요.
영상에서 설명하는 것처럼 Lean과 Rust 같은 것의 결과를 비교한 사례가 있나요?
저는 Lean에 기호 오차항이 있는데, 이걸 샘플링해서 몬테카를로 분석과 비교할 수 있을 것 같아요. 하지만 이미 샘플링 기반 분석은 갖고 있었고, 그래서 이 모든 걸(이중 슬릿 실험과 GrC(2,4)를 쓴 중력) Lean 4로 해야 했던 거죠.
Lean과 Rust로 된 TLA+ 구현을 하나 이상 결합하려면 무엇이 필요할까요? 에이전트는 이걸 어떻게 계획하고 구현하며, 장단점은 무엇일까요?
"Isabelle/HOL, Lean, HOL4, Agda 비교: 네 가지 정리 증명기 이야기"(2026)는 있는데 Rocq는 없나요? https://news.ycombinator.com/item?id=50043202
좋은 글이네요. HN 게시물에는 아무도 댓글을 안 달았으니 직접 링크를 올립니다.
정리 증명기 네 가지 이야기 - https://blueberrywren.dev/blog/primes/
저도 문장을 전치사로 끝내는 글을 꽤 써 봤지만, 오랜 세월 글을 읽으면서 "via"로 문장이 끝나는 건 처음 봅니다. 저자는 독일인이나 덴마크인, 아니면 수학자겠죠.
이 약어들은 쓰기 전에 정의되지 않았습니다.
LCF: Logic for Computable Functions(계산 가능 함수 논리) - https://en.wikipedia.org/wiki/Logic_for_Computable_Functions
HOL: Higher Order Logic(고차 논리) - https://en.wikipedia.org/wiki/HOL_(proof_assistant)
... 이분이 이제 AWS 소속이라는 게 조금 실망스럽네요. 비영리 단체였으면 했거든요.
이분은 관련 비영리 단체인 Lean FRO의 최고 설계자이자 공동 창립자이기도 합니다. https://lean-lang.org/fro/team/
AI 에이전트를 쓰는 상황에서 형식 검증을 배우고 적용해 보면서 느끼는 건, 때로는 제 생각을 형식 검증으로 표현하기가 어렵다는 점입니다. 그보다 더 의심스러운 건, 형식 검증을 제대로 한다고 해서 AI가 특정 작업에서 제자리를 맴도는 현상이 정말 해결되느냐는 겁니다.
예를 들어 저는 치킨을 먹고 싶어서 "치킨 요리"를 형식적으로 검증하려고 하는데, GPT나 Claude는 매번 치킨 요리에 들어간 소스의 기원이나 닭의 품종을 파고들기 시작합니다. 그러면 치킨 요리는 끝내 완성되지 않고 저녁상에도 오르지 못한 채, 저는 닭의 기원에 대한 깊은 지식만 얻게 됩니다.
물론 형식 검증에 활성(liveness), 즉 작업에 진전이 있어야 한다는 성질도 포함된다는 건 압니다. 하지만 AI는 닭의 기원을 알아내는 것도 진전이라고 판단합니다. 그러다 실제로는 하지 말아야 할 일을 하게 되고요.
개인적으로 이런 AI 안티패턴을 정리하면서 느낀 건, 한 조건을 형식적으로 검증하면 다른 조건의 검증이 약해지고, 그 현상 속에서 AI가 다시 제자리를 맴도는 게 보인다는 점입니다. 결국 저는 모든 걸 하나하나 직접 읽고 병합하는 과정을 거치게 되는데, 이런 경험을 하는 게 저뿐인지 궁금합니다.
"형식 검증"을 표준과 다른 뜻으로 쓰고 계신 것 같습니다.
표준적인 형식 검증에서는 이런 문제가 없습니다. "조건_1 AND 조건_2"라는 복합 조건을 형식적으로 검증하면 되니까요.
제가 자주 부딪히는 문제는 이렇습니다. 형식 검증은 아니지만, 먼저 UML 다이어그램을 만들어서 전체 뼈대를 잡습니다. 보통 공개된 아키텍처 책들이 있어서 거기서 가져옵니다.
그러면 UML 뼈대 전체를 구현해야 하잖아요? 그런데 하다 보면 중간쯤에서 "이 알고리즘이 너무 느린가? 음... 더 빠르게 만들어야겠다" 하면서 국소 최적화를 시도하고, 그래서 원하는 결과, 그러니까 적어도 돌아가는 MVP를 못 얻을 때가 있습니다.
전체 목표는 제가 분명히 알고 있는데, 특정 하위 목표에 집착하거나 그 하위 목표를 계속 키우는 문제가 있습니다.
문제는 AI에게 "가드레일"을 세워 두지 않았다는 점입니다. 그래서 AI가 당신을 돕겠다고 할 수 있는 모든 걸 하려고 하는 겁니다(기본 페르소나가 "비위 맞추는 사람"입니다).
AI는 "부정 제약"을 아주 잘 이해하니, 가능한 한 매 단계마다 "하지 말아야 할 것"을 명시적으로 알려 주세요.
하향식 및 단계적 정제 방법론으로 먼저 "인터페이스"를 만들고 그다음 "구현"을 만드세요. 방법은 이렇습니다.
UML에서 1:1로 곧바로 스텁/목을 갖춘 "명확한 인터페이스를 가진 뼈대 앱"만 만들게 하세요. UML을 텍스트 형태로 쓰면 AI를 위한 힌트와 메모를 쉽게 달 수 있어서 더 좋을 수 있습니다. "뼈대 앱"에는 a) LKM/ioctl처럼 공개 인터페이스가 좁은 시스템 모듈 b) 서브디렉터리 하나에 모듈 하나씩, 순환이 없는 DAG로 이루어진 디렉터리 구조 c) 사용할 서드파티 라이브러리/프레임워크의 명시적 목록 d) 클래스/추상 클래스/인터페이스 e) 전체 타입 시그니처를 갖춘 자유 함수와 클래스 메서드 등이 포함되어야 합니다.
위 결과를 확인하고, UML과 생성된 코드가 만족스러운 인터페이스 상세 수준에서 맞아떨어질 때까지 반복하세요. 이 상태는 컴파일되어야 하고, 동작하는 MVP가 나올 때까지는 바꿀 수 없는 절대적인 기준선입니다.
위 뼈대를 바탕으로 인터페이스는 일절 바꾸지 않고, 구현만 최대한 단순하게(즉 "순진한" 선형, 무차별 대입 등으로) 채우게 하세요. 최적화는 전혀 하지 않습니다. 여기서 사전조건/사후조건/불변식에 대한 런타임 단언을 추가하라고 명시적으로 요청하세요. 단언에는 어떤 부작용도 없어야 한다는 점도 분명히 하세요. 이렇게 하면 "순진한" MVP로 컴파일될 겁니다.
포괄적인 테스트 스위트를 생성해 위 결과를 테스트하세요.
이제 인터페이스와 단언을 바꾸지 말고 엄격히 지키면서 전부 최적화하게 하세요. 컴파일하고 위 테스트 스위트로 검증하세요. 그러면 "최적화된" MVP가 나옵니다.
위 단계를 통과하면, 성능이 중요한 경우 "사전조건" 외의 모든 단언을 주석 처리하게 하세요. 사전조건은 항상 남겨 둡니다. 이것이 최소한의 "건전성 검사"입니다.
마지막으로 UML의 모든 "유스케이스"(즉 기능)마다, 앞서 생성한 코드에서 사전조건/사후조건/불변식(이것들이 명세가 됩니다)을 표시한 제어 흐름 그래프를 유스케이스 하나당 하나씩 생성하게 하세요. 이것이 구현의 호출 그래프가 유스케이스, 즉 기능 명세를 만족하는지 확인하는 "화이트박스" 검증 문서가 됩니다.
이 과정을 거치면 "순진한" 구현과 "최적화된" 구현, 두 가지 구현이 생깁니다. 앞으로 기능을 수정하거나 추가할 때 한쪽을 다른 쪽과 대조해 볼 수 있도록 항상 둘을 함께 유지하면 매우 유용합니다.
UML 대신 텍스트로 된 요구사항 문서 등을 써서 같은 과정을 거칠 수도 있습니다. 필요하다면 요구사항에서 AI에게 UML을 생성하게 해서 시스템의 그래픽 명세도 만들 수 있습니다.
이것이 "계약에 의한 설계"(DbC) 방법론을 쓰는 "구성에 의한 정확성"(CbC) 접근법입니다.
또한 정적 타입 언어로 생성한다면, 1단계의 인터페이스부터 의존 타입 등을 적절히 써서 코드의 정확성을 위한 제약을 세우고 코드가 올바름을 증명할 수 있도록, 타입 시스템을 충분히 활용하라고 AI에게 명시적으로 요청할 수 있습니다. 이것이 "타입 주도 설계"입니다. 다만 다소 고급 기법이므로 구현 언어를 잘 아는 경우에만 하세요. AI가 너무 영리하게 굴며 코드를 이해하기 어렵게 만드는 "타입 곡예"를 구현하려 할 수 있습니다.
예전 IDE(Visual Studio MFC 등)에서 마법사로 스텁/목이 있는 기본 뼈대 앱 코드를 먼저 생성하고, 컴파일되게 만든 다음 거기에 코드를 추가하면서 매 단계마다 테스트하고 검증하던 방식을 떠올려 보세요. AI가 그렇게 결정론적으로 움직이게 만들고 싶은 겁니다.
PS: 시작하려면 제 댓글을 AI에게 넣고, 쓰시는 AI 인터페이스에 필요한 프롬프트를 생성하게 해 보세요 ;-)