Agentproof: 에이전트 워크플로우 그래프의 정적 검증에 대한 기술 요약

이 논문은 Agentproof라는 시스템을 제안하며, 이는 대규모 언어 모델 (LLM) 기반 에이전트 프레임워크에서 정의된 워크플로우 그래프의 구조적 결함과 안전성 정책을 배포 전 (pre-deployment) 에 자동으로 검증하는 도구입니다.

1. 문제 정의 (Problem)

현재 에이전트 프레임워크 (LangGraph, CrewAI, AutoGen, Google ADK 등) 는 에이전트의 행위를 명시적인 워크플로우 그래프로 인코딩하고 있습니다. 그러나 안전성 검증은 주로 **런타임 (실행 시간)**에 의존하고 있습니다.

• 현행 런타임 가드레일의 한계: NeMo Guardrails 나 LlamaGuard 와 같은 도구는 실행 시 LLM 호출이나 도구 호출을 차단하지만, (i) 호출당 지연 시간을 유발하고, (ii) 실제 실행 경로가 트리거될 때만 위반을 감지하며, (iii) 테스트 중 실행되지 않은 경로에 대해서는 커버리지를 보장하지 못합니다.
• 구조적 결함의 간과: 개발자가 실수로 만든 '데드엔드 (dead-end)' 노드, '접근 불가능한 종료 지점', 또는 필수적인 '인간 승인 게이트'가 누락된 경로와 같은 위상학적 (topological) 오류는 런타임 가드레일로 발견하기 어렵습니다. 이러한 오류는 에이전트가 특정 경로를 실행할 때만 발생하며, 그렇지 않으면 시스템이 조용히 멈추거나 무한 루프에 빠질 수 있습니다.
• 기존 모델 체커의 비효율성: SPIN, NuSMV 와 같은 일반적인 모델 체커는 이러한 오류를 감지할 수 있지만, 개발자가 워크플로우를 전용 모델링 언어 (Promela, SMV 등) 로 수동으로 변환해야 하므로 에이전트 개발자에게 과도한 오버헤드를 요구합니다.

2. 방법론 (Methodology)

Agentproof 는 프레임워크별 소스 코드에서 워크플로우를 자동으로 추출하여 통합된 추상 그래프 모델로 변환한 후, 정적 분석을 수행합니다.

2.1 크로스-프레임워크 추출 파이프라인

LangGraph, CrewAI, AutoGen, Google ADK 등 4 가지 주요 프레임워크의 이질적인 API 를 자동으로 파싱하여 **통일된 추상 그래프 모델 (AgentGraph)**로 변환합니다.

• 추출기 (Extractors): 각 프레임워크의 노드 (LLM, 도구, 라우터, 인간 승인 등) 와 엣지 (조건부, 병렬, 루프) 를 식별하여 타입이 지정된 노드와 엣지로 매핑합니다.
• 자동화: 수동 모델링 없이 프레임워크 내부 객체에서 직접 그래프를 추출합니다.

2.2 검증 파이프라인

추출된 그래프에 대해 두 가지 계층의 검증을 수행합니다.

1. 구조적 검증 (Structural Checks):

   • 종단 도달성 (Exit Reachability): 시작 노드에서 모든 종료 노드에 도달 가능한지 확인.
   • 역방향 도달성 (Reverse Reachability): 모든 도달 가능한 노드가 종료 노드로 향하는지 확인 (무한 루프/데드락 감지).
   • 데드엔드 감지: 종료 노드가 아닌데 나가는 엣지가 없는 노드 발견.
   • 라우터 형태 검증: 라우터 노드의 모든 엣지가 조건부인지 확인.
   • 인간 게이트 존재 여부: 민감한 도구 사용 경로에 인간 승인 노드가 포함되었는지 확인.
   • 도구 선언 확인: 도구 노드에 명시된 도구 이름이 비어있지 않은지 확인.
   • 증거 경로 생성 (Witness Trace): 검증 실패 시 결함이 있는 구체적인 실행 경로를 생성하여 디버깅을 지원합니다.

