論文の概要: On the Formal Limits of Alignment Verification
- arxiv url: http://arxiv.org/abs/2603.08761v1
- Date: Sun, 08 Mar 2026 23:03:21 GMT
- ステータス: 翻訳完了
- システム内更新日: 2026-03-11 15:25:23.731057
- Title: On the Formal Limits of Alignment Verification
- Title(参考訳): 配向検証の形式的限界について
- Abstract要約: AIの安全性に関する根本的な疑問は、アライメントが正式に認定されるかどうかである。
検証手順が3つの特性を同時に満たさないことを証明する。音性(不整合系が認定されない)、一般性(検証は時間内に実行される)、トラクタビリティである。
その結果、完全なニューラルネットワーク検証の計算複雑性、行動観察による内部目標構造の非識別性、無限領域上で定義された特性に対する有限証拠の限界という3つの独立した障壁が導かれる。
- 参考スコア(独自算出の注目度): 0.24049560288708582
- License: http://creativecommons.org/licenses/by-nc-nd/4.0/
- Abstract: The goal of AI alignment is to ensure that an AI system reliably pursues intended objectives. A foundational question for AI safety is whether alignment can be formally certified: whether there exists a procedure that can guarantee that a given system satisfies an alignment specification. This paper studies the nature of alignment verification. We prove that no verification procedure can simultaneously satisfy three properties: soundness (no misaligned system is certified), generality (verification holds over the full input domain), and tractability (verification runs in polynomial time). Each pair of properties is achievable, but all three cannot hold simultaneously. Relaxing any one property restores the corresponding possibility, indicating that practical bounded or probabilistic assurance remains viable. The result follows from three independent barriers: the computational complexity of full-domain neural network verification, the non-identifiability of internal goal structure from behavioral observation, and the limits of finite evidence for properties defined over infinite domains. The trilemma establishes the limits of alignment certification and characterizes the regimes in which meaningful guarantees remain possible.
- Abstract(参考訳): AIアライメントの目標は、AIシステムが意図した目的を確実に追求することを保証することだ。
AI安全性に関する基本的な疑問は、アライメントが正式に認定されるかどうか、すなわち、アライメント仕様を満たすことを保証できるプロシージャが存在するかどうかである。
本稿ではアライメント検証の性質について考察する。
検証手順が3つの特性を同時に満たさないことを証明する。音性(不整合系が認証されない)、一般性(完全入力領域上の検証)、トラクタビリティ(多項式時間内での検証)。
それぞれの性質は達成可能であるが、3つとも同時に保持することはできない。
任意のプロパティを緩和することは、現実的な有界あるいは確率的保証が引き続き有効であることを示す、対応する可能性を取り戻す。
その結果、完全なニューラルネットワーク検証の計算複雑性、行動観察による内部目標構造の非識別性、無限領域上で定義された特性に対する有限証拠の限界という3つの独立した障壁が導かれる。
トリレンマはアライメント認定の限界を確立し、有意義な保証が可能な体制を特徴づける。
関連論文リスト
- Towards Trustworthy Embodied Intelligence: A Systems Framework and Graded Trustworthiness Levels [53.63220028820581]
身体的知性は、学習した知覚と意思決定をリアルタイムの計算、制御、物理的相互作用と統合する。
我々は,信頼に値するインテリジェンスを,特定のタスクを確実に実行するための持続能力として定義する。
論文 参考訳(メタデータ) (2026-07-28T17:50:44Z) - The Undecidability of Artificial General Intelligence (AGI) Alignment [0.0]
本稿では,AGI(Artificial General Intelligence)の安全性の基本的な数学的限界を確立する。
AGIアライメントの非可視性理論と有限構造的非可視性理論という2つの中心的不可視性結果を通してこの境界を定式化する。
論文 参考訳(メタデータ) (2026-06-26T22:51:16Z) - Making Embodied AI Reliable: A Community Agenda from Testing to Formal Verification [38.209854965937495]
Embodied AIシステムは、ますますオープンな環境にデプロイされている。
この記事では、組み込みAIの信頼性は本質的にライフサイクル保証の問題である、と論じる。
論文 参考訳(メタデータ) (2026-06-02T12:58:40Z) - Value Functions as Supermartingale Certificates [48.922124609307566]
適切な報酬の下では、$$-regularプロパティをほぼ確実に満足するポリシーに関連する値関数が、その仕様のStreet Supermartingale証明書を符号化していることを示す。
我々の結果は有限マルコフ決定過程で実験的に検証され、有限で数え切れないほど無限で連続的な状態空間を保ち、RLによる証明書合成への原則的経路を示唆している。
論文 参考訳(メタデータ) (2026-05-29T16:39:02Z) - Uncertainty-DTW for Sequences and Visual Tokens [43.798398689900075]
本研究では,不確実性を考慮した対応をモデル化し,アライメントパスに沿って構造化されたマッチングを行う確率的フレームワークである不確実性認識アライメントを導入する。
我々は、このフレームワークを時間列からトークン化された視覚表現に一般化し、視覚トークンの集合に対する構造化マッチングを可能にする。
これらの知見は、構造化データから学習するための一般的な、堅牢で解釈可能なフレームワークとして、不確実性を考慮したアライメントを確立する。
論文 参考訳(メタデータ) (2026-05-24T14:49:43Z) - Monitoring Data-aware Temporal Properties (Extended Version) [56.386411908764494]
有限トレース上の任意のSMT理論に富む線形時間特性の予測モニタリングについて考察する。
この設定での予測モニタリングは非常に困難であり、監視状態はこれまでのトレースプレフィックスと可能な有限継続の両方に依存している。
本研究は,表現的フラグメントオフMTにおける特性モニタリングのための新しい基礎的枠組みの正しさを提示し,正式に証明するものである。
論文 参考訳(メタデータ) (2026-05-14T10:23:11Z) - Incompleteness of AI Safety Verification via Kolmogorov Complexity [0.20305676256390928]
本研究は,本質的な情報理論の限界から検証の限界が生じることを示す。
任意の高複雑性のポリシーに準拠する全てのインスタンスを証明できる有限形式検証器は存在しない。
論文 参考訳(メタデータ) (2026-04-06T17:26:09Z) - Verification of Robust Properties for Access Control Policies [51.736723807086385]
既存のアクセス制御ポリシーの検証方法は、検証が進む前に、ポリシーを完全かつ完全に決定する必要がある。
本稿では,政策構造がどのような決定を下すか,どのような決定を下すか,あるいはその後の拡張に拘わらず,その決定を行うかという課題について,ロバストなプロパティ検証を導入する。
可能なすべてのポリシー拡張を普遍的に定量化しているにもかかわらず、判断は二階述語論理プログラミング言語における探索の証明に還元されることを示す。
論文 参考訳(メタデータ) (2026-03-13T17:14:38Z) - Upholding Epistemic Agency: A Brouwerian Assertibility Constraint for Responsible AI [0.0]
責任を負うAIに対して,Brouwerにインスパイアされたアサービビリティ制約を提案する。
ハイテイクドメインでは、公に検査可能でコンテスト可能な権利証明書を提供する場合に限り、システムはクレームを主張または否定することができる。
論文 参考訳(メタデータ) (2026-03-04T12:14:21Z) - Formal Mechanistic Interpretability: Automated Circuit Discovery with Provable Guarantees [5.156069978876762]
証明可能な保証付き回路を出力する自動アルゴリズムの組を提案する。
Input domain robustness*、*robust patching*、*minimality*の3つの保証にフォーカスします。
これら3つの保証のファミリーの間には、様々な理論的な関係が発見され、アルゴリズムの収束に重要な意味を持つ。
論文 参考訳(メタデータ) (2026-02-18T19:41:01Z) - Alignment Verifiability in Large Language Models: Normative Indistinguishability under Behavioral Evaluation [0.0]
部分観測可能性下での統計的識別可能性のレンズによるアライメント評価について検討した。
我々は、アライメント検証可能性問題を定式化し、ノーマティブ識別可能性を導入する。
以上の結果から,行動ベンチマークは,評価意識下での遅延アライメントに必要だが不十分な証拠を提供することが示された。
論文 参考訳(メタデータ) (2026-02-05T13:40:56Z) - Agentic Uncertainty Quantification [76.94013626702183]
本稿では,言語化された不確実性をアクティブな双方向制御信号に変換する統合されたデュアルプロセスエージェントUQ(AUQ)フレームワークを提案する。
システム1(Uncertainty-Aware Memory, UAM)とシステム2(Uncertainty-Aware Reflection, UAR)は、これらの説明を合理的な手段として利用し、必要な時にのみターゲットの推論時間解決をトリガーする。
論文 参考訳(メタデータ) (2026-01-22T07:16:26Z) - 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) - SONA: Learning Conditional, Unconditional, and Mismatching-Aware Discriminator [54.562217603802075]
帰納的バイアスを伴う最終層において,自然性(美容性)とアライメントを別々に投影するSONA(Sum of Naturalness and Alignment)を導入する。
クラス条件生成タスクの実験により、SONAは最先端の手法に比べて優れたサンプル品質と条件アライメントを達成することが示された。
論文 参考訳(メタデータ) (2025-10-06T08:26:06Z) - Core Safety Values for Provably Corrigible Agents [2.6451153531057985]
我々は,複数段階の部分的に観察された環境において,検証可能な保証を付与し,適応性のための最初の実装可能なフレームワークを紹介した。
私たちのフレームワークは、単一の報酬を5つの*構造的に分離された*ユーティリティヘッドに置き換えます。
敵がエージェントを修正できるオープンエンド設定では、任意のポストハックエージェントが調整性に反するかどうかを判断することは不可能である。
論文 参考訳(メタデータ) (2025-07-28T16:19:25Z) - Beyond 'Aha!': Toward Systematic Meta-Abilities Alignment in Large Reasoning Models [86.88657425848547]
大型推論モデル(LRMs)はすでに長い連鎖推論のための潜在能力を持っている。
我々は、自動生成の自己検証タスクを使用して、モデルに推論、帰納、誘拐の3つのメタ能力を持たせることを明確にした。
我々の3つのステージ・パイプラインの個別アライメント、パラメータ空間のマージ、ドメイン固有の強化学習は、命令調整ベースラインと比較して10%以上のパフォーマンス向上を実現します。
論文 参考訳(メタデータ) (2025-05-15T17:58:33Z) - Enumerating Safe Regions in Deep Neural Networks with Provable
Probabilistic Guarantees [86.1362094580439]
安全プロパティとDNNが与えられた場合、安全であるプロパティ入力領域のすべての領域の集合を列挙する。
この問題の #P-hardness のため,epsilon-ProVe と呼ばれる効率的な近似法を提案する。
提案手法は, 許容限界の統計的予測により得られた出力可到達集合の制御可能な過小評価を利用する。
論文 参考訳(メタデータ) (2023-08-18T22:30:35Z) - Evidential Turing Processes [11.021440340896786]
我々は、明らかなディープラーニング、ニューラルプロセス、ニューラルチューリングマシンのオリジナルの組み合わせを紹介する。
本稿では,3つの画像分類ベンチマークと2つのニューラルネットアーキテクチャについて検討する。
論文 参考訳(メタデータ) (2021-06-02T15:09:20Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト(すべての情報・翻訳含む)の品質を保証せず、本サイト(すべての情報・翻訳含む)を使用して発生したあらゆる結果について一切の責任を負いません。