Causal Past Logic for Runtime Verification of Distributed LLM Agent Workflows

기술 요약: 분산 LLM 에이전트 워크플로우의 런타임 검증을 위한 인과적 과거 논리

문제 제기
여러 에이전트가 공유 메모리 없이 비동기적으로 상호작용하는 분산 대규모 언어 모델 (LLM) 에이전트 워크플로우는 단일 순차 로그를 생성하는 것처럼 효과적으로 모니터링될 수 없습니다. 비동기 실행에서 에이전트가 내린 결정 (생명선) 은 해당 에이전트에게 인과적으로 가시적인 사건들에만 의존합니다. 글로벌 순차 로그에서 더 일찍 발생한 사건은 아직 로컬에 알려지지 않았을 수 있으며, 로컬에서 최근 발생한 사건은 원격 에이전트의 최신 상태를 반영하지 못할 수 있습니다.

기존 런타임 검증 접근법은 종종 순차적 추적이나 사후 로그 분석에 의존합니다. 그러나 에이전트 워크플로우의 경우, 모니터링이 결정 시점에 실행에 영향을 미쳐야 하므로 이는 불충분합니다. 의사결정자 (예: 커미터) 가 인과적으로 깨끗한 테스트 결과를 보지 못했다면, 시스템은 나중에 위반 사항을 병합하고 보고해서는 안 되며, 병합을 차단하거나 즉시 재실행을 요청해야 합니다. 또한, LLM 애플리케이션의 표준 가드 메커니즘은 종종 실행을 순차 로그로 취급하여, 올바른 분산 의사결정에 필요한 인과 구조를 무시합니다.

방법론
저자들은 ZipperGen 프레임워크 (분산 LLM 에이전트를 위한 춤추기 프로그래밍 시스템) 를 인과적 과거 논리 (Causal Past Logic, CPL) 를 도입하여 확장했습니다.

1. 형식 모델 (MSCs): 실행은 사건이 생명선 위에 분포된 메시지 시퀀스 차트 (Message Sequence Charts, MSCs) 로 모델링됩니다. 인과적 순서는 로컬 후속 관계와 메시지 전달의 반사적 전이 폐포로 정의됩니다. 각 사건은 로컬 변수의 할당값을 지닙니다.
2. 인과적 과거 논리 (CPL): CPL 은 소스 레벨 가드 언어로 설계된 작은 과거 시간 논리입니다.
   • 구문: 공식에는 단일 생명선을 따라 해석되는 표준 과거 시간 모달리티 (이전 $Y$, 이후 $S$) 와, 현재 사건에 인과적으로 가시적인 생명선 $A$의 최신 사건에서 $\phi$를 평가하는 인과 모달리티 $@A(\phi)$가 포함됩니다.
   • 변수 접근: 논리는 $@A.x$와 같은 항을 지원하며, 이는 생명선 $A$의 최신 인과적으로 가시적인 사건에서 변수 $x$의 값을 읽습니다.
   • 의미론: 가드 $\phi@A$는 분기점이나 루프와 같은 결정 시점에서 소유자 생명선 $A$가 로컬로 평가합니다. 참/거짓 값은 제어 흐름을 결정합니다. 이 논리는 비엄격적 (non-strict) 입니다. 즉, $A$의 사건이 가시적이지 않으면 공식은 거짓으로 평가됩니다.
3. 온라인 모니터링 알고리즘:
   • 저자들은 각 생명선이 벡터 시계와 최신 값 뷰를 유지하는 분산 모니터링 알고리즘을 제안합니다.
   • 상태: 각 에이전트는 다른 모든 생명선에서 본 사건의 수를 추적하기 위해 벡터 시계를 유지합니다. 또한 다른 생명선으로부터의 불리언 공식과 변수 값에 대한 "최신 값 뷰"의 부분 맵을 유지합니다.
   • 전파: 에이전트가 메시지를 보낼 때 현재 벡터 시계와 최신 값 뷰를 첨부합니다. 메시지를 수신하면 에이전트는 이러한 뷰를 로컬 상태와 병합하고 벡터 시계를 업데이트한 후 모든 가드를 하향식 (bottom-up) 으로 재평가합니다.
   • 정확성: 이 알고리즘은 로컬로 계산된 모니터링 값이 MSC 에 대한 가드의 의미론적 의미와 일치함을 보장합니다.

주요 기여

• 인과적 과거 논리 (CPL): 표준 과거 시간 연산자와 다른 에이전트의 최신 가시 상태에 대한 인과적 접근을 결합한 분산 에이전트 워크플로우를 위한 새로운 논리입니다. 이를 통해 가드는 "필요한 테스트가 통과되었고 인과적 과거 이후로 실패가 관찰되지 않았다"와 같은 조건을 표현할 수 있습니다.
• 소스 레벨 가드: 사후에 로그를 확인하는 외부 모니터링과 달리, CPL 공식은 워크플로우 소스 코드에 통합됩니다. 의사결정자가 이를 온라인으로 평가하여 제어 흐름에 직접 영향을 미칩니다.
• 벡터 시계를 통한 분산 모니터링: 중앙 관찰자나 글로벌 순차 로그를 요구하지 않고 인과적 가시성을 추적하기 위해 벡터 시계와 최신 값 뷰를 사용하는 효율적인 온라인 모니터링 알고리즘입니다.
• 형식 검증: MSC 정의, CPL 만족도, 로컬 평가기, 그리고 모니터링 정확성 정의를 Lean 4에서 기계화하고 검증했습니다. 이 논문은 가드의 로컬 런타임 평가가 현재 사건에서의 의미론적 의미와 일치함을 증명합니다.
• 프로토타입 구현: ZipperGen 프레임워크 (Python) 에 구현된 프로토타입은 이 접근법의 실현 가능성을 보여주며, 가드가 생명선 간 변수를 비교하는 방법 (예: 테스트 결과가 현재 병합 후보에 해당하는지 확인) 을 시연합니다.

결과

• 이론적: 이 논문은 보조정리 1(로컬 평가 정확성) 과 보조정리 2(모니터 상태 불변성) 를 증명하여 정리 1(모니터 정확성) 으로 이어집니다. 이러한 증명들은 분산 알고리즘이 소유자 생명선에 가시적인 인과적 과거를 기반으로 모든 CPL 공식의 참/거짓 값을 올바르게 계산함을 입증합니다.
• 실용적: ZipperGen 에서 구현된 프로토타입은 분산 코드 리뷰 예제를 성공적으로 처리합니다. 여기서 커미터는 특정 후보에 대한 통과 테스트 및 보안 스캔을 인과적으로 보았을 때만 패치를 병합하고, 인과적 과거에 실패가 가시적이라면 병합을 차단합니다.

의의
이 논문은 분산 LLM 에이전트 워크플로우에 대한 런타임 검증이 순차 로그 분석을 넘어설 필요가 있음을 주장합니다. 모니터링을 춤추기 언어의 필수 부분 (소스 레벨 가드를 통해) 으로 간주함으로써, 시스템은 글로벌 로그나 중앙 관찰자를 기다리는 대신 결정 시점에 이용 가능한 인과적으로 가시적인 정보를 기반으로 올바른 결정을 내릴 수 있습니다. 이 접근법은 로컬 결정이 부분적 인과 뷰에 의존하는 분산 프로그래밍의 근본적인 어려움을 해결합니다. 이 작업은 전역 명세를 로컬 에이전트에 투영하는 춤추기 프로그래밍과 런타임 강제 사이의 간극을 메워, 안전성 및 조정 속성이 역동적이고 인과적으로 올바르게 강제되도록 합니다.