Autoformalization of Agent Instructions into Policy-as-Code

기술 요약: 에이전트 지침의 코드로서의 정책(Policy-as-Code)으로의 자동 정형화

문제 정의
고위험 도메인(예: 의료)에서 자율형 대규모 언어 모델(LLM) 에이전트를 배포하는 것은 중대한 보안 트레이드오프를 수반한다. 에이전트는 복잡한 과업을 수행하기 위해 높은 권한을 필요로 하지만, 이러한 권한은 프롬프트 인젝션과 같은 적대적 기법에 대한 공격 표면을 확장시킨다. 현재 업계 관행은 Llama Guard와 같은 미세 조정된 안전 분류기나 프롬프트 기반 스티어링과 같은 확률적 가드레일에 크게 의존하고 있다. 이러한 방법들은 어느 정도 유용성을 제공하지만, 결정론적 강제가 필요한 보안 중심 애플리케이션에서는 형식적 보증(formal guarantees)이 부족하며 종종 불충분하다. 반대로, 수동으로 코딩된 심볼릭 강제(symbolic enforcement)는 형식적 보증을 제공하지만, 현실 세계의 광범위하고 복잡한 정책 명세의 폭과 복잡성을 따라잡지 못한다.

방법론
저자들은 자연어 에이전트 지침, 모델 컨텍스트 프로토콜(MCP) 도구 설명, 그리고 정책 문서를 Cedar 정책 언어로 작성된 형식적으로 검증된 정책으로 변환하는 자동 정형화 파이프라인을 제안한다. 이 파이프라인은 "검증 샌드위치(Verification Sandwich)"라고 불리는 세 가지 뚜렷한 계층으로 구성된 **생성자-비판자 루프(generator-critic loop)**를 통해 작동한다:

1. 그라운딩 계층 (하단): 이 계층는 엔티티를 추출하고, 도구 스키마(예: OpenAI JSON 스키마)를 식별하며, 주체-리소스-액션 온톨로지를 정의함으로써 기초를 확립한다. 이는 에이전트가 실제 엔티티와 유효한 시스템 식별자에 매핑되는 가능한 행동 범위 내에서 작동하도록 보장한다. 결정적으로, 이 계층는 MCP 도구 정의로부터 Cedar 스키마를 프로그래밍 방식으로 생성하여 엄격한 타입 체킹 메커즘 역할을 하게 한다.
2. 모델 계층 (중단): 최첨단 LLM을 활용하는 이 계층는 자연어 지침을 해석하고 후보 정책 세트를 생성한다. 이는 파라미터 지식을 활용하여 의도된 에이전트 로직을 반영하는 정책을 제안한다.
3. 안전 계층 (상단): 이 계층는 두 가지 비판자 메커니즘을 사용하여 후보를 검증한다:
   • 하드 비판자 (Hard Critic): Cedar의 내장 정적 분석 도구를 사용하는 결정론적, 프로그래밍 방식의 체크이다. 이는 구문(syntax)을 검증하고, 스키마 준수를 강제하며, 논리적 모순(예: 공허한 정책 또는 충돌하는 규칙)을 탐지한다.
   • 소프트 비판자 (Soft Critic): 사전 정의된 루브릭(rubric)에 따라 의미론적 정렬을 평가하는 LLM-as-a-judge이다. 이는 형식적 로직이 원래의 자연어 지침 및 정책 문서의 정신을 정확하게 반영하는지 확인한다.

루프는 두 비판자로부터의 피드백을 생성자에게 다시 전달하여 정책 세트가 두 가지 하드/소프트 체크를 모두 통과할 때까지 반복된다. 결과물인 정책은 외부의 결정론적 정책 엔진에 의해 런타임 시 강제되며, 이를 통해 안전 로직을 LLM의 추론 컨텍스트로부터 분리한다.

주요 기여

