← Archive
lm-005444 · 2026-11

RGC–DPIED-09|多機體協同中的動態重規劃:局部修復、證據依賴閉合與契約重驗證

下載 MD 檔 ⬇
📎 附件 · Companion files — 隨文交付的程式 / 證明 / 資料,可獨立下載重驗
  • 研究套件:RGC_DPIED_09_Research_Package_2026-11-05.zip zip · 365 KB · 26 檔 · 9651caa4422c
  • 內嵌研究圖:01_proof_invalidation_scope.png 🖼️ 內嵌研究圖:01_proof_invalidation_scope.png (png · 91 KB)
  • 內嵌研究圖:02_dependency_impact_matrix.png 🖼️ 內嵌研究圖:02_dependency_impact_matrix.png (png · 81 KB)
  • 內嵌研究圖:03_replacement_gate_matrix.png 🖼️ 內嵌研究圖:03_replacement_gate_matrix.png (png · 55 KB)
  • 內嵌研究圖:04_risk_budget_reserve.png 🖼️ 內嵌研究圖:04_risk_budget_reserve.png (png · 113 KB)

RGC–DPIED-09|多機體協同中的動態重規劃:局部修復、證據依賴閉合與契約重驗證

English title: Dynamic Replanning in Multi-Embodiment Cooperation: Local Repair, Evidence-Dependency Closure, and Contract Revalidation

  • 研究系列: 關係幾何與載體展開(RGC)× 數位—實體智能演化解耦論(DPIED)
  • 篇次: RGC–DPIED-09;不是原始 DPIED-09〈數位豐裕先行,物理生產力何時追上〉
  • 版本與日期: v1.0,2026-11-05
  • 署名: Neo.K Polaris|EveMissLab
  • 研究成果型態: 有限狀態數學建模、依賴圖充分性定理、局部重驗演算法、精確有理數檢查、故障與替代方案反例、可重現程式碼與接口草案
  • 證據範圍: 形式化條件下的解析證明與人工有限情境;非實體機器人實驗、非硬體安全認證、非實際部署的分散式事務協定
  • 正式原稿: 本 UTF-8 Markdown;數學唯一 canonical delimiter 為 $...$ 與 $$...$$

作者: Neo.K
機構: EveMissLab/一言諾科技有限公司
日期: 2026-11-05
版本: v1.0

摘要

第八篇 RGC–DPIED-08 的組合式作用契約圖 CACG-0.1 指出:多台具身載體的局部任務合格,並不直接推出整體能源、時間、條件風險與聯合安全條件也合格。然而,真實跨載體協作不可能永遠保持組合前提不變。攝影機的校準版本可能過期,操作機器人的致動能力可能下降,物理空間可能新增障礙,一次任務交接也可能因觀察者座標或資料通道不同而失效。將任何一處變更都視為整套系統必須全部重證,可以保持概念上的保守性,卻未充分利用已建立的局部證據;反過來,若僅重新檢查出現故障的載體,又可能漏掉共享能源、整體期限、風險耦合或空間干擾。

本篇提出研究候選 CRRV-0.1(Contract-Referenced Revalidation and Repair,契約參照式重驗與修復),區分四種對象:物理/觀察條件的來源事實、以這些事實為前提的衍生證據節點、允許重新選擇的候選修復方案,以及仍需獨立決定的真實物理行動授權。本篇核心是將 CACG 的作用交接圖與證據依賴圖分開。作用圖記載誰與誰交接;證據圖則記載某項局部或全域合格判斷究竟依賴哪些來源、模型版本與共享約束。

對有限無環、依賴宣告完整、求值器確定、來源快照一致的證據圖,本文證明:只對來源變更的有向後繼閉包重新求值,保留其他證據節點,所得結果與整圖從頭求值完全相同。此結論屬增量計算的標準歸納原理在本研究接口上的條件式特例,並不是一般情況下「永遠只需局部驗證」的新定理。本文另外構造一個依賴漏登記反例:六段合成任務中,若某機體能源需求由 2 改為 100,而證據圖錯漏其通向全域能源閘門的邊,錯誤的增量程序會保留舊的通過值,導致研究模型誤判合格。

在具體有限模型中,六段協作含 23 個衍生證據節點;一台中間機體變更需重算 9 個節點、保留 14 個;改動全域時鐘則需重算全部 23 個。四種替代方案中,高能源使用、共享空間衝突及座標不匹配均被拒絕,只有滿足全域聲明契約者得到 CONTRACT_CANDIDATE_WITHIN_DECLARED_MODEL。程式通過 43 項單元測試;另以獨立算術實作在 2,160 組有限情境中比較全量與增量求值,結果一致。這些數字是模型的證據節點數及合成檢查結果,不能外推為實際機器人的效能、安全性或可部署性。

本篇最後區分事件更新、方案模擬與研究契約提交:真實環境已改變時必須撤回舊結論,不能藉「拒絕更新」假裝故障沒有發生;候選方案與所依附的來源版本不同時不得沿用舊驗證;即使重新通過研究契約,也不產生實體致動許可。研究結論是:局部重驗的正當性來自依賴閉合、時間與模型證據一致,而不是來自變更看起來很小。

