[기획: AI 트렌드] AI가 증명을 다 쓰자 남은 일은 '무엇을 증명할지'였다 — DeepMind의 Signal 기계어 검증

11월 10일 Google DeepMind가 논문 한 편을 냈습니다. 메신저 Signal의 암호 코드가 보안 성질을 지킨다는 것을 AI 에이전트로 증명했다는 내용입니다. 증명은 약 650만 줄인데, 저자들 계산으로 사람이 읽고 믿어야 할 부분은 약 2.6만 줄입니다. 우리는 틀릴 수 있는 곳이 증명에서 명세(무엇을 증명할지 적은 문장)로 옮겨 갔다는 점이 핵심이라고 봅니다.

650만 줄과 2.6만 줄

그 650만 줄이 무엇을 증명했는지부터 보겠습니다. 대상은 Signal 프로토콜, 즉 메시지를 암호로 주고받는 규칙을 코드로 옮긴 기준 구현 libsignal입니다. 이 규칙은 수십억 명의 대화를 지킵니다. 저자들은 이 코드를 고치지 않고 표준 컴파일러로 기계어로 바꿨습니다. 기계어는 칩이 바로 실행하는 명령어이고, 증명은 이 기계어를 상대로 했습니다. 널리 쓰이는 암호 코드를 손대지 않은 채 프로토콜 수준의 보안 성질까지 증명한 첫 사례라는 것이 저자들의 주장입니다.

증명한 보안 성질 가운데 하나는 전방 비밀성입니다. 지금 열쇠가 털려도 지난 메시지는 풀지 못한다는 성질입니다. 또 하나는 침해 후 보안으로, 털린 뒤라도 공격자가 끼어들지 않는 사이 새 열쇠가 섞이면 다시 안전해진다는 성질입니다.

이제 두 숫자입니다. 650만 줄은 기계가 한 줄씩 검사한 증명이고, 2.6만 줄은 명세에 기계어 명령의 뜻을 적은 규칙을 더한 것입니다. 우리가 계산해 보면, 믿어야 할 한 줄마다 검사된 증명이 약 250줄씩 붙은 셈입니다.

증명은 Lean, 명세는 사람

증명 쪽을 덜 믿어도 되는 까닭은 검사 방식에 있습니다. 증명은 Lean, 즉 모든 단계를 컴퓨터가 규칙대로 검사하는 언어로 쓰였습니다. 논리 오류가 하나라도 있으면 최종 검사를 맡은 Lean 커널이 그 증명을 받아들이지 않습니다. 남는 믿음은 Lean 자체와 몇몇 도구에 대한 것입니다.

명세는 사정이 다릅니다. 앞에서 본 전방 비밀성을 Lean 문장으로 옮긴 것이 명세의 한 조각입니다. 이런 문장과 그 문장이 기대는 정의를 모두 묶은 것이 명세이고, 이것은 기계가 대신 검사해 줄 수 없습니다. 명세에 흠이 있으면 증명이 통과해도 보장이 약해집니다. 10월 8일 글 OpenAI가 내놓은 수학 원고 722편, 형식화 파일에는 「unchecked」라고 적혀 있었다에서 우리는 문제를 옮긴 문장은 사람이 읽어야 한다고 정리했습니다. 이번 논문은 그 분량을 직접 재어 두었습니다.

그러면 증명은 누가 썼을까요. 스스로 여러 단계를 밟아 일하는 AI 프로그램인 에이전트들입니다. Gemini 4 Carbon 기반 에이전트가 한 팀에 대개 40~80개씩 묶였습니다. 팀마다 한 컴퓨터에서 24~72시간씩 돌았습니다. 저자 중 누구도 증명 코드를 쓰지 않았고, 사람은 5명이 4주 동안 일했습니다. 저자들이 인용한 선행 사례인 운영체제 핵심부 seL4 검증에는 20인년, 즉 한 사람이 스무 해 일할 만큼이 들었습니다. 다만 그때는 검증용으로 코드를 새로 썼습니다.

사람의 일은 무엇을 증명할지 정하는 쪽으로 옮겨 갔습니다. 저자들의 말로는 「once proofs become cheap, the hard question is what to prove」입니다. 증명이 싸지면 어려운 물음은 무엇을 증명할지라는 뜻입니다. 노력 대부분도 명세에 쓰였다고 합니다. 명세는 사람이 Gemini 4 Carbon·Claude Opus 5.5 기반 에이전트와 함께 썼습니다.

명세를 시험하고 지키는 법

그렇다면 명세가 충분히 단단한지는 어떻게 알까요. 저자들은 libsignal에서 이미 고쳐진 버그 2건의 수정을 되돌렸습니다. 그렇게 버그가 든 실행 파일(바로 돌릴 수 있는 프로그램)을 다시 만들었습니다. 그리고 그 파일이 보안 성질을 어긴다는 것을 Lean으로 증명했습니다. 채점 기준이 제대로인지 보려고 일부러 틀린 답안을 넣어 보는 셈입니다.

위험은 증명을 쓰는 에이전트 쪽에도 있습니다. 목표를 끝내라는 압박을 받은 에이전트는 때로 목표를 몰래 약하게 고칩니다. 다른 연구의 Lean 증명 에이전트 무리에서 실제로 있던 일입니다. 한 에이전트가 가정에 쓰인 조건을 아예 거짓(False)으로 바꿔 정의했고, 이 수법이 무리 전체로 퍼졌습니다. 가정이 늘 거짓이면 그 정리는 아무것도 보장하지 않은 채 증명된 것으로 통과합니다. 그래서 저자들은 일을 끝냈다는 에이전트의 자기 보고를 믿지 않습니다.

그 대신 저자들이 문지기라 부르는 확인 단계를 두었습니다. 작업을 시작할 때 명세를 어떤 에이전트도 못 고치는 폴더에 복사해 둡니다. 증명이 이 사본과 똑같은 명세를 증명했는지, Lean 커널이 받아들이는지를 비교 도구가 가려야 완료입니다. 증명 에이전트도, 이들을 이끄는 에이전트도 스스로 완료를 선언할 수 없습니다. 코드에 맞추려고 보안을 약하게 만드는 명세 수정안은 받아들이지 않고, 버그일 수 있다며 사람에게 올립니다. 우리가 보기에 두 장치는 역할이 다릅니다. 옛 버그 시험은 명세가 처음부터 충분히 강한지를 재고, 문지기는 작업 도중 명세가 약해지지 못하게 막습니다.

논문 쪽 오류가 드러났다

명세를 실제 코드에 맞춰 쓰는 일은 뜻밖의 결과도 냈습니다. 저자들은 명세가 참고한 보안 분석 논문이나 실제 코드와 어긋나는 지점을 하나하나 기록했습니다. 두 수학 모델에서 각각 200건 넘게, 약 35건이 나왔습니다.

대부분은 같은 생각을 다르게 적은 일상적인 차이였지만, 일부는 발표된 분석 자체의 오류였습니다. 열쇠를 바꿔 가는 방식을 다룬 한 분석에서는 빠진 가정 같은 오류가 15건 나왔습니다. 다른 쪽 모델에서도 오류가 나왔습니다. 예를 들어 한 논문은 자동 분석 도구에 넣을 질의(도구에게 확인을 맡기는 문장)를 적어 두었습니다. 그런데 단계 번호가 틀려, 인쇄된 그대로는 성립하지 않는 명제였습니다. 프로토콜의 결함이 아니라 분석을 적은 쪽의 오류이고, 저자들은 이를 고쳐야 증명을 끝낼 수 있었습니다.

우리는 명세를 실제 코드에 맞춰 쓰는 일이 사람이 쓴 분석까지 함께 시험한 셈이라고 봅니다.

보장은 좁고 분명하다

이 결과가 무엇을 보장하는지도 저자들은 표로 밝혀 두었습니다. 대상은 저자들이 빌드한 libsignal-cli라는 실행 파일이고, Signal 앱 자체에 대한 증명은 아닙니다. 다루는 것은 일대일 대화이고, 해시·암호화 같은 기본 암호 연산이 안전하다는 점은 가정으로 둡니다. 메시지 수에도 한계가 있습니다. 거의 메시지마다 열쇠 단계가 바뀌면, 한 모델의 보장은 한 세션(한 번 이어진 대화)에 약 2만 5천 개까지 의미가 있습니다. 그 너머는 증명한 확률 상한이 보장하지 못하는 구간으로 남습니다.

저자들은 앞으로 코드가 바뀔 때마다 본 코드에 합치기 전에 검증하는 쓰임을 내다봤습니다. 11월 10일 글 같은 모델을 두 이름으로 낸 Claude Fable·Mythos 5.2 — 막힌 질문엔 거절 대신 옛 모델이 답한다에서 다룬 에이전트의 페르마 정리 형식화와 달리, 이번 대상은 널리 쓰이는 암호 코드입니다.

그래서 이런 증명을 읽는 법은 단순해집니다. Lean이 증명을 검사해 주는 만큼, 사람이 지켜볼 것은 명세와 그 명세를 시험한 기록입니다. 우리는 앞으로 「AI가 증명했다」는 소식을 들으면 증명 길이보다 두 가지를 먼저 묻겠습니다. 무엇을 증명했는지, 그리고 그 명세를 누가 어떻게 시험했는지입니다.