AlphaProof, 암호화 기반을 4주 만에 수학적 검증

Google DeepMind의 인공지능 시스템 'AlphaProof'가 메시지 앱 'Signal'의 암호화 기반 코드를 수학적으로 검증했다. 통상적으로 수년이 걸린다고 알려진 이 프로세스를 DeepMind는 단 4주 만에 완료했다고 발표했다.

'수학적 검증'이란 코드가 논리적으로 올바르고 결함이 없음을 수식으로서 엄밀히 증명하는 작업을 의미한다. 버그 찾기나 동작 테스트와는 달리, 모든 조건 하에서 코드가 의도대로 작동함을 수학적으로 보장하는 것이다. 암호화와 같은 안전 보장에 직결되는 영역에서는 이러한 종류의 증명이 특히 중시되지만, 전문가가 수작업으로 진행하면 막대한 시간이 소요되므로 실용상 장벽이 높았다.

이번 작업에서는 Google의 대규모 언어 모델 'Gemini'를 기반으로 한 인공지능 에이전트군이 600만 줄 이상의 증명 코드를 자동 생성했다. 그 중에서 인간에 의한 확인이 필요한 것은 전체의 약 1%에 불과했으며, 나머지는 인공지능이 자율적으로 처리했다. 인공지능이 증명 작업의 대부분을 담당하고 인간 전문가가 최종 판단만 담당하는 분업 체제가 이번의 단기 완료를 가능하게 했다고 할 수 있다.

DeepMind는 이 기법을 향후 전력망이나 의료기기와 같은 중요 인프라에 적용할 계획을 밝혔다. 이러한 분야에서는 시스템의 오작동이 사회와 인명에 직접 영향을 미치므로, 소프트웨어의 신뢰성에 대한 요구 수준이 특히 높다. 인공지능에 의한 수학적 검증이 이러한 영역에서 실용화되면, 안전성 확보에 소요되는 비용과 시간을 대폭 단축할 수 있다는 평가가 가능하다.

Signal은 개인정보 보호를 중시하는 통신 앱으로 세계적으로 널리 사용되고 있으며, 그 암호화 프로토콜은 많은 보안 연구자와 전문가로부터 높은 평가를 받고 있다. 그 핵심이 되는 암호화 기반이 이번 검증 대상으로 선택된 배경에는 실용상의 중요성과 기술적 복잡성의 양면이 있다고 생각된다.

인공지능을 활용한 형식 검증(formal verification)의 연구는 이전부터 진행되어 왔지만, 실제 대규모 프로젝트에 적용하여 단기간에 성과를 낸 사례는 제한적이었다. AlphaProof가 600만 줄 규모의 증명 코드를 자동 생성한 것은, 인공지능 에이전트가 단순한 작업 보조를 넘어 고도의 논리 추론을 요하는 전문적 과제를 실행할 수 있는 단계에 가까워지고 있음을 보여주는 것으로 위치지을 수 있다.

향후 주목되는 것은 이 기법이 실제로 어느 중요 인프라 분야로 전개되는지, 그리고 인공지능이 생성한 증명을 업계와 규제 당국이 어떻게 평가하는지라는 점이다. 수학적 검증이라는 기법은 그 성질상, 인공지능의 판단을 다른 각도에서 검증하는 체계로서 기능할 가능성을 가진다. 인공지능에 의한 검증 프로세스 자체의 신뢰성 확보가 다음의 실천적 과제가 된다는 견해도 가능하다.