2. 시간적 정책 검증 (Temporal Policy Verification):

   • DSL 및 DFA 컴파일: LTL(Linear Temporal Logic) 의 안전성 하위 집합을 다루는 7 가지 형태의 DSL 을 정의하고, 이를 결정적 유한 오토마타 (DFA) 로 컴파일합니다.
   • 정적 검증: 그래프와 DFA 의 곱 (Product Construction) 을 구성하여 에이전트 실행 없이 모든 가능한 경로를 탐색하고 정책 위반을 감지합니다.
   • 런타임 모니터링: 실제 이벤트 스트림에서 DFA 를 평가하여 위반 시 경고, 차단, 중단 등의 조치를 취합니다.

3. 주요 기여 (Key Contributions)

1. 자동 추출 파이프라인: 4 가지 주요 에이전트 프레임워크의 이질적인 표현을 통일된 추상 모델로 자동 변환하여 수동 모델링의 필요성을 제거했습니다.
2. 검증 시스템: 6 가지 구조적 검사와 시간적 정책 DSL 을 통합한 배포 전 검증 시스템을 구축했습니다.
3. 실증적 평가: 18 개의 커스텀 워크플로우 벤치마크를 통해 구조적 결함과 정책 위반이 실제로 존재하며, Agentproof 가 이를 효과적으로 감지함을 입증했습니다.
4. 성능: 5,000 개의 노드를 가진 그래프에서도 검증이 1 초 미만 (약 100ms) 에 완료되는 것을 확인했습니다.

4. 평가 결과 (Results)

• 데이터셋: 18 개의 워크플로우 (LangGraph 6 개, CrewAI 4 개, AutoGen 4 개, Google ADK 4 개).
• 결함 발견:
  • 구조적 결함: 18 개 중 5 개 (27%) 에서 결함 발견 (데드엔드 노드 2 개, 접근 불가 종료 지점 1 개, 라우터 형태 위반 1 개, 도구 선언 누락 1 개).
  • 정책 위반: 18 개 중 10 개 (55%) 에서 인간 게이트 누락 발견 (정책이 강제될 경우).
  • 시간적 정책: 15 개의 다양한 안전 정책 (예: "삭제 도구 사용 전 승인 필요", "개인정보 수집 후 3 단계 내 익명화") 이 모두 DSL 로 표현 가능했고, 정적 검증으로 모든 위반을 감지했습니다.
• 성능: 구조적 검증은 그래프 크기 (노드 + 엣지) 에 대해 선형적으로 확장되었으며, 5,000 노드 기준 약 105ms 에 검증 완료.
• 정확도: 구조적 검사의 정밀도 (Precision) 는 1.0 이었으며, 인간 게이트 검사에서는 낮은 위험 작업에 대한 과잉 경보 (False Positive) 가 1 건 발생하여 정밀도는 0.75 였습니다.

5. 의의 및 중요성 (Significance)

• 보완적 접근: Agentproof 는 런타임 가드레일을 대체하는 것이 아니라 보완합니다. 런타임 도구가 놓치는 **위상학적 결함 (토폴로지 레벨)**을 배포 전에 포착함으로써, 실행 시 발생할 수 있는 안전 사고의 표면을 줄입니다.
• 개발 효율성: 개발자가 수동으로 모델링 언어를 학습하거나 변환할 필요 없이, 기존 에이전트 코드를 기반으로 즉시 안전성을 검증할 수 있게 합니다.
• 실용성: 에이전트 시스템이 복잡해지고 다중 에이전트 구성으로 발전함에 따라, 워크플로우의 구조적 무결성을 보장하는 것은 필수적이며, Agentproof 는 이를 위한 실용적인 솔루션을 제공합니다.
• 한계 및 향후 과제: LLM 의 출력 의미 (진실성 등) 는 검증하지 않으며, 프레임워크 버전 변경에 따른 추출기 휴리스틱의 일반화 문제와 런타임 중 그래프 변형 (Mutation) 에 대한 대응이 향후 연구 과제로 남아있습니다.

결론적으로, Agentproof 는 에이전트 워크플로우의 구조적 안전성을 자동화하고 검증 가능한 형태로 만드는 첫 번째 체계적인 도구로서, 에이전트 시스템의 신뢰성 확보에 중요한 기여를 합니다.