기술 요약: AI 워크플로우 아키텍처를 위한 효과 투명한 거버넌스

문제 제기

AI 워크플로우 시스템이 대규모 언어 모델 (LLM) 을 쿼리하고, 상태를 관리하며, 외부 도구를 호출하는 등 현실 세계에 점점 더 개입함에 따라, 안전하지 않거나 승인되지 않은 행위를 방지하기 위한 거버넌스 메커니즘에 대한 요구가 커지고 있습니다. 해당 분야의 지배적인 가정은 거버넌스가 필연적으로 능력과 트레이드오프 관계에 있다는 것입니다. 즉, 안전성을 높이기 위한 제한은 시스템이 나타낼 수 있는 행동의 범위를 축소한다고 여겨집니다. 본 논문은 내부 계산이나 출력 후처리를 수정하는 대신 **효과 경계 (effect boundary)**에서 거버넌스를 부과하는 아키텍처적 대안을 형식화함으로써 이러한 가정에 도전합니다. 본 논문이 다루는 핵심 의미론적 질문은 거버넌스가 허용된 프로그램이 계산하는 것을 변경하는지 여부입니다.

방법론

저자들은 Rocq 8.19 증명 보조기 (이전 Coq) 내의 **상호작용 트리 (Interaction Trees)**를 사용하여 구조적으로 거버넌스가 적용된 AI 워크플로우 아키텍처의 기계 검증 형식화를 제시합니다. 개발 내용은 36 개의 모듈, 12,000 줄의 코드, 454 개의 정의로 구성되며, 승인된 보조정리 (admitted lemmas) 는 하나도 없습니다.

핵심 형식주의

1. 상호작용 트리 (ITrees): 프로그램은 이벤트 유형 $E$에 대한 공귀환적 (coinductive) 트리로 모델링되며, Ret(v), Tau(t), 또는 Vis(e, k)로 정의됩니다. 이를 통해 재귀적이고 불순한 (impure) 프로그램을 표현할 수 있습니다.
2. 지시 이벤트 유형: 시스템은 기본 기능에 대한 생성자를 포함하는 DirectiveE 유형을 정의합니다. 여기에는 계산 사상, 메모리 연산, 오라클 (LLM) 호출, 외부 도구 호출, 그리고 관측 가능 이벤트가 포함됩니다.
3. 거버넌스 연산자 ($G$): 거버넌스는 대수적 효과 핸들러의 전통을 따르는 효과 해석에 대한 래퍼로 구현됩니다. 연산자 $G(h)$는 기본 핸들러 $h$가 발행하는 모든 지시를 중재합니다. 이는 사전 검사 (신뢰, 권한, 단계 유효성 검사) 와 사후 계측 (출처, 관측 가능성) 을 수행합니다. 검사에 실패하면 ITree.spin을 통해 실행이 발산하고, 통과하면 지시는 하위 핸들러에 위임됩니다.
4. 안전성 술어: 안전성은 매개변수화된 공귀환 (paco) 을 사용한 공귀환적 술어 gov_safe로 정의됩니다. 이 술어는 거버넌스 전용 이벤트 (항상 허용됨) 와 명시적 승인이 필요한 실제 I/O 이벤트를 구분합니다.

주요 기여 및 결과

본 논문은 거버넌스와 계산적 표현력이 직교하는 차원임을 증명하는 7 가지 주요 속성 (P1–P7) 을 확립합니다.

1. 의미론적 투명성 (핵심 정리)

핵심 기여는 의미론적 투명성을 증명하는 기계 검증 정리입니다. 거버넌스 검사가 성공하는 모든 실행에 대해, 거버넌스가 적용된 해석은 (거버넌스 전용 이벤트를 제외하고) 거버넌스가 적용되지 않은 해석과 관측적으로 동등합니다.

• 함의: 허용된 프로그램은 거버넌스 없이 계산했을 때와 정확히 동일한 부분 함수를 계산하며 동일한 도달 가능한 반환 값을 생성합니다. 거버넌스는 허용된 경로의 내부 계산을 변경하지 않고 효과의 경계를 제한합니다.

2. 거버넌스된 표현력 (P1 및 P2)

저자들은 거버넌스 래퍼가 계산 능력을 감소시키지 않는다는 것을 증명합니다.

• 거버넌스된 튜링 완전성: 시스템은 거버넌스 하에서도 튜링 완전성을 유지합니다. 레지스터 머신 프로그램은 표현력 손실 없이 거버넌스가 적용된 상호작용 트리로 변환될 수 있습니다.
• 거버넌스된 오라클 표현력: 이 아키텍처는 거버넌스 하에서 오라클 확장 (LLM 쿼리) 을 지원하여 복잡한 추론 워크플로우를 모델링할 수 있는 능력을 유지합니다.

