💻 computer science

Cryptographic certificates of validity for trustworthy AI

이 논문은 에이전트의 행동이 형식적으로 명시된 정책을 준수함을 수학적으로 증명하는 간결한 암호화 인증서를 생성함으로써, 재실행이나 에이전트에 대한 신뢰 없이도 독립적인 검증을 가능하게 하는 신뢰할 수 있는 에이전트형 AI를 위한 프레임워크를 제안한다.

원저자: Murdoch J. Gabbay

게시일 2026-06-24

📖 4 분 읽기☕ 가벼운 읽기

CC BY 4.0

원저자: Murdoch J. Gabbay

원본 논문은 CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/) 라이선스로 제공됩니다. ✨ 이것은 아래 논문에 대한 AI 생성 설명입니다. 저자가 작성하거나 승인한 것이 아닙니다. 기술적 정확성을 위해서는 원본 논문을 참조하세요. 전체 면책 조항 읽기

핵심 아이디어: 사람이 아닌 증명을 믿으세요

당신이 당신을 대신해 비행기를 예약할 로봇을 고용한다고 상상해 보세요. 과거에는 우리는 로봇을 만든 곳이 어디인지 알거나, "나는 X 회사에서 보낸 메시지입니다"라는 디지털 서명이 있기 때문에 로봇(또는 AI 에이전트)을 신뢰했습니다.

하지만 만약 그 로봇에 버그가 있거나, 혹은 "비잔틴(Byzantine)" 로봇(로봇이 이상하게 행동하거나 악의적으로 행동할 수 있다는 것을 뜻하는 멋진 용어입니다)이라면 어떻게 될까요? 서명은 메시지를 보낸 이가 '누구'인지는 증명하지만, 그 메시지가 '정확한지' 또는 '안전한지'까지는 증명하지 못합니다.

머독 개비(Murdoch Gabbay)의 논문은 AI를 신뢰하는 새로운 방법을 제안합니다. 로봇의 정체를 신뢰하는 대신, 로봇의 행동이 규칙을 따랐음을 증명하는 **암호학적 인증서(cryptographic certificate)**를 신뢰하는 것입니다.

이렇게 생각해보세요:

과거 방식: 당신은 요리사가 특정 모자를 쓰고 자격증을 가졌기 때문에 그를 신뢰합니다. 그리고 그가 수프에 독을 넣지 않았기를 바랍니다.
새로운 방식: 요리사가 당신에게 봉인된, 깨뜨릴 수 없는 영수증을 건넵니다. 이 영수증은 수학적으로 수프가 적절한 온도에서 조리되었고, 올바른 재료가 들어갔으며, 독이 첨가되지 않았음을 증명합니다. 당신은 요리사의 이름을 알 필요도, 요리하는 과정을 지켜볼 필요도 없습니다. 그저 영수증만 확인하면 됩니다.

작동 원리: "마법의 번역기"

이 논문은 이러한 영수증을 만드는 3단계 과정을 설명합니다.

1. 규칙 작성 ( "법" )

먼저, 우리가 AI가 따르기를 원하는 규칙(예: "500달러 이상 쓰지 마라" 또는 "여행 경보가 발령된 국가로만 비행기를 예약하라")을 정하고, 이를 **논리(logic)**라고 불리는 엄격한 수학적 언어로 작성합니다.

비유: 컴퓨터가 "아마도"나 "내 생각에는" 같은 모호함 없이 완벽하게 이해할 수 있는 언어로 보드게임의 규칙을 작성한다고 상상해 보세요.

2. 번역 ( "컴파일러" )

다음으로, 특수한 도구(컴파일러)를 사용하여 이러한 논리적 규칙을 수학적 퍼즐로 번역합니다.

마법 같은 점: 이 논문은 "참(True)"은 숫자 0이 되고, "거짓(False)"은 양수가 되는 기발한 트릭을 설명합니다.
비유: 저울을 상상해 보세요. 만약 AI가 규칙을 따랐다면 저울은 0에서 완벽하게 균형을 이룹니다. 만약 AI가 규칙을 어겼다면 저울은 기울어져서 무거운 양수를 나타낼 것입니다. 목표는 저울이 0이 되도록 만드는 것을 증명하는 것입니다.

3. 인증서 ( "영수증" )