關鍵詞: 跨載體智能;關係幾何;具身協同;假設—保證契約;動態重規劃;局部修復;增量驗證;證據依賴圖;版本化快照;失配監測;共享風險;物理授權;CACG;CRRV

Abstract

Prior RGC–DPIED research links observer-conditioned visual correction, model mismatch, and cross-embodiment action realization to compositional action-contract graphs. This paper addresses a complementary problem: after a sensor, actuator, observer model, or resource condition changes, which existing proofs may be safely reused, and which obligations must be revalidated before any candidate recovery is accepted? We introduce CRRV-0.1, a research-level contract-referenced revalidation and repair interface. It separates action handoffs from a directed proof-dependency graph, environmental events from hypothetical repair proposals, and mathematical contract status from physical authorization.

For finite directed acyclic proof graphs with complete extensional dependencies, deterministic evaluators, and a coherent immutable source snapshot, we prove that recomputing only the downstream dependency closure of changed sources yields exactly the same node values as a full recomputation. An intentionally incomplete dependency graph gives the opposite result: a globally infeasible energy increase is accepted when an omitted resource dependency permits stale evidence reuse. Exact synthetic experiments show 9 of 23 proof nodes recomputed after a middle-robot change, but 23 of 23 after a global time change. Four repair proposals are checked against handoffs, shared energy and deadline budgets, conservative marginal-risk union bounds, a declared total-variation recursion, and exclusive space reservations. Across 2,160 finite configurations, independent direct arithmetic matches both full and incremental evaluation; 43 unit tests pass. The implemented epoch guard rejects stale candidate plans in a sequential simulation; it does not establish distributed atomicity, real-time guarantees, provenance authenticity, or robot safety. The results define a falsifiable interface and precise proof-reuse conditions, not a physical deployment certificate.


0. 與 RGC–DPIED-01 至 -08 的連接

本系列先由三線成方的載體—投影區分開始,轉入不同觀察者的視覺幾何、觀測可辨識性與具身轉譯。-01 v1.1 將 RGC-BV04 螳螂蝦偏振視覺案例納入感測通道盲區;-02 研究異質觀測條件遺失造成的資料衝突;-03 分開對齊圖冊、任務充分性與動態閉合;-04 處理自適應主動補觀測;-05 聯合維護世界與觀察者信念;-06 討論既有觀察模型無法解釋新資料時的保守診斷;-07 建立 CATC-0.1 的跨機體作用轉譯判準;-08 提出 CACG-0.1 的多機體組合契約。

RGC–DPIED-08 的充分條件是在指定任務圖及交接前提下完成的。當觀察者版本、場景、機體或共享資源改變時,原先部分前提可能不再成立。本篇不重證第八篇的完整組合定理,而是提出如何判定先前證據仍可用,以及如何分開處理局部失效與全域約束。

本篇 CRRV-0.1 是研究候選接口,不宣稱已整合 ROS 2、實際相機、VLA 模型、硬體安全控制器或多機體通訊中介。

1. 文獻位置與研究增量

組件式系統的 assume–guarantee(假設—保證)推理、修改後局部重驗與執行期安全架構已有相當長的歷史。Becker 與 Giese [E1] 討論自適應系統運行時的增量不變量檢查;Tran 等人 [E2] 已研究演化式軟體的假設—保證回歸驗證;分散式組件重組的驗證綜述 [E3] 更明確涵蓋影響分析與依賴追蹤。自適應契約的研究 [E4] 處理重組後的全域前提;2026 年的執行期驗證研究 [E5] 也已展示對改變中需求保留中間驗證結果的做法。以多機體安全為中心,分散式 Simplex [E6] 與多代理 shielding [E7] 則討論獨立監督與全域約束。

所以,本篇不聲稱發明依賴閉包、快取失效、回歸驗證、版本化控制、聯集界或安全屏障。本篇研究的組合性增量是:把 RGC 視覺來源與校準版本、DPIED 作用可實現性、CACG 交接約束及模型風險證據,放入同一個可拒絕的變更重驗接口;為它提出充分條件、失效反例、可重現的源碼與資料結構。已存在相關工程研究不使本篇沒有價值,但新意必須如實限定在這個跨研究線的定義、組合與可檢查實例,而不能無條件宣稱普遍首創。

2. 研究問題與證據範圍

本篇解決以下問題:

  1. 某台機體或觀察者的條件發生改變後,哪些證據可以重用,哪些不得重用?
  2. 為何只檢查「受影響的機器人」不足以保證全域能源、時限、風險、空間與轉移誤差?
  3. 在什麼條件下,增量重新驗證與全量重新驗證完全等價?
  4. 證據依賴漏登記時,能否構造可窮舉的假陽性反例?
  5. 修復方案的確認與環境已經改變的事件,為何應使用不同的語義?
  6. 方案取得研究契約通過,為何仍不能直接授權物理行動?

本篇採有限、離散、聲明式證據模型。所謂 PASS,僅表示輸入的人工契約在被檢查的邏輯內相容。它不替換真實校準、感測器證據、碰撞幾何、動力學模型驗證或硬體保護機制。

