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

금융 시장에서 LLM 에이전트의 확률적 판단은 자산 고갈이나 시스템 붕괴를 초래할 수 있는 치명적인 위험을 내포하고 있다. 이 논문은 Lean 4 정리 증명기를 활용하여 에이전트의 모든 행동을 실행 전 수학적으로 검증함으로써, SEC 등 규제 기관이 요구하는 절대적인 안전성과 투명성을 동시에 확보하는 방법을 제시한다.

기존의 LLM은 단어와 단어 사이의 통계적 확률에 기반하여 다음 토큰을 예측하므로, 99.9% 정확하더라도 나머지 0.1%의 확률로 금융 규정을 위반하는 '환각'을 일으킬 수 있다. 이는 마치 숙련된 운전자가 가끔 신호를 위반하는 것과 같아, 절대적인 안전이 필요한 금융 시스템에서는 수용 불가능한 한계이다.

이 논문은 이 문제를 해결하기 위해 LLM의 '생각'과 '행동'을 분리한다. 에이전트가 어떤 행동을 하겠다고 제안하면, 이를 수학적 가설(Conjecture)로 취급한다. 그리고 미리 정의된 금융 규정(공리, Axioms)을 바탕으로 이 가설이 참인지 거짓인지 Lean 4라는 엄격한 수학적 증명 도구로 검사한다. 증명되지 않은 행동은 아예 실행 자체가 불가능하도록 시스템 수준에서 차단한다.

결과적으로 시스템은 확률에 의존하는 '추측'의 영역에서 벗어나, 수학적으로 증명된 '사실'의 영역에서만 동작하게 된다. 이는 LLM의 유연한 문제 해결 능력은 유지하면서도, 그 결과물은 전통적인 하드코딩 시스템만큼이나 견고하고 예측 가능하게 만든다는 점에서 혁신적이다.

Lean-Agent 프로토콜은 크게 두 단계의 워크플로우로 구성된다. 첫 번째 단계는 비동기 정책 설정 단계로, 규정 준수 담당자가 자연어로 작성한 정책을 Aristotle 모델이 Lean 4 코드로 변환한다. 이 과정에서 Aristotle은 Lean 4 컴파일러의 에러 메시지를 피드백으로 받아 논리적 결함이 없는 완벽한 공리(Axioms) 세트를 생성하여 정책 환경(Policy Environment)에 저장한다.

두 번째 단계는 동기식 런타임 승인 단계이다. 에이전트가 API 호출(예: 주식 매수)을 시도하면 오케스트레이터가 이를 가로채어 매개변수를 추출한다. 추출된 값은 [입력값 → Lean 4 가설 공식화 → 커널 타입 체크 → 이진 결과(True/False)] 순으로 처리된다. Lean 4 커널은 C++로 작성된 최소한의 연산만 수행하므로 매우 빠르게 결과값을 도출하며, 오직 'True'가 반환된 경우에만 실제 API 실행 레이어로 명령을 전달한다.

보안 강화를 위해 전체 실행 환경은 WebAssembly(WASM) 내부에 구축된다. WASM의 선형 메모리 모델과 기능 기반 보안(WASI)을 통해 에이전트가 생성한 코드가 파일 시스템이나 네트워크에 직접 접근하는 것을 차단하며, 이는 [에이전트 코드 → WASM 컴파일 → 격리된 메모리 실행 → 시스템 보호]의 과정을 거쳐 제로 트러스트 보안 경계를 형성한다.

실험 결과, Lean 4 기반의 검증 시스템은 평균 5마이크로초의 지연 시간을 기록했다. 이는 고도로 최적화된 Rust 코드의 평균 지연 시간인 7마이크로초보다 빠른 수치로, 고빈도 매매(HFT) 환경에서도 충분히 적용 가능한 성능임을 보여준다. 특히 증명 생성 과정을 비동기화하고 런타임에는 타입 체크만 수행하는 구조적 분리가 이러한 성능 향상의 핵심 요인으로 분석됐다.

규제 준수 측면에서는 SEC Rule 15c3-5(시장 접근 규칙)와 FINRA Rule 3110 등의 요구사항을 100% 결정론적으로 충족함을 입증했다. 기존의 확률적 가드레일(NVIDIA NeMo 등)이 벡터 유사도 검색에 의존하여 우회 공격에 취약했던 것과 달리, Lean-Agent는 수학적 논리 구조를 강제함으로써 '환각 기반의 규정 준수' 위험을 근본적으로 제거했다. 또한 실패한 증명 과정을 RAG를 통해 자연어로 재번역하는 '역자동 형식화'를 통해 규제 기관이 요구하는 설명 가능성(Explainability) 수치도 만족했다.

Lean-Agent 프로토콜의 핵심은 Aristotle 모델의 뉴로-심볼릭 아키텍처에 있다. 이 모델은 단순한 토큰 예측을 넘어 Lean 4의 CIC(Calculus of Inductive Constructions) 규칙에 따라 내부 추론 과정을 지속적으로 검증한다. 특히 '에피스테믹 갭(Epistemic Gaps)'을 처리하기 위해 Lean의 'sorry' 택틱을 활용하여 미완성된 증명 구조를 식별하고, 이를 자가 복구 루프를 통해 채워나가는 방식을 취한다.

런타임 오케스트레이터는 SMT(Satisfiability Modulo Theories) 해결 능력이 통합된 Lean 4의 'grind' 택틱을 사용하여 산술적 제약 조건을 서브 밀리초 단위로 해결한다. 이는 [거래량 ≤ 자본 한도]와 같은 단순 비교부터 다변수 리스크 모델까지 수학적으로 엄밀하게 처리할 수 있게 한다. 또한 Herald 데이터셋 방법론을 차용한 역자동 형식화 파이프라인은 Lean 4의 에러 트레이스를 구조화된 메타데이터로 추출하여 소비자에게 친숙한 자연어 설명으로 변환하는 기술적 차별점을 가진다.

Aristotle 모델의 번역 레이어가 주요 취약점으로 지적된다. 공격자가 자연어 정책을 교묘하게 조작하여 구조적으로는 유효하지만 의미적으로는 악의적인 Lean 코드를 생성하게 만드는 '논리적 탈옥(Logical Jailbreaks)'이나 '기호 표류(Symbol Drift)' 현상이 발생할 수 있다. 이를 방지하기 위해 개념-기호 매핑 테이블(Concept-Symbol Mapping)과 같은 추가적인 제약 구조가 필요하다.