AI(또는 조력자)는 수학 퍼즐을 풀고 아주 작은 암호학적 **증명(proof)**을 생성합니다. 이 증명은 "나는 저울이 0에서 균형을 이루게 만드는 비밀스러운 해답을 가지고 있다"라고 말합니다.

멋진 점: 검증자(AI를 확인하는 사람)는 이 작은 증명을 보고 규칙이 지켜졌음을 즉시 알 수 있습니다. 검증자는 AI의 사적인 생각을 볼 필요도 없고, 전체 계산을 다시 실행할 필요도 없으며, AI를 믿을 필요도 없습니다. 그저 수학을 확인할 뿐입니다.

구체적인 예시: 2의 거듭제곱의 힘

논문은 이 과정이 어떻게 작동하는지 보여주기 위해 $2^2$ ($2 $의$ 2$승)을 계산하는 간단한 예를 사용합니다.

AI가 "나는 $2^2 = 4$ 를 계산했다"라고 주장한다고 가정해 봅시다.
이것이 거짓이 아님을 증명하기 위해, AI는 단순히 "4"라고 말하는 것이 아니라 유도 트리(derivation tree)(단계별 이력)를 제공합니다.

1단계: $2^0 = 1$ (시작점).
2단계: $2^1 = 2$ (1단계를 바탕으로 함).
3단계: $2^2 = 4$ (2단계를 바탕으로 함).

암호학적 인증서는 이 단계들이 올바르게 연결되어 있음을 증명합니다. 만약 AI가 단계를 건너뛰거나 숫자를 바꾸려고 시도한다면, 수학 퍼즐은 실패할 것이고 인증서는 유효하지 않게 됩니다.

이것이 AI 에이전트에게 중요한 이유

이 논문은 AI 에이전트가 실제 행동(비행기 예약, 송장 승인, 코드 배포 등)을 하기 시작함에 따라, 사후에 로그를 확인하는 것이 아니라 행동이 일어나기 전에 검증할 방법이 필요하다고 주장합니다.

재실행 불필요: 인증서를 확인하는 것은 빠릅니다. AI의 작업을 다시 수행할 필요가 없습니다.
개인정보 보호: "영지식(Zero-Knowledge)" 기능을 사용하여, AI는 자신의 개인 데이터(예: 신용카드 번호나 비밀 전략)를 공개하지 않고도 규칙을 준수했음을 증명할 수 있습니다.
맹목적 신뢰 방지: 당신은 AI 개발자를 믿을 필요가 없습니다. 오직 수학만을 믿으면 됩니다.

이 논문이 하지 않는 것 (중요한 한계)

저자는 이 기술이 할 수 없는 것에 대해 매우 주의 깊게 명시하고 있습니다:

규칙을 대신 써주지 않습니다. 인증서는 당신이 준 규칙을 AI가 잘 따랐음을 증명할 뿐입니다. 만약 당신이 나쁜 규칙(예: "모든 돈을 다 써버려라")을 썼다면, 인증서는 AI가 그 나쁜 규칙을 완벽하게 따랐음을 증명할 것입니다.
안전을 보장하지 않습니다. 이것은 오직 특정 수학적 조건이 충족되었음을 보장할 뿐입니다. 그 조건 자체가 현명하거나, 윤리적이거나, 안전하다는 것을 증명하는 것은 아닙니다.
인간의 감독을 대체하지 않습니다. 인간은 여전히 규칙이 무엇이어야 하는지 결정하고 시스템을 감사해야 합니다.

요약

이 논문은 AI를 위한 "증명을 동반한 행동(Proof-Carrying Action)" 시스템을 제안합니다. 운전자가 운전할 자격이 있음을 증명하기 위해 면허증을 소지하는 것처럼, AI 에이전트는 자신의 행동이 올바르다는 것을 증명하기 위해 암호학적 인증서를 지니게 됩니다.

이는 형식 논리(Formal Logic)(규칙)와 암호학(Cryptography)(증명) 사이의 간극을 메워주며, 우리가 AI를 믿거나 그 내부의 사적인 데이터를 볼 필요 없이 AI가 올바르게 행동하고 있는지 검증할 수 있게 해줍니다. 이것은 다음과 같이 말하는 방법입니다: "당신을 믿지는 않지만, 당신이 방금 건넨 수학은 믿습니다."