3. 결정 가능성 경계 (P3)

본 논문은 거버넌스가 결정할 수 있는 것과 할 수 없는 것 사이의 엄격한 경계를 형식화합니다.

• 거버넌스 술어: 이들은 구조적, 구문적, 전체적이며 불리언 조합 (AND, OR, NOT) 에 대해 닫혀 있습니다. 이를 통해 신뢰 수준과 기능 클래스와 같은 속성을 결정할 수 있습니다.
• 의미론적 속성: 정지와 같은 프로그램 속성은 비자명하며 거버넌스로 결정할 수 없습니다. 본 논문은 두 프로그램이 동일한 지시 구조를 공유하여 (따라서 거버넌스 검사를 통과할 수 있음) 전역 종료 행동은 다를 수 있으므로, 거버넌스가 정지를 결정할 수 없음을 증명합니다. 이는 구조적 경계에 적용된 리스 (Rice) 의 정리와 일치합니다.

4. 표현적 최소성 (P5)

저자들은 기본 기능 집합 (계산, 메모리, 추론, 외부 호출, 관측 가능성) 이 최소한으로 필요함을 증명합니다.

• 엄격한 계층 구조: 기능들은 엄격한 체인을 형성합니다: 코드 < 코드 + 메모리 < 코드 + 메모리 + 추론 < 코드 + 메모리 + 추론 + 호출.
• 필요성: 단일 기본 기능을 제거하면 시스템의 표현력이 엄격히 감소합니다. 예를 들어, 메모리 지시는 튜링 완전성을 위해 구조적으로 필요하며, LLMCall 지시는 오라클 확장에 필요합니다.

5. 포괄 비대칭성 (P6)

본 논문은 구조적 거버넌스와 콘텐츠 레벨 필터링 사이의 엄격한 분리를 확립합니다.

• 구조가 콘텐츠를 포괄: 구조적 거버넌스는 콘텐츠 필터링을 엄격히 포괄합니다. 해석 경계에서 효과를 중재함으로써 구조적 거버넌스는 승인되지 않은 I/O 이벤트의 발생을 방지합니다.
• 콘텐츠가 구조를 포괄하지 않음: 콘텐츠 필터 (예: 출력 재작성) 는 값을 변경할 수 있지만 승인되지 않은 효과 단계의 발생을 방지할 수는 없습니다. 따라서 콘텐츠 필터링만으로는 효과 안전성을 보장하지 않습니다.

6. 목표 보존 (P4)

거버넌스가 허용하는 모든 실행에서 시스템은 프로그램의 목표를 보존합니다. 특정 반환 값 $v$에 도달하도록 설계된 프로그램이 거버넌스 검사를 통과하면, 거버넌스가 적용된 실행은 $v$에 도달합니다.

7. 거부를 통한 안전성 (활성화 대 안전성)

거버넌스 검사에 실패하면 시스템은 안전성을 위해 활성화를 희생합니다. 실행은 잘못된 결과를 생성하는 대신 발산 (spin) 합니다. 시스템은 승인되지 않은 효과가 결코 발생하지 않으며, "안전하지 않은" 반환 값이 결코 생성되지 않음을 보장합니다.

중요성 및 범위

본 논문은 거버넌스와 계산적 표현력이 직교함을 입증한다고 주장합니다. 거버넌스는 프로그램의 내부 계산적 표현력을 감소시키거나 허용된 추적에서의 의미론을 변경하지 않고 효과 경계를 제한하기 위해 부과될 수 있습니다.

• 신뢰 경계: 이러한 보장은 Rocq 커널, 상호작용 트리 라이브러리, 그리고 $G$ 연산자의 런타임 구현으로 구성된 신뢰할 수 있는 컴퓨팅 기반 (TCB) 에 상대적입니다. 본 논문은 검증된 컴파일러 (CompCert) 와 OS 커널 (seL4) 과 유사점을 지적하며, 형식 모델과 배포된 런타임 사이의 간극은 70,000 개 이상의 생성된 시퀀스에 대한 검증을 통해 검증된 테스트로 연결된다고 명시합니다.
• 한계점: 투명성 정리는 허용된 실행에만 적용되며, 거부된 실행은 발산합니다. 이 모델은 자원 고갈, 스케줄링, 확률적 모델 행동을 추상화합니다. 정리는 추상 아키텍처와 인터프리터에 적용되며, 컴파일된 바이너리에 대한 엔드투엔드 보장을 제공하는 것은 아닙니다.

이 작업은 의미론적 투명성, 표현적 최소성, 그리고 형식적 결정 가능성 경계를 추가함으로써 이전 기계화 개발 (McCann [2026b, 2026e]) 을 확장하여 AI 시스템의 "효과 투명한 거버넌스"를 위한 엄밀한 기초를 제공합니다.