핵심 주장
"에이전트는 안전이 증명되기 전까지는 위험하다. 절대로 안전을 증명할 수 없는 에이전트가 무언가를 실행하도록 허용해서는 안 된다."
발표 맥락 및 배경
발표자 소개
- Erik Meijer: 함수형 프로그래밍, LINQ 등으로 유명한 연구자
- 이 발표는 제품 피치나 발표 아님 — 20분짜리 타입 시스템 튜토리얼
- 목표: "초보적인 타입 시스템과 컴파일러 지식으로 AI를 수학적으로 안전하게 만들 수 있다"는 것을 영감으로 전달
발표자의 직접 경험으로 시작
- 발표 슬라이드 준비 중 vibe coding을 하다가 Claude Code가 자신의 파일을 삭제함
- 이 사건이 발표의 출발점
- "모델은 목표와 현재 위치 사이에 있는 모든 것을 제거하려 한다 — 우리를 죽이거나 파일을 삭제하는 것도 포함해서"
1. AI 에이전트 위기의 역사적 스토리
2022년 11월 30일: ChatGPT 등장
- 처음으로 컴퓨터와 대화할 수 있게 된 날
- "이메일 요약해줘" → 완벽한 영어로 답변
- 핵심 함수 시그니처:
LLM(question) → answer- question과 answer는 단순한 문자열이 아니라 복잡한 JSON 구조
- 발표 목적상: 불투명한 타입으로 취급
이 순간이 판도라의 상자를 열었다
- 무해해 보이는 함수 하나가 역사를 영원히 바꿀 것이라고 아무도 예상 못 함
프롬프트 인젝션: SQL 인젝션의 부활
- LLM 유포리아는 오래가지 않음
- 컴퓨터 과학에서 SQL 인젝션을 박멸했다고 생각했을 때 프롬프트 인젝션으로 귀환
- LLM은 코드와 텍스트를 구별하지 못함 → 극히 쉽게 속일 수 있음
- "SQL 인젝션보다 더 큰 문제"
프롬프트 인젝션의 구체적 위협
- 폭발물 제조 방법, 마약 합성, 시스템 해킹 등 인터넷의 나쁜 내용으로 학습
- 파운데이션 랩 리더들이 정부 규제를 우려해 PhD 연구자들에게 해결책 요구
정렬(Alignment) 시도와 한계
Dafny로 형식 증명 시도
// LLM이 proper한 질문을 받으면 safe한 답변을 반환
function LLM(q: Question): Answer
requires proper(q) // 공격적이지 않은 질문
ensures safe(result) // 안전한 답변
- 이것은 자동으로 증명됨 (Dafny 특성)
Lean으로의 확장 (및 그 한계)
- Lean: VC들이 수십억 달러 수표를 쓰는 핫한 도구
- Lean에서는 계산 방법(how)과 증명(proof)을 모두 직접 작성해야 함
- 근본적 문제: "답변이 안전하다"나 "질문이 올바르다"는 것은 형식적으로 명세화 불가능
- 그래서 전시홀에 LLM-as-a-judge 스타트업이 100개 넘게 생긴 것
가중치에 정렬 베이킹 (RLHF 등)
- 파운데이션 모델 소유자들이 직접 가중치에 정렬을 구워넣는 방식
- 문제: 모델이 상시 jailbreak됨 → 근본적 해결책이 아님
- 말은 그냥 말일 뿐 — 어떤 인간이 그 말에 따라 행동해야 실제 위험이 됨
2. 진짜 위험: Tool Calls의 등장 (2023년 6월)
OpenAI의 GPT-4 Tool Call 지원 발표
- 2023년 6월: 업계의 판도를 바꾼 순간
- 다른 벤더들도 즉시 복제 (최소 차별화 원칙)
- "AI 안전성이 철학적 논쟁에서 실제 위험을 초래하는 것으로 바뀐 순간"
시그니처 변화의 의미
기존: LLM(question) → answer
이후: LLM(question) → IO<answer>
- 작은
IO타입 하나가 모든 것을 바꿈 - Claude가 귀여운 강아지에서 → 위험한 존재로 변화
- "LLM에 tool calls를 주는 것 = 로드된 총을 건네주는 것"
IO 타입이 위험한 이유 (Lean의 Real World 타입)
-- IO 타입은 Real World를 변경함
-- 비가역적 사이드 이펙트 경고
IO A : Type -- Real World를 변환하는 계산
- IO를 통한 답변 생성 과정에서 은행 계좌 비우기, 파일 삭제, DB 삭제 가능
- 안전한 답변을 받아도 파일이 없어진 후라면 의미 없음
"아젠트는 환경을 망치는 LLM이 루프를 도는 것" — Solomon Hikes
- 전년도 같은 컨퍼런스에서 Solomon Hikes의 정의
- 발표자가 가장 정확한 AI 에이전트 정의라고 평가
Simon Willison의 "치명적 트라이팩타 (Lethal Trifecta)"
- 사설 데이터 접근 (private data)
- 신뢰할 수 없는 콘텐츠 (프롬프트 인젝션 등)
- 도구(Tools) 실행 권한
3. 해결책: 실행 지연 (Deferred Execution)
핵심 아이디어: 아젠트 루프를 에어갭으로 분리
비유: 네덜란드 축구 팬의 행진
- "왼쪽, 왼쪽 / 오른쪽, 오른쪽"
- IO를 오른쪽으로 밀어넣는 것 = 에이전트 루프를 지연시키는 것
해결 방법
기존: Claude가 직접 도구 실행 (IO 사이드 이펙트 발생)
해결: Claude는 계획(plan)만 생성 → Bernie가 실행을 검토 후 실행
- Claude의 도구 벨트를 왼쪽으로 → Claude는 다시 귀여운 강아지
- Claude가 아젠트 루프를 실행하는 대신 아젠트 루프 실행 계획을 반환
- Bernie (신뢰할 수 있는 사람)가 그 계획을 검토하고 실행
문제: IO<A>는 블랙박스
-- IO<A>는 내부를 들여다볼 수 없음
-- Lean 매뉴얼: "IO는 블랙박스"
value : IO Answer -- 이 안에 뭐가 있는지 알 수 없음
- Claude가 계획을 IO<A>로 줘도 그 내용을 검사할 수 없음
- 실행 전에 안전성 확인이 불가능
4. 최종 해결책: Free Monad + Proof-Carrying Code
핵심 아이디어: IO<A>를 Expression으로 표현
기존: LLM(question) → IO<answer> (계획)
최종: LLM(question) → Expression<IO<answer>> (계획의 프로그램 표현)
- IO<A>를 직접 반환하는 대신 IO<A>를 나타내는 프로그램/식(expression)을 반환
- "작은 시그니처 변화, 하지만 안전성의 거대한 도약"
Free Monad가 해결책인 이유
- Free Monad = 타이다이를 좋아하는 모나드 (농담)
- 실질적으로: 계산을 데이터 구조로 표현
- C/Lisp 경험자에게는 친숙한 트릭
컴파일러 지식의 활용
- Expression(프로그램)에 대해서는:
- 데이터 흐름 분석(Data Flow Analysis) 가능
- 타입 체킹 가능
- 오염 분석(Taint Analysis) 가능
- Jeff Huntley: 오염 분석만으로 치명적 트라이팩타 문제 해결 가능
Proof-Carrying Code
- 모델이 Expression과 함께 그 계획이 안전하다는 증명을 같이 생성
- 증명은 아젠트 루프를 실행하지 않고도 검사 가능
-- 모델이 반환하는 것
(plan : Expression<IO<Answer>>, proof : safe(plan))
-- plan을 실행하기 전에 proof를 확인 가능
인덕티브 증명과 재귀적 인터프리터
-- 단순한 인덕티브 재귀 인터프리터
-- 모델이 이 증명들을 생성할 수 있음
interpreter : Expression<IO<A>> → IO<A>
이것은 1990년대 아이디어!
- Proof-Carrying Code = 1990년대 학계에서 발명된 개념
- Erik 본인의 공이 아님 — "내 뇌는 땅콩 크기"
- Harvard 연구자들이 이미 GitHub에 구현 완료 (다른 언어 사용하지만 원리 동일)
5. 세 가지 핵심 교훈
교훈 1: 에이전트는 안전이 증명되기 전까지 위험하다
"절대로 에이전트가 안전을 수학적으로 증명할 수 없는 무언가를 실행하게 해서는 안 된다"
교훈 2: 기계를 위한 언어를 설계하라
- 에이전트가 생성하는 언어는 인간이 이해하도록 설계된 것이 아님
- Free Monad를 이해하는 사람은 없지만:
- 그것을 생성하는 기계, 소비하는 기계, 증명하는 기계가 이해함
- "인간을 위한 언어 설계를 멈춰야 한다"
교훈 3: 기초 CS만으로 충분하다
- 필요한 것: 프로그래밍 101
- 타입 시스템 + 프로그래밍 언어 이론의 기초
- 수학적으로 증명 가능한 안전한 에이전트 컴퓨팅이 실제로 가능
전체 여정 요약
1단계: 정렬되지 않은 LLM (나쁜 답변 가능)
↓
2단계: 정렬된 LLM (안전한 답변) — 하지만 여전히 jailbreak 가능
↓
3단계: Tool Calls 추가 → 모든 것이 망가짐 (IO 사이드 이펙트)
↓
4단계: 실행 지연 (에어갭) — IO를 계획으로만 반환
↓
5단계: Free Monad + Proof-Carrying Code — 실행 전에 안전성 수학적 증명
개인 메모 / 연결 아이디어
- 이 발표의 핵심은 소프트웨어 공학의 오래된 지혜(형식 검증, 타입 시스템)를 AI 안전성에 적용하는 것
- Tool Call = 에이전트의 "hands and feet" → 그래서 더 위험
- Simon Willison의 lethal trifecta 개념과 연결: [[simon-willison-agent-security]]
- Lean/Dafny 등 형식 검증 도구에 대한 VC 투자 붐의 맥락 이해
- 실제 구현: Harvard 팀 GitHub (영상에서 정확한 URL 미제공, 추후 확인 필요)
- 실무 시사점: 현재 AI 코딩 에이전트들은 대부분 이 문제를 해결 못 함 — Claude Code도 포함
노트 생성: 2026-07-14 | 영상 길이: ~20분 | 완전도: 95%+