3. 雙層圖:作用交接圖與證據依賴圖

3.1 作用交接圖

沿用 CACG-0.1,定義機體任務圖:

GA=(VA,EA).\mathcal{G}_{A}=(V_A,E_A).

VAV_A 是感測、控制、動作或協調任務片段, EAE_A 表示資料、狀態或動作目標的交接。某條邊的存在可以敘述來源載體向目標載體發送資訊,並不代表該資訊已具備正確幾何、時序與物理含義。

3.2 證據依賴圖

另定義:

GP=(B∪Q,EP),\mathcal{G}_{P}=(B\cup Q,E_P),

其中 BB 是基礎來源集合,例如相機校準版本、感測通道集合、機體能力參數、目前觀察時鐘、物理場景變數、全域預算與交接協定; QQ 是衍生證據節點集合,例如影像來源是否有效、作用是否可實現、交接是否相容、能源及風險是否仍在約束內。

若 u→vu\rightarrow v,表示 vv 的求值需要 uu 的結果。重要的是, GP\mathcal{G}_{P} 與 GA\mathcal{G}_{A} 不必同構。例如「共享能源上限」可能沒有對應的機體交接邊,卻是全域候選能否成立的必要證據依賴;「同一個保留格點」可能讓兩個作用分支經共享空間閘門發生關聯。

假設每個衍生節點 vv 都有明示的依賴集合 D(v)D(v) 和求值函數 fvf_v,則:

qv=fv((zu)u∈D(v)),q_v=f_v\bigl((z_u)_{u\in D(v)}\bigr),

其中 zuz_u 可以是來源變量或前序衍生值。完整性要求 fvf_v 實際使用的一切可能改變其結果的外部條件都已被記入 D(v)D(v) ;這是一個嚴格的前提,不是一般程式自動滿足的事實。

3.3 觀察者版本不只是一個欄位

一筆來自攝影機的資料即使張量維度正確,仍需攜帶或關聯其觀察模型、座標、通道、時間與可追溯證據。若更換攝影機或校準版本,可能影響來源證明、對應機體的作用映射、上下游的交接、世界模型誤差及全域安全約束。此時把變更當作「只有影像來源字串不同」並不足夠。

而若 BV04 式的感測通道本來就缺失,例如無法觀測所需圓偏振分量,依賴重驗不會創造該物理資訊;它應回報模型缺口或觀測不足,而不是虛構可用通道。

4. 定義:變更影響閉包與證據再使用

令第 ee 個來源快照為 σe\sigma_e。令變更來源集合為 Δ⊆B\Delta\subseteq B,定義其證據影響閉包:

I(Δ)={v∈Q:∃b∈Δ, b⇝v},\mathcal{I}(\Delta)=\{v\in Q:\exists b\in\Delta,\ b\leadsto v\},

其中 b⇝vb\leadsto v 表示在證據圖中存在由 bb 到 vv 的有向路徑。若 Δ\Delta 為空,閉包為空;若全域時鐘連到全部觀察節點,時間變更可能導致整張證據圖都受影響。

一項未被閉包覆蓋的舊證據 qv(e)q_v^{(e)} 可以候選重用,須至少符合:

  • 它在前一快照的求值是有效且可追溯的,而非未檢查的自我宣告;
  • 所有真正影響其求值的來源都已登記成依賴,沒有未聲明的共享效應;
  • 其語義、模型版本及適用範圍沒有因系統重組而改變;
  • 所依附的來源快照與新計算之間有一致、不可混搭的版本邊界;
  • 任何明示的期限或實體狀態變更都納入相應依賴。

注意: 當前程式可以證明「輸入聲明一致」,但不能自行證明聲明的物理真實性。此處的重用充分條件是相對於給定證據語義的。

5. 定理一:完整依賴下,局部重驗與全量重驗等價

定理 5.1|有限證據圖的增量求值正確性

給定 GP\mathcal{G}_{P},假設:

  1. GP\mathcal{G}_{P} 是有限有向無環圖。
  2. 所有衍生節點由確定性的純求值函數 fvf_v 計算;不存在未登記的全域狀態、時間、隨機數或外部呼叫影響結果。
  3. 所有來源變更都已精確記錄於 Δ\Delta,未改變的來源值在兩個快照中確實相同。
  4. 每個 D(v)D(v) 完整覆蓋 fvf_v 的全部外延依賴;圖結構與求值函數本身沒有未登記的修改。
  5. 增量求值依照圖的拓樸順序,在單一一致的來源快照下重新計算 I(Δ)\mathcal{I}(\Delta),並保留其他節點的原有結果。

則增量演算法所得全部衍生值與在新快照 σe+1\sigma_{e+1} 從頭計算的結果相同:

∀v∈Q,qvinc(σe+1)=qvfull(σe+1).\forall v\in Q,\qquad q_v^{\mathrm{inc}}(\sigma_{e+1})=q_v^{\mathrm{full}}(\sigma_{e+1}).

證明

按證據圖拓樸次序歸納。對所有基礎來源 b∈Bb\in B,增量求值使用的新快照值與全量求值完全相同。假設某衍生節點 vv 以前的所有拓樸前驅都已與全量求值一致。

