title: ARKE-06｜多元研究校驗：形式證明、反例、實驗與證據耦合
english_title: ARKE-06 | Plural Research Verification: Formal Proofs, Counterexamples, Experiments, and Evidence Coupling
series: ARKE Research — AI 原生自主科研完備與知識演化論
series_english: AI-Native Research Completion and Knowledge Evolution
series_id: ARKE
paper_id: ARKE-06
series_part: 第二部：AI 自主查核與雙向知識檢驗
sequence: 6
series_total: 12
author: Neo.K with GPT（AI 協作）
institution: EveMissLab／一言諾科技有限公司
version: v0.1
date: 2026-10-28
timezone: Asia/Taipei
language: zh-TW
status: FORMAL_RESEARCH_MANUSCRIPT_V0.1; THEORY_AND_METHOD_PROPOSAL; EMPIRICAL_VALIDATION_NOT_RUN
document_type: 跨領域研究校驗理論／證據型別契約／驗證方法路由／可否證實驗設計
canonical_source_encoding: UTF-8
canonical_math_delimiters: inline= $...$ ; display=$$...$$
source_verification_cutoff: 2026-10-28
repository_policy: ARKE 為獨立軟體工程規劃；本篇不宣稱 ARKE 引擎已建成或已整合 EveTrain、Lean、數學 AI
license: 作者權利保留；正式授權條款尚未決定

ARKE-06｜多元研究校驗：形式證明、反例、實驗與證據耦合

Q: 19.1 案例 A：一個反例能否代替四十次正面測試？

考慮被過度擴張的主張：

Q: 19.2 案例 B：ETH 類型的演算法突破應如何驗證？

假設有一份研究候選聲稱找到次指數時間 SAT 演算法。即使在很多樣本上求解正確，ARKE 仍需分開建立：

Plural Research Verification: Formal Proofs, Counterexamples, Experiments, and Evidence Coupling

系列： ARKE Research，第 06／12 篇
作者： Neo.K with GPT（AI 協作）
機構： EveMissLab／一言諾科技有限公司
日期： 2026 年 10 月 28 日（Asia/Taipei）
版本與狀態： v0.1，正式方法論原稿；定義、條件命題與實驗協議均已撰寫；ARKE-06 自身跨領域實測未執行。
承接： ARKE-01（受約束研究完備）、ARKE-02（合法來源可達性）、ARKE-03（來源定址）、ARKE-04（先例查核）、ARKE-05（跨表示比較）。
後續： ARKE-07（雙向知識修正）、ARKE-08 至 ARKE-12（歸屬、演算法、知識演化、發表閘道與跨領域實證）。

版本： v0.1

摘要

當 AI 能自行生成數學證明、計算演算法、實驗假說與理論模型時，研究校驗不應退化為「有沒有通過 Lean」或「一個工具回傳 PASS」。形式證明可以在指定形式語言與假設下檢查推導，卻不自動確認研究命題忠實對應原問題、文獻新穎性、實驗適用域或物理實在；反例能在適當條件下推翻全稱命題，卻不代表對全部關聯理論完成總結；計算重播、統計檢定與實驗重複各能提供不同種類的證據，不能相互替代。若 AI 將這些不相容的證據全部合併成單一「可信度」或以多個相關來源當作多次獨立確認，反而可能放大錯誤。

本文提出 多元研究校驗與證據耦合契約（Plural Research Verification and Evidence Coupling Contract，PRVECC），將研究校驗定義為一項由主張型別、成立域、量詞、信任基礎、可用資源、合法權利、證據角色與停止條件共同約束的 AI 自主工作。其核心不是用多個工具「投票」決定真理，而是讓 AI 對每個研究主張明示應由哪一類證據支持、可用哪些方法反駁、哪些工具能檢查哪一段義務，以及哪些結果仍只能列為 UNKNOWN、BLOCKED 或 NOT_RUN。

本文建立研究主張與驗證義務的有型別模型、形式證明的語義橋與公理信任界線、反例搜尋及反模型有效性、演算法的正確性與複雜度雙重檢驗、經驗研究的測量與統計限制、因果與物理模型的適用域契約、可回訪的證據依賴結構，以及避免證據重複計數的獨立性檢查。本文給出十項條件命題或反例論證，並設計八組可否證實驗，評估相對於單一驗證器、單一分數與無型別多 Agent 共識的實際改善程度。

本研究尤其主張：AI 應自行執行其目前能力足以支持的常規科研校驗，不把人類專家視為每一輪基本校驗的必經節點；但也不將尚無證據支持的 AI 判斷當成已通過獨立驗證。本篇不聲稱已建成萬用科學真理判定器、不宣稱每一個研究問題均能演算法決定，也不把研究程序完成混同於任何世界下的絕對正確。本篇所有 H1–H8 實證均為 NOT_RUN。

關鍵詞： ARKE、多元研究校驗、形式證明、反例搜尋、模型檢查、實驗重播、獨立複現、統計不確定性、證據耦合、AI 自主科研、證據依賴、驗證路由、研究完備、雙向知識演化。

0. 研究地位、主張型別與術語邊界

0.1 D／P／N／M／H／B 的分型

本篇遵循先前研究系列對論述的明確分型：

標記	意義	必要證據或限制
`D`	Definition，本文提出的形式定義	固定型別、欄位、作用域及語義
`P`	Proposition，條件命題／邏輯反例	明列前提，提供論證或構造
`N`	Normative Principle，研究程序規範	說明理由、成本與適用界線
`M`	Method Proposal，尚待工程實作的方法	可追溯流程、輸入輸出及阻擋條件
`H`	Empirical Hypothesis，需以研究資料驗證的假說	可否證、保留集、對照與評分契約
`B`	Boundary，不能由證據推出的結論	反例、無法判定或尚未驗證

本文所稱「條件命題」是理論契約的結構結果，不是聲稱在 Lean 中已完成其機器證明。除有實際重播工件及版本化證據外，本文不宣稱方法已通過工程測試。

0.2 不應把所有 verification 翻成同一種「證明」

本篇區分：

Formal proof checking（形式證明檢查）：依形式系統確認證明項是否符合指定命題。
Program verification（程式驗證）：檢查實作對規格的契約、性質或行為。
Falsification／counterexample（否證／反例）：給出足以排除特定主張的合法反例或反模型。
Computational reproduction（計算重現）：相同資料、程式及條件下重算結果。
Independent replication（獨立複現）：以新資料、新研究或獨立條件檢查相同問題是否取得一致結果。
Empirical validation（經驗有效性檢驗）：評估資料與方法是否支持聲稱的現實關係或預測。
Prior-art verification（先例查核）：查證某項成果是否已有歷史提出、方法先例或既有證明。

本文在計算重現／獨立複現上採用美國國家科學院 2019 年報告的區分；各學科可能另有術語使用習慣，正式契約應載明所用版本 [5]。

0.3 本篇不是單一萬能驗證器的提案

問題不在於證明器、實驗或搜尋工具誰「比較高級」。在不同研究對象中，它們回答的是不同問題。把研究主張 $c$ 的某一種義務通過誤寫為全研究完成，是典型的型別錯誤。

本文主張：

\mathrm{CheckPassed}(c,v,\Gamma) \not\Rightarrow \mathrm{ResearchComplete}(c,\Gamma).

其中 $v$ 是指定校驗方法， $\Gamma$ 是研究契約。此非蘊含並不貶低 $v$ 的價值，而是要求明確指出其支持範圍。

1. 問題背景：從「證明通過」到「研究有適當證據」

1.1 三種經常被混合的成功

假設 AI 宣稱提出一項新成果。至少可以區分：

推導成功：某個形式證明器接受指定推導，或一個計算檢查器輸出一致。
研究有效性成功：經過與主張相配的測量、對照、反例及適用域檢查後，可支持一個有範圍的科學結論。
知識貢獻查核成功：已對照先例、方法、既有錯誤及引用歷史，能說明相對於舊知識的增量。

三者可同時成立，也可以彼此獨立。某項數學命題的形式證明可成功，但已有百年前的證明；某項物理數值模擬可完美重現，但仍不具備實驗代表性；某位歷史研究者很早提出一項猜想，但其證明未必可靠。

1.2 AI 的科研工作不應只擅長生成

ARKE-01 主張，AI 應在宣稱完成前自主履行基本查核義務。這不是額外發明人類沒有做過的研究步驟，而是將既有科研實務中的確認、比較、反駁、重播、統計與來源記錄內建於 AI 工作流程。獨立模型的輸出可以充當候選推理或查核線索，但如果多個模型讀取相同材料並共用同一錯誤，不能以模型數量直接增加證據強度。

1.3 形式系統的精密性與研究世界的開放性

Lean 具有小型核心、證明項與公理依賴檢查機制，適合處理其可表述的形式命題 [1–3]。然而，形式聲明的符號可能與研究者原來要回答的現實問題發生錯置。Lean 官方文件也要求審查依賴公理與形式聲明的意義；某些 sorry 產生的公理可讓未完成的推導通過部分表面顯示，故必須進行公理稽核 [2,3]。

反過來，數學以外的許多成果依賴現實測量、外部資料與因果設計，不是把文字寫成公式就能證成。將多種驗證路線視為互補而非彼此替代，是本篇的出發點。

2. ARKE-01 至 ARKE-05 的正式接口

2.1 承接 ARKE-01：研究完備契約

ARKE-01 將研究契約定為：

\Gamma=\langle\mathcal U,\mathcal S,\mathcal A,\mathcal V,\mathcal B,\tau\rangle.

其中 $\mathcal U$ 是可達來源， $\mathcal S$ 是搜尋策略， $\mathcal A$ 是合法操作與權限， $\mathcal V$ 是可用的驗證方法， $\mathcal B$ 是資源預算， $\tau$ 是契約要求的證據與公開宣稱門檻。

本篇對 $\mathcal V$ 的校驗語義提出深化，而不是另造取代 $\Gamma$ 的總契約。ARKE-01 的硬性義務狀態維持：

