Conformité Vérifiée par Types : Des Garde-Fous Déterministes pour les Systèmes Financiers Agentiels Utilisant la Preuve de Théorèmes Lean 4
Type-Checked Compliance: Deterministic Guardrails for Agentic Financial Systems Using Lean 4 Theorem Proving
April 1, 2026
Auteurs: Devakh Rashie, Veda Rashi
cs.AI
Résumé
L'évolution rapide de l'intelligence artificielle autonome et agentique au sein des services financiers a introduit une crise architecturale existentielle : les grands modèles de langage (LLM) sont des systèmes probabilistes et non déterministes opérant dans des domaines qui exigent des garanties de conformité absolues et mathématiquement vérifiables. Les solutions de garde-fou existantes — incluant NVIDIA NeMo Guardrails et Guardrails AI — reposent sur des classificateurs probabilistes et des validateurs syntaxiques qui sont fondamentalement inadéquats pour faire respecter les contraintes réglementaires complexes à multiples variables imposées par la SEC, la FINRA et l'OCC. Cet article présente le Protocole Lean-Agent, une plateforme de garde-fou pour l'IA basée sur la vérification formelle, qui exploite le modèle neuro-symbolique Aristotle développé par Harmonic AI pour auto-formaliser les politiques institutionnelles en code Lean 4. Chaque action agentique proposée est traitée comme une conjecture mathématique : l'exécution est autorisée si et seulement si le noyau Lean 4 prouve que l'action satisfait des axiomes réglementaires pré-compilés. Cette architecture offre une certitude de conformité de niveau cryptographique avec une latence de l'ordre de la microseconde, satisfaisant directement la Règle 15c3-5 de la SEC, le Bulletin 2011-12 de l'OCC, la Règle 3110 de la FINRA et les mandats d'explicabilité du CFPB. Une feuille de route de mise en œuvre en trois phases, allant de la vérification en shadow jusqu'au déploiement à l'échelle de l'entreprise, est fournie.
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.