구글 딥마인드가 현지 시각 11월 10일 여러 AI 모델이 함께 소프트웨어의 정확성을 수학적으로 증명하는 ‘알파프루프 코드(AlphaProof Code)’를 공개했다. 구글 딥마인드 연구진은 이 도구로 메신저 앱 시그널이 쓰는 암호 프로토콜의 핵심 코드를 기계어 수준까지 형식 검증했다.

알파프루프 코드는 여러 대형언어모델(LLM)이 역할을 나눠 작업하는 에이전트 방식의 검증 체계다. 형식 검증은 프로그램이 정해진 조건대로만 작동한다는 사실을 수학적 증명으로 확인하는 방법이다. 구글 딥마인드에 따르면, 널리 쓰이는 암호 프로토콜을 AI가 이 수준까지 검증한 사례는 이번이 처음이며, 이런 프로토콜의 실제 구현 코드가 어떤 방식으로든 형식 검증된 것도 처음이다.

린(Lean)은 수학 명제와 프로그램의 성질을 증명하고 컴퓨터로 검사하는 증명 보조 언어다. 알파프루프 코드의 에이전트들은 구글의 AI 모델 ‘제미나이 카본’을 기반으로 린으로 작성한 코드를 600만 줄 넘게 생성했다. 이후 에이전트들이 증명을 다시 점검해 전체 코드의 약 1%를 사람이 검토할 부분으로 표시했다. 검증 작업 기간은 4주다. 구글 딥마인드는 같은 작업에 지금까지는 전문가 팀이 몇 년을 들였다고 설명했다.

연구진은 도구의 성능을 시험하려고 과거에 고친 버그 2건을 격리한 시그널 코드 사본에 다시 넣었다. 두 경우 모두 알파프루프 코드는 버그가 들어간 코드가 안전하지 않다는 사실을 기계로 확인 가능한 증명으로 제시했다.

에렌 크렛 시그널 최고기술책임자(CTO)는 이 방식으로 기존 검증 작업의 범위를 크게 넓힐 수 있게 됐고, 시그널 코드가 약속한 개인정보 보호 수준에 대한 확신도 높아졌다고 밝혔다. 구글 딥마인드는 검증에 쓴 산출물을 깃허브 페이지(google-deepmind.github.io/code-verification)에 오픈소스로 공개하고 기술 논문도 함께 공개했다. 검증 방법에 의견을 준 시그널 직원들에게는 감사를 표했다. 이번 블로그 글은 구글 딥마인드의 푸시밋 콜리와 스와랏 차우두리가 작성했다.

자세한 내용은 구글 딥마인드에서 확인할 수 있다.

이미지 출처: 구글 딥마인드