\sigma(o,\pi)\in \{\mathrm{PASS},\mathrm{FAIL},\mathrm{UNKNOWN},\mathrm{NA}\}.

這套四值輸出是整體研究義務的聚合層。本文另定義更細的驗證動作狀態，並明確給出向上投影規則。

2.2 承接 ARKE-02：來源與實驗材料的合法可達性

在資料來源 $w$ 、使用操作 $u$ 與時間 $t$ 下，ARKE-02 有：

\mathcal R(w,u,t)\in \{\mathrm{ALLOW},\mathrm{DENY},\mathrm{UNKNOWN}\}.

即使來源可見，也不能直接推定允許下載、建立 embedding、訓練或重新發布。ARKE-06 要求驗證器合法取得必要證據；不能因為需要反例或獨立複現，就繞過存取權與來源政策。

2.3 承接 ARKE-03：可回訪的研究證據地址

ARKE-03 定義 Research Trace Anchor（RTA）：

A=\langle w,v,m,\ell,\sigma,h,t,\rho,\pi\rangle.

其區分作品、版本、載體、片段、主張與證據。ARKE-06 要求每一項影響判定的證據，盡可能引用可回訪的 RTA；不可將「已找到論文網址」誤當成已確認其中特定定理的證明完整性。

2.4 承接 ARKE-04：先例的存在鏈與有效性鏈

ARKE-04 已區分「先前有人聲稱」與「先前已經證明」。ARKE-06 將其延伸為：先例有效性須走相應的校驗型別；無效的早期證明仍可能構成重要的歷史先例，不應被默默刪除。

2.5 承接 ARKE-05：跨表示比較見證

ARKE-05 區分 FORMAL_DERIVATION、FINITE_EXHAUSTIVE、COUNTERMODEL_OR_TRACE、EMPIRICAL_EVIDENCE 等見證；它也明確區分 CANDIDATE 與 CHECKED_RELATION，以及 BLOCKED 與 NOT_RUN。

本篇不修改跨表示同一性的語義，而是使其比較結論可由適當驗證方法檢查。兩篇研究「命題相似」時，仍要看正式定義、假設、量詞、成本及資料是否相容。

3. D1：有型別的研究主張物件

3.1 不把一篇論文當作只有一個主張

一篇論文可能同時包含：定義、數學定理、演算法效率、實驗效果、物理詮釋、歷史首次性、因果解釋與治理建議。它們彼此有依賴，但不能接受相同的驗證程序。

定義主張物件：

C=\langle i,k,\varphi,D,A,Q,T,O,F,P\rangle.

其中：

$i$ ：主張的穩定識別碼；
$k$ ：主張型別（claim kind）；
$\varphi$ ：明確主張內容，可以是公式、程式規格或自然語言命題；
$D$ ：成立域、數量尺度、時間與任務身分；
$A$ ：前提、測量假設、外部資訊及必要依賴；
$Q$ ：量詞與全稱／存在／機率／經驗聲稱；
$T$ ：原始證據與研究產物之定位；
$O$ ：對此主張必須完成的檢驗義務；
$F$ ：可使主張被否定或被降階的條件；
$P$ ：此主張的來源、修訂與審核歷程。

上式是本文的概念物件，不是宣稱目前已有可通行所有學科的標準資料結構。

3.2 主張型別的最低集合

K=\{K_{form},K_{alg},K_{impl},K_{emp},K_{causal}, K_{phys},K_{hist},K_{norm},K_{mixed}\}.

型別	典型主張	主要證據義務
`FORMAL`	在前提下某定理成立	公理、形式化一致性、有效推導
`ALGORITHM`	對所有合規輸入正確且有上界	任務正確性、資源計算模型、上界證明
`IMPLEMENTATION`	程式碼遵循規格	測試、靜態檢查、形式契約或重播
`EMPIRICAL`	觀測效果或預測存在	測量、樣本、估計、偏差與不確定性
`CAUSAL`	干預造成特定效應	因果識別、混雜控制、設計與反事實限制
`PHYSICAL`	模型符合某物理範圍	單位、尺度、校準、獨立實驗、外部有效性
`HISTORICAL`	某研究最早提出某結果	版本、時間與原始先例證據
`NORMATIVE`	某種研究制度應被採納	價值前提、適用情境、權衡與可反駁的後果預測
`MIXED`	同時涉及多種上述主張	拆分成可檢驗的子主張與依賴

即使同一段文字使用多個型別，實作也不得讓某一類型的 PASS 自動提升其他類型。

3.3 混合主張分解

例如「這個演算法在現實物理模擬上速度提高 30%，因此證明某物理定律」至少包含：演算法輸出等價、執行效能、實驗設計、物理量測、模型與實在對應，以及因果或理論推論。若未拆分，單一 benchmark 的 PASS 可能偷渡成物理理論的真值證明。

本文規範：

C_{mixed}\rightsquigarrow\{C_1,\ldots,C_r\}

但拆分應保留原始段落、作者原意與各子主張的邏輯關係；不能靠拆分偷換命題。

4. D2：主張—方法—證據三元契約

4.1 驗證不能只記錄工具名稱

對主張 $C$ 、可用方法 $v$ 與證據 $e$ ，定義相容關係：

\mathrm{Fits}(C,v,e\mid\Gamma) \in\{1,0,?\}.

1 表示在已記錄前提下， $v$ 的輸出可以處理主張的一項具體義務；0 表示型別或適用域不相容；? 表示缺少資訊。此函數只是方法適用性判定，不是聲稱 $C$ 已經被驗證為真。

例如：

Lean 內核可檢查指定形式證明項；不直接提供文獻學術首次性的證據。
反例搜尋能否定某個精確的全稱命題；找到「疑似反例」時須排除模型抽象假象或規格翻譯錯誤。
統計檢定能在模型假設與樣本設計下提供觀察證據；單獨一個 $p$ 值不是物理法則或因果效果的證明 [6,7]。
來源引用鏈能確認某內容的公開先後；不會自行證明引文中的定理有效。

4.2 校驗動作的明確輸入與輸出

V=\langle c,o,v,I,\kappa,E,s,t,\eta\rangle.

$c$ ：被檢查的主張 ID；
$o$ ：要處理的具體研究義務；
$v$ ：方法、工具、模型及其版本；
$I$ ：已凍結輸入、測試樣本、方法規格及來源錨點；
$\kappa$ ：信任基礎、假設與方法限制；
$E$ ：原始輸出與可重播證據；
$s$ ：本次動作狀態；
$t$ ：執行與觀察時間；
$\eta$ ：環境與計算資源使用紀錄。

驗證動作 $V$ 的狀態不是整篇研究的真理值：

s\in\{\mathrm{PASS},\mathrm{FAIL},\mathrm{UNKNOWN}, \mathrm{BLOCKED},\mathrm{NOT\_RUN}\}.

FAIL 可表示該義務有反例、測試失敗或前提違反，但必須另列失敗類型；不能不問原因就寫「命題被證偽」。BLOCKED 是權限、來源、工具或環境限制，不是數學上的假。NOT_RUN 是未執行。三者不可混同。

4.3 證據角色與可支持範圍

每個 $e$ 另需保存：

\mathrm{Role}(e,C)\in \{\mathrm{supports},\mathrm{refutes},\mathrm{qualifies}, \mathrm{context},\mathrm{unknown}\}.

context 表示有助於理解主張，不等於支持其真實性。qualifies 表示限制成立域、測量誤差或前提，未必直接否定主張。refutes 必須記錄反例如何落在被宣稱成立域之內，並確認見證可重播。

4.4 證據不具自動跨型別遷移權

對某個驗證動作，應標出其保證範圍：

\mathrm{Guarantee}(V)=\langle k,D,A,Q,o\rangle.

任何對外宣稱 $c'$ 若超出此範圍，便需要新的校驗義務。這相當於把「證據能說什麼」變成一個可檢查的型別契約。

5. N1：主張驅動，而不是工具驅動的驗證路由

5.1 問題先於驗證器

AI 應先辨識：這是全稱數學陳述、演算法正確性、實例性質、統計結果、物理觀測、因果主張，還是歷史學術歸屬？然後才選擇最適當、當下合法且可支付的驗證方法。

不應先決定「所有研究都用 Lean」，再要求現實世界的所有問題被勉強投影成 Lean 可檢查的語句；也不應因為單項 Lean 形式化成本高，就將所有研究驗證降為純 LLM 意見一致。

5.2 驗證路由的三種輸出

每一條路由至少有：

Primary route：對該主張能給出最直接支持或否證的檢查。
Independent challenge：相對獨立的反例、替代測量或另一方法，用來發現錯置和脆弱前提。
Scope／provenance audit：來源、版本、適用域與未決資訊的查核。

這不是說三條路線每一項研究都必須同時跑滿，而是要根據主張風險和明確的發表門檻，規定哪些屬硬性義務、哪些可以保留待辦，並在拒絕強宣稱時給出原因。

5.3 否證優先不等於永遠只找反例

若候選是全稱命題，對已凍結的成立域進行低成本反例搜索，可能很有效率；若找到合法反例，可以立即拒絕該全稱主張。但找不到反例並不能立即證明全稱成立，反例搜索不應被無限延長以取代應有的正面證明。

5.4 節制的成本優化

令可用合法驗證動作集合為 $\mathcal V_{adm}$ ，其資源成本為向量 $\mathbf c(v)$ ，預算上限為 $\mathbf B$ 。可行動作滿足：

\mathbf c(v)\preceq\mathbf B.

若某種預先註冊的驗證收益估計函數為 $g(v)$ ，可在候選中選擇效率較高者，但不能把未經校準的 $g(v)$ 當作「真理機率」。特別是無窮持續生成低品質檢查並不構成更強的證據。

6. M1：形式證明校驗（Formal Proof Checking）

6.1 形式化完成的最低四項必要條件

對於被聲稱已形式驗證的數學主張，應分離：

