論文の概要: Mechanized Foundations of Structural Governance: Machine-Checked Proofs for Governed Intelligence

• arxiv url: http://arxiv.org/abs/2604.27289v1
• Date: Thu, 30 Apr 2026 01:03:15 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-05-01 16:31:53.854858
• Title: Mechanized Foundations of Structural Governance: Machine-Checked Proofs for Governed Intelligence
• Title（参考訳）: 構造的ガバナンスの機械的基礎: 統治された知性のための機械式証明
• Authors: Alan L. McCann,
• Abstract要約: 認知ワークフローシステムにおける構造ガバナンス理論の5つの結果を示す。 Coq 8.19の3つは、相互干渉木ライブラリーと機械化造幣を用いており、2つは明らかに還元された紙上で証明されている。 6番目のコントリビューションは、抽象モデルをデプロイされたランタイムに接続する。
• 参考スコア（独自算出の注目度）: 0.0
• License: http://creativecommons.org/publicdomain/zero/1.0/
• Abstract: We present five results in the theory of structural governance for cognitive workflow systems. Three are mechanized in Coq 8.19 using the Interaction Trees library with parameterized coinduction; two are proved on paper with explicit reductions. The Coinductive Safety Predicate (gov_safe) is a coinductive property that captures governance safety for infinite program behaviors, indexed by a boolean permission flag that is provably false for ungoverned I/O and true for governed interpretations (mechanized). The Governance Invariance Theorem establishes that governance is uniform across the meta-recursive tower: governance at level n+1 reduces to governance at level n by definitional equality of the type (mechanized). The Sufficiency Theorem proves that four atomic primitives (code, reason, memory, call) are expressively complete for any discrete intelligent system, formalized as compositional closure of a Kleisli category (mechanized). The Alternating Normal Form provides a canonical decomposition of any machine into alternating code and effect layers, with a confluent rewriting system (paper proof). The Necessity Theorem proves via explicit reduction to Rice's theorem that an architecturally opaque component (the reason primitive) is mathematically necessary for problems requiring semantic judgment (paper proof). A sixth contribution connects the abstract model to the deployed runtime: the Verified Interpreter Specification formalizes the BEAM runtime's trust, capability, and hash chain logic in Coq, then tests the running system against this specification using property-based testing with over 70,000 randomly generated directive sequences and zero disagreements. The mechanization comprises approximately 12,000 lines across 36 modules with 454 theorems and zero admitted lemmas.
• Abstract（参考訳）: 認知ワークフローシステムにおける構造ガバナンス理論の5つの結果を示す。 Coq 8.19では3つがパラメータ化コインダクションを備えたInteraction Treesライブラリを使用して機械化されている。 Coinductive Safety Predicate (gov_safe) は、無限のプログラム動作に対するガバナンスの安全性をキャプチャする造語である。 ガバナンス不変性理論は、ガバナンスがメタ再帰的タワー全体にわたって一様であることを確立する。 レベル n+1 のガバナンスは、(機械化された)型の定義的平等によってレベル n のガバナンスに還元される。 十分定理(Sufficiency Theorem)は、4つの原子原始体(符号、理由、記憶、呼び出し)が任意の独立した知的系に対して表現的に完備であることを証明し、クライスリ圏の構成的閉包(機械化)として定式化している。 オルタネート正規形式は、任意のマシンをコードとエフェクト層を交互に分解し、簡潔な書き換えシステム(紙の証明)を備える。 必要定理は、意味的判断を必要とする問題(紙の証明)に対して、アーキテクチャ的に不透明な要素(原始的理由)が数学的に必要であることを示すライスの定理への明示的な還元によって証明される。 検証解釈仕様(Verified Interpreter Specification)は、BEAMランタイムの信頼性、能力、およびハッシュチェーンロジックをCoqで形式化し、70,000以上のランダムに生成されたディレクティブシーケンスとゼロの不一致を持つプロパティベースのテストを使用して、この仕様に対して実行システムをテストする。 機械化は36個の加群に約12,000行あり、454の定理と既定の補題はゼロである。

