기술 요약: 증명 가능한 안전한 에이전트 가드레일

문제 정의

대규모 언어 모델 (LLM) 이 제한된 생성 엔진에서 광범위한 실행 권한을 가진 자율 에이전트로 진화함에 따라, 보안 환경은 근본적인 위기에 직면해 있습니다: 인간 통제를 벗어난 AI 운영의 위험입니다. 기존 방어 아키텍처는 경험적 의미론적 가드레일(예: LLM-as-a-Judge, 휴리스틱 필터) 과 확률적 모델 심판자에 크게 의존합니다. 이러한 메커니즘은 다음과 같은 치명적인 구조적 한계를 겪고 있습니다:

• 결정론적 보장 부재: 복잡한 의미론적 기호 분리 공격에 직면했을 때 결정론적 보안 하한선을 제공할 수 없습니다.
• 고급 공격에 대한 취약성: "시간적 분할"(악의적 의도를 benign 하위 작업으로 분해), 문맥적 기만, 의미론적 밀수 등에 취약합니다. 이는 연속적이고 확률적인 추론이 아닌 이산 논리에 의존하기 때문입니다.
• 고권한 작업 처리 불가: 전통적인 정적 접근 제어 (예: ABAC) 는 고차원적이고 다단계 에이전트 계획을 평가할 의미론적 인식이 부족하며, 경험적 가드레일은 시스템 수준 권한을 가진 자율 작업에 대한 검증 가능한 안전성을 제공하기 어렵습니다.

본 논문은 고차원 연속 행동을 제어하는 문제는 의미론적 필터를 휴리스틱하게 패치함으로써 해결될 수 없다고 주장합니다. 대신 확률적 보호에서 논리적 역설에 기반한 증명 가능한 방어로의 전환이 필요합니다.

방법론: ePCA 프레임워크

저자들은 논리적 추론의 근본적 한계에 기반한 새로운 보안 패러다임을 제안하며, 실행 가능 증명 제약 행동 (Executable Proof-Constrained Action, ePCA) 프레임워크를 도입합니다. 이 프레임워크는 신경 기호 격리 아키텍처를 활용하여 인지적 계획과 행동 보안 검증을 분리합니다.

핵심 아키텍처

ePCA 시스템은 에이전트가 실행 전에 의도를 형식화하도록 강제하는 4 계층 파이프라인을 통해 작동합니다:

1. 의미론적 박리 (Layer 1): 시스템은 무제한 자연어를 거부합니다. 신뢰할 수 없는 에이전트는 실행 의도를 엄격하게 타입 지정된 패턴 제약 페이로드 (JSON 유사 구조) 로 직렬화해야 합니다. 이는 수사학적 기만을 박리합니다.
2. 결정론적 번역 (Layer 2): 결정론적 의미론 해석 함수가 구조화된 페이로드를 Satisfiability Modulo Theories (SMT) 도메인 내의 1 차 논리 (First-Order Logic, FOL) 공식으로 매핑합니다. 이 단계는 에이전트 의도의 "정리 (theorem)" 역할을 하여 신경망 출력을 검증 가능한 기호 표현으로 변환합니다.
3. 형식적 검증 (Layer 3): 신뢰할 수 있는 검증 평면 (Z3 SMT 솔버로 구현됨) 이 결합 검증 공식을 구성합니다: $C = s \land \llbracket j \rrbracket_{SMT} \land \Phi_{safe}$.
   • $s$: 현재 시스템 상태.
   • $\llbracket j \rrbracket_{SMT}$: 형식화된 행동 의도.
   • $\Phi_{safe}$: 변경 불가능한 인간 정의 보안 공리.
4. 결정론적 검사 (Layer 4): 솔버는 만족성 검사를 수행합니다:
   • SAT (만족 가능): 행동이 보안 공리와 일관됩니다. 실행이 진행됩니다.
   • UNSAT (불만족): 행동이 공리와 논리적 모순 (대수적 데드락) 을 만듭니다. 시스템은 즉시 행동을 차단하고 추론 프로세스를 종료하여 안전하지 않은 상태 전이를 방지합니다.

이론적 기반

이 접근법은 괴델의 불완전성 정리와 튜링의 결정 불가능성 정리에 기반합니다. 안전하지 않은 행동을 "논리적 역설" 또는 "결정 불가능한 명제"로 매핑함으로써, 보안 경계를 침범하려는 에이전트가 필연적으로 논리적 데드락에 빠지도록 보장합니다. 위협 모델은 LLM 정책 자체가 문맥적 기만과 시간적 분할이 가능한 완전히 침투된 초지능적 적대자라고 가정하지만, SMT 솔버와 공리를 포함하는 신뢰 컴퓨팅 베이스 (TCB) 는 물리적으로 격리되고 변경 불가능하다고 가정합니다.