Statement alignment：形式命題與原研究語義、假設、量詞及成立域相符。
Kernel／checker acceptance：指定版本的可信檢查器確認其推導項合法。
Assumption／axiom audit：依賴何種公理、非可建構假設、外部計算結果與未完成推導均可列示。
Artifact reproducibility：原始碼、依賴版本、建置命令及結果可重播，或明確說明不可重播原因。

只有第二項通過，不能自動將其升格為全部四項都通過。

6.2 Lean 的信任與公理界線

Lean 官方文件指出：形式證明由小型核心檢查，使用者可以用 #print axioms 列出定理的依賴公理；sorryAx 代表未完成推導依賴，新增任意公理可能破壞系統可靠性；某些 native evaluation 路線還引入超出小核心的信任 [1–3]。

因此 AI 不能只讀取 UI 的成功圖示，就宣稱論文所有問題均得到嚴格證明。至少需保存：

形式命題文字及其所在版本；
核心與庫版本／鎖定摘要；
驗證執行與輸出；
公理清單及非標準公理理由；
定義及建模所對應的自然語言主張；
尚未形式化的引理、外部計算與詮釋部分。

6.3 無須強制所有數學研究立即形式化

某些研究階段旨在尋找猜想、局部反例、構造思路或確定正確的假設域；立即要求整篇 Lean 形式化可能成本極高，甚至妨礙候選方法探索。本文不主張從研究開始就把全部計算資源用在形式化上。

但當研究明確宣稱形式證明已完成時，該宣稱本身必須符合形式校驗義務。若尚未完成，可以發布 PROOF_CANDIDATE、CHECKED_IN_SUBDOMAIN 或 FORMALIZATION_NOT_RUN 等如實狀態。

6.4 形式正確不代表非平凡性

假設背景理論在所採邏輯下不一致，使用爆炸原理的形式證明即使成功，也可能只反映公理或前提的矛盾。對於存在性或優化問題，還可能發生 vacuous truth、空集合、無效域等錯置。

若研究聲稱的是具有實際內容的存在性或一般性結論，必須提出背景相容性、非空域或非平凡性義務；不以單純的核心接受代替科學理解。

7. M2：反例、反模型與有限窮舉

7.1 全稱主張的反例位置

對精確全稱主張：

\forall x\in D,\ P(x),

若找到可由受信查核程序確認的 $x_0$ 且：

x_0\in D\land\neg P(x_0),

即可否定這一條指定形式與成立域的全稱主張。反例的效力來自量詞與域的邏輯，而非反例來源是否知名。

7.2 疑似反例不等於有效反例

搜尋結果若來自抽象模型、近似數值、可疑文獻翻譯或有誤解析器，需要做 witness validation。CEGAR 方法已示範抽象模型可能產生 spurious counterexample，需檢查其是否對應真實系統，再決定精化抽象 [4]。

對研究 AI，反例工件至少包含：輸入或世界狀態、命題適用域、檢查器、解析度與精度、重播方式，以及其對原主張的反駁方向。

7.3 有限窮舉的明確邊界

如果已知 $D$ 是完整而有限的集合，且對每項 $x\in D$ 均成功檢查 $P(x)$ ，則可以在該有限域內建立全稱結論。但對任意無限域的前 $N$ 個樣本成功，無法推出整個無限域成立。

\forall x\in D_N,\ P(x) \not\Rightarrow \forall x\in D_{\infty},\ P(x).

除非額外存在已證成的歸納、單調或規約證據，否則不能偷渡此推論。

7.4 模型檢查與 SMT 的完成邊界

形式模型檢查、SMT 求解或有限狀態檢查，可以依特定理論、編碼與模型給出有用的 SAT／UNSAT 結果或見證。但對高風險研究，AI 應保存求解器版本、編碼、使用的量詞／理論片段、資源限制，以及必要時的可檢查證書。UNKNOWN、逾時與近似抽象均不可寫成 UNSAT。

8. M3：演算法正確性與複雜度聲稱的雙重校驗

8.1 「程式跑得出來」不等於「演算法有證明」

對演算法主張，至少分離：

C_{alg}=C_{sem}\land C_{correct}\land C_{cost}\land C_{model}.

其中：

$C_{sem}$ ：實作所解的是同一任務，而非改題後的替代問題；
$C_{correct}$ ：對契約輸入的輸出正確性；
$C_{cost}$ ：時間、空間、前處理、建置與外部資訊的成本界限；
$C_{model}$ ：複雜度分析所用運算模型與資源量測可追溯。

例如，有限多組 SAT 實例成功，不等於對所有公式證成次指數最壞情況上界。

8.2 正確性與上界應由不同義務支持

某一程序可總是得到正確解，卻仍需要指數時間；也可能在測試案例中極快，但隱藏了預計算或僅對特定分布有效。程序的 correctness 與 complexity 不能用同一個 benchmark 分數涵蓋。

對每個可比較演算法，至少記錄：輸入編碼、長度參數、所允許 oracle／advice、隨機性來源、誤差容忍、最壞／平均／攤銷概念、成本單位、輸出證書與計算環境。

8.3 反例對演算法主張的不同作用

對聲稱「永遠正確」的演算法，找到一個合規輸入回傳錯誤即可反駁。對聲稱「所有 $n$ 具有某時間上界」的演算法，觀察一個大型慢案例一般不足以否定帶有未知常數的漸近上界，除非可以推導出違反其全部合法常數或固定顯式界限的證據。

因此，反例的型別與其被反駁的主張型別必須一致。

8.4 計算重播與獨立演算法驗證

獨立重播可以發現實作錯誤、環境依賴、資料預處理、結果錯誤標記與性能偏差；它本身不能取代無限輸入的上界證明。對使用 GPU 的模型訓練，應把 CUDA／驅動／張量函式庫版本、隨機種子、資料摘要、模型權重、訓練流程與檢測方式獨立記錄。

這與 EveTrain 現有的凍結 RunSpec、Grant、重新載入驗收等工程規則相容，但本文不宣稱已執行任何新的 EveTrain 訓練。

9. M4：經驗研究的測量、統計與再現性

9.1 研究不是只問數字能否重算

一個經驗命題可能寫成：「在指定樣本與條件下，方法 A 的效果優於方法 B」。即使研究者提供程式、資料和統計結果，仍須問：

樣本如何選取，排除哪些群體或條件？
測量工具是否測得研究者真正欲宣稱的量？
有無選擇性報告、資料洩漏或多重比較？
信賴區間、效果量、樣本數與不確定性是否被完整呈現？
當研究轉移到另一時間、地點或資料分布時，結論是否仍受支持？

美國統計學會的聲明反對只用一個 $p$ 值門檻作為科學結論的全部依據；NIST 的量測規範要求對結果與不確定性採取明確而可追蹤的說明 [6–8]。

9.2 測量與主張域必須綁定

令觀測資料為 $D_{obs}$ ，測量規則為 $M$ ，欲推論的母體／情境域為 $D_{target}$ 。研究結果的有效性不能僅由：

\widehat\theta=f(D_{obs},M)

推出，而必須檢查樣本機制、測量偏差、統計模型與 $D_{target}$ 是否相容。即使數值完全重現，也不能保證外推到未取樣情境成立。

9.3 不確定性不是可被刪掉的註腳

對有統計性測量誤差與系統性不確定性的結果，ARKE 至少需保留：估計量定義、單位、區間或其他不確定性表示、選定模型、校準方式、資料品質，以及推論所依賴的假設。

當研究沒有足夠資訊量化不確定性時，應記為 UNCERTAINTY_NOT_ESTIMATED，而不是填入虛構的信賴度。

9.4 計算重現與獨立複現

美國國家科學院 2019 年報告明確區分：使用相同資料、計算方法及分析條件取得一致結果的計算重現，與透過新的資料取得相容結果的獨立複現 [5]。因此：

\mathrm{ComputationalReproduction} \not\Rightarrow \mathrm{IndependentReplication}.

兩者都可能有價值，但後者包含額外資料與研究設計上的獨立性要求。Open Science Collaboration 在 2015 年對心理學研究的多項複現結果提醒我們，原始研究中的顯著結果並不保證獨立研究能取得同樣結論 [9]。本文引用該研究作為方法論先例，不是宣稱所有學科具有同樣複現率。

9.5 預註冊與事後探索

AI 可以大量產生探索性分析，但若反覆嘗試後只公開最成功的一項，就容易製造選擇性報告。應分別保存：

PREREGISTERED：在查看結果前凍結的主要分析與停止條件；
EXPLORATORY：資料查看後提出的新問題、指標與模型；
CONFIRMATORY_REPEAT：在獨立保留資料上檢驗探索結果。

後驗探索不應一概視為無效；問題在於是否將探索性結果偽裝成事前指定的確認性證據。Cochrane 的 RoB 2 架構亦明列缺失結果、測量偏差與選擇性報告等風險 [10]。

10. M5：因果主張與反事實驗證

10.1 相關性不自動等於因果性

若研究以 $X$ 、 $Y$ 的共同變動主張「改變 $X$ 造成 $Y$ 」，則必須確認可識別的介入、因果結構或其他有力的識別假設。僅取得高相關係數，不能自動為因果命題通過硬性義務。

以潛在結果記號示例：

\Delta_{causal}=\mathbb E[Y(1)-Y(0)].

研究能否辨識此量，取決於處置指派、混雜、缺失資料、測量以及研究模型等條件，不能因為寫出公式就聲稱已得到它。

10.2 三種不能混用的資料情況

Randomized intervention：在合理隨機化及執行符合協議的情況下，可降低部分混雜風險，但仍需檢查遵循、缺失與結果測量。
Observational study：可以提供關聯或在額外識別假設下支持因果估計，但需顯示假設與敏感性。
Simulation／counterfactual model：可展示某模型條件下的情境反應，但不能自動取代真實世界干預證據。

跨域 AI 若將三者輸出看成同一種 EMPIRICAL_PASS，便可能把模型內真實誤寫成現實因果真實。

