論文の概要: Secure Formal Raising: Protecting the Development of AI through Executable Properties
- arxiv url: http://arxiv.org/abs/2611.08042v1
- Date: Thu, 05 Nov 2026 13:59:27 GMT
- ステータス: 翻訳完了
- システム内更新日: 2026-11-07 04:55:13.528479
- Title: Secure Formal Raising: Protecting the Development of AI through Executable Properties
- Title(参考訳): セキュアなフォーマルレイジング - 実行可能な特性を通じてAI開発を保護する
- Abstract要約: 未知および矛盾した評価を保存した公式な起立環境を提案する。
我々は6つのセキュリティの不変性を証明し、彼らが承認された証拠のみを受け入れるように強制することを示します。
平C参照実装は、境界付き徹底探索において不変量を満たす。
- 参考スコア(独自算出の注目度): 1.4910833190248318
- License: http://creativecommons.org/licenses/by/4.0/
- Abstract: Model raising revisits Turing's developmental view of machine intelligence. Formal Raising (FR) has recently been proposed to complement this view with explicit behavioral properties. This paper extends that proposal to the security of the raising environment. Secure Formal Raising (SFR) models policy integrity, authorization, and confidential data flow using four-valued evidence that preserves unknown and inconsistent assessments. We prove six security invariants and show that they force admission to accept only confirmed evidence. A plain-C reference implementation satisfies the invariants in a bounded exhaustive exploration, which also exposes a confused-deputy gap for tool calls that a provenance requirement closes.
- Abstract(参考訳): モデル上昇はチューリングのマシンインテリジェンスに関する発達的な見解を再考する。
フォーマルレイジング(FR)は、最近、この見解を明示的な行動特性で補完するために提案されている。
本稿では,この提案を高揚環境の安全性に拡張する。
Secure Formal Raising (SFR)は、未知の、一貫性のない評価を保持する4つの重要な証拠を使用して、ポリシーの整合性、認可、機密データフローをモデル化する。
我々は6つのセキュリティの不変性を証明し、彼らが承認された証拠のみを受け入れるように強制することを示します。
プレーンC参照実装は、境界付き徹底的な探索において不変性を満足しており、また、証明要求が終了するツールコールに対する混乱した議論のギャップを露呈する。
関連論文リスト
- Beyond Plausible Prediction: Safety Sufficiency in Web World Models [61.50474448579379]
ウェブワールドモデルはエージェントが行動する前に候補行動の結果を予測する傾向にあるが、予測可能な未来は必ずしも正しい安全判断を支持するとは限らない。
いくつかのモデルは高度に非対称なオーソライゼーションの振る舞いを示し、低いフェイルセーフの実行と、解明可能なASKのケースのリコールを組み合わせている。
予測インターフェースが、UTEDされたり、ASKによる明確化を必要としたり、あるいはBLOCKEDでなければならないアクションを識別するために必要とされるポリシー決定情報を保存し公開するかどうか。
論文 参考訳(メタデータ) (2026-10-29T18:00:55Z) - A Deterministic and Auditable AI Security Risk Assessment Framework with ATLAS Aligned Executable Rules and Formal Verification [6.94323027313601]
決定論的決定関数としてのアセスメントを運用する,AIセキュリティアセスメントのエビデンスを提示する。
このフレームワークは、異質な成果物を、有界な4段階の順序スケールで測定されたプロジェクト独立制御ID分類に正規化する。
明示的なリポジトリスナップショットにピン留めされた5つの公開オープンソースAIプロジェクトで、このフレームワークを評価した。
論文 参考訳(メタデータ) (2026-10-01T10:33:04Z) - Stored Is Not Supported: Typed Provenance and Assertion Guardrails for Persistent AI Agents [2.124730017640531]
永続AIエージェントは、リフレクション、検索、統合を通じて自伝的状態を構築する。
自伝的アサーション境界性に対する型付き前置詞とアサーションガードレールを指定する。
論文 参考訳(メタデータ) (2026-09-02T05:35:33Z) - Mechanizing Typed Regulatory Actions for Security Tokens: Semantics, Falsification, and Bounded EVM Evidence [9.32030540168344]
セキュリティ標準は、実行された法的効果や、それが持つ証拠やリバース義務を特定せずに、特権的なコントロールを公開します。
我々はIsabelle/HOLで、FREEZE、SEIZE、CONFISCATE、LIQUIDATE、RESTRICT、RECOVERの6つのERC-8319の参照実行セマンティクスを定式化する。
論文 参考訳(メタデータ) (2026-08-29T08:23:27Z) - AI Slop and Hallucinations in Vulnerability Assessment: A Survey on Reasoning Failures and Trustworthy Mitigation [48.55515767840701]
AIスロープ(AI slop)は、アーティファクト、幻覚的脆弱性、可視だが正しくないパッチ、セマンティックに再パッケージされたバグレポートである。
本稿では,実証的証拠を調査し,統一メカニズムを特定し,信頼に値するトリアージへの道筋をたどる。
論文 参考訳(メタデータ) (2026-08-26T11:48:38Z) - Semantic Quorum Assurance: Collective Certification for Non-Deterministic AI Infrastructure [2.124730017640531]
非決定論的エージェント基盤を管理するためのコントロールプレーンプリミティブであるQuorum Semantic Assurance(SQA)を紹介する。
SQAは暗号エビデンスチェーンに縛られた宣言的実行契約として提案を表現し、それを読み取り専用でサンドボックス化されたバリデータエージェントのさまざまなパネルにルーティングする。
インフラにインスパイアされた500の突然変異シナリオでは、曖昧なシナリオを除く安全/安全でない試験の安全性が報告され、SQAはシングルエージェント検証の18.5%から0.3%まで安全でない承認を減じている。
論文 参考訳(メタデータ) (2026-06-06T07:31:04Z) - Compliance-by-Construction Argument Graphs: Using Generative AI to Produce Evidence-Linked Formal Arguments for Certification-Grade Accountability [0.0]
本稿では、生成AI(GenAI)と構造化された形式的引数表現を統合したコンプライアンス・バイ・コンストラクションアーキテクチャを提案する。
アーキテクチャは、各AI支援ステップを、検証済みの証拠によって支持され、明示的な推論制約に対して検証されなければならないクレームとして扱う。
この分析は、GenAIが議論構築を加速させながら、疑わしい主張が決定記録に入るのを防ぐことができることを示唆している。
論文 参考訳(メタデータ) (2026-04-05T12:55:16Z) - Ring-A-Bell! How Reliable are Concept Removal Methods for Diffusion Models? [52.238883592674696]
Ring-A-Bellは、T2I拡散モデルのためのモデルに依存しないレッドチームツールである。
これは、不適切なコンテンツの生成に対応する拡散モデルに対する問題的プロンプトを特定する。
この結果から,安全プロンプトベンチマークの操作により,既存の安全メカニズムを回避できると考えられるプロンプトを変換できることが示唆された。
論文 参考訳(メタデータ) (2023-10-16T02:11:20Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト(すべての情報・翻訳含む)の品質を保証せず、本サイト(すべての情報・翻訳含む)を使用して発生したあらゆる結果について一切の責任を負いません。