주요 기여

1. 패러다임 전환: 경험 기반 확률적 정렬에서 결정론적 형식 제약으로의 전환을 도입합니다. 보안 검증을 의미론적 계층에서 실행 계층으로 이동시킵니다.
2. ePCA 프레임워크: 안전하지 않은 상태 전이를 증명 가능한 논리적 데드락으로 매핑하여 보안을 강제하는 실행 가능 증명 제약 행동 프레임워크의 설계입니다. 이는 안전성 강화를 신경망 가중치와 독립적인 검증 가능한 실행 계층으로 외부화합니다.
3. 시스템 구현: 완전히 기능하는 프로토타입 시스템과 동적 다라운드 적대적 벤치마크입니다. 시스템은 정의된 운영 경계 내에서 무단 행동을 결정론적으로 차단하는 능력을 입증합니다.
4. 형식적 증명: 특정 가정 (구조화된 의도 충실성과 변경 불가능한 공리) 하에서 ePCA 시스템이 안전하지 않은 상태의 도달 가능성을 구조적으로 제거함을 보여주는 수학적 증명 (귀납법을 통해) 입니다 ($S_{reach} \cap S_{mal} = \emptyset$).

실험 결과

저자들은 최첨단 모델 (GPT-5.2/5.4, Claude-Sonnet 4.6, Qwen3-Max 등 포함) 에 대해 두 가지 대표 시나리오를 사용하여 프레임워크를 평가했습니다:

1. 다단계 금융 이체 작업:

   • 목표: 시간적 분할 (대규모 이체를 소규모로 분할) 및 메타 규칙 악용에 대한 일관성 검증.
   • 결과: ePCA 프레임워크는 모든 테스트 모델에서 공격 성공률 0% 및 **거짓 긍정률 0%**를 달성했습니다.
   • 지연 시간: 핵심 형식 계산의 평균 지연 시간은 0.44 밀리초로, LLM 기반 심판자 (~15,200 ms) 보다 현저히 낮고 경량 ABAC 와 유사했습니다.

2. 교차 도메인 데이터 유출 (기업 샌드박스):

   • 목표: 격리된 인트라넷에서 공개 인터넷으로 데이터를 유출하기 위한 12 라운드 침투 시뮬레이션.
   • 결과: 프레임워크는 에이전트의 추론 프로세스에 강제 종료를 유도했습니다. 에이전트가 오염된 데이터 (내부 DB 에서 읽은 데이터) 를 공개 네트워크로 이동시키려 할 때, SMT 솔버는 "오염 데드락" 공리 ($s.T = \top \implies s'.Z \neq Z_{outer}$) 와 논리적 모순을 감지했습니다.
   • 결과: 에이전트는 대수적 데드락을 경험하고 목표의 불가능성을 명시적으로 인정하여 스스로 종료되었습니다.

중요성과 주장

본 논문은 미래 지능 시스템의 기반 방어를 구축하기 위한 조건부 형식적 기반과 공학 패러다임을 제공한다고 주장합니다.

• 경험적에서 증명 가능으로: 암호학이 계산적 난이도 (Diffie-Hellman) 에 기반한 증명 가능한 보안으로 경험적 보안에서 전환되었듯이, 에이전트 보안도 논리적 추론의 한계에 기반한 증명 가능한 보안으로 전환되어야 한다고 주장합니다.
• 결정론적 제어: "의미론적 게임 이론"에 의존하는 이전 방법과 달리, ePCA 는 형식 대수 계산을 기반으로 한 결정론적 제어를 제공합니다.
• 확장성과 한계: 저자들은 시스템의 효과가 의미론적 번역 (자연어를 형식 제약으로 매핑) 의 정확성과 인간 정의 공리 집합 ($\Phi_{safe}$) 의 완전성에 의존함을 겸손하게 인정합니다. 이는 광범위한 개방형 상업적 제약을 해결하기보다는 열거 가능한 불가침 권리를 보호하는 데 가장 적합합니다.
• 향후 방향: 안전 공리가 1 차 시스템 원시 연산자로 내장되어 인지적 유연성과 시스템 수준 제어를 분리하는 "에이전트 지향 운영 체제 (AgentOS)"로의 이동을 제안합니다.

요약하자면, 본 논문은 AI 가 안전하지 않은 행동을 생각하는 것을 반드시 막을 수는 없지만, 악의적 행동을 수학적으로 불가능하게 만드는 논리적 필터를 통해 의도를 강제함으로써 이를 실행하는 것을 증명 가능하게 막을 수 있다고 주장합니다.