10.3 因果證據的最低契約

至少保存：處置／暴露定義、結果測量、受試群體、研究時間、混雜或干預機制、識別假設、失效條件、估計方法、敏感性與異質性分析，以及對應可回訪的資料與研究版本。

N2（因果不得偷渡）： 若一項研究尚未有因果識別的合格依據，AI 可以發布其相關性、預測性或模型內情境結果，但不能自動升格為一般因果結論。

11. M6：物理與工程研究的多尺度校驗

11.1 數學模型成立與物理世界成立不同

一個微分方程的解存在，不代表方程完整刻畫所研究的物理世界；一個數值求解器收斂，不代表輸入的物理模型正確；一項模擬在一批資料上擬合良好，也不保證它能預測尚未測量的情況。

因此對物理或工程主張，本文區分：

V_{math},\quad V_{numerical},\quad V_{model},\quad V_{physical}.

$V_{math}$ ：在指定形式前提下的推導或存在性；
$V_{numerical}$ ：離散化、求解器、截斷誤差、數值穩定性；
$V_{model}$ ：物理參數、邊界條件、理論理想化、模型尺度；
$V_{physical}$ ：與校準／留出實驗觀測的對應及不確定性。

四者有關聯，但不能彼此替代。

11.2 校驗與不確定性量化（VVUQ）

工程模型的可信度評估已有 Verification、Validation、Uncertainty Quantification 等研究實務。NIST 2026 年一份報告也討論了如何以風險為基礎統合計算模型校驗、測量學和不確定性方法 [11]。ARKE 應承接這些已有方法，而非宣稱多元校驗的概念是由本系列第一次發明。

11.3 單位、尺度、邊界與模型版本

物理研究中的差異不一定是公式錯誤，也可能來自：

單位制、常數約定與非量綱化不一致；
實驗儀器校準與資料轉換；
微觀、介觀、宏觀模型的尺度不可直接互換；
邊界條件或外力在不同實驗下改變；
理想化條件在真實設備上不可達；
模擬器或數值求解版本差異。

若一項物理命題只對特定域 $D_0$ 有證據，AI 不應默認將它外推到更大的 $D_1$ ：

\mathrm{Supported}(C\mid D_0) \not\Rightarrow \mathrm{Supported}(C\mid D_1).

11.4 不能用「形式化成功」排除實驗衝突

當模型的數學推導與可靠實驗發現衝突時，應檢查兩者的成立域、實驗誤差、模型理想化、前提與外部因果。不能因為某一部分有形式證明就宣布實驗數據必錯；也不能因單次測量差異就否認整套數學內部推導。

12. M7：來源、語義與歷史先例的驗證

12.1 歷史證據有自己的驗證型別

對「某項演算法在 2021 年已有公開主張」的歷史命題，合適證據是可核查的版本時間、作者與原始文本。對「當年已經正確證明」的強命題，則還需獨立檢查原研究的證明或實驗。

兩者應保持分離：

\mathrm{HistoricalClaimFound} \not\Rightarrow \mathrm{HistoricalResultValid}.

而新研究通過某形式工具，亦不代表它在歷史上首次出現。

12.2 語義比對自身也有失敗可能

ARKE-05 的 CRRIC 需要共同的比較契約。研究文獻常有不同術語、符號、資料欄位或數學模型；若翻譯錯誤，兩個表面相同的命題可能並不等價。故研究校驗應先確認比較目標與翻譯，而不是拿文字相似度給出「先例已驗證」結論。

12.3 來源歷史不應只依據最新版本

原研究可以在後續修訂中撤回、修改假設或新增證明。AI 應保留舊版引用的歷史事實，又要標記其當前有效性可能已改變。此處使用 ARKE-03 的 RTA 及來源版本定址，並預留 ARKE-07 的歷史修訂接口。

12.4 歷史不完備時的誠實陳述

如果只能找到一篇早期論文的摘要，而無法合法取得完整證明，AI 可以說「有此先例主張」，但不應說「該證明已被核實」「該成果與新成果在方法上完全相同」。來源無法取得與證明已被反駁，亦是不同狀態。

13. D3：證據耦合圖與可追溯依賴

13.1 證據之間不是無序投票

將某項研究的校驗歷程表為有型別的依賴結構：

G_E=(N_E,R_E).

節點至少可包含：研究主張、來源錨點、證據工件、校驗動作、方法契約、版本化資料、反例、未決問題。邊至少可表示：支持、反駁、修正、來源衍生、方法依賴、工具依賴、共享資料與取樣依賴。

本篇不預設實作必須使用 RDF、圖資料庫、關聯式資料庫或特定 AI 原生圖；上述是研究語義結構，底層實作可替換。

13.2 三種證據依賴必須明示

Logical dependency：某證明或結果依賴另一個已凍結的假設、定理、引理或規格。
Data dependency：兩份實驗結果使用相同或重疊的資料、標註、測量程序或前處理。
Operational dependency：不同 Agent 使用同一模型、工具、檢索來源、權重或共享錯誤的校驗器。

即使三個 AI 獨立輸出「我同意」，只要共用同一錯誤前提，也不能自動視為三份獨立證據。

13.3 證據的二階依賴

一項研究推論可能使用：

e_1\rightarrow e_2\rightarrow C,

例如原始測量經轉換形成統計估計，再形成研究結論。若 $e_1$ 有資料污染， $e_2$ 的計算可以完全正確，但仍無法保證 $C$ 有效。

因此，每一個 PASS 應記錄其依賴閉包中哪些假設已檢查、哪些仍未知。W3C PROV-O 的 Entity、Activity、Agent 與 derivation 關係，可作為既有來源追蹤標準的參考，而非將每條依賴邊都強行當作引用 [12]。

13.4 支持與反對可以同時存在

允許在同一研究主張節點上同時存在支持證據與反對證據。系統不應因為一方分數較高就自動刪除另一方，而要檢查雙方的型別、成立域與可信條件。

例如，一個模型在 $D_1$ 有強支持，在 $D_2$ 發現合規反例，合理結論可能是：原先全域主張失效，但在 $D_1$ 的局部結果仍成立。這不是「多數決」，而是理論成立域的重新定位。

13.5 無法完全序列化的判斷應保留可查核摘要

某些物理現場觀測、人類主觀知覺測量或第三方授權內容不能完整上傳。此時可保存合法的 metadata、內容地址、權利狀態、有限的檢查結果與未決理由；不得假裝已保存原始全部證據。

14. D4：證據獨立性與重複計數防護

14.1 獨立性不是「由不同 Agent 說出」

對兩份證據 $e_i,e_j$ ，定義依賴描述：

\delta(e_i,e_j)=\langle d_{data},d_{method},d_{source},d_{model},d_{process}\rangle.

每項分量可以記 INDEPENDENT_SUPPORTED、SHARED 或 UNKNOWN。不在沒有資料時擅自將它們換算成相關係數。

14.2 兩份報告也可能是一份資料

例：同一實驗資料被轉製為 CSV 與 JSON，再由兩個模型各自分析並同意一個結論。這可以增加對計算實作無誤的信心，但通常不能像兩次真正獨立抽樣那樣增加對母體效果的證據。

若把它們當作兩次獨立重複，就會高估證據量。反之，不同分析器對同一資料得出不同結論，也可能揭露資料處理或模型規格上的重要問題。

14.3 一般的證據加總公式需要前提

若有人試圖以：

S(C)=\sum_i w_i s_i

直接表示某主張可信度，至少應說明 $w_i$ 如何取得、 $s_i$ 的尺度是否可比較，以及各證據依賴如何處理。沒有這些條件，數值 $S(C)$ 並無自動的機率詮釋。

本篇初版不引入全領域通用的「真理分數」。建議使用可稽核的分層證據與義務狀態，必要時在某個已明確校準的統計子問題內，才使用合法的定量推論。

14.4 不同方法能有互補價值

獨立的定理證明、演算法的差異測試、對核心假設的反例搜尋、留出資料上的實驗與來源歷史查核，可能檢查不同的失敗模式。其價值來自覆蓋不同義務，不是把不同工具當作票數越多越好。

15. D5：校驗動作狀態與整體研究義務的映射

15.1 兩套狀態是不同層次

ARKE-05 的驗證／比較動作可有：

\sigma_V\in\{\mathrm{PASS},\mathrm{FAIL},\mathrm{UNKNOWN}, \mathrm{BLOCKED},\mathrm{NOT\_RUN}\}.

ARKE-01 的研究義務維持：

\sigma_O\in\{\mathrm{PASS},\mathrm{FAIL},\mathrm{UNKNOWN},\mathrm{NA}\}.

對映原則： 行動層的 BLOCKED 或 NOT_RUN 對尚屬必要的研究義務，通常應投影為 UNKNOWN，同時保留完整阻擋原因。不能因為一項檢查 BLOCKED 就對真值宣稱 FAIL，也不能將 NOT_RUN 變成 NA。

15.2 多方法的義務聚合

令 $\mathcal O_V(C,\Gamma)$ 為研究主張在契約下必須履行的驗證義務，每個義務有事前設定的合格見證集合 $W_o$ 。定義：

\sigma_O(o)=\mathrm{PASS} \iff [\exists e\in W_o:\mathrm{ValidWitness}(e,o,\Gamma)] \land\mathrm{DefeaterClear}(o,E).

其中 $\mathrm{DefeaterClear}(o,E)$ 表示沒有尚未處理、足以直接動搖本義務結論的擊敗性證據。此條件屬於本文提出的程序性聚合契約，而非可以在任何開放世界下自動判定的真值 oracle。若尚未能確認是否存在重大矛盾，就不得將其設定為真；應標記 UNKNOWN 並保留衝突。

例如一項原本被檢查為 PASS 的「所有輸入均正確」主張，後來出現可重播的合規反例，不能繼續僅以先前證明器的 PASS 維持原來的同一狀態。

