論文の概要: Type-Checked Compliance: Deterministic Guardrails for Agentic Financial Systems Using Lean 4 Theorem Proving
- arxiv url: http://arxiv.org/abs/2604.01483v1
- Date: Wed, 01 Apr 2026 23:39:43 GMT
- ステータス: 翻訳完了
- システム内更新日: 2026-04-03 14:21:10.162491
- Title: Type-Checked Compliance: Deterministic Guardrails for Agentic Financial Systems Using Lean 4 Theorem Proving
- Title（参考訳）: 型付きコンプライアンス:Lean 4理論を用いたエージェントファイナンシャルシステムのための決定論的ガードレール
- Authors: Devakh Rashie, Veda Rashi,
- Abstract要約: 本稿では,形式検証ベースのAIガードレールプラットフォームであるLean-Agent Protocolを提案する。
提案されたすべてのエージェント作用は、数学的予想として扱われる。
このアーキテクチャは、マイクロ秒レイテンシで暗号レベルのコンプライアンスを保証する。
- 参考スコア（独自算出の注目度）: 0.0
- License: http://creativecommons.org/licenses/by/4.0/
- Abstract: 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.
- Abstract（参考訳）: 大規模言語モデル(LLMs)は、絶対的かつ数学的に検証可能なコンプライアンス保証を要求するドメインで動作する確率論的で非決定論的システムである。
NVIDIA NeMo GuardrailsやGuardrails AIなど、既存のガードレールソリューションは、SEC、FINRA、OCCが管理する複雑な多変量規制の実施に基本的に不十分な確率的分類器と構文検証器に依存している。
本稿では、Harmonic AIによって開発されたAristotleニューラルシンボリックモデルを利用して、機関方針をLean 4コードに自動変換する形式検証ベースのAIガードレールプラットフォームであるLean-Agent Protocolを提案する。
実行は、Lean 4カーネルが、そのアクションが事前コンパイルされた規制公理を満たすことを証明した場合にのみ許可される。
このアーキテクチャは、SEC Rule 15c3-5、OCC Bulletin 2011-12、FINRA Rule 3110、CFPB説明責任を直接満足する、マイクロ秒レイテンシにおける暗号レベルのコンプライアンスの確実性を提供する。
シャドー検証からエンタープライズ規模のデプロイメントまでの3段階の実装ロードマップが提供されている。
関連論文リスト
- FormalJudge: A Neuro-Symbolic Paradigm for Agentic Oversight [21.731032636844237]
本稿では,双方向のフォーマル・オブ・サートアーキテクチャを用いたニューロシンボリック・フレームワークを提案する。
行動安全,マルチドメイン制約順守,エージェントによる上向き偽装検出の3つのベンチマークにまたがって検証を行った。
論文 参考訳（メタデータ） (2026-02-11T18:48:11Z) - Self-Evolving Coordination Protocol in Multi-Agent AI Systems: An Exploratory Systems Feasibility Study [0.0]
自己進化コーディネーションプロトコル(SECP)
SECP: 限定的で、外部から検証された自己修正を可能にする調整プロトコル。
本稿では,自己進化コーディネーションプロトコルの探索システムの実現可能性について述べる。
論文 参考訳（メタデータ） (2026-02-02T14:45:04Z) - Pushing the Boundaries of Natural Reasoning: Interleaved Bonus from Formal-Logic Verification [49.506412445511934]
大きな言語モデル(LLM)は目覚ましい能力を示すが、その次は論理的不整合と報奨ハックを生み出す。
本稿では,自然言語生成プロセスと形式的記号的検証を動的にインターリーブする形式論理検証誘導フレームワークを提案する。
我々はこのフレームワークを,形式論理検証誘導制御による微調整とポリシー最適化の相乗効果を生かした,新しい2段階のトレーニングパイプラインを通じて運用する。
論文 参考訳（メタデータ） (2026-01-30T07:01:25Z) - Towards Verifiably Safe Tool Use for LLM Agents [53.55621104327779]
大規模言語モデル(LLM)ベースのAIエージェントは、データソース、API、検索エンジン、コードサンドボックス、さらにはその他のエージェントなどのツールへのアクセスを可能にすることで、機能を拡張する。
LLMは意図しないツールインタラクションを起動し、機密データを漏洩したり、クリティカルレコードを上書きしたりするリスクを発生させる。
モデルベースセーフガードのようなリスクを軽減するための現在のアプローチは、エージェントの信頼性を高めるが、システムの安全性を保証することはできない。
論文 参考訳（メタデータ） (2026-01-12T21:31:38Z) - The Agentic Regulator: Risks for AI in Finance and a Proposed Agent-based Framework for Governance [6.107950696680386]
現在のモデルリスクフレームワークは、静的で明確に定義されたアルゴリズムとワンタイム検証を前提としている。
我々はこれらの技術を、複数の時間スケールに沿って伝播する分散アンサンブルとしてモデル化する。
我々は、監視を「規制ブロック」の4つの層に分解するモジュラーガバナンスアーキテクチャを提案する。
論文 参考訳（メタデータ） (2025-12-12T05:57:32Z) - Towards a Science of Scaling Agent Systems [79.64446272302287]
エージェント評価の定義を定式化し,エージェント量,コーディネーション構造,モデル,タスク特性の相互作用として,スケーリング法則を特徴付ける。
協調指標を用いて予測モデルを導出し,R2=0をクロスバリデーションし,未知のタスク領域の予測を可能にする。
ツールコーディネーショントレードオフ: 固定的な計算予算の下では, ツールヘビータスクはマルチエージェントのオーバーヘッドから不均衡に悩まされ, 2) 能力飽和: 調整が減少または負のリターンを, 単一エージェントのベースラインが45%を超えると達成できる。
論文 参考訳（メタデータ） (2025-12-09T06:52:21Z) - BRIDGE: Building Representations In Domain Guided Program Verification [67.36686119518441]
BRIDGEは、検証をコード、仕様、証明の3つの相互接続ドメインに分解する。
提案手法は, 標準誤差フィードバック法よりも精度と効率を著しく向上することを示す。
論文 参考訳（メタデータ） (2025-11-26T06:39:19Z) - Making LLMs Reliable When It Matters Most: A Five-Layer Architecture for High-Stakes Decisions [51.56484100374058]
現在の大規模言語モデル(LLM)は、実行前にアウトプットをチェックできるが、不確実な結果を伴う高い戦略決定には信頼性が低い検証可能な領域で優れている。
このギャップは、人間と人工知能(AI)システムの相互認知バイアスによって引き起こされ、そのセクターにおける評価と投資の持続可能性の保証を脅かす。
本報告では、7つのフロンティアグレードLDMと3つの市場向けベンチャーヴィグネットの時間的圧力下での系統的質的評価から生まれた枠組みについて述べる。
論文 参考訳（メタデータ） (2025-11-10T22:24:21Z) - Agentic AI for Financial Crime Compliance [0.0]
本稿では、デジタルネイティブ金融プラットフォームにおける金融犯罪コンプライアンス(FCC)のためのエージェントAIシステムの設計と展開について述べる。
このコントリビューションには、リファレンスアーキテクチャ、現実世界のプロトタイプ、およびAgentic AIが規制下で再構成できる方法に関する洞察が含まれている。
論文 参考訳（メタデータ） (2025-09-16T14:53:51Z) - Safe and Certifiable AI Systems: Concepts, Challenges, and Lessons Learned [45.44933002008943]
この白書は、T"UV AUSTRIA Trusted AIフレームワークを提示する。
エンド・ツー・エンドの監査カタログであり、機械学習システムの評価と認定のための方法論である。
セキュアなソフトウェア開発、機能要件、倫理とデータプライバシという3つの柱の上に構築されているのは、EU AI Actの高レベルの義務を、特定かつテスト可能な基準に翻訳するものです。
論文 参考訳（メタデータ） (2025-09-08T17:52:08Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。