関連論文リスト

• Benchmarking Testing in Automated Theorem Proving [39.65133452374143]
  T は形式定理の意味的正しさを評価する枠組みである。 5つの実世界のLean 4リポジトリからベンチマークを構築します。 実験により、最先端のモデルでは高いコンパイル成功を達成できるが、セマンティック・メトリックでは著しく性能が低下することが示された。
  論文  参考訳（メタデータ） (2026-04-26T13:24:20Z)
• 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)
• Yanasse: Finding New Proofs from Deep Vision's Analogies, Part 1 [51.56484100374058]
  システムはマドリブの27の上位領域の戦術的利用分布を抽出する。 zスコアを計算して、ソースエリアで多用されるが、ターゲットエリアで稀または欠落している戦術を特定する。 これは、GPUアクセラレーションされたNPハードアナログを用いて、ソースとターゲットの証明状態と一致する。
  論文  参考訳（メタデータ） (2026-04-19T03:27:16Z)
• Structured Abductive-Deductive-Inductive Reasoning for LLMs via Algebraic Invariants [0.0]
  大規模言語モデルは、構造化論理的推論において体系的な制限を示す。 LLM支援推論のための明示的なプロトコルとして、パースの三部構造推論を運用するシンボリックな足場を提案する。
  論文  参考訳（メタデータ） (2026-04-17T05:59:16Z)
• BRIDGE: Building Representations In Domain Guided Program Verification [67.36686119518441]
  BRIDGEは、検証をコード、仕様、証明の3つの相互接続ドメインに分解する。 提案手法は, 標準誤差フィードバック法よりも精度と効率を著しく向上することを示す。
  論文  参考訳（メタデータ） (2025-11-26T06:39:19Z)
• Transfinite Fixed Points in Alpay Algebra as Ordinal Game Equilibria in Dependent Type Theory [0.0]
  本稿では, 自己参照プロセスの安定な結果が, システムと環境との非有界リビジョン対話のユニークな平衡と同一であることを示すことによって, アルペイ・アルゲブラに寄与する。 固定点論、ゲームセマンティクス、順序解析、型理論から概念を統一することにより、この研究は無限の自己参照システムについての推論において、広くアクセス可能で形式的に厳密な基礎を確立する。
  論文  参考訳（メタデータ） (2025-07-25T13:12:55Z)
• Emergent Cognitive Convergence via Implementation: A Structured Loop Reflecting Four Theories of Mind [0.0]
  我々は、心の4つの影響力のある理論の間に構造的な収束を報告する。 収束は、エージェントフローと呼ばれる実用的なAIアーキテクチャの中で意図せずに現れる。 本稿では,知的アーキテクチャが,実践的制約によって形成される共有構造パターンへと進化する可能性を示唆する。
  論文  参考訳（メタデータ） (2025-07-22T02:54:45Z)
• DeepTheorem: Advancing LLM Reasoning for Theorem Proving Through Natural Language and Reinforcement Learning [67.93945726549289]
  DeepTheoremは、数学的推論を強化するために自然言語を活用する包括的な非公式な定理証明フレームワークである。 DeepTheoremには、121Kの高品質なIMOレベルの非公式な定理と証明からなる大規模なベンチマークデータセットが含まれている。 我々は、証明された定理の変種を利用して堅牢な数学的推論を動機付けることによって、非公式な定理証明に適した新しい強化学習戦略(RL-Zero)を考案する。
  論文  参考訳（メタデータ） (2025-05-29T17:59:39Z)
• Alchemy: Amplifying Theorem-Proving Capability through Symbolic Mutation [71.32761934724867]
  この研究は、記号的突然変異を通じて形式的な定理を構成するデータ合成のフレームワークであるAlchemyを提案する。 マドリブにおける各候補定理について、書き直しや適用に使用できるすべてのイベーシブルな定理を同定する。 その結果、マドリブの定理の数は110kから6Mへと桁違いに増加する。
  論文  参考訳（メタデータ） (2024-10-21T08:04:21Z)

関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。

指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。