类型校验合规性：基于Lean 4定理证明的智能金融系统确定性护栏

摘要

金融服务领域自主智能体的快速发展正引发一场根本性的架构危机：大型语言模型作为概率性、非确定性系统，却需在要求绝对数学可验证合规性的领域运行。现有防护方案——包括英伟达NeMo护栏与Guardrails AI——依赖的概率分类器与语法验证器，本质上无法满足美国证交会、金融业监管局及货币监理署对复杂多变量监管约束的要求。本文提出精益智能体协议，该基于形式化验证的AI护栏平台运用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.

类型校验合规性：基于Lean 4定理证明的智能金融系统确定性护栏

Type-Checked Compliance: Deterministic Guardrails for Agentic Financial Systems Using Lean 4 Theorem Proving

摘要

Support