型チェック準拠：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
要旨
金融サービスにおける自律的エージェント人工知能の急速な進化は、存亡に関わるアーキテクチャ上の危機をもたらしている。すなわち、大規模言語モデルは確率的で非決定論的なシステムである一方、その適用領域である金融分野では、絶対的かつ数学的に検証可能なコンプライアンス保証が要求されるという根本的な矛盾である。既存のガードレールソリューション（NVIDIA NeMo GuardrailsやGuardrails AIなど）は、確率的分類器や構文検証器に依存しており、SEC（米国証券取引委員会）、FINRA（米国金融業規制機構）、OCC（米国通貨監査官）が義務付ける複雑な多変数規制制約を強制するには根本的に不十分である。本論文は、Lean-Agent Protocolを提案する。これは、Harmonic AIが開発したAristotleニューロシンボリックモデルを活用し、機関のポリシーをLean 4コードへ自動形式化する、形式検証ベースのAIガードレールプラットフォームである。全てのエージェント行動提案は数学的予想として扱われ、当該行動が事前コンパイルされた規制公理を満たすことをLean 4カーネルが証明した場合にのみ、実行が許可される。このアーキテクチャは、マイクロ秒レベルの遅延で暗号学的なレベルのコンプライアンス確実性を提供し、SEC規則15c3-5、OCC通達2011-12、FINRA規則3110、およびCFPB（米国消費者金融保護局）の説明責任要件を直接満たす。シャドウ検証からエンタープライズ規模での導入までの3段階からなる実装ロードマップも提示する。
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.