15.3 FAIL 與 UNKNOWN 的優先邏輯

先檢查是否有可支持的直接反例或義務失效。如果有，應標記該具體義務 FAIL 並說明失效位置。若沒有足夠支持亦沒有足夠反駁，則標記 UNKNOWN。

對混合主張可保留：某子主張 PASS、另一子主張 FAIL、第三子主張 UNKNOWN，無須強行給整篇研究一個全域真偽值。

15.4 補證不等於改寫舊歷史

新證據可以使當前狀態由 UNKNOWN 轉 PASS，也可能由 PASS 轉 REVISION_REQUIRED 或 FAIL。每次轉移都要保留舊版本、時間與證據，不應將後來才取得的測試結果倒灌成「當年已驗證」。

16. N3：風險、資源與停止條件

16.1 成本不對稱不代表可以跳過基本工作

文獻檢索、測試執行、方法比較、反例搜索與重新計算，在很多情況下已可使用成熟工具自動化。ARKE-06 對 AI 的要求是：在允許的資源與權利內，主動完成合理可做的基本工作，不能把常規校驗全部留給人類補做。

但「基本可自動化」不等於任何問題都能以有限成本得到絕對真值。不同主張型別要選擇合適的終止方式，避免無限驗證吞沒全部資源。

16.2 風險不是單一數值

可用多維風險向量作程序規劃：

\mathbf r(C)=\langle r_{claim},r_{impact},r_{uncertainty},r_{source},r_{cost}\rangle.

例如學術上高曝光的全新基礎定理，其「過度宣稱」後果可能遠高於一般方法草稿；臨床或工程安全研究可能另須更嚴格的標準。但此風險向量不能直接宣稱為全球標準量表；每個分量仍需操作化與實測校準。

16.3 停止理由與可公開主張

停止事件	應保存的狀態	不可偷偷升格為
`COUNTEREXAMPLE_CONFIRMED`	主張在指定域被反駁	整個研究領域都錯
`REQUIRED_EVIDENCE_MET`	契約義務處理完成	全域無條件真理
`BUDGET_EXHAUSTED`	未完成義務及成本	證明沒有反例
`SOURCE_POLICY_BLOCKED`	無權限／無可用資料	證明來源不存在
`TOOL_UNAVAILABLE`	工具與環境限制	假裝測試已執行
`CONFLICT_UNRESOLVED`	未解的支持／反對證據	用平均票數宣布通過
`DOMAIN_RESTRICTED`	局部有效或適用域降階	舊版全域主張仍通過
`REQUEST_FOR_HUMAN_REVIEW`	特殊治理或學術協作需求	人類必然是基本自動校驗唯一途徑

16.4 發表閘道的最小要求

若候選被宣稱為 SCOPED_COMPLETION，至少應具備：原稿已凍結、主張型別與成立域清楚、指定硬性義務具有合格見證、未決項與反證已處理、來源合法且可追蹤，以及先例檢查不被驗證結果取代。

若只完成其中部分，可以依 ARKE-01 的分級發布 RAW_CANDIDATE 或 VALIDITY_CHECKED，但不能將早期原始研究發表等同於經完整查核的學術新貢獻。

17. 雙向知識驗證：由新研究回查舊主張

17.1 本篇不是只為新稿提供 PASS

如果新研究建立新的反例、方法或結果，它可能使一條先前被接受的知識依賴失去支持。ARKE 應能沿 ARKE-03 的來源與依賴路線，回查哪些舊主張使用了被修訂的前提。

例如：

C_{old}\xleftarrow{depends}\ A_{old},

若新證據證明 $A_{old}$ 不適用於某個域，AI 應重新評估 $C_{old}$ 在該域的支援，而不是一律宣布所有使用 $A_{old}$ 的定理均為假。

17.2 錯誤、前提失效與局部有效要分開

至少保留：

DERIVATION_ERROR：推導步驟或論證本身有缺口；
ASSUMPTION_INVALID_IN_DOMAIN：使用的假設在指定情況下不成立；
SCOPE_OVERCLAIM：局部證據被提升成全域結論；
MODEL_MISMATCH：形式對象或模擬與現實研究目標不一致；
HISTORICAL_PRECEDENCE_CORRECTION：研究首次性或引用先例需修正；
UNKNOWN：現有材料不足以判斷。

修訂方向取決於錯誤型別；本篇只建立查核接口，具體補丁及知識演化流程由 ARKE-07 及 TVK 系列深化。

17.3 跨領域反向驗證的難點

一項數學新結果可能對物理模型的形式部分有影響，但不會自動成為現場觀測證據；一項新的量測結果可能迫使原本的物理近似模型限縮成立域，但不會使作為抽象數學命題的微分方程定理失效。

AI 應在不同研究層之間保存有型別的作用邊，否則會把「發現新知識」錯誤轉化為「粗暴刪除舊知識」。

18. P1–P10：多元校驗的條件命題與反例論證

下列命題不宣稱獨創一般邏輯或統計學定理。其目的是明確指出研究 AI 常見的無效推論，作為未來工程 Gate 的可檢查規格。

18.1 P1：形式證明接受不蘊含學術新穎性

命題。 若形式校驗器只檢查一個證明項是否符合指定形式命題，則其接受訊號不足以推出此命題在學術歷史上首次成立。

論證。 同一形式命題可由不同研究者在不同年代提出並證明。兩份歷史不同、但證明項相同或等價的研究，可取得同一檢查器輸出。故形式校驗器的輸出不能區分歷史先後。證畢。

邊界。 若額外使用可靠的歷史文獻索引與先例檢驗，則能取得限定範圍的新穎性證據；這是新增的義務，而非校驗器的內生功能。

18.2 P2：有限樣本成功不保證無限域全稱成立

命題。 若 $D_N$ 是無限域 $D$ 的真子集，則即使對所有 $x\in D_N$ 都確認 $P(x)$ ，一般仍不能推出 $\forall x\in D, P(x)$ 。

論證。 選取 $x_0\in D\setminus D_N$ ，構造在 $D_N$ 全部為真、但在 $x_0$ 為假的述詞。即得反例。證畢。

邊界。 若有涵蓋整個無限域的獨立定理，如有效歸納證明，此反例不適用。

18.3 P3：合規反例足以推翻對應全稱命題

命題。 對主張 $\forall x\in D,P(x)$ ，若合法見證 $x_0\in D$ 且 $\neg P(x_0)$ ，則該全稱主張為假。

論證。 由全稱命題可推出 $P(x_0)$ ，與 $\neg P(x_0)$ 矛盾。證畢。

邊界。 若 $x_0$ 不屬於原宣稱域、解析器有錯或反模型只存在於不精確抽象中，不能套用此結論。

18.4 P4：計算重現不蘊含獨立複現

命題。 使用同一資料與同一分析程式成功重算結果，並不足以推出使用新資料的獨立研究也會取得一致結果。

論證。 可構造一個僅對原資料過度擬合的模型：每次重新執行相同程式都返回同一結果，但在新樣本上性能降低。故一者不能推出另一者。證畢。

18.5 P5：證據數量增加不必然增加獨立支持

命題。 若新增的多份證據全部是同一原始測量的複製或轉換，則新增報告數量不必然帶來更多獨立觀測資訊。

論證。 從一筆原始資料產生任意多個格式不同的複本，不新增任何原始觀測。若將它們計作多次獨立抽樣，即把一份觀測錯當多份。證畢。

邊界。 不同方法重新分析同一資料仍可能增加對資料處理或模型穩健性的知識；只是不能直接視為獨立抽樣。

18.6 P6：模擬成功不蘊含物理理論已受實驗確認

命題。 一個數值方法在給定模型中成功計算結果，不能僅因此推出該模型準確反映原先欲研究的真實物理系統。

論證。 可選一個數學上良定、數值上可精確求解，卻缺失真實系統重要效應的理想化模型。模型內求解成功不提供外部世界符合該模型的證據。證畢。

18.7 P7：相關性結果不蘊含因果識別

命題。 僅有 $X$ 與 $Y$ 的共同變動資訊，若未排除合適的混雜或替代因果圖，通常不能唯一識別 $X$ 對 $Y$ 的因果效應。

論證。 可構造兩種因果機制，產生相同或相近的觀察分布，一種由 $X$ 造成 $Y$ ，另一種由共同原因 $Z$ 同時影響 $X$ 與 $Y$ 。觀測關聯不區分這兩種機制。證畢。

18.8 P8：無法執行驗證不等於驗證失敗

命題。 當一項必要校驗因授權、資源或環境限制未能執行時，不能僅由該阻擋推論被檢查的主張為假。

論證。 同一命題可在兩個世界中分別為真或假，而兩個世界的校驗工具均因相同停機原因未執行。阻擋訊號不足以區分真值。證畢。

18.9 P9：共享錯誤會破壞多模型投票的證據解釋

命題。 若多個模型均依賴同一個錯誤來源，則其一致輸出不能被等同於獨立來源的多次驗證。

論證。 設三個模型皆以同一誤植數值為前提，各自重算得到相同結論。即使運算正確，這種一致性不能排除共同前提錯誤。證畢。

18.10 P10：驗證域的擴張可撤銷既有有限完成判定

命題。 若原研究只在 $D_0$ 達到受約束完備，而新版本主張在更大的 $D_1$ 成立，且 $D_0\subsetneq D_1$ ，則原有對 $D_0$ 的校驗見證一般不足以支持 $D_1$ 的全部新增義務。

論證。 在 $D_1\setminus D_0$ 可以存在原檢驗未涵蓋的反例；先前見證的作用域並未自動改變。故必須新增查核或限縮主張。證畢。

19. 四組可供演算法設計的研究案例

以下是方法論演示，不是 ARKE 軟體完成的實際測試，也不代表完整的歷史證據查核。

19.1 案例 A：一個反例能否代替四十次正面測試？

考慮被過度擴張的主張：

\forall n\in\mathbb N,\quad n^2+n+41\ \mathrm{is\ prime}.

