LLMが証明自動化でLean実用化を加速
원제: We have proof automation now
왜 중요한가
LLM에 의한 정리 증명 자동화는 형식 검증 기술의 도입 비용을 대폭 줄여, 안전·보안 크리티컬 소프트웨어 개발의 실용화를 앞당길 수 있다.
Google의 보안 엔지니어 Adam Langley가 2026년 7월 26일, LLM을 활용한 정리 증명 자동화により依存型言語Leanが実用的になったと報告した。Zstandard 디컴프레서를 Lean으로 구현し、LLM이 증명 코드 생성을 자동화할 수 있음을 실증した。
imperialviolet.org에 게재된 기술 블로그에서 저자는 의존 타입(dependent type) 언어인 Lean을 사용해 Zstandard 디컴프레서를 구현한 실험 결과를 보고했다.
의존 타입 언어는 타입 시스템 안에 임의로 세밀한 불변 조건(invariant)을 형식적으로 기술하고 기계가 검증할 수 있는 장점이 있다. 그러나 seL4 프로젝트의 회고록에 따르면, 설계·구현 시간 대비 증명에 약 10배의 시간이 소요되었으며, C 코드 대비 20배 이상의 증명 코드가 생성되었다. 이 높은 비용이 의존 타입 언어의 실용화를 방해해 왔다.
종래의 자동화 시도로는 SMT 솔버를 이용한 F*이 있었으나, 복잡한 경우 솔버가 수 시간 동안 종료되지 않는 문제가 있었고, 사용자는 솔버를 만족시키는 코드 스타일에 대한 경험적 감각을 개발해야 했다.
저자는 "증명의 내용이 아닌 존재 자체가 중요하다"는 증명 비관련성(proof irrelevance) 원칙 아래, LLM이 증명 코드를 자동 생성하는 데 적합하다고 주장했다. 실제로 Lean에서 LLM을 활용한 증명 자동화를 시도한 결과, 타입 체커를 과부하시키지 않으면서 증명을 생성할 수 있음을 확인했다. 이로 인해 증명 엔지니어링(proof engineering)에 드는 부담도 크게 줄어들 가능성이 있다고 밝혔다.