유형 검증된 규정 준수: Lean 4 정리 증명기를 활용한 에이전트 기반 금융 시스템의 결정론적 가드레일
Type-Checked Compliance: Deterministic Guardrails for Agentic Financial Systems Using Lean 4 Theorem Proving
April 1, 2026
저자: Devakh Rashie, Veda Rashi
cs.AI
초록
금융 서비스 분야에서 자율적 에이전트 인공지능의 급속한 발전은 실존적 아키텍처 위기를 초래했습니다: 대규모 언어 모델(LLM)은 절대적이고 수학적으로 검증 가능한 규제 준수를 요구하는 영역에서 작동하는 확률적, 비결정론적 시스템입니다. NVIDIA NeMo Guardrails 및 Guardrails AI를 포함한 기존 가드레일 솔루션은 SEC, FINRA, OCC에서 의무화하는 복잡한 다변수 규제 제약 조건을 시행하기에는 근본적으로 부적합한 확률적 분류기와 구문 검증기에 의존합니다. 본 논문은 Harmonic AI가 개발한 Aristotle 신경-심볼릭 모델을 활용하여 기관 정책을 Lean 4 코드로 자동 형식화하는 형식 검증 기반 AI 가드레일 플랫폼인 Lean-Agent 프로토콜을 제시합니다. 모든 제안된 에이전트 행동은 수학적 추론으로 취급되며, Lean 4 커널이 해당 행동이 사전 컴파일된 규제 공리들을 만족함을 증명할 때에만 실행이 허용됩니다. 이 아키텍처는 마이크로초 단위의 지연 시간으로 암호학 수준의 규제 준수 확실성을 제공하며, SEC Rule 15c3-5, OCC Bulletin 2011-12, FINRA Rule 3110 및 CFPB 설명 가능성 의무를 직접적으로 충족합니다. 섀도우 검증부터 기업 규모 배포에 이르는 3단계 구현 로드맵을 제시합니다.
English
The rapid evolution of autonomous, agentic artificial intelligence within financial services has introduced an existential architectural crisis: large language models (LLMs) are probabilistic, non-deterministic systems operating in domains that demand absolute, mathematically verifiable compliance guarantees. Existing guardrail solutions -- including NVIDIA NeMo Guardrails and Guardrails AI -- rely on probabilistic classifiers and syntactic validators that are fundamentally inadequate for enforcing complex multi-variable regulatory constraints mandated by the SEC, FINRA, and OCC. This paper presents the Lean-Agent Protocol, a formal-verification-based AI guardrail platform that leverages the Aristotle neural-symbolic model developed by Harmonic AI to auto-formalize institutional policies into Lean 4 code. Every proposed agentic action is treated as a mathematical conjecture: execution is permitted if and only if the Lean 4 kernel proves that the action satisfies pre-compiled regulatory axioms. This architecture provides cryptographic-level compliance certainty at microsecond latency, directly satisfying SEC Rule 15c3-5, OCC Bulletin 2011-12, FINRA Rule 3110, and CFPB explainability mandates. A three-phase implementation roadmap from shadow verification through enterprise-scale deployment is provided.