Typprüfende Compliance: Deterministische Schutzmaßnahmen für agentenbasierte Finanzsysteme mittels Lean 4 Theorembeweiser
Type-Checked Compliance: Deterministic Guardrails for Agentic Financial Systems Using Lean 4 Theorem Proving
April 1, 2026
Autoren: Devakh Rashie, Veda Rashi
cs.AI
Zusammenfassung
Die rasante Entwicklung autonomer, agentenbasierter künstlicher Intelligenz im Finanzdienstleistungssektor hat eine existenzielle Architekturkrise ausgelöst: Große Sprachmodelle (LLMs) sind probabilistische, nicht-deterministische Systeme, die in Domänen operieren, die absolute, mathematisch verifizierbare Compliance-Garantien erfordern. Bestehende Guardrail-Lösungen – einschließlich NVIDIA NeMo Guardrails und Guardrails AI – verlassen sich auf probabilistische Klassifikatoren und syntaktische Validierer, die grundsätzlich ungeeignet sind, um komplexe multivariable regulatorische Vorgaben durchzusetzen, wie sie von der SEC, FINRA und OCC vorgeschrieben werden. Dieses Papier stellt das Lean-Agent-Protokoll vor, eine auf formaler Verifikation basierende KI-Guardrail-Plattform, die das von Harmonic AI entwickelte Aristotle neuralsymbolische Modell nutzt, um institutionelle Richtlinien automatisch in Lean-4-Code zu formalisieren. Jede vorgeschlagene Agentenhandlung wird als mathematische Vermutung behandelt: Die Ausführung ist nur dann zulässig, wenn der Lean-4-Kernel beweist, dass die Aktion vorkompilierte regulatorische Axiome erfüllt. Diese Architektur bietet kryptografische Compliance-Sicherheit bei Mikrosekunden-Latenz und erfüllt direkt die Anforderungen der SEC Rule 15c3-5, des OCC Bulletin 2011-12, der FINRA Rule 3110 sowie die Transparenzvorgaben des CFPB. Ein dreiphasiger Implementierungsfahrplan von der Schattenverifikation bis zum unternehmensweiten Einsatz wird dargelegt.
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.