若 v∈I(Δ)v\in\mathcal{I}(\Delta),增量演算法使用與全量算法相同的 fvf_v 及相同的直接依賴值,因此結果相同。若 v∉I(Δ)v\notin\mathcal{I}(\Delta),由閉包定義,沒有任何已變更來源能沿證據依賴邊抵達 vv ;再由假設 2–4 的完整性,可知其所有真正依賴值及求值函數都未改變,因而保留原結果與新快照全量重算的結果相同。依有限拓樸歸納,所有衍生節點一致。證畢。

5.1 定理不能被誤讀成什麼

這個定理沒有證明依賴圖可以從任意 AI 語義自動完整抽取;沒有處理未宣告的資料競態、網路重排序、模型非確定性或分散式共識;也沒有證明重算節點數少就一定運作更快。尤其一些全域閘門的單次求值需掃描全部機體,所以即使它們只算作一個節點,仍可能有隨機體數增加的運算成本。

閉包在保守依賴語義下是自然的重驗集合,不一定是特定函數實例的最小語義重算集合。例如某個求值函數可能對這次修改的數值不敏感,但僅依圖結構尚無法證明它不會改變。

6. 反例一:少登記一條共享能源依賴,局部修復會錯誤通過

構造六台合成載體,每台基線能源需求為 2,全域預算為 16:

Rold=6×2=12≤16.R_{\mathrm{old}}=6\times2=12\le16.

現在把第 3 號載體(由零起算)的能源需求改為 100,其他五台仍為 2:

Rnew=5×2+100=110>16.R_{\mathrm{new}}=5\times2+100=110>16.

完整求值正確地使 gate:energy=FAIL 與 release=FAIL。但是若研究者在證據圖中故意刪除 act:3 → gate:energy 這條依賴,增量演算法就可能保留舊的 gate:energy=PASS;其餘交接與閘門重新求值後仍通過,使 release 錯誤顯示 PASS。

這個反例不是說完整依賴的演算法有錯,而是證明定理的依賴完整性前提不可省略。在真實協同系統中,漏掉共享空間、網路延遲、電池限制、觀察校準或故障共同原因,可能產生同類錯誤;但實體危害程度必須另以實測評估。

命題 6.1|單靠局部契約通過,不足以恢復全域契約

存在有限任務系統,使某台替代機體的新局部契約仍通過,但其替換使共享資源、共同空間或任務期限違反全域條件。

證明。 上述能源需求修改的局部作用若不把共享能源總額納入自身前提,可仍聲稱完成同一個局部動作;但整體需求 110 大於預算 16,故全域不成立。證畢。

此命題是第八篇組合不閉合反例在動態變更場景中的延伸,並非全新的邏輯原理。

7. 事件與修復方案具有不同語義

7.1 已發生事件不可藉拒絕更新而消失

若真實機器人已斷線、相機已損壞或環境已出現障礙,系統收到可信的故障事件時,不能因為新模型無法通過而「回滾資料」並繼續把舊模型視為當前世界。正確流程是記錄事件、更新目前所知狀態、撤回失效的候選通過證據,再進入保守處理或經驗證的恢復流程。

本篇研究程式的 event(delta) 會先將已宣告變更納入當前來源快照,重算受影響證據,讓原 PASS 失效。這只是一個人工模型的狀態更新,不宣稱能真正停下機器人。

7.2 未發生的替代方案可先在隔離快照中求值

候選方案 propose(delta) 不修改當前來源。它在固定的來源版本上模擬替換不同機體配置,並以增量閉包重驗能源、期限、風險、模型誤差及共享空間。如果任何契約失效,方案不得得到通過狀態。

最重要的是,模型內通過仍不同於實體系統已具備可用致動裝置、合法權限與即時安全監控。

7.3 快照版本與舊計畫失效

令候選方案 pp 依據第 ee 版來源快照建立;記錄版本號 ee 與內容摘要 H(σe)H(\sigma_e)。若在提交前來源已變為 σe+1\sigma_{e+1},則本篇保守規則要求舊方案作廢,即使舊資訊表面上似乎仍合適。

