AI 시대, 형식검증이 소프트웨어 엔지니어링을 바꾼다

핵심 요약

• Lean 개발자 Leo de Moura는 AI가 형식검증을 실용적으로 만들고 있으며, 코드 생성이 쉬워진 지금이 검증의 중요성이 높아진 순간이라고 주장한다.
• Lean은 프로그래밍 언어이자 정리증명기로, 코드의 성질을 명시하고 기계검증되는 증명을 작성할 수 있다. 신뢰하려면 Lean 커널만 믿으면 되고, 다중 커널이 존재한다.
• AI 기반 자동형식화(autoformalization)로 어떤 언어의 코드든 Lean 모델로 변환할 수 있게 됐다. 예로 Microsoft의 SymCrypt 암호화 라이브러리는 Aeneas 도구를 통해 Lean으로 검증된다.
• Mathlib은 인간이 10년에 걸쳐 작성한 250만 줄의 수학 라이브러리인데, AI는 현재 5천만 줄 규모의 형식증명을 작성하고 있으며, Anthropic AI로 작성된 페르마의 마지막 정리 증명은 1천3백만 줄이다.
• AI로 코드 모델을 작성할 때 그 모델이 원본 코드와 정확히 일치하는지 확인해야 하며, 미분 테스트와 같은 방법으로 버그를 찾을 수 있다.
• 테스트는 버그의 존재를 보여줄 뿐 부재를 증명하지 못하지만, 형식검증은 모든 가능한 입력에 대해 프로그램의 정확성을 증명한다.
• Navier-Stokes 방정식 증명에서 OpenAI의 비형식 증명과 형식 증명 사이에 불일치가 있었는데, Verso Blueprint 도구를 사용하면 자연언어와 Lean을 혼합하여 이런 오류를 줄일 수 있다.
• 형식증명은 정적 객체가 아니며, 리팩터링하고 단순화할 수 있다. 예를 들어 Anthropic의 페르마 정리 증명은 이미 절반으로 축약되었다.
• AI로 증명을 최적화할 때 새로운 증명이 원래 코드와 동일하게 계산되는지 보장하는 증명이 '가이드레일' 역할을 한다.
• 미래 소프트웨어 엔지니어링은 형식 명세서와 성질 정의에 초점을 맞추게 될 것이며, 요구사항 격차와 모델 격차를 해결하는 과정이 중요해진다.
• 설계 문서가 비형식적인 자연언어에서 형식적 명세로 바뀌면, 도구가 설계와 구현의 일치 여부를 자동으로 검사할 수 있다.
• 형식 명세가 소스 제어의 중심이 되고 코드는 명세로부터 AI가 작성하므로, 엔지니어의 핵심 역량은 '정확한 요구사항 정의'가 된다.