Cumplimiento Verificado por Tipos: Barreras de Seguridad Deterministas para Sistemas Financieros Autónomos Utilizando la Demostración de Teoremas de Lean 4
Type-Checked Compliance: Deterministic Guardrails for Agentic Financial Systems Using Lean 4 Theorem Proving
April 1, 2026
Autores: Devakh Rashie, Veda Rashi
cs.AI
Resumen
La rápida evolución de la inteligencia artificial autónoma y agente dentro de los servicios financieros ha introducido una crisis arquitectónica existencial: los grandes modelos de lenguaje (LLM) son sistemas probabilísticos y no deterministas que operan en dominios que exigen garantías de cumplimiento absolutas y matemáticamente verificables. Las soluciones de barreras de protección existentes —incluyendo NVIDIA NeMo Guardrails y Guardrails AI— dependen de clasificadores probabilísticos y validadores sintácticos que son fundamentalmente inadecuados para hacer cumplir las complejas restricciones regulatorias multivariable exigidas por la SEC, FINRA y la OCC. Este artículo presenta el Protocolo Lean-Agent, una plataforma de barreras de protección para IA basada en verificación formal que aprovecha el modelo neuro-simbólico Aristóteles desarrollado por Harmonic AI para autoformalizar políticas institucionales en código Lean 4. Cada acción agente propuesta se trata como una conjetura matemática: la ejecución se permite si y solo si el kernel de Lean 4 demuestra que la acción satisface axiomas regulatorios precompilados. Esta arquitectura proporciona una certeza de cumplimiento a nivel criptográfico con latencia de microsegundos, satisfaciendo directamente la Regla 15c3-5 de la SEC, el Boletín 2011-12 de la OCC, la Regla 3110 de FINRA y los mandatos de explicabilidad del CFPB. Se proporciona una hoja de ruta de implementación en tres fases, desde la verificación en modo sombra hasta el despliegue a escala empresarial.
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.