論文の概要: Proof-Carrying Certificates for LLM Pipelines: A Trust-Boundary Architecture
- arxiv url: http://arxiv.org/abs/2605.16407v1
- Date: Wed, 13 May 2026 12:01:41 GMT
- ステータス: 翻訳完了
- システム内更新日: 2026-05-19 17:57:46.298792
- Title: Proof-Carrying Certificates for LLM Pipelines: A Trust-Boundary Architecture
- Title（参考訳）: LLMパイプラインの証明証明:信頼境界アーキテクチャ
- Authors: George Koomullil,
- Abstract要約: 本稿では,大規模言語モデルを取り巻く決定論的構造化計算を検証するためのフレームワークを提案する。
リーン4の信頼境界アーキテクチャを,現代的なLLMパイプラインの汎用インターフェースに拡張しています。
- 参考スコア（独自算出の注目度）: 0.0
- License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
- Abstract: We present a framework for verifying the deterministic structured computations surrounding a large language model rather than the model itself, extending a Lean 4 trust-boundary architecture to the generic interfaces of modern LLM pipelines. Certificate validity is a Lean 4 kernel type-check plus a sorry-free transitive axiom audit against the trusted set {propext, Classical.choice, Quot.sound}; other assumptions are declared and partitioned by tier (mathematical placeholders, cryptographic assumptions, ML/human oracles). The technical contribution comprises three local certificate families and two operators. The families are conflict-aware bilattice grounding (with an emission-gate soundness lemma), embedding sensitivity and paraphrase stability, and Hoare-style agent action. The operators are a Maximal Certifiable Residue, which turns abstention into the maximum-weight certifiable residue with audit-logged dropped claims, and a Compositional Stability theorem, which yields a closed-form pipeline-wide perturbation budget from per-layer gains and margins. The three families plus a Universal Assurance Card consolidator form the per-call deliverable for high-stakes deployments: patent and legal retrieval, regulated finance, clinical decision support, and agentic systems with irreversible side effects. A compiled Lean 4 reference artifact (Lean v4.30.0-rc2, Mathlib) covers all 22 certificate types, with 17 of 46 kernel-audited declarations axiom-free, the rest depending only on the trusted set and declared assumptions, and zero uses of sorryAx or Lean.ofReduceBool. The three families are empirically tested through four registered pilots: bilattice grounding on adversarially perturbed HotpotQA, embedding sensitivity in short- and long-form settings, and Hoare-style agent action on a filesystem sandbox with adversarial prompt injection.
- Abstract（参考訳）: 本稿では,モデル自体ではなく,大規模言語モデルを取り巻く決定論的構造化計算を検証し,リーン4信頼境界アーキテクチャを現代のLLMパイプラインの汎用インターフェースに拡張する枠組みを提案する。
証明された妥当性は、Lean 4カーネルの型チェックと、信頼された集合 {propext, Classical.choice, Quot.sound} に対する不注意な推移的公理監査であり、その他の仮定は層(数学的プレースホルダー、暗号的仮定、ML/ヒューマンオラクル)によって宣言され、分割される。
技術貢献は3つの地方認証ファミリと2つのオペレーターから構成されている。
家族は対立に敏感なビラチン質の接地(エミッションゲート・サウンドネス・レムマ)、感受性とパラフレーズ安定性の埋め込み、ホーアスタイルのエージェント・アクションである。
演算子は最大認定残差(Maximal Certible Residue)であり、これはアプテンションを最大級認定残差に変換し、オーディエンス付きドロップクレーム(英語版)と合成安定定理(英語版)は、階層ごとの利得と利得から閉形式のパイプライン全体の摂動予算を生成する。
ユニバーサル・アシュアランス・カード・コンソリエーター(Universal Assurance Card Consolidator)を含む3つのファミリーは、特許と法的検索、規制された財政、臨床決定支援、および不可逆的な副作用を持つエージェントシステムという、高額な展開のための呼び出しごとの配送を構成している。
コンパイルされたLean 4参照アーティファクト(Lean v4.30.0-rc2, Mathlib)は、46のカーネル監査済み宣言のうち17が公理フリーで、残りは信頼されたセットと宣言された仮定のみに依存し、 sorryAx や Lean.ofReduceBool の使用はゼロである。
3つのファミリーは、4つの登録パイロットによって実証的にテストされている。ビラチンは逆向きに乱れたHotpotQAに接地し、短距離および長径の設定に感度を埋め込む。
関連論文リスト
- Certified Purity for Cognitive Workflow Executors: From Static Analysis to Cryptographic Attestation [0.0]
以前の3層ガバナンスアーキテクチャは、ガバナンスの完全性、証明の完全性、そして過度な効果の不可能性を証明します。
本稿は4つのメカニズムを通してギャップを埋める。
構成による構造的純度、BEAMの5つのバイパスクラスすべてに対する排除、証明書の完全性、ゲート完全性という4つの定理を証明します。
論文 参考訳（メタデータ） (2026-05-01T19:04:37Z) - GSAR: Typed Grounding for Hallucination Detection and Recovery in Multi-Agent LLMs [0.0]
クレームを4方向のタイポロジー(接地,非接地,矛盾,相補的)に分割する基盤性フレームワークを提案する。
GSARは、明示的な計算予算の下で、結合された回復を伴うエビデンス型スコアリングを結合した最初の基盤フレームワークである。
論文 参考訳（メタデータ） (2026-04-25T16:20:28Z) - Trust but Verify: Introducing DAVinCI -- A Framework for Dual Attribution and Verification in Claim Inference for Language Models [53.279391576560755]
大規模言語モデル(LLM)は、広範囲のNLPタスクにおいて顕著な流速と汎用性を示してきたが、実際的な不正確さと制限が伴う傾向にある。
これは、信頼と妥当性が最優先される医療、法律、科学コミュニケーションといった、高リスク領域に重大なリスクをもたらす。
LLM出力の事実的信頼性と解釈可能性を高めるために設計されたDAVinCI - Dual Attribution and Verificationフレームワークを紹介する。
論文 参考訳（メタデータ） (2026-04-23T01:37:50Z) - Formally Verified Patent Analysis via Dependent Type Theory: Machine-Checkable Certificates from a Hybrid AI + Lean 4 Pipeline [0.0]
我々は、ハイブリッドAI+Lean 4パイプラインとして、特許分析のための正式に検証されたフレームワークを提示します。
DAG被覆コア(Algorithm1b)は、有界マッチスコアが固定されると完全に機械検証される。
クレームは、Lean 4でDAGとしてエンコードされ、強みを検証された完全な格子の要素と一致させ、信頼スコアは、証明された正しいモノトーン関数を通じて依存関係を通じて伝播する。
論文 参考訳（メタデータ） (2026-04-20T22:02:57Z) - Claw-Eval: Toward Trustworthy Evaluation of Autonomous Agents [66.97968363332465]
エージェントベンチマークの3つのギャップに対処するエンドツーエンド評価スイートであるClaw-Evalを紹介した。
Claw-Evalは3つのグループにまたがる9つのカテゴリにまたがる300の人間検証タスクで構成されている。
すべてのエージェントアクションは、3つの独立したエビデンスチャネルを通じて記録される。
論文 参考訳（メタデータ） (2026-04-07T17:43:18Z) - Type-Checked Compliance: Deterministic Guardrails for Agentic Financial Systems Using Lean 4 Theorem Proving [0.0]
本稿では,形式検証ベースのAIガードレールプラットフォームであるLean-Agent Protocolを提案する。
提案されたすべてのエージェント作用は、数学的予想として扱われる。
このアーキテクチャは、マイクロ秒レイテンシで暗号レベルのコンプライアンスを保証する。
論文 参考訳（メタデータ） (2026-04-01T23:39:43Z) - Towards Comprehensive Stage-wise Benchmarking of Large Language Models in Fact-Checking [64.97768177044355]
大規模言語モデル(LLM)は、現実のファクトチェックシステムにますます多くデプロイされている。
FactArenaは、完全に自動化されたアリーナスタイルの評価フレームワークである。
本研究では,静的クレーム検証精度とエンドツーエンドのファクトチェック能力の相違点を明らかにした。
論文 参考訳（メタデータ） (2026-01-06T02:51:56Z) - Eigen-1: Adaptive Multi-Agent Refinement with Monitor-Based RAG for Scientific Reasoning [53.45095336430027]
暗黙的な検索と構造化された協調を組み合わせた統合フレームワークを開発する。
Humanity's Last Exam (HLE) Bio/Chem Goldでは,48.3%の精度を実現している。
SuperGPQAとTRQAの結果はドメイン間の堅牢性を確認した。
論文 参考訳（メタデータ） (2025-09-25T14:05:55Z) - Towards Copyright Protection for Knowledge Bases of Retrieval-augmented Language Models via Reasoning [58.57194301645823]
大規模言語モデル(LLM)は、現実のパーソナライズされたアプリケーションにますます統合されている。
RAGで使用される知識基盤の貴重かつしばしばプロプライエタリな性質は、敵による不正使用のリスクをもたらす。
これらの知識基盤を保護するための透かし技術として一般化できる既存の方法は、一般的に毒やバックドア攻撃を含む。
我々は、無害な」知識基盤の著作権保護の名称を提案する。
論文 参考訳（メタデータ） (2025-02-10T09:15:56Z) - SORRY-Bench: Systematically Evaluating Large Language Model Safety Refusal [64.9938658716425]
SORRY-Benchは、安全でないユーザ要求を認識し拒否する大規模言語モデル(LLM)能力を評価するためのベンチマークである。
まず、既存の手法では、安全でないトピックの粗い分類を使い、いくつかのきめ細かいトピックを過剰に表現している。
第二に、プロンプトの言語的特徴とフォーマッティングは、様々な言語、方言など、多くの評価において暗黙的にのみ考慮されているように、しばしば見過ごされる。
論文 参考訳（メタデータ） (2024-06-20T17:56:07Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。