타입 체크 기반 컴플라이언스: Lean 4 정리 증명을 활용한 금융 에이전트 시스템용 결정론적 가드레일

금융 시장에서 AI 에이전트의 자율적 활동이 늘어남에 따라, 확률적인 LLM이 규제를 위반할 위험이 커지고 있다. 이 논문은 Lean 4 정리 증명기를 사용하여 AI의 행동을 수학적으로 검증함으로써, 100% 확실한 규제 준수와 초저지연 실행을 동시에 달성하는 아키텍처를 제시한다.

기존의 LLM 가드레일은 또 다른 AI 모델을 사용하여 출력을 검사하는 방식이다. 이는 검사기 자체도 확률적으로 동작하기 때문에 99.9%의 정확도를 가져도 0.1%의 치명적인 규제 위반 가능성을 남겨둔다. 금융 시장에서는 단 한 번의 오류가 수억 달러의 손실로 이어질 수 있으므로, 확률이 아닌 수학적 확실성이 필요하다.

이 논문은 Lean 4라는 정리 증명 언어를 가드레일의 핵심 엔진으로 도입한다. 에이전트가 특정 거래를 제안하면, 시스템은 이를 하나의 '수학적 정리'로 간주한다. 예를 들어 '이 거래는 회사의 가용 자본 한도를 넘지 않는다'는 명제를 세우고, Lean 4 커널이 미리 정의된 규제 규칙(공리)을 바탕으로 이 명제가 참임을 증명해야만 실제 거래 API가 실행된다.

이 과정은 딥러닝의 임베딩 공간에서 유사도를 찾는 것이 아니라, 논리적 기호 체계 내에서 엄격한 타입 체크를 수행하는 것이다. 결과적으로 AI 에이전트가 아무리 창의적이거나 할루시네이션이 섞인 제안을 하더라도, 수학적으로 증명되지 않은 행동은 물리적으로 실행 계층에 도달할 수 없게 차단된다.

Lean-Agent Protocol은 크게 두 단계의 워크플로우로 구성된다. 첫 번째는 비동기 정책 설정 단계로, Aristotle 모델이 자연어 규제 문서를 입력으로 받아 Lean 4 코드로 변환한다. 이 과정에서 Lean 4 컴파일러가 논리적 오류를 발견하면 Aristotle이 이를 피드백으로 받아 자가 수정(Self-repair)을 반복하며, 최종적으로 오류가 없는 공리 세트를 정책 환경(Policy Environment)에 저장한다.

두 번째는 동기식 런타임 승인 단계다. 에이전트가 API 호출 의도를 생성하면 오케스트레이터가 이를 가로채어 매개변수를 추출한다. 추출된 값들은 정책 환경의 정리들과 결합되어 하나의 수학적 추측(Conjecture)으로 정형화된다. [입력된 거래 데이터 → Lean 4 커널의 타입 체크 연산 → 이진 논리값(True/False) 출력] 과정을 거치며, 오직 True인 경우에만 게이트웨이가 열려 실제 실행 계층으로 명령이 전달된다.

보안 강화를 위해 전체 실행 환경은 WebAssembly(WASM) 상에 구축된다. WASM의 선형 메모리 모델과 기능 기반 보안(WASI)을 활용하여, 에이전트가 생성한 코드가 호스트 시스템의 파일이나 네트워크에 직접 접근하는 것을 원천 차단한다. 또한 '역자동 형식화(Reverse Auto-Formalization)' 기술을 통해 복잡한 수학적 오류 메시지를 다시 자연어로 번역하여 감사자에게 제공한다.

성능 벤치마크 결과, Lean 4 기반의 검증 속도는 평균 5마이크로초(μs)로 나타났다. 이는 고도로 최적화된 Rust 코드로 구현된 유사 시스템의 7마이크로초보다 빠른 수치이며, 고빈도 매매(HFT) 환경에서도 충분히 적용 가능한 수준이다. 특히 SMT(Satisfiability Modulo Theories) 솔버를 통합한 최신 Lean 4 기능을 통해 단순 산술 제약 조건은 밀리초 미만의 지연 시간으로 처리됨이 확인됐다.

규제 준수 측면에서는 SEC Rule 15c3-5(시장 접근 규칙)와 FINRA Rule 3110(감독 의무)의 요구 사항을 완벽하게 충족한다. 기존의 확률적 필터(NVIDIA NeMo 등)가 벡터 공간의 유사도에 의존하여 우회 공격에 취약한 것과 달리, 본 프로토콜은 수학적 논리 구조를 강제함으로써 규제 기관이 요구하는 '직접적이고 독점적인 통제'를 증명 가능하게 구현했다.

아키텍처의 핵심은 Lean 4의 종속 타입(Dependent Types) 시스템을 활용한 정적 분석이다. 모든 규제 제약 조건은 Lean 4의 공리(Axiom)로 정의되며, 에이전트의 행동은 이 공리들을 만족해야 하는 증명 객체(Proof Object)를 생성해야 한다. Lean 4 커널은 C++로 작성된 최소한의 신뢰할 수 있는 코드 베이스(Trusted Code Base)로 구성되어 있어 검증 과정의 무결성을 보장한다.

기존 연구인 NL2Lean 및 Herald 데이터셋의 방법론을 계승하여, 실패한 증명 추적(Error Trace)을 RAG 파이프라인에 입력해 자연어 설명으로 변환하는 구조를 취한다. 이는 규제 당국이 요구하는 '설명 가능성(Explainability)'을 수학적 근거에 기반하여 제공한다. 또한 'Concept-Symbol Constraints' 기법을 도입하여 자연어의 모호함이 논리적 기호로 변환될 때 발생할 수 있는 '심볼 드리프트(Symbol Drift)' 현상을 방지하고 일관된 매핑을 유지한다.

가장 큰 취약점은 자연어 정책을 Lean 4 코드로 변환하는 '번역 계층'에 있다. 만약 공격자가 Aristotle 모델을 조작하여 구조적으로는 유효하지만 논리적으로 결함이 있는 Lean 코드를 생성하게 만든다면(Logical Jailbreak), 커널 검증을 통과할 위험이 있다. 또한 현재 시스템은 명시적으로 정의된 규칙에 대해서만 동작하므로, 규정되지 않은 새로운 형태의 시장 조작 행위를 탐지하는 데는 한계가 있을 수 있다.