• 검증 샌드위치 아키텍처: 비정형 정책을 형식적 코드로 변환하기 위해 그라운딩, 생성적 추론, 그리고 이중 모드 검증(하드/소프트)을 결합한 새로운 계층적 접근 방식.
• 오픈 소스 구현: 커스텀 Python 바인딩을 포함하여 Cedar로 구현된 에이전트 스캐폴드(scaffold)를 위한 오픈 소스 정책 하네스 공개.
• 확장 가능한 자동 정형화: 에이전트 카드(지침 + 도구 스키마)를 검증된 권한 정책으로 자동으로 변환하는 파이프라인을 통해 수동 심볼릭 강제의 확장성 한계를 해결.
• 평가 프레임워크: 수동 코딩된 심볼릭 가드레일과 자동 정형화된 접근 방식을 비교하는 MedAgentBench 벤치마크를 통한 엄격한 평가.

결과
시스템은 도구 사용 전자 의료 기록(EMR) 에이전트를 위한 벤치마크인 MedAgentBench에서 평가되었다. 연구는 세 가지 조건(Raw HTTP 도구, 타입형 MCP 도구가 있는 Baseline, 저자의 Cedar 정책을 사용하는 Guardrail 조건 vs Hong 등의 수동 코딩된 심볼릭 가드레일)을 비교했다.

• 커버리지: 자동 정형화 파이프라인은 23개의 규칙만을 구현한 수동 코딩 방식에 비해 소스 88개 규칙의 자연어 명세를 실질적으로 더 많이 커버했다.
• 차단율: "Guardrail" 조건에서, Cedar 정책 엔진은 특히 적대적 시나리오에서 수동 코딩된 베이스라인보다 훨씬 높은 비율의 정책 위반을 차단했다.
  • Original 데이터셋에서, Cedar는 궤적(trajectories)의 55.7%(167/300)를 차단한 반면, 수동 코딩된 가드레일은 (구조상 일부 규칙만 커버하므로) 0%를 차단했다.
  • Adversarial 데이터셋에서, Cedar는 궤적의 85.7%(42/49)를 차단했다.
• 쓰기 시도 분석: 실제 쓰기 시도(POST 요청)를 포함하는 궤적을 필터링했을 때, Cedar의 차단율은 **100%**에 근접했다(예: Adversarial Guardrail 조건에서 100.0%). 이는 시스템이 승인되지 않은 데이터 수정을 발생시킬 때 이를 효과적으로 방지함을 입증한다.
• 강건성: 시스템은 규칙을 LLM의 컨텍스트 윈도우 외부에서 강제함으로써 "탈옥(jailbreaking)"과 간접 프롬프트 인젝션을 성공적으로 방지했다.

의의 및 주장
본 논문은 이 접근 방식이 확률적 가드레일에는 없는 강력한 형식적 보증에 대해 에이전트 행동에 대한 보증을 제공한다고 주장한다. 정책 강제를 LLM의 추론 컨텍스트로부터 분리함으로써, 이 아키텍처는 공격자가 보안 계층이 규칙을 무시하도록 설득할 위험을 완화한다. Cedar의 사용은 정책을 인간이 읽을 수 있고, 감사 가능하며, 형식적으로 검증 가능하게 만들어 자연어의 유연성과 심볼릭 로직의 엄격함 사이의 간극을 메운다.

저자들은 "마찰-유용성 트레이드오프(friction-utility trade-off)"를 인정하며, 지나치게 제한적인 정책은 에이전트의 유용성을 저해할 수 있다고 언급했다. 저자들은 생성자-비판자 루프, 특히 소프트 비판자의 포함이 에이전트가 충분히 제약되면서도 기능적으로 유지되는 "골디락스 존(Goldilocks zone)"을 달성하는 데 필수적이라고 상정한다. 본 연구는 자동 정형화가 고위험 도메인에 요구되는 형식적 보증을 희생하지 않으면서도 복잡한 현실 세계의 명세로 정책 강제를 확장할 수 있음을 보여준다.

한계 및 향 향후 과제
저자들은 Cedar가 설계상 상태 비저장(stateless) 방식임을 지적하며, 이는 액션 순서나 지속적인 컨텍스트에 의존하는 멀티 턴 워크플로우를 처리하는 데 한계가 있음을 언급했다. 향후 연구는 선행 조건 시퀀스를 위한 **시계열 로직(temporal logic)**을 통합하고, 엔진이 에이전트의 궤적 이력을 참조할 수 있도록 하는 **메모리 인식 정책(memory-aware policies)**을 개발하는 것을 목표로 한다.