Типобезопасное соответствие: детерминированные защитные механизмы для агентских финансовых систем с использованием верификатора теорем 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. В данной статье представлен Lean-Agent Protocol — платформа защитных барьеров ИИ на основе формальной верификации, которая использует нейросимволическую модель Aristotle, разработанную Harmonic AI, для автоформализации институциональных политик в код на Lean 4. Каждое предлагаемое агентное действие рассматривается как математическая гипотеза: выполнение разрешается тогда и только тогда, когда ядро Lean 4 доказывает, что действие удовлетворяет предварительно скомпилированным регуляторным аксиомам. Данная архитектура обеспечивает криптографический уровень определенности соответствия при микросекундной задержке, напрямую удовлетворяя требованиям Правила SEC 15c3-5, Бюллетеня OCC 2011-12, Правила FINRA 3110 и предписаниям CFPB относительно объяснимости. Представлена дорожная карта трехфазной реализации — от теневой верификации до развертывания в масштабах предприятия.
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.