Lean 창시자 Leo de Moura, AI가 쓴 코드를 누가 증명하는가: 명세와 형식 검증의 부상

AI 에이전트로 형식 검증 배우면서 느낀 건데, 내 생각을 형식 검증으로 표현하는 것 자체가 어렵더라. 치킨 먹고 싶어서 '치킨 요리'를 형식 검증하면 GPT나 Claude가 소스의 기원이나 닭 품종부터 파고들어서 치킨은 영영 안 나옴. liveness가 있으니 진척은 있어야 하는데, AI는 닭 기원 학습도 진척이라고 판단해버림.

형식 검증을 표준과 다른 의미로 쓰는 것 같은데. 조건 하나를 검증하면 다른 조건 검증이 약해진다는 건 표준 형식 검증에선 문제가 안 됨. '조건_1 AND 조건_2'를 통째로 검증하면 되니까.

충분히 강력하고 작업 호라이즌이 긴 에이전트는 먼저 우주를 처음부터 발명하고 나서야 치킨 요리를 끝낼 거임.

그 예시는 애초에 형식 검증할 수 있는 대상이 아님.

그 사람이 이제 AWS에 있는 게 좀 아쉽더라. 비영리 단체였으면 했는데.

'앞으로 몇 달, 몇 년간 사람들이 명세와 모델, 소프트웨어가 가져야 할 속성에 훨씬 집중하게 될 것'이라고 하던데, 형식 검증용 모델링 배울 자료 있음? Lean 아니어도 됨.

여기서 시작하면 됨. github.com/bendlang/bend

Lamport 책이나 Hillel Wayne 책 둘 다 좋음. 상태 기계를 명세 언어로 쓰는 게 접근하기 쉽고 깊이도 있음. 증명 보조 도구로 들어가려면 Software Foundations가 좋고, Rocq에서 Lean으로 넘어가는 간극은 작음.

배경용으로는 Monin의 Understanding Formal Methods가 최고임. 개념과 도구를 훑기에 좋고 250페이지 정도라 신호 대 잡음비가 높음. 실전은 Daniel Jackson의 Software Abstractions로 Alloy를 써서 구조 모델링, Lamport의 Specifying Systems로 TLA+를 써서 상태 기계 모델링을 배우면 되고, Lean4 사이트 무료 책을 병행하면 됨.

진짜 조합은 Lean 4/TLA+/Rocq에 AI, 그리고 결정적 생성기를 붙이는 거라고 봄. 큰 시스템에선 단언을 사람이 이해할 크기로 압축해야 하는데, 생성기가 만든 코드의 증명을 생성기가 내놓으면 사람은 생성기 자체만 확인하면 됨. Open Markets Initiative에서 Lean 4, TLA+, Rocq로 수백만 줄을 생성해 전자 거래 프로토콜 코드를 검증했는데, Lean이 잘못된 단계를 실제로 찾아냈음.

property based testing은 어떻게 생각함? 몇 개 세팅해봤는데 거의 형식 검증 같더라. 상태 관련이든 서비스 간이든 내가 생각도 못 한 버그를 잡아줌. 단점은 세팅이 지루하다는 건데 그건 LLM이 해결해줌.

맞음, LLM이 PBT나 mutation testing 같은 귀찮은 세팅을 쉽게 만들어줌.

PBT랑 퍼징은 내 머릿속에선 거의 같은 거임. 커버리지 기반 퍼징 AFL이 원조 혁신이었는데, '내 테스트가 포괄적인가'라는 질문은 한계에서 형식 검증만큼 어려운 열린 문제임. 결국 수렴할 거라고 봄.

PBT가 좋은 건 여러 언어에서 라이브러리로 구현돼 있어서임. 코드베이스를 Lean으로 다시 쓸 필요가 없음.

AI가 미래라는 쪽 사람들을 보면 하는 일이 별로 안 끌림. 예전엔 사람이 쓴 GitHub 프로젝트를 보는 게 재미있었는데, AI 생성 프로젝트엔 연결되고 싶은 마음이 전혀 안 듦. 유튜브도 AI 생성 영상은 피하게 되더라. 언제 hype가 꺾일지 궁금함.

지금 mathlib의 기초 이론은 형식 증명이 비싸다는 가정 위에 세워져 있어서 개념이 쪼개져 있음. LLM 시대엔 그 가정이 더는 맞지 않고, 개념과 증명을 인간 사고에 맞게 만들고 증명은 LLM이 이론 간에 옮기면 Lean이 번역이 맞는지 보장해줌.

아무도 검증 안 함. 소프트웨어 개발용 공리 체계 같은 게 없고, 증명하려면 먼저 명세가 필요함. 그 전에 구멍이 있다는 Lean 타입 시스템부터 고쳐야 하고.