對 $n=40$ ，可直接計算：

40^2+40+41=1681=41^2.

因此，對包含 $40$ 的全稱域，此命題有明確的反例。這裡不需要先把整個命題形式化成一個巨大工程，也不需要跑到無限大；只需要可信的整數計算與域檢查。

但如果原作者實際主張的是「僅對 $0\le n<40$ 的有限集合成立」，則 $n=40$ 不屬於其定義域，不能用它反駁。這個示例的核心不是數字大小，而是：反例只有與主張的正式量詞和成立域相匹配時才有效。

此案例的 ARKE 決策應至少區分：

原始主張是否真的使用全稱量詞；
$40$ 是否屬於受檢驗的域；
算術分解是否可重播；
被反駁的是全球性主張，還是僅針對某版本中一行誤寫；
原先受支持的局部範圍是否仍應保留。

19.2 案例 B：ETH 類型的演算法突破應如何驗證？

假設有一份研究候選聲稱找到次指數時間 SAT 演算法。即使在很多樣本上求解正確，ARKE 仍需分開建立：

歷史存在鏈： 過去是否已有相近演算法或類似次指數主張？
任務語義鏈： 是判定 SAT，還是精確 #SAT 計數？固定子句寬度與輸入編碼有無特別限制？
正確性鏈： 對指定全部輸入有何可靠論證？
複雜度鏈： 是最壞時間、預期時間，還是某分布下的實測速度？空間與預處理有無完整記帳？
實作鏈： 可以重播或只附有形式證明草稿？若形式化，公理與語義對齊有無核查？
比較鏈： 與早期工作的關係是相同上界、不同方法、較強結果，或尚無法判定？

若其中一條鏈仍不確定，應限定宣稱，而非把所有驗證壓縮成「Lean 通過」或「AI 跑得很快」。同樣，找到較早的研究主張，不代表較早的證明已被確認正確。

本案例只說明 ARKE 的流程要求，不對具體現代 ETH 反證作出新的科學裁決。

19.3 案例 C：物理模擬結果與實驗測量不一致

假設模型 $M_1$ 在測試情境 $D_0$ 上的計算誤差很小，但新儀器在域 $D_1$ 觀察到不同結果。AI 不應直接做下列任一判定：

「數學模型有正式推導，所以新儀器一定錯」；
「新儀器顯示不同數值，所以原模型全部無效」。

最低應先檢查：測量量是否相同、單位與校準、儀器誤差、不同尺度／邊界條件、資料處理、模型參數及新的結果是否可獨立複現。

合理可能結果包括：模型只在 $D_0$ 有效、儀器存在系統偏差、兩個研究實際測量不同量、舊假設須修訂，或暫時 INCONCLUSIVE。這可以成為 ARKE-07 的知識修正輸入，而不會抹除原先正確的局部推導。

19.4 案例 D：同一原始實驗的三份「獨立確認」

假設原資料檔 $D$ 被轉為兩個格式，Agent A 用程式分析，Agent B 用另一個語言重算，Agent C 讀取 A 的結論再產生評論。

可以得到：

A、B 的一致結果支持某些計算流程的可重現性；
B 若使用不同計算庫，可能檢出 A 的實作錯誤；
C 的文字同意若沒有獨立證據，不增加新的原始測量資訊；
若三者皆基於同一個偏差樣本，對目標母體的外部有效性仍未得到新保障。

因此 ARKE 的證據圖必須保留資料共享依賴，不可將三份文字輸出視為三次獨立實驗。

20. M8：AI 自主多元校驗的最小演算法契約

20.1 從生成候選到驗證路由

在研究候選凍結後，建議的程序是：

建立不可變的候選快照與其來源錨點；
把混合主張拆成有型別、有限作用域的子主張；
根據 ARKE-01 的 $\Gamma$ 指定每條主張的硬性義務與發表層級；
識別每個義務可適用的檢查方法、依賴與信任範圍；
計算合法權限及預算條件，選擇有限、可重播的行動；
優先處理可快速推翻核心全稱主張的合法反例機會；
執行正面校驗、重播與適當的獨立挑戰；
保存每個校驗動作的來源、輸出、成本、環境及失敗原因；
建立支持／反對／限定／未知的證據依賴結構；
檢查證據互相依賴、語義對齊及未解決的擊敗性證據；
向 ARKE-01 的研究義務狀態投影，決定可公開宣稱的範圍；
將新反例與假設變化傳遞給 ARKE-07 的知識修正模組，但不自行改寫 canonical 原稿。

20.2 主要偽代碼（proposal only）

以下是演算法規格文字，不是已運行的程式碼：

function ARKE06_Verify(candidate, research_contract, source_index):
    frozen := freeze(candidate)
    claims := type_and_split_claims(frozen, preserve_original=true)
    audit_log := new_append_only_log()

    for claim in claims:
        obligations := select_obligations(claim, research_contract)
        record(audit_log, "obligations_frozen", obligations)

        for obligation in obligations:
            routes := admissible_verifiers(obligation, research_contract)
            routes := require_semantic_alignment(routes, claim)
            routes := filter_by_lawful_access(routes)
            routes := filter_by_budget(routes)

            if routes is empty:
                record_unresolved(obligation, "BLOCKED_OR_UNAVAILABLE")
                continue

            for route in select_bounded_plan(routes):
                result := run_in_bounded_environment(route)
                witness := check_witness_type_and_scope(result)
                record(audit_log, route, result, witness)

                if witness is confirmed_refuter_of(claim):
                    record_refutation(claim, witness)
                    break

        evidence_graph := build_typed_evidence_graph(claim, audit_log)
        inspect_shared_dependencies(evidence_graph)
        inspect_defeaters_and_open_assumptions(evidence_graph)
        claim_status := evaluate_scoped_obligations(claim, evidence_graph)
        store_without_overwriting_history(claim_status)

    novelty := inspect_prior_art_results_separately(source_index)
    release := classify_publishable_claims(claims, novelty, research_contract)
    return release, audit_log, claims, unresolved_queue

拒絕規則： 上述 run_in_bounded_environment 不提供任何隱含權限；若外部工具需要檔案、網路、算力或實驗設備，必須另受合法權限契約控制。novelty 也不能由校驗器 PASS 自動生成。

20.3 機器可讀物件示例

此 JSON 僅展示提案中的資料欄位形狀，不宣稱已在 ARKE GitHub 有 JSON Schema 或成功驗證的紀錄：

{
  "schema": "arke/research-verification-candidate-v0.1-proposed",
  "claim_id": "C-DEMO-01",
  "claim_kind": "FORMAL",
  "statement_ref": "local:example/theorem-1",
  "domain": "nonnegative integers",
  "assumptions": [],
  "quantifier": "forall",
  "required_obligations": [
    "claim_semantics_alignment",
    "formal_proof_or_valid_refutation",
    "axiom_dependency_audit",
    "source_traceability"
  ],
  "tool_chain": [],
  "evidence_items": [],
  "shared_dependencies": [],
  "action_state": "NOT_RUN",
  "obligation_state": "UNKNOWN",
  "conclusion": "NO_VERIFICATION_CLAIM",
  "research_completion_authorized": false,
  "rsi_verified": false
}

tool_chain 待執行時應保存版本、SHA-256、輸入與輸出定址、驗證方法、環境及相容性；此處不放虛假的已執行摘要。

20.4 出口物件不應只有一個布林值

最小輸出應包含：

被檢查的研究主張與凍結版本；
每條義務的狀態及合格見證；
可靠反例、未解衝突與被否定的具體範圍；
來源、工具、資料及模型的版本地址；
資料與方法依賴及獨立性說明；
可重播方式、失敗日誌及成本；
殘餘未知和下一次重開的條件；
可公開宣稱與不可公開宣稱的分離；
對舊研究的可能影響清單（非直接覆寫）。

21. 典型失敗模式與拒絕門檻

編號	失敗模式	應採取的行動
F01	`LEAN_ONLY_COMPLETION`：把 Lean PASS 當成整個研究完成	只認形式義務，另查語義、來源與新穎性
F02	`SORRY_OR_UNAUDITED_AXIOM`：未檢查形式證明依賴	保留公理清單，必要時不允許強宣稱
F03	`FORMALIZATION_DRIFT`：形式命題與欲研究命題不同	設立語義對齊義務，不通過即降階
F04	`FINITE_TO_UNIVERSAL`：有限樣本誤推全稱	限定測試域，或要求獨立一般性證明
F05	`SPURIOUS_COUNTEREXAMPLE`：抽象模型的假反例	回到具體系統、原始域及可信 checker
F06	`RUNTIME_AS_PROOF`：benchmark 當複雜度證明	分離正確性、最壞情況上界及成本模型
F07	`REPLAY_AS_REPLICATION`：同資料重跑當獨立複現	紀錄資料來源與新樣本的真正獨立性
F08	`P_VALUE_AS_TRUTH`：顯著性門檻當真理布林值	結合設計、效果量、偏差及不確定性
F09	`CORRELATION_AS_CAUSE`：關聯當因果	啟動因果識別與敏感性義務
F10	`SIMULATION_AS_REALITY`：模型內結果當物理證據	建立測量、校準、適用域與外部驗證
F11	`EVIDENCE_DOUBLE_COUNT`：同源資料多次計票	證據依賴去重，但不刪除版本和歷史
F12	`HISTORICAL_CLAIM_AS_VALIDITY`：早期主張當既有正確證明	分離來源存在鏈與有效性鏈
F13	`BLOCKED_AS_FAIL`：取不到證據當命題已假	保留 BLOCKED 與 UNKNOWN；不得偽報
F14	`RESULT_LAUNDERING`：新證據被回寫到舊時間點	只增加新事件，舊版歷史不可覆寫
F15	`BENCHMARK_LEAKAGE`：評估資料進入訓練／調參	固定評估域，追蹤資料與模型污染
F16	`VERIFIER_CAPTURE`：受檢 AI 控制評估器或標籤	記錄執行權限與 evaluator independence
F17	`LINK_AS_EVIDENCE`：只有 URL 卻假稱讀完證明	使用 RTA 精確分層記錄可達與已驗證程度
F18	`PERMISSION_BYPASS`：以科學驗證名義繞過存取權	遵守 ARKE-02 權利契約，允許 BLOCKED

