AI 안전성을 수학적으로 증명한다 - 타입 시스템과 도구 호출의 위험, 에릭 마이어 강연

핵심 메시지

• LLM은 코드와 텍스트를 구분하지 않아 속이기 쉬우며, 프롬프트 인젝션은 과거 SQL 인젝션보다 더 큰 문제다.
• 도구 호출이 더해지면서 AI 안전은 철학적 논쟁에서 실제 피해를 낳는 문제로 바뀌었다.
• 부작용(IO)을 수반하는 에이전틱 루프는 '안전한 답'을 주면서도 그 과정에서 파일을 지우거나 계좌를 비울 수 있다.
• 해법은 계산을 실행하지 않고도 그 계획이 안전함을 증명할 수 있는 프로그램 표현으로 다루는 것이다.
• 이 모든 것이 Lean·Dafne 같은 기초적인 타입 시스템과 컴파일러 지식만으로 가능하다.

쉽게 이해하기

강연자는 이 발표가 제품 홍보가 아니라, 기초적인 타입 시스템과 컴파일러 지식으로 AI를 증명 가능하게 안전하게 만드는 방법을 다루는 튜토리얼임을 분명히 한다. 화려한 신기술이 아니라 오래된 프로그래밍 언어 이론을 재조명하는 자리다.

먼저 문제를 진단한다. LLM은 코드와 텍스트를 구분하지 않기 때문에 속이기 쉽고, 프롬프트 인젝션은 SQL 인젝션이 그랬던 것보다 더 심각한 위협이라는 것이다. 게다가 인터넷 전체로 학습한 모델은 폭탄 제조나 해킹 같은 유해 지식도 담고 있어 규제 우려를 키웠다.

핵심 통찰은 도구 호출에 있다. 도구 호출이 붙는 순간 LLM의 시그니처에 IO가 들어오고, 모델은 답을 계산하는 동안 부작용을 일으킨다. 강연자는 이를 '타입에게는 작은 한 걸음이지만 혼돈에게는 거대한 도약'이라 표현하며, 안전한 답을 돌려줘도 그 사이 내 파일이 사라졌다면 무슨 소용이냐고 반문한다.

해결의 실마리는 답을 직접 계산하는 대신, 답을 만드는 '계획'을 IO 타입의 값으로 생성하고 그 계획이 안전하다는 증명을 함께 만드는 것이다. 중요한 점은 에이전틱 루프를 실제로 돌리지 않고도 그 증명을 얻을 수 있다는 데 있다.

마지막 단계에서는 계획을 단순한 값이 아니라 계산을 표현하는 프로그램(표현식)으로 다룬다. 모델이 실행 결과가 아니라 계산을 나타내는 프로그램을 반환하게 함으로써, 실행 전에 안전성을 검증할 수 있다. 하버드 등의 연구자들이 유사한 아이디어를 GitHub에 구현해 두었다고 소개한다.

주요 인사이트

• 프롬프트 인젝션의 근본 원인은 LLM이 코드와 데이터를 구분하지 않는다는 데 있다.
• 도구 호출은 모델에 '손과 입'을 쥐여주는 것과 같아, 안전 문제를 이론에서 실제 피해로 끌어내린다.
• 부작용을 IO 타입으로 드러내면, 답을 신뢰하기 전에 그 계산이 안전한지 따질 근거가 생긴다.
• 실행하지 않고도 계획의 안전성을 증명할 수 있다는 점이 형식적 접근의 핵심 이점이다.
• 최첨단 도구가 아니라 Lean·Dafne 같은 기초 타입 시스템만으로도 증명 가능한 안전성에 도달할 수 있다.

자주 묻는 질문

관련 AI 소식