기술 요약: 통제된 실행의 대수적 의미론

문제 제기

현재의 AI 워크플로우 시스템은 언어 모델 호출을 데이터 검색, 코드 실행, 외부 API 접근과 결합하지만, **통제된 실행 (governed execution)**을 위한 공식적인 프레임워크가 부재합니다. 기존 거버넌스 접근법은 두 가지 범주로 나뉩니다:

1. 행위적 접근법 (예: RLHF, 헌법적 AI, 가드레일) 은 모델 출력을 필터링하거나 학습시키지만, 시스템의 구조적 효과 (API 호출, 파일 쓰기) 가 거버넌스 경계를 통과하는지 여부를 다루지 못합니다.
2. 구조적 접근법은 실행 계층에서 불변성을 강제하지만, 종종 기계 검증된 증명이 없거나 **합성 (composition)**을 다루지 못합니다. 이러한 접근법은 일반적으로 개별 프로그램을 검증할 뿐, 거버넌스가 시스템의 합성 연산자 하에서 닫혀 있음을 증명하지는 못합니다.

핵심 과제는 거버넌스를 단순한 외부 필터가 아닌 실행 모델 자체의 고유하고 합성 가능한 속성으로 정의하는 의미론을 확립하여, 표현 가능한 프로그램의 집합이 통제된 프로그램의 집합과 일치하도록 보장하는 것입니다.

방법론

본 논문은 32 개의 Rocq 모듈(약 12,000 줄의 코드, 454 개의 정리, 0 개의 허용된 보조정리) 에서 기계화된 통제된 실행을 위한 대수적 의미론을 개발합니다. 이 프레임워크는 세 가지 주요 기술적 기둥에 의존합니다:

1. 상호작용 트리 (ITrees): 프로그램은 세 가지 노드 유형인 Ret(순수 값), Tau(침묵 단계), Vis(가시적 이벤트) 를 가진 공귀환적 (coinductive) 트리로 표현됩니다. 시스템은 14 가지의 서로 다른 외부 기능 (예: LLM 호출, HTTP 요청, 파일 작업) 을 모델링하기 위해 DirectiveE 타입을 사용합니다.
2. 거버넌스 대수: 거버넌스는 세 가지 공리로 정의된 매개변수 레코드 (GovernanceAlgebra) 로 공리화됩니다:
   • 안전성: 거버넌스 연산자 G는 해석된 프로그램이 공귀환적 안전성 술어 (gov safe) 를 만족하도록 보장합니다.
   • 투명성: 허용적인 조건 (모든 검사 통과) 하에서, 통제된 해석은 통제되지 않은 해석과 관찰적으로 동등합니다.
   • 적절성 (Properness): 동등한 핸들러는 동등한 통제된 핸들러를 생성합니다.
3. 모노이드 범주와 대수적 효과: 이 프레임워크는 프로그램의 범주 (Mashin) 를 대칭 모노이드 구조로 확장합니다. 이는 대수적 효과 시스템을 제약하여, 안전성 증명서 (GovernedHandler) 를 기계 검증한 핸들러만 안전 조각 내에서 구성될 수 있도록 합니다.

형식화는 gov safe 및 within caps(기능 범위) 와 같은 속성을 증명하기 위해 paco 라이브러리를 통한 **매개변수 공귀환 (parameterized coinduction)**을 사용합니다. 시스템은 OCaml 로 추출되어 BEAM 런타임에 네이티브 구현 함수 (NIF) 로 통합되었으며, 속성 기반 테스트 (70,000 개 이상의 무작위 입력) 를 통해 명세와 런타임 간의 행동적 동등성이 검증되었습니다.

주요 기여

1. 매개변수 거버넌스 대수와 모노이드 구조

본 논문은 GovernanceAlgebra 레코드를 정의합니다. 세 가지 공리로부터 이 공리를 만족하는 모든 시스템에 대한 수렴성, 합성적 닫힘, 그리고 목표 보존을 유도합니다.

• 모노이드 구조: 범주 Mashin은 검증된 오각형, 삼각형, 육각형 일관성을 가진 대칭 모노이드 구조를 허용함이 증명되었습니다.
• 거버넌스 보존: 핵심적으로, 모든 텐서 합성 (병렬/직렬 독립 합성) 은 거버넌스를 보존합니다. 구조적 사상이 순수하므로 증명들은 공귀환적이 아닌 계산적입니다.

2. 통제된 대수적 효과

어떤 핸들러든 유효한 표준 대수적 효과 시스템과 달리, 이 프레임워크는 핸들러 대수를 제한합니다.

• 통제된 핸들러 (GovernedHandlers): 해석이 gov safe를 만족한다는 증명이 번들된 핸들러만 GovernedHandler 타입을 가질 수 있습니다.
• 암묵적 효과 부재: 하나의 정리는 빈 기능 집합의 프로그램이 오직 관찰 지시문만 방출함을 증명합니다. 명시적으로 기능 집합에 의해 승인되지 않는 한 LLM 호출, HTTP 요청 또는 기타 효과를 수행할 수 없습니다.