這些失敗模式是未來測試與阻擋規則提案，不表示本篇已建立對應程式測試，也不是對任何具名研究機構已發生違規的斷言。

22. H1–H8：可否證的跨領域實驗規格（全部 NOT_RUN）

22.1 共同研究設計

22.1.1 實驗目的

檢查「有型別多元校驗」是否優於只看單一驗證器、沒有類型的多 Agent 投票，以及僅依語義相似度自動判定，而不預設 ARKE 一定更好。

22.1.2 最低對照組

B0_SINGLE_VERIFIER：依預設工具輸出單一成功／失敗，不檢查證據型別及依賴。
B1_LLM_SELF_REVIEW：由同一個模型生成後再自行閱讀、評論其成果。
B2_MULTI_AGENT_UNTYPED：多個 Agent 各自評論，無共享資料與來源依賴稽核。
B3_DOMAIN_STANDARD：採用該研究領域的既有適當校驗流程，作為必要的成熟方法基線。
T_ARKE06：本文提出的有型別路由、證據依賴與受約束義務聚合。

對照不應把已知成熟的研究程序故意削弱到不合理程度。模型能力、工具允許集、來源可達性及算力上限應盡量固定或分層配對。

22.1.3 測試集組成

至少包含：

已知且可重播的數學正確命題與錯誤命題；
帶有形式化語義漂移、額外公理或 sorry 依賴的合成案例；
有限樣本成功但全稱失敗的反例設計；
演算法正確但複雜度主張不支持的案例；
統計分析與獨立複現不一致的案例；
相關／因果混淆及物理模型尺度錯配案例；
先例存在但先前證明尚未確認的歷史案例；
工具不可用、權利受限、來源斷鏈與多 Agent 共用錯誤的案例。

所有測試案例的真值、反例見證、限制與樣本來源須由獨立的已驗證 reference artifacts 或明確可重播的研究程序固定。對尚無公認裁決的開放科研問題，只能評價校驗流程是否正確保留未決，不得假裝有金標答案。

22.1.4 盲測、版本及洩漏控制

在評估之前凍結任務與標準答案來源；模型訓練、檢索、提示及留出資料的相互可達性必須明確記錄。若無法排除先前訓練污染，應降低「獨立發現」的宣稱，而不抹除同一系統在研究核查中的可測表現。

22.1.5 指標、成本與失敗準則

最低報告：

False Attestation Rate（FAR）：未滿足硬性義務卻被系統宣稱已驗證的比例；
Valid Refutation Recall：對可核實反例的辨識率；
Spurious Refutation Rate：將無效反例判作有效的比例；
Unknown Retention Accuracy：應保留未知時是否正確保留；
Evidence Provenance Completeness：必要來源及方法欄位的可查比例；
Dependency Leakage Rate：同源證據被當作獨立證據的比例；
Scope Calibration：所發表的主張與實際通過域是否一致；
Cost Vector：時間、token、CPU／GPU、API、儲存、能源與金錢等實際使用。

指標需依主張型別、學科、資料可達性及風險層分組報告。整體平均值不能掩蓋高風險主張的錯誤。事前須定義主要比較指標與允許成本差距，避免根據結果事後選擇最有利的指標。

22.2 H1：有型別路由能降低不當通過

假說。 與 B0_SINGLE_VERIFIER 相比，在相同可用方法與預算下，T_ARKE06 的 FAR 較低，尤其在形式證明與物理實驗混合的案例中。

失敗判準。 若控制研究型別與成本後，FAR 沒有可辨識改善、反而更高，或改善完全來自拒絕處理所有案例，則不支持假說。

狀態： NOT_RUN。

22.3 H2：語義橋與公理稽核可降低形式化誤判

假說。 在混入形式命題漂移、自訂不安全公理與不完整依賴的測試集中，明確審查公理及 Statement Alignment 能減少「形式化通過所以原主張已證成」的錯判。

失敗判準。 若方法仍大量漏掉錯配、或因過度阻擋使正常證明也不能使用，則必須修訂相關義務。

狀態： NOT_RUN。

22.4 H3：反例有效性檢查能減少假反駁

假說。 相對於把模型檢查器回傳的所有 counterexample 直接接受，加入具體系統回驗與成立域查核可降低 Spurious Refutation Rate。

失敗判準。 若假反駁率未降低，或真反例召回損失超過事先設定的容忍度，則不支持假說。

狀態： NOT_RUN。

22.5 H4：依賴稽核可改善多 Agent 證據判讀

假說。 在刻意設計共享錯誤來源、多格式資料複製與同一模型鏈式轉述的案例中，記錄資料與方法依賴可降低錯誤獨立性宣稱。

失敗判準。 若依賴圖無法區分真正獨立的複現與純粹衍生資料，或將所有證據都過度合併，則不支持假說。

狀態： NOT_RUN。

22.6 H5：多元校驗能降低跨域外推錯誤

假說。 在經驗研究、因果與物理模擬案例中，分離統計、因果、測量及模型域義務，可降低「局部成立 → 全域成立」的不當外推。

失敗判準。 若 Scope Calibration 沒有改善或成本顯著過高而無實際收益，則不支持此假說。

狀態： NOT_RUN。

22.7 H6：保留 UNKNOWN 可提高開放問題的校驗誠實性

假說。 在沒有金標真值或資料受限的題目中，T_ARKE06 比無型別投票系統更少生成無根據的強宣稱，而不是一律隨機選擇 PASS 或 FAIL。

失敗判準。 若系統大量使用 UNKNOWN 以逃避本可完成的校驗義務，導致必要查核完成率顯著下降，亦不支持假說。

狀態： NOT_RUN。

22.8 H7：適當的驗證路由可以改善成本—錯誤前沿

假說。 相對於所有問題都執行全套方法，使用主張型別與風險選擇驗證路線，可以在類似的 FAR 與有效反例召回下減少平均資源消耗。

失敗判準。 若效率收益來自跳過關鍵硬性義務，或錯判率升高超過預註冊界限，則不支持假說。

狀態： NOT_RUN。

22.9 H8：雙向知識查核可提高正確的修訂定位

假說。 當新成果與舊研究發生衝突時，T_ARKE06 輸出的有型別證據鏈能比僅給「舊研究錯誤」的系統，更準確區分推導錯誤、前提失效、成立域限縮及學術歸屬修正。

失敗判準。 若反而增加誤退役、錯誤刪除有效局部內容，或無法重建舊版的依賴歷程，則不支持假說。

狀態： NOT_RUN。

22.10 防止「用合成測試替代真實研究」

本篇允許用數學構造及合成故障測試工程規格，但正式科學結論必須在其聲稱範圍內另作真實資料或領域基準檢驗。若只在合成資料取得高分，只能宣稱「合成測試有效」，不能宣稱「已能自行審查所有新數學、物理或生物研究」。

23. 外部研究與既有標準的承接

23.1 Lean 與形式驗證不是 ARKE 的競爭對象

Lean 的小型可信核心、公理依賴稽核與形式證明檢查，是 ARKE 可選的重要校驗能力 [1–3]。本文主張將它放回正確的義務型別，而非否定或取代 Lean；Coq、Isabelle、SMT、模型檢查和專用數學驗證工具也應視需求選用，使用時需固定相應的信任基礎。

23.2 反例與模型精化已有深厚研究

CEGAR 自 2000 年起便將抽象模型的疑似反例、具體系統確認與抽象精化連成自動化流程 [4]。ARKE 應學習其假反例防護，但其所研究的文獻先例、物理測量與學術歸屬超出傳統軟體模型檢查問題。

23.3 可重現與獨立複現不是新術語

國家科學院對 reproducibility／replicability 的區分 [5]、The Turing Way 對研究程式、環境與資料重播的實務 [13]，以及 ACM SIGIR 的 artifact 評估制度 [14]，都已為研究可重播性建立具體參考。ARKE 的新增目標是：把不同證據義務交給 AI 自主路由，而不是重複宣稱這些科研實務第一次被發明。

23.4 統計、量測與風險標準應繼續承接

ASA 的統計證據與選擇性報告提醒 [6,7]、NIST 的測量不確定性規範 [8]、Cochrane 的偏差分析 [10] 及 NIST AI RMF 對有效性與外部泛化的要求 [15]，都應被視為對應領域的工具與方法背景，而非 ARKE 的原創命題。

23.5 檢索與文獻歷史義務不可被驗證器取代

PRISMA-S 設計了文獻搜尋報告的可追溯項目 [16]。ARKE-02／04 已承接學術索引與先例搜尋的責任。本篇強調：不論使用何種校驗器，來源歷史及學術新穎性仍是需獨立查核的研究義務。

24. 與獨立 ARKE 軟體及 EveTrain RAI／RSI 的邊界

24.1 ARKE 工程獨立於論文系列

十二篇 ARKE Research 是理論及方法論原稿；未來 ARKE GitHub 專案是獨立工程載體。本文不宣稱該獨立倉庫目前已有完整引擎，也不直接修改 EveTrain、數學 AI、ISQL、EML-NOVA 或任何私人系統。

24.2 AI 可自主完成，並不等於 AI 可自我授權

AI 應自主檢索、比對、提出反例、執行可用的本地校驗、保存證據、定義未決。但自主執行權仍受操作系統、來源權利、GPU 預算、設備安全及研究倫理約束。

禁止的推論： 研究器可以提出方法或產出證據，就表示它有權私自修改其他研究原稿、訓練模型、取得未授權資料或宣稱學術認證。

24.3 ARKE → EveTrain 的預期資料方向

ARKE 可向 EveTrain 的 RAI Registry 提供：

