AI가 짠 코드, 버그 없는지 기계로 완벽 증명하는 방법

요약 인공지능(AI)이 코드를 빠르게 생성하는 시대가 열리면서 소프트웨어의 신뢰성을 어떻게 검증할 것인가에 대한 논의가 활발해지고 있습니다. 프로그래밍 언어이자 정리 증명기(theorem prover)인 'Lean'의 창시자이자 AWS의 특훈 과학자인 레오 데 모우라(Leo de Moura)는 팟캐스트 인터뷰를 통해 '형식 검증(formal verification)'이 AI 시대의 핵심 열쇠가 될 것이라고 강조했습니다. 그는 기존의 단위 테스트나 속성 기반 테스트(property-based testing)는 버그를 찾아내는 데는 유용하지만 버그가 전혀 없음을 증명할 수는 없다는 본질적인 한계를 지적했습니다. 반면 Lean과 같은 도구를 활용한 형식 검증 체계에서는 코드가 충족해야 할 수학적 속성을 먼저 정의한 뒤, AI에게 해당 속성을 만족하는 코드와 기계가 검증할 수 있는 증명(machine-checked proof)을 함께 작성하도록 요구할 수 있습니다. 실제로 그의 동료 킴 모리슨(Kim Morrison)은 데이터 압축 라이브러리인 zlib을 Lean으로 포팅한 뒤, '데이터를 압축했다가 다시 풀었을 때 데이터가 손실되거나 손상되지 않고 온전히 복원된다'는 중요한 성질을 완벽히 수학적으로 증명하는 실험을 진행하기도 했습니다. 이러한 기계 검증 증명 체계는 거대한 코드베이스 중에서도 오직 신뢰할 수 있는 소형 검증 커널만 믿으면 되기 때문에, AI가 쏟아내는 수많은 코드에 대한 인간의 신뢰 병목 현상을 해소할 강력한 대안으로 주목받고 있습니다.