Lean 창시자 Leo de Moura: AI가 코드를 쓰는 시대, 증명이 신뢰를 만든다
AI, Lean, and the Future of Formal Verification, with Lean Creator Leo de Moura
AWS의 Leo de Moura가 Lean을 통해 AI 생성 코드의 신뢰 문제를 어떻게 해결하는지 이야기한다. AI가 코드를 작성하는 시대에 형식 검증은 선택이 아닌 필수가 된다. Kim Morrison이 zlib을 Lean으로 포팅해 압축-해제 무손실 속성을 증명했고, Microsoft는 Aeneas로 Rust 암호 라이브러리를 검증한다. Mathlib은 2,500만 줄인데, AI는 5,000만 줄 증명을 만들어낸다. Claude Code 개발자는 Lean을 모른 채 AI로 실제 버그를 찾아냈다. 핵심은 모델이 코드와 일치하는지 확인하는 일이다.
Lean으로 증명된 결과를 신뢰하려면 커널만 신뢰하면 됩니다. 증명이 검사되는 곳이 바로 거기니까요.
HN 토론
32- chamomeal
속성 기반 테스팅(property based testing)에 대해 사람들은 어떻게 생각하나요? 몇 가지 속성 기반 테스트를 설정해 봤는데 거의 형식 검증(formal verification) 같다는 느낌이 들었어요.
같은 건 아니라는 건 알지만, PBT는 제가 생각지도 못한 온갖 미친 버그를 잡아낼 수 있어요. 상태 관련된 것, 서비스 간 연동 관련된 것 등등. PBT에 대한 유일한 불만은 항상 설정이 지루하다는 점이었는데, LLM이 그걸 해결해 주네요.
최근에 PBT에 대한 논의를 별로 못 봤지만, LLM 시대에 가성비가 정말 뛰어납니다.
- wbeckler
Lean 4/TLA+/등등에 AI와 결정적 생성기를 더한 것이 최고의 조합이라고 생각해요. 대규모 시스템의 경우 형식적 방법의 단언(assertion)은 인간이 이해할 수 있는 크기로 압축되어야 합니다. 이는 단언이 모델과 그에 연결된 코드 생성기의 정확성을 확인할 때 가능합니다. 생성기는 생성된 코드에 대한 증명을 생성할 수 있고, 인간은 생성기가 증명 가능하게 올바른 대규모 단언을 생성하는지만 확인하면 됩니다.
이것이 형식적 방법이 대규모 시스템에서 AI를 제약할 수 있는 방식입니다.
우리는 Open Markets Initiative에서 이를 하고 있으며, 수백만 줄의 Lean 4, TLA+, Rocq 코드를 생성하여 오픈 소스 전자 거래 프로토콜 코드가 정확함을 보장했습니다. 예상치 못했지만 Lean 증명기가 몇 가지 잘못된 단계를 식별해냈습니다.
- PandaRider
> ... 하지만 앞으로 몇 달, 몇 년 안에 사람들은 명세(specification), 모델, 소프트웨어가 가져야 할 속성에 훨씬 더 집중할 것으로 예상합니다.
형식 검증을 위한 모델링 학습 자료를 가진 분 있나요? (꼭 Lean일 필요는 없습니다)
- fspeech
현재 mathlib의 기초 이론은 형식 증명이 비싸다는 가정 하에 구축되어 있습니다. 개념들은 가능한 한 많은 증명을 공유하기 위해 분할되어 있습니다. LLM이 등장하면서 그 가정은 더 이상 맞지 않습니다. 개념과 증명은 인간의 사고에 최대한 맞게 구축되어야 하며, 증명은 LLM이 이론 간에 이식할 수 있습니다. Lean은 번역이 올바른지 보장할 것입니다.
- zujkas
소프트웨어 개발을 위한 ZFS 공리 체계가 없고 무언가를 증명하려면 먼저 명세가 필요하기 때문에 아무도 검증하지 않습니다-
그렇다면 차라리 Lean의 타입 시스템을 고치세요. 제대로 이해되지도 않았고 구멍도 있습니다.
AI 돈을 가진 사람들은 한 시간만이라도 입 좀 다물 수 없나요?