待查核的演算法候選及其主張類型；
形式／經驗／歷史的多種驗證義務與結果；
可追溯來源、實驗假說、對照與未決風險；
新理論或資料可能改善某研究策略的候選假說。

但即使 ARKE 在某種局部證據契約下通過，也不證明研究 AI 的遞迴自我改進：

\mathrm{ARKE06\_CheckPassed} \not\Rightarrow \mathrm{RSI\_Verified}.

RAI／RSI 的能力提升需要真正凍結的前後比較、獨立評估、成本與因果歸因；此項由 ARKE-12 的實驗線承接。

24.4 認知層、研究層與實證層的非同一性

即使 AI 找到正確反例，這本身是一次校驗成果；即使 AI 經常找到反例，也不自動證明它已具備完整數學創造或跨領域科學理解能力。研究工具的改進、模型內部能力的改進、實際科研產出的增量，是三個應分別驗證的命題。

25. B1–B12：本篇不能推出的結論

B1：未提供一個可決定全部數學真假的萬用演算法。
B2：不主張任何人或 AI 可以在有限資源內查盡全部文獻。
B3：不主張 Lean 形式證明無用；只反對將其誤作一切科研義務的充分條件。
B4：不主張同一物理模型的數值收斂可代替實驗證據。
B5：不主張反例搜索沒有找到反例就證成全稱命題。
B6：不主張多個 Agent 意見一致等於多項獨立證據。
B7：不主張所有經驗科學證據可以換算成單一跨域真理分數。
B8：不主張系統能在無法確認來源、授權及條件時自動補全缺失值。
B9：不主張 ARKE 的驗證程序能自動判定全部學術優先權或研究倫理爭議。
B10：不主張本文假說 H1–H8 已經獲得任何實驗支持。
B11：不主張研究校驗 PASS 可以轉成模型訓練、系統控制或數據存取權限。
B12：不主張目前的 AI 已因本文存在而達到普遍可靠的自動科研完備能力。

26. 核心結論

本文將「多元研究校驗」從工具列表轉為有型別、有證據依賴、有成立域、有權利與成本界線的 AI 自主科研義務。

其最低結構可概括為：

\mathrm{Claim} \longrightarrow \mathrm{TypedObligations} \longrightarrow \mathrm{AdmissibleMethods} \longrightarrow \mathrm{EvidenceAndCounterevidence} \longrightarrow \mathrm{ScopedDecision}.

其中最重要的原則有五項。

原則一：方法依主張選擇。 定理應有適當的邏輯見證，演算法須分離正確性與複雜度，經驗研究須處理資料與不確定性，物理理論須顧及實驗與成立域，歷史主張須保留可回訪先例。

原則二：反例與證據要有型別。 一個合法反例可以推翻被精確陳述的全稱主張，但隨機測試、近似模擬或找不到反例並不自動成為普遍證明。

原則三：證據耦合不等於多數決。 支持、反對、限定、共享來源與工具依賴必須保留；不得把同一資料的多個轉述計為獨立複現。

原則四：未知是有效且必要的研究狀態。 遇到來源不可得、工具未執行、可信度不足或不同證據無法解開的衝突時，應限縮結論或保留未決，而非勉強宣稱 PASS／FAIL。

原則五：AI 應自主承擔基本研究工作。 在可行的合法方法與預算內，AI 能自行執行檢索、校驗、實驗及反例分析；不必把常規科研程序預設為人類專家才能替它完成。但這項自主性不能被誤用成自我授權或自我認證。

最終，本篇提出的研究方法並不是證明 AI 已具備全部科學能力，而是定義下一代 AI 研究工具應如何對自己的主張提出適當的證據，並對其缺口保持可追溯的認識論誠實。

27. 與下一篇 ARKE-07 的接口

ARKE-06 完成了「如何判斷一項研究證據在什麼條件下支持、反駁或限縮主張」的理論接口。ARKE-07 將進一步處理：

當新證據與舊知識衝突時，如何定位真正失效的前提？
如何避免因局部反例而錯誤退役整個理論？
如何將新舊研究構成雙向校驗，而不是單向更新？
如何從證據狀態轉換成可回滾、可分叉及保留歷史的理論修正候選？
如何辨認研究中的「真實錯誤」、實驗失效、範圍限縮與歷史先例訂正？
如何讓 AI 提出知識修正，但在適當驗證及授權之前不覆寫正式原稿？

下一篇：ARKE-07｜《新舊知識雙向驗證與歷史修正：研究衝突、有效核與證據演化》。

參考文獻與核查來源（截至 2026-10-28）

以下引用既有研究、標準與官方技術文件作為背景和先例，不將其功能或外部實測視為 ARKE 自身完成的實驗。任何引用中的論文版本或網站內容日後可能更新，後續軟體應以 ARKE-03 RTA 記錄更細的版本與片段定址。本文未執行外部文獻系統的實測 benchmark。

Lean Project. The Lean Language Reference. https://lean-lang.org/doc/reference/latest/ （Lean 4 形式系統、核心與語言參考）。
Lean Project. The Lean Language Reference — Axioms. https://lean-lang.org/doc/reference/latest/Axioms/ （公理依賴、sorryAx、信任邊界）。
Lean Project. Validating a Lean Proof. https://lean-lang.org/doc/reference/latest/ValidatingProofs/ （證明依賴、公理檢查及形式聲明對應問題）。
Clarke, E. M., Grumberg, O., Jha, S., Lu, Y., and Veith, H. (2000). Counterexample-Guided Abstraction Refinement. CAV 2000, Lecture Notes in Computer Science 1855, 154–169. https://doi.org/10.1007/10722167_15
National Academies of Sciences, Engineering, and Medicine. (2019). Reproducibility and Replicability in Science. National Academies Press. https://doi.org/10.17226/25303 ; https://www.nationalacademies.org/read/25303/chapter/3
American Statistical Association. (2016). ASA Releases Statement on Statistical Significance and P-Values. https://magazine.amstat.org/blog/2016/03/07/pvalue-mar16/
American Statistical Association. (2021). ASA President’s Task Force Statement on Statistical Significance and Replicability. https://magazine.amstat.org/blog/2021/08/01/task-force-statement-p-value/
Taylor, B. N., and Kuyatt, C. E. (1993). Guidelines for Evaluating and Expressing the Uncertainty of NIST Measurement Results, NIST Technical Note 1297. https://www.nist.gov/pml/nist-technical-note-1297
Open Science Collaboration. (2015). Estimating the reproducibility of psychological science. Science, 349(6251), aac4716. https://doi.org/10.1126/science.aac4716 ; https://pubmed.ncbi.nlm.nih.gov/26315443/
Cochrane. Cochrane Handbook for Systematic Reviews of Interventions — Chapter 8: Assessing risk of bias in a randomized trial. https://www.cochrane.org/authors/handbooks-and-manuals/handbook/current/chapter-08
Srinivasan, V. (2026-10-05). On Methods of Uncertainty Quantification in Computational Modeling and Simulation: Harmonizing Modeling and Metrology Practices. NIST. https://www.nist.gov/publications/methods-uncertainty-quantification-computational-modeling-and-simulation-harmonizing
W3C. (2013). PROV-O: The PROV Ontology. W3C Recommendation. https://www.w3.org/TR/prov-o/
The Turing Way Community. Guide for Reproducible Research; Reproducible Environments. https://book.the-turing-way.org/reproducible-research/reproducible-research/ ; https://book.the-turing-way.org/reproducible-research/renv/
ACM SIGIR. Artifact Badging: Results Replicated and Results Reproduced. https://sigir.org/general-information/acm-sigir-artifact-badging/
NIST. AI Risk Management Framework — AI Risks and Trustworthiness: Valid and Reliable. https://airc.nist.gov/airmf-resources/airmf/3-sec-characteristics/
Rethlefsen, M. L. et al. (2021). PRISMA-S: an extension to the PRISMA Statement for Reporting Literature Searches in Systematic Reviews. Systematic Reviews, 10, 39. https://doi.org/10.1186/s13643-020-01542-z ; https://www.prisma-statement.org/prisma-search

本系列內部研究脈絡（非外部實證引用）

ARKE-01. 從答案生成到研究完備：AI 自主科研的基本義務. v0.1，2026-10-28。
ARKE-02. 全域知識可達性：學術資料來源、合法取得與覆蓋邊界. v0.1，2026-10-28。
ARKE-03. 來源定址、超連結與研究依賴結構：可追溯知識承接論. v0.1，2026-10-28。
ARKE-04. 先例發現與學術新穎性：AI 自主研究的前置查核. v0.1，2026-10-28。
ARKE-05. 跨表示研究同一性：定理、演算法、方法與證據的結構比較. v0.1，2026-10-28。
Neo.K with GPT. ARKE Research 十二篇研究總綱. v0.2，2026-10-28。
EveTrain RAI Algorithm Registry v0.1（既有研究管理層；非本篇實驗結果）。
TVK-EPE／TVK-TIA（有效核、成立域、殘差及理論補丁；僅作後續整合接口）。

原始檔與版本註記

Canonical source： 本檔原始 UTF-8 Markdown 位元組；聊天畫面不作為正式論文 source。
數學分隔符： $...$ 與 $$...$$，未引入第二套 canonical delimiter。
方法論狀態： 定義／規範／條件命題／待驗證方法；非已運行 ARKE 引擎。
實證狀態： H1–H8 全部 NOT_RUN；未報告任何自造 benchmark、原生模型提升或硬體實驗結果。
工程狀態： ARKE 工程獨立 GitHub 專案規劃，本文不要求在本輪建立 repo、推送程式或修改 EveTrain 主分支。
後續關係： ARKE-07 處理知識修正；ARKE-09 處理自主核查演算法；ARKE-11 處理研究完成與公開發表閘道；ARKE-12 處理跨領域實證與 RAI／RSI。
修訂政策： 後續勘誤必須另列版本與差異，不能以新證據倒寫 v0.1 的原有驗證狀態。