제공된 텍스트를 바탕으로 한 머독 J. 개비(Murdoch J. Gabbay)의 논문 "신뢰할 수 있는 AI를 위한 암호학적 유효성 증명(Cryptographic certificates of validity for trustworthy AI)"에 대한 상세한 기술 요약입니다.

문제 정의

AI 시스템이 권고(recommendation)를 생성하는 단계에서 자율적 실행(예: 항공권 예약, 송장 승인, 코드 배포)을 수행하는 단계로 전환됨에 따라, 전통적인 보증 메커니즘은 불충분해지고 있습니다. 암호학적 서명은 메시지의 *출처(origin)*는 인증하지만, 특정 동작이 사전에 정해진 정확성, 안전성 또는 준수 조건을 충족하는지는 증명할 수 없습니다. 마찬가지로, 사후 로깅(retrospective logging)은 정책 위반이 발생하기 전에 이를 방지할 수 없습니다. 본 논문은 검증자가 에이전트의 내부 구현을 신뢰하거나 계산을 재실행할 필요 없이, 에이전트의 동작이 합의된 공식 정책을 만족한다는 것을 독립적으로 검증 가능한 증거를 제공하는 메커니즘의 필요성을 다룹니다.

방법론

본 논문은 형식 논리(formal logic)와 간결한 암호학적 증명(succinct cryptographic proofs)을 결합하여 **암호학적 유효성 증명(cryptographic certificates of validity)**을 생성하기 위한 프레임워크를 제안합니다. 이 방법론은 다음과 같은 3단계 파이프라인을 따릅니다.

형식적 명세(Formal Specification): 관련 정책 또는 정확성 조건을 특정 1차 논리의 술어(predicate)로 표현합니다.
산술화(Arithmetisation): 이 술어를 다항식 제약 조건(polynomial constraints)에 대한 위트니스 확인(witness-checking) 문제로 컴파일합니다. 핵심적인 수학적 기여는 1차 논리의 타당성을 다음과 같은 다항식 제약 조건에 대한 판단으로 변환하는 것입니다.
- 타당성(truth/validity)은 값 0으로 표현됩니다.
- 거짓(falsehood/invalidity)은 양수(strictly positive) 값으로 표현됩니다.
- 논리 연산자는 대수적 연산으로 매핑됩니다:
  - 등식( $t=t'$ )은 $(t-t')^2$ 으로 매핑됩니다.
  - 논리곱( $\phi \land \psi$ )은 합 $[\phi] + [\psi]$ 로 매핑됩니다.
  - 논리합( $\phi \lor \psi$ )은 곱 $[\phi] \times [\psi]$ 로 매핑됩니다.
  - 범위에 대한 전칭 양화(universal quantification)는 해당 범위에 대한 합산(summation)으로 매핑됩니다.
- 재귀 및 귀납적 정의(예: 지수 연산)는 위트니스 데이터(witness data)를 행렬로 구조화함으로써 인코딩됩니다. 이때 열(column)은 유도 단계(derivation steps)를 나타내며, 전용 행에 포함된 포인터(pointer)가 재귀적 구조가 올바르게 형성되었음을 보장합니다.
암호학적 인증(Cryptographic Certification): 에이전트(또는 관련 증명자)는 정책으로부터 도출된 다항식 제약 조건이 특정 동작 데이터에 의해 충족됨을 입증하는 간결한 암호학적 증명(잠재적으로 영지식 증명)을 생성합니다.

검증 과정에서 검증자는 공개 키와 파라미터를 사용하여 증명을 확인합니다. 증명이 검증되면, 시스템은 검증자가 에이전트의 개인적인 위트니스 데이터를 조사하거나 계산을 다시 실행하지 않고도 해당 동작이 형식적 술어를 만족한다고 수용합니다.

주요 기여