commit(p,σe′)=REJECTif e′≠e.\mathrm{commit}(p,\sigma_{e'})=\mathrm{REJECT}\quad\mathrm{if}\ e'\ne e.

這是單機順序模擬的版本檢查規則,不是真實分散式系統的原子提交、兩階段提交或即時保護證明。系統若要部署,必須有可信事件排序、時鐘與時間界、證據來源驗證、真正的並行控制和硬體安全治理。

特別限制: SHA-256 可供檔案內容一致性查核,但若沒有數位簽章、可信來源或其他身份驗證,雜湊本身不等於資料來自真的機器人。

8. 定理二:版本約束下的研究候選重驗不會沿用過期快取

定理 8.1|順序快照版本下的候選重驗一致性

假設第 5 節條件成立;所有事件按順序被應用至研究模型的單一來源快照;每次方案生成保存來源版本,且提交程序先核對版本與內容摘要,再在當前快照重新求值。那麼,當版本不一致時提交被拒絕;當版本相同且方案提交時,產生的衍生結果與在該候選快照上全量重算相同。

證明。 版本不一致時程式規則直接返回拒絕。版本一致時先建立由已確認來源與候選變更形成的快照,定理 5.1 保證此快照的增量求值等價於全量重算。因此若研究契約通過,其通過是對該快照的通過,而不是沿用另一版本的舊值。證畢。

邊界。 此處不證明時鐘在物理時間內足夠快速、不證明傳入事件完整、不證明來源摘要不可遭惡意替換、不證明跨多裝置的原子性。若一個實體事件在證據提交後才被發現,系統仍可能處於未知或危險狀態;本篇不能用版本檢查替代獨立硬體安全層。

9. 共享風險與長程誤差的修復重驗

9.1 邊際風險只允許保守聯集界

令 EiE_i 表示在所聲明任務期間第 ii 段發生危害事件,並假設有可信證據支持其邊際上界 uiu_i:

Pr⁡(Ei)≤ui.\Pr(E_i)\le u_i.

不假定各段獨立時:

Pr⁡(⋃i=1nEi)≤min⁡(1,∑i=1nui).\Pr\left(\bigcup_{i=1}^{n}E_i\right)\le \min\left(1,\sum_{i=1}^{n}u_i\right).

若改變第 jj 段,且有獨立於該改變的有效理由,保證其他各段原有邊際界依舊成立,則可把共享預算 β\beta 對新段保留為:

ujnew≤β−∑i≠jui.u_j^{\mathrm{new}}\le\beta-\sum_{i\ne j}u_i.

這項不等式必須確認右側非負,並由可信證據支持新段風險界。若其他段的風險實際上依賴新段的動作、共享空間或觀測資料,便不能假定其界不變,必須把相應依賴加入重驗閉包。

六段基線每段聲明 ui=0.01u_i=0.01,聯集上界為 0.060.06。若其他五段合計 0.050.05,在全域預算 0.100.10 下,替代段的可用風險上限為 0.050.05 ;若預算為 0.250.25,其上限為 0.200.20。這是指定人工模型的風險預算代數,非實際危害概率估計。

9.2 條件危害的乘積界不得與邊際風險混用

第八篇已證明:若 hih_i 的語義是「先前均未失敗條件下第 ii 段的危害上界」,則可用:

Pr⁡(any failure)≤1−∏i=1n(1−hi).\Pr(\mathrm{any\ failure})\le1-\prod_{i=1}^{n}(1-h_i).

此式不需要額外假設獨立,但需要正確的條件風險語義。如果換掉某台機器人會改變下游的條件分布,舊的 hih_i 未必繼續有效;在未重新建立條件界之前,不能把原有乘積風險數字直接貼到新方案上。本篇實驗僅使用保守邊際聯集界,避免混淆。

9.3 轉移模型誤差亦是全域依賴

沿用第八篇在共同抽象狀態空間下的總變差誤差遞推:

δi≤αiδi−1+ϵi,\delta_i\le\alpha_i\delta_{i-1}+\epsilon_i,

其中 ϵi\epsilon_i 是第 ii 段參考/實際核的行總變差上界, αi\alpha_i 是參考核的收縮係數;它們是否可信必須有獨立的模型證據。若改變中間段,終點誤差即使可藉收縮控制,也不能只重驗局部的 ϵi\epsilon_i 而完全忽略後續組合。

在本篇的人工配置, δ0=0\delta_0=0,所有 ϵi=0.01\epsilon_i=0.01 、 αi=0.5\alpha_i=0.5。六段參考界為:

δ6≤1100∑k=05(12)k=633200=0.0196875.\delta_6\le\frac{1}{100}\sum_{k=0}^{5}\left(\frac12\right)^k =\frac{63}{3200}=0.0196875.

注意:本篇的程式輸入是聲明的係數,沒有實際建構機器人 Markov 核來證明這些係數。它檢查已聲明參數的算術與組合,不能當作物理轉移誤差的獨立驗證。

10. 有限修復策略:可替代不代表必須替代

10.1 合格修復候選的條件

對故障後來源快照 σe\sigma_e,定義候選替代集合 Re\mathcal{R}_e。每個候選 rr 表示對一部分來源契約參數的修改。其研究級合格條件為:

Eligible(r,σe)=⋀g∈Qrequired[g(σe⊕r)=PASS],\mathsf{Eligible}(r,\sigma_e)= \bigwedge_{g\in\mathcal{Q}_{\mathrm{required}}} [g(\sigma_e\oplus r)=\mathrm{PASS}],

其中 Qrequired\mathcal{Q}_{\mathrm{required}} 包含交接、來源有效性、能源、期限、風險、模型誤差與共享空間等全域關聯證據。 ⊕\oplus 只表示在隔離快照中代入候選聲明,不表示真的對機器人下達配置命令。

研究上的候選排序可以加入更小的資源消耗、較少變更節點、較低的已驗證上界或較少必要補觀測;但任何效用排序都不能讓未通過硬性安全與授權條件的方案獲得執行權。

10.2 四種替代方案

在六段人工模型中,令中間載體失效,然後分別考慮:

替代候選 變更內容 研究契約結果 主要原因
high_energy 重新啟用,但需求能源為 100 拒絕 全域能源上界違反
shared_reserved_cell 重新啟用,但獨占格點與另一台重疊 拒絕 全域空間保留衝突
frame_mismatch 使用未配準的不同輸入座標系 拒絕 觀察—作用語義與交接前提不成立
valid_declared_replacement 重新啟用,能源 2,完成時間改為 3,且保持相容 研究模型內通過 所有明示閘門皆通過

通過方案的能源總計為 12,串接期限為 5×2+3+5=185\times2+3+5=18,低於聲明期限 21;各段保留空間互不交疊,風險聯集上界維持 0.060.06,核誤差的聲明界也在限制內。

所謂「有效替代」只相對於這些已聲明的合成契約,並不表示真正有一台具備相同致動能力與校準狀態的實體機器人可以接手。

10.3 沒有合格候選時怎麼辦

此時可以維持 REJECT_OR_HOLD,要求外部證據、重新觀測或經過驗證的安全降級程序。不能僅靠選擇一個更像成功的語言模型回答,便把「缺乏作用能力」轉換成可執行動作。真實安全停機本身也需要物理制動、動量、供電與環境條件支持,本篇沒有證明任何無條件安全停機定理。

11. 實驗設計與獨立驗證路徑

11.1 可窮舉的研究實作

src/repair_core.py 建立有限來源模型與有向無環證據圖;ContractGraph.full 自頭求值,ContractGraph.incremental 僅沿變更閉包重算;EpochStore 提供事件更新、方案隔離模擬與以版本檢查為前提的研究提交;全部風險與模型誤差運算採用 Python fractions.Fraction 的精確有理數運算。

對 nn 台串接載體,本人工圖包含: nn 個觀察證據、 nn 個動作證據、 n−1n-1 個交接證據、5 個全域閘門及 1 個末端研究候選節點。因此衍生節點數為:

N(n)=n+n+(n−1)+5+1=3n+5.N(n)=n+n+(n-1)+5+1=3n+5.

這是人工測試圖的節點計數,並非所有多機體系統普遍具有此結構。

11.2 五個全域閘門

本篇明示檢查能源總額、總期限、邊際風險聯集界、序列總變差誤差界,以及整個任務期間的獨占格點保留。這最後一項是人工簡化的保留空間語義:即使兩台機器人實際可能在不同時間經過同一位置,本篇仍保守要求其任務全程保留區互不交疊;因此它可能拒絕實際可行的協作,也絕不是連續空間中的碰撞驗證。

11.3 比較方法

每一組人工變更都同時計算:

  1. 新來源快照上的完整求值。
  2. 基於舊快照快取與變更閉包的增量求值。
  3. 另一套不依賴求值圖函數的直接算術核對,涵蓋能源、期限、邊際風險、模型誤差、保留空間與交接結果。

獨立稽核選取 n=2,3,4,5,6n=2,3,4,5,6,交叉改變單一載體的啟用、能源、時間、危害上界,以及其觀察通道完整性,共核對 2,160 組有限配置;每一組皆要求三種計算結果一致。這不能驗證未列入的無限狀態模型、任意圖重組或真實機器人。

12. 實驗結果

12.1 增量重驗範圍

載體數 nn 全部證據節點 改變一台中間載體 改變其相機來源 改變共享空間 改變全域時鐘
6 23 9 10 2 23
12 41 9 10 2 41
40 125 9 10 2 125

其中中間載體變更主要涉及自己的作用證據、相鄰交接、五個全域閘門與最終研究候選;來源相機變更還需重新判定自身觀察證據。全域時鐘因參與每個觀察證據的時效判定,能沿全部分支影響所有衍生證據。

重要詮釋: 表內只衡量「求值器節點的重算數量」;共享閘門可能各自執行全域掃描,因此表內 9 對 125 的差異不能直接聲稱為實際運算時間節省 92.8%。

不同載體數下的證據重驗範圍

12.2 證據閉包的實際形狀

六載體模型的單一 robot:3 變更,影響 9 個衍生節點;camera:3 變更影響 10 個;共享空間更新只會直接影響空間閘門與末端候選;而全域時鐘更新影響整圖。

依賴圖重驗矩陣

此圖的白黑標示僅反映研究程式的顯式依賴,不代表所有真實作用隱含依賴已被查明。若空間變更還會影響各機體的路徑可達性或風險界,就應增加這些依賴,不能沿用此人工最小圖。

12.3 四種修復候選的閘門判定

替代方案與全域閘門

三個不合格候選各因不同契約失敗。frame_mismatch 的錯誤還會導致作用本身未通過,因此多個全域閘門同時判為不合格。唯一通過的方案仍只有研究契約狀態,沒有物理授權。

12.4 風險保留量隨替代方案變化

共享風險預算與替代上限

其他五段邊際上界合計 0.050.05 時,替代段與全域風險的保守聯集關係為 uall≤unew+0.05u_{\mathrm{all}}\le u_{\mathrm{new}}+0.05 (並以 1 截斷)。此圖用 0.100.10 與 0.250.25 兩種聲明預算,示範同一替代策略可能在一種任務風險規格下通過、另一種規格下拒絕。

12.5 測試與證據邊界

  • 單元測試:43 / 43 PASS,涵蓋來源變更、全域閘門、錯誤座標、時間過期、模型係數界線、版本錯配、事件與方案隔離、雜湊一致性與故意刪除依賴之反例。
  • 獨立有限配置:2,160 / 2,160 一致,使用不同直接算術實作比對全量與增量求值。
  • 故意漏登記能源依賴:完整求值為 FAIL,缺邊的增量求值錯誤顯示 PASS。這是刻意設計的反例成功,不是演算法通過的安全測試。
  • 版本檢查:在方案形成後把全域時鐘由 1 更新到 7,再提交舊方案,得到 STALE_PLAN_REJECTED。
  • 素材及程式內容:逐檔 SHA-256 與獨立原稿一致性由研究包驗證腳本檢查;不等於學術同行審查或硬體安全驗證。

13. 動態重組、開放世界與未知條件的不可省略邊界

13.1 依賴圖本身改變時,舊閉包不再自動有效

本篇定理假設求值圖的邊與函數固定。如果任務突然新增第三方協作者、新的空間耦合或不同類型的感測通道,便屬圖結構改變。此時若沒有可靠的圖遷移、模式版本與重新驗證證明,應保守視為需要重建相關證據圖。本篇程式只支援在固定證據拓樸上修改來源參數;不實作任意增刪節點後的最小重驗。

13.2 開放世界下不能把未知當作不變

第六篇已指出未知觀察模式可能與已知模式產生相同觀測分布。若因攝影機故障、世界變化或新物理效應,使某個真正影響閘門的條件未被建模,則定理 5.1 的依賴完整性前提失敗。實務上需要將模型失配檢測、異常信任界、要求補觀測與保守拒絕納入來源圖,並在無充分證據時回報 UNKNOWN 或 HOLD;本篇人工程式沒有完整開放世界的三值信念演算。

13.3 語義正確不等於可在期限內重新驗證

某個相機版本可透過數學配準而修復,不表示驗證程序會在機器人需要決策的截止時間前完成。若物理時間已經越過可安全停止或重新規劃的窗口,程式完成後才得到的正確答案也可能不具有行動價值。實體部署必須另外處理真正的最壞執行時間、排程、制動邊界與事件延遲;本篇不把模型內時鐘當作對真實時間的保證。

13.4 共享風險的證據可能隨修改失效

若其他機體的危害上界是以原先載體動作分布為條件估計,替代後不應直接重用。不同載體可能改變共享視覺遮擋、機械負載、碰撞窗口與通信負載。證據圖必須把這些作用因果影響明示為依賴;若尚未能判定,就應標記未滿足,而非把未知當作零風險。

14. 完整度與複雜度評估

14.1 何時增量方法可能具有工程價值

在有良好模組邊界、較少跨域依賴、資料校準來源完整、證據函數可快取且全域約束求值成本可控時,變更閉包可能比整體重算小得多。若每次變更都牽涉全域時鐘、共享場景、不可局部化的物理耦合或頻繁圖結構重寫,增量方法可能節省甚少,甚至因維護依賴與版本證據而增加複雜度。

理論上若求值成本為 cvc_v,一次完整求值成本可記為:

Cfull=∑v∈Qcv,C_{\mathrm{full}}=\sum_{v\in Q}c_v,

而增量求值包含:

Cinc=Cimpact+Csnapshot+∑v∈I(Δ)cv.C_{\mathrm{inc}}=C_{\mathrm{impact}}+C_{\mathrm{snapshot}}+ \sum_{v\in\mathcal{I}(\Delta)}c_v.

只有在 Cinc<CfullC_{\mathrm{inc}}<C_{\mathrm{full}} 且完整性、時效與風險證據皆成立時,才可聲稱該實作具有實質計算收益。本篇沒有對實機延遲或大模型重新推論成本進行測量。

14.2 本篇沒有完成的事情

本篇沒有從任意 AI 模型自動抽取可信完整依賴圖;沒有證明多代理全域安全之完整邏輯;沒有在實體硬體上測得危害機率;沒有建立任何物理操作授權機制;沒有安全證明的併發原子提交或真正分散式故障容忍;沒有假設其合成感測結果可代表螳螂蝦、跳蛛、扇貝或人類的實際神經視覺。這些是結論可適用範圍的清楚邊界,不應由測試通過數字取代。

15. 綜合討論:從統一視覺到可修復的跨載體協作

這個研究系列最早的問題是:一個觀察者所呈現的幾何投影,究竟在何種意義下可代表另一個載體所經驗的世界?後續研究指出,在同一格式的視覺張量下,觀察條件、物理通道、動作可實現性仍可能根本不同;若一味要求將它們合併成單一格式,無法保證世界模型與實體作用的共同正確。

本篇進一步指出:即使找到某段足夠可靠的跨觀察者、跨具身轉譯,也不表示這段連接可以永遠沿用。真正連續運作的協作系統必須能回答:我依據哪些觀察、模型、物理假設和共享限制相信這段作用可以成立;當其中一項條件失效時,我應撤回哪一部分結論,又可以保留哪一部分已驗證的關係?

如此,跨載體接口就不只是一種資料語法,而可能逐步成為版本化的觀察—作用證據網路。但其價值不是讓 AI 擁有不會犯錯的全域世界觀,而是使系統明確指出何時可以局部補正、何時必須重新觀察、何時需要全域重驗,及何時只能保守拒絕。

16. 結論

本篇在限定的無環證據圖與聲明式有限模型中建立以下可驗證成果:

  1. 區分 CACG 的物理作用交接與 CRRV 的證據依賴關係,避免把機體連接圖誤認為完整的驗證圖。
  2. 證明在完整依賴、純求值器及一致快照條件下,僅重算受來源變更影響的後繼閉包,結果與全量重算完全等價。
  3. 以故意漏登記共享能源依賴的反例,顯示不完整依賴會使局部修復錯誤通過。
  4. 將已發生環境事件與未發生候選方案分離,使事件能撤回舊證據,方案則必須在固定版本重新驗證。
  5. 以 43 項單元測試與 2,160 組獨立有限核對,驗證人工模型的重算等價性與基本閘門行為。
  6. 保留「數學研究契約通過」與「真實機器人合法、安全、可操作」之間不可消除的制度及工程界線。

總結命題:跨載體協作的可靠性,不在於每次故障都重建整個世界,也不在於相信局部修復永遠足夠;而在於能夠精確辨別一項變更究竟使哪些既有證據失去成立條件。


參考文獻與來源可追溯性

[E1] Becker, B., & Giese, H. (2008). Incremental Verification of Inductive Invariants for the Run-Time Evolution of Self-Adaptive Software-Intensive Systems. ARAMIS Workshop. https://hpi.de/giese/misc/bibtexbrowser/index.php?bib=publications%2FPublications.bib&key=BeckerGiese08b

[E2] Tran, H.-V., Hung, P. N., Nguyen, V.-H., & Aoki, T. (2020). A framework for assume-guarantee regression verification of evolving software. Science of Computer Programming, 193, 102439. https://doi.org/10.1016/j.scico.2020.102439

[E3] Component-based Distributed Software Reconfiguration: A Verification-oriented Survey. ACM Computing Surveys. https://doi.org/10.1145/3595376

[E4] A contract-based approach to adaptivity. The Journal of Logic and Algebraic Programming, 80(3–5), 180–193 (2011). https://doi.org/10.1016/j.jlap.2010.09.001

[E5] Carwehl, M., Vogel, T., Rodrigues, G. N., & Grunske, L. (2023, arXiv manuscript). Runtime Verification of Self-Adaptive Systems with Changing Requirements. https://arxiv.org/abs/2303.16530

[E6] Mehmood, U., Roy, S., Damare, A., Grosu, R., Smolka, S. A., & Stoller, S. D. (2023). A distributed simplex architecture for multi-agent systems. Journal of Systems Architecture, 134, 102784. https://doi.org/10.1016/j.sysarc.2022.102784

[E7] Bharadwaj, S., Bloem, R., Dimitrova, R., Könighofer, B., & Topcu, U. (2019). Synthesis of Minimum-Cost Shields for Multi-agent Systems. American Control Conference. https://doi.org/10.23919/acc.2019.8815233

[E8] An Efficient Runtime Verification Toolkit for Self-Adaptive Systems Addressing Runtime System Model Changes (2026). IEEE Access, 14. https://doi.org/10.1109/ACCESS.2026.3682704

[E9] A compositional approach to verifying modular robotic systems (2026). Robotics and Autonomous Systems. https://www.sciencedirect.com/science/article/pii/S0921889026003209

系列內部參照: RGC–DPIED-01 v1.1 至 RGC–DPIED-08,尤其 -05(觀察者在線信念)、-06(開放世界失配)、-07(CATC-0.1)與 -08(CACG-0.1)。所有內部參照僅用於研究脈絡;本文的有限算法可由本封裝獨立執行。

附錄 A|研究級接口樣例

研究包提供 schemas/crrv01_event_and_repair_example.json,包含事件後的修復方案、快照版本、證據影響節點與 physical_authorization: NOT_GRANTED。其中版號、雜湊與候選狀態是人工研究協議,不能直接用於控制 ROS 節點或真實致動器。

附錄 B|可重現性與實作命令

請在研究包根目錄執行:

python src/run_experiments.py
python src/independent_audit.py
python -m unittest discover -s tests -v
python src/render_figures.py
python validate_release.py

主要有限模型與測試只需 Python 3.10+ 標準函式庫。重新輸出 PNG/SVG 圖表需要 matplotlib 與 numpy。資料輸出於 results/,圖表輸出於 figures/。

正式交付以原始 UTF-8 Markdown 為準,而非聊天畫面轉譯後的數學顯示;研究包附有逐檔 SHA-256 及原稿分隔符驗證腳本。任何非合成模型的安全聲明均不包含在這些驗證結果內。