3. 기능 인덱스 합성과 이중 보장

프로그램은 신뢰 격자에 의해 검증된 기계 검증된 기능 범위 (CapMorphisms) 와 함께 번들됩니다.

• 합성: 직렬, 텐서, 분기 합성 연산자는 기능 범위를 보존합니다.
• 이중 보장: 하나의 핵심 정리는 모든 프로그램에 대해 기능 범위(프로그램이 할 수 있는 것) 와 거버넌스 안전성(프로그램이 허용된 것) 이 동시에 성립함을 확립합니다. 정적 기능은 잠재적 효과를 제한하는 반면, 동적 거버넌스는 실행 전 모든 효과가 검사를 통과하도록 보장합니다.

4. 동시 종료 경계

본 논문의 정점 결과는 공식 모델 내에서 표현 가능성과 거버넌스 간의 관계를 정의합니다:

• 표현 가능 (E): 네 가지 기본 사상 (code, reason, memory, call) 으로 구성 가능한 프로그램.
• 통제됨 (G): G를 통한 해석이 gov safe를 만족하는 프로그램.
• 결과: $E = G$. 모든 표현 가능한 프로그램은 해석 하에서 통제되며, 모든 통제된 프로그램은 표현 가능한 프로그램의 이미지입니다.
• 함의: 튜링 완전성은 거버넌스 내부에서 보존됩니다. 비매개 I/O 는 구조적으로 통제된 조각에서 제외됩니다. 거버넌스 거부는 안전한 공귀환 발산 (비종료) 으로 모델링되어, 안전하지 않은 결과가 결코 생성되지 않도록 보장합니다.

결과 및 검증

• 공식 검증: 전체 프레임워크는 허용된 보조정리가 없는 Rocq 에서 기계화되었습니다.
• 런타임 추출: 추출된 OCaml 코드는 BEAM 런타임에서 NIF 로 실행됩니다.
• 테스트: 70,000 개 이상의 무작위 입력을 사용한 속성 기반 테스트는 Rocq 명세, 추출된 NIF, 그리고 Elixir 인터프리터 간에 0 개의 불일치를 보였습니다.
• 성능: 통제된 실행 경로는 측정 가능한 오버헤드를 추가하지 않습니다 (통제되지 않은 실행의 0.24 ms 대비 중앙값 0.23 ms).
• 추적 의미론: 이 프레임워크는 추적 수준의 속성을 유도하여, 통제된 실행이 모든 I/O 이벤트가 통과한 거버넌스 검사를 선행하는 "잘 통제된" 추적을 생성함을 증명합니다. 이러한 추적은 해시 체인을 통해 위변조 방지 원장에 매핑됩니다.

중요성과 주장

본 논문은 상호작용 트리 기반 실행 모델에 대한 거버넌스 제약 해석, 기능 제한 대수적 효과, 그리고 동시 종료 표현 가능성/거버넌스 정리를 결합한 최초의 기계화된 프레임워크를 제공한다고 주장합니다.

• 구조적 대 내용 거버넌스: 이 작업은 출력을 필터링하는 행위적 접근법과 구별되어 구조적 거버넌스(효과 중재) 를 강제합니다. 정리 3.3 은 이 공식 모델 내에서 출력 지향적 제어로는 재현할 수 없는 보장을 구조적 거버넌스가 제공함을 확립합니다.
• 매개변수성: GovernanceAlgebra는 매개변수적입니다. 유도된 정리는 특정 Mashin 인스턴스뿐만 아니라 세 가지 공리를 만족하는 모든 시스템에 대해 성립합니다.
• 합성성: 이 프레임워크는 거버넌스가 모든 시스템 합성 연산자 하에서 닫혀 있음을 증명하여, 개별 프로그램은 검증했으나 그 합성은 검증하지 못했던 기존 연구의 격차를 해소합니다.
• 한계: 저자들은 텐서 곱이 순차적 독립적 (진짜 동시성이 아님) 이며, 해시 체인은 추상적 단사 해시에 의존하므로 (구체적 암호학적 해시를 위한 추가 작업 필요), NIF 래퍼 자체는 공식적으로 검증되지 않았음을 지적합니다. 동시 종료 경계는 네 가지 기본 실행 모델에 대해 구체적으로 확립됩니다.

요약하자면, 본 논문은 거버넌스를 상호작용 트리 위의 대수적 구조로 공리화함으로써, 거버넌스가 표현 가능성과 동시 종료되는 시스템을 달성할 수 있음을 주장합니다. 즉, 시스템 내에서 프로그램을 작성할 수 있다면, 그것은 구조적으로 통제됨이 보장됩니다.