수학적 변환: 본 논문은 1차 논리의 타당성을 다항식 제약 조건으로 압축하여 응용 분야에 구애받지 않는 산술화 방법을 제공합니다(정의 2.3–2.7, 정리 2.9). 또한 복잡한 논리 구조(재귀 및 귀납적 유도를 포함)를 암호학적 백엔드에 적합한 대수적 관계로 인코딩하는 방법을 보여줍니다.
증명을 동반한 에이전트 동작(Proof-Carrying Agent Actions): 본 논문은 에이전트의 동작을 특정한 암호학적 의미에서의 "증명 전달(proof-carrying)"로 개념화합니다. 소스 코드를 조사해야 하는 경우가 많은 기존의 증명 전달 코드(Proof-Carrying Code, PCC)와 달리, 이 방식은 신뢰할 수 없는 블랙박스 형태의 에이전트가 준수 여부에 대한 간결한 증거를 제공할 수 있게 합니다.
기존 기술과의 통합: 이 프레임워크는 기존의 간결한 논증 시스템(예: SNARC, Cairo 또는 RISC0와 같은 zkVM) 및 다항식 약속 스킴(예: Halo2, Zinc)과 상호작용하도록 설계되었습니다. 이는 제안된 논리를 이러한 암호학적 프리미티브로 컴파일되는 고수준 명세 계층으로 위치시킵니다.
런타임 검증과의 차별점: 이 접근 방식은 사후적인 트레이스(trace)를 제공하는 런타임 검증과 달리 선제적이고 간결한 인증서를 제공하며, 에이전트의 내부 설계를 공개하거나 신뢰할 필요가 없는 표준 PCC와는 다릅니다.

결과 및 예시

본 논문은 경험적 벤치마크 대신 이론적 예시를 통해 접근 방식을 검증합니다.

기초 논리: 참/거짓 값, 등식, 논리곱, 논리합, 그리고 범위 체크가 어떻게 0을 평가하는 다항식으로 인코딩되는지 보여줍니다.
재귀적 계산: 지수 연산( $a^b$ )의 귀납적 정의를 인코딩하는 상세한 예시를 제시합니다. 논문은 위트니스 데이터 행렬이 어떻게 유도 트리(derivation tree)를 인코딩하는지 보여주며, 여기서 1~3행은 입력/출력 샘플을 저장하고 4행은 이전 단계에 대한 포인터를 저장합니다. 유효성 술어는 이 포인터들이 올-폼(well-formed) 재귀 구조를 형성하는지 확인합니다.
강건성(Robustness): 논문은 행렬이 올바른 입출력 값을 포함하더라도 "증명 전달" 구조(포인터)가 누락되거나 잘못된 경우 유효성 술어를 통과하지 못할 수 있음을 언급하며, 인증서가 결과 자체뿐만 아니라 그 결과의 유도 과정을 검증함을 보여줍니다.

의의 및 범위

본 논문은 이 작업을 형식적 코드 검증과 암호학적 인증 사이의 "중간 지점"으로 위치시킵니다. 주요 의의는 자율적 AI 에이전트 시스템을 위해 증명을 전달하는 코드(proof-carrying code)의 암호학적 아날로그를 제공한다는 데 있습니다.

저자는 제안된 내용의 한계와 범위를 명시적으로 밝힙니다.

범위: 수학적 아키텍처는 검증 가능한 증거를 제공해야 하는 모든 도메인에 일반적이고 적용 가능합니다. AI 에이전트에 대한 구체적인 적용은 자율적 행동이 선제적 보증에 대한 시급한 필요성을 창출하기 때문에 선택되었습니다.
한계: 유효성 증명은 형식적 명세가 충족되었음을 증명합니다. 이는 형식적 명세 자체가 "올바른" 것(즉, 안전, 법률 또는 윤리적 요구 사항을 정확하게 포착하는 것)임을 증명하는 것은 아닙니다. 본 논문은 형식적 술어와 현실 세계의 안전 사이의 간극을 메우기 위해서는 수학이나 암호학만으로는 해결할 수 없는 거버넌스, 감사 및 리스크 관리 프로세스(NIST 프레임워크 참조)가 필요함을 강조합니다.
향러 연구: 본 논문은 컴파일러 설계, 증명 비용 벤치마킹, 정책 저작 및 감사를 위한 거버넌스 확립을 포함한 실질적인 구현 세부 사항의 필요성을 식별합니다.

요약하자면, 본 논문은 AI 에이전트의 동작에 간결하고 암호학적으로 검증 가능한 정책 준수 증명을 부착하기 위한 이론적, 수학적 토대를 제안하며, 신뢰 모델을 "출처를 신뢰하라"에서 "증거를 신뢰하라"로 전환합니다.