AI Trend Research
KR

← AI 용어집

AI 용어집 · 기초 · AI 보안 · 에이전트 · 언어 모델

AlphaProof Code 알파프루프 코드

AlphaProof Code는 Google DeepMind가 공개한 다중 LLM 에이전트 프레임워크다. 사람 전문가와 AI 에이전트가 일을 나눠 맡아, 실제 소프트웨어 코드가 정해 둔 보안 속성을 지키는지 수학적으로 증명하는 형식 검증을 한다.

용어 정보
난이도
기초 · 소식을 읽을 때 자주 만나는 기술 용어
카테고리
보안·안전
추가
2026-11-11
쉽게 말하면 건물을 지을 때 설계도만 검사하는 것이 아니라 실제로 지은 건물의 벽돌 하나하나까지 설계대로인지 확인하는 것과 같다. 검사 기준은 사람이 정하고, 수많은 확인 작업은 AI 조수들이 맡는다. 다만 건물 검사는 눈으로 보는 일이지만 형식 검증은 수학적 증명이라서, 기준 자체가 잘못 정해지면 증명이 맞아도 놓치는 것이 생길 수 있다.

무엇인가

형식 검증은 코드가 결함 없이 올바르게 동작함을 수학적으로 증명하는 방법이다. 보안 보증 중에서도 가장 높은 수준으로 꼽히지만, 어렵고 사람 손이 많이 든다. AlphaProof Code는 이 작업을 연구팀처럼 나누는 다중 LLM 에이전트 프레임워크다. Google DeepMind는 2026년 11월 10일 이 프레임워크로 Signal 프로토콜의 실제 코드가 핵심 보안 속성을 충족함을 증명했다고 발표했다. Signal 프로토콜은 Signal, Google Messages 같은 메신저에서 사적인 대화를 보호하는 암호화 기술이다.

어떻게 작동하나

먼저 사람 전문가가 여러 AI 모델과 함께 Signal의 보안 목표를 형식적인 수학 명세(무엇을 증명할지 정확히 적은 문장)로 옮기고, 사람이 그 명세를 하나하나 검토한다. 다음으로 Gemini Carbon 기반 에이전트들이 Lean이라는 언어로 600만 줄이 넘는 증명을 만들었다. Lean은 컴퓨터가 증명이 맞는지 자동으로 검사해 주는 언어라서, AI가 쓴 증명이 틀리면 통과하지 못한다. 마지막으로 에이전트가 증명을 감사해 사람이 다시 봐야 할 부분을 표시했는데, 그 범위는 코드베이스의 1%였다고 한다.

AlphaProof Code 검증 흐름보안 목표 → 형식 명세; 형식 명세 → 에이전트 증명; 에이전트 증명 → Lean 자동 검사; Lean 자동 검사 → 에이전트 감사; 에이전트 감사 → 사람 재검토; 사람 재검토 → 검증 완료보안 목표Signal이 지켜야 할 성질형식 명세사람 전문가가 검토에이전트 증명Gemini CarbonLean 600만 줄+Lean 자동 검사틀린 증명은 통과 못 함에이전트 감사다시 볼 곳 표시사람 재검토코드베이스의 1%검증 완료컴파일된 코드까지
AlphaProof Code 검증 흐름 윗줄은 왼쪽에서 오른쪽으로, 아랫줄은 오른쪽에서 왼쪽으로 읽는다. 무엇을 증명할지는 사람이 정하고 검토하며, 증명을 만들고 감사하는 일은 에이전트가 맡는다.

왜 주목받나

지금까지 암호 프로토콜 검증은 대부분 설계 단계에서 멈췄다. 실제 취약점은 설계와 구현 사이의 틈에 숨어 있는 경우가 많은데, 이번에는 기기에서 실제로 실행되는 컴파일된 코드까지 검증했다. 검증한 속성에는 기기가 잠시 침해되더라도 그 전후의 메시지를 보호하는 성질이 들어 있다. Google DeepMind는 전통적으로 전문가 팀이 몇 년 걸리던 일을 4주 만에 마쳤고, 널리 쓰이는 프로토콜을 이 깊이까지 형식 검증한 것은 AI를 쓰든 안 쓰든 처음이라고 밝혔다. 이미 고쳐진 실제 버그 2개를 다시 넣은 실험에서도 두 경우 모두 안전하지 않다는 증명을 만들어 냈다고 한다.

Signal 검증 핵심 수치

600만 줄+AI가 만든 Lean 증명
4주전체 검증 기간
1%사람이 다시 본 범위
2개다시 넣은 실제 버그
Google DeepMind가 발표한 수치다. 회사가 밝힌 내용이다.

알아 둘 점

증명은 사람이 정한 명세에 대해서만 보증한다. 명세에 담기지 않은 위험까지 없다는 뜻은 아니어서, 사람이 명세를 검토하는 단계가 핵심으로 남는다. 성과와 '최초'라는 평가는 대부분 Google DeepMind의 발표에 근거하므로 외부 검토를 함께 지켜볼 필요가 있다. 회사도 더 큰 규모로 넓히려면 연구가 더 필요하다고 밝혔다. 형식 검증 산출물은 오픈소스로 공개됐고 기술 논문도 나와 있어, 다른 사람이 결과를 확인해 볼 수 있다.

예시

이 사이트에 실린 소식 'Google DeepMind AlphaProof Code 공개…AI 에이전트가 Lean 증명으로 Signal 핵심 암호화 코드를 기계어 수준까지 형식 검증'이 대표적인 사례다. 연구진은 Signal 프로토콜의 참조 구현인 libsignal을 기계어로 컴파일한 뒤, 그 코드가 명세한 보안 속성을 지키는지를 에이전트가 Lean으로 증명하게 했다. Lean이 나머지를 자동으로 검사하므로 전문가들은 에이전트가 표시한 부분만 집중해서 살폈다. Google DeepMind는 이 방식이 앞으로 의료기기 펌웨어나 전력망 소프트웨어처럼 중요한 시스템을 지키는 데 쓰일 수 있다고 내다봤다.

이 사이트에서 나온 사례

함께 보면 좋은 용어

AI 에이전트 멀티 에이전트 보안 AI 휴먼 인 더 루프 코딩 에이전트 LLM

참고