AI 原生知識展開 Runtime：BKSE 端到端架構、可信邊界與 MVP

English Title: AI-Native Knowledge Expansion Runtime: End-to-End Architecture, Trust Boundaries, and an MVP for BKSE
Series: AI-Native Knowledge Expansion, Paper VII
Author: Neo.K
Collaborator: Aletheia (GPT-5.6 Sol)
Institution: EveMissLab / 一言諾科技有限公司
Version: v0.1
Date: 2026-08-10
Status: Series I — Phase I Integration Paper

摘要

本系列前六篇依次建立 Base Knowledge Space Expansion（BKSE）的核心理論部件：可靠基礎知識的大規模結構展開、變種身份與命題分叉、錯誤鄰域與反例空間、多證法與交叉驗證的 Proof Lattice、AI-Native Research Graph，以及在有限資源下控制組合爆炸的 Frontier Scheduler。本篇作為 Series I 第一階段的整合篇，不再主要增加新的哲學命題，而是把上述元件收斂為一套可實作、可測試、可失敗、可重播的 AI-Native Knowledge Expansion Runtime（ANKER）。

ANKER 的核心不是讓大型模型自由生成無限數學文本，而是建立一個嚴格的閉環：

\boxed{ \text{Seed} \rightarrow \text{Expand} \rightarrow \text{Classify} \rightarrow \text{Attack} \rightarrow \text{Prove / Verify} \rightarrow \text{Commit} \rightarrow \text{Schedule} \rightarrow \text{Expand Again}. }

系統將生成器視為不可信候選來源，將 parser、type checker、formal prover、external checker、counterexample search、tests 與 provenance tracking 視為不同驗證層；將「未證明」「已否證」「形式有效但語義未審核」「內部新穎但文獻未檢查」分別保存，禁止壓縮成單一 verified=true。BKSE Runtime 的主要知識單位不是論文，而是帶有穩定身份、lineage、變種證書、反例、proof family、驗證矩陣、狀態與 open frontier 的 machine-first knowledge object。

本文提出七層 runtime、最小資料 schema、五個核心服務、任務佇列、failure taxonomy、trust boundary、Lean/Python 驗證接口、budget-aware frontier loop，以及三階段 MVP 實驗。第一階段僅需 100–500 個基礎數學 seed、SQLite/PostgreSQL、Python、Lean、單一 LLM 與 deterministic scheduler 即可驗證核心假說。第二階段加入多 prover、external checker、literature bridge 與 learned scheduler。第三階段才進入長期自主研究與跨領域擴張。

本文的核心工程主張是：

\boxed{ \text{AI-native research should treat generation as cheap and verification state as precious.} }

當候選生成逐漸廉價，真正需要保存、調度與保護的資源將是 verified attention、typed lineage 與可重播的知識狀態。

關鍵詞： BKSE；AI 原生知識展開；AI 原生數學；Research Runtime；Proof Lattice；Research Graph；Frontier Scheduler；形式化驗證；Counterexample；MVP

1. Series I 第一階段的整合問題

前六篇分別回答：

\begin{aligned} P_1 &: \text{基礎知識能否形成高價值結構閉包？}\\ P_2 &: \text{如何區分表面變種、結構變種與命題分叉？}\\ P_3 &: \text{如何系統生成錯誤鄰域與反例？}\\ P_4 &: \text{如何從單一 proof 進入多路徑交叉驗證？}\\ P_5 &: \text{若論文只是 rendering，機器內部要保存什麼？}\\ P_6 &: \text{候選爆炸後，下一單位研究注意力投向哪裡？} \end{aligned}

Paper VII 的問題只有一個：

\boxed{ \text{Can these six ideas form one runnable system?} }

如果不能，那麼前六篇仍只是方法論集合。

如果能，則 BKSE 從理論假說進入：

\boxed{ \text{research infrastructure hypothesis}. }

2. 系統名稱與定位

本文暫稱整合 runtime 為：

\boxed{ \text{ANKER} }

即：

AI-Native Knowledge Expansion Runtime。

名稱只是工程代號，不是新的理論分支。

ANKER 的定位不是：

通用 AGI；
完整數學家替代系統；
自動論文工廠；
無限制 conjecture generator；
單一 theorem prover。

而是：

\boxed{ \text{a stateful verified knowledge-expansion runtime}. }

它的工作是維持：

G_t

並把每次生成、失敗、驗證與修正變成：

G_t\rightarrow G_{t+1}.

3. Runtime 核心 LOOP

ANKER 的最小循環：

\boxed{ G_t \rightarrow F_t \rightarrow A_t \rightarrow C_t \rightarrow V_t \rightarrow \Delta G_t \rightarrow G_{t+1}. }

其中：

$G_t$ ：當前 Research Graph；
$F_t$ ：可執行 frontier；
$A_t$ ：被 scheduler 選中的 action；
$C_t$ ：生成的 candidate；
$V_t$ ：驗證結果；
$\Delta G_t$ ：經分類後的 knowledge commit。

更具體：

1. Load current graph state
2. Generate frontier actions
3. Score actions
4. Select a budget-feasible portfolio
5. Generate candidate objects
6. Canonicalize and classify
7. Attack / search counterexamples
8. Prove / test / verify
9. Extract provenance and dependencies
10. Commit typed results
11. Recompute frontier
12. Repeat or stop

因此：

\boxed{ \text{generation is one stage, not the runtime itself}. }

4. 七層架構

本文提出七層。

Layer 0：Seed Layer

保存初始可靠知識：

theorem；
definition；
axiom；
tested algorithm；
verified program；
reference dataset。

要求：

\boxed{ \text{seed provenance must be explicit}. }

Seed 不能只是「模型記得這是真的」。

Layer 1：Representation & Identity Layer

負責 Paper II：

parse；
type；
structural fingerprint；
canonicalization；
equivalence class；
proposition identity；
branch detection。

輸出：

\operatorname{IdentityRecord}(K).

Layer 2：Expansion Layer

負責 Paper I：

equivalent rewrite；
specialization；
generalization；
converse；
composition；
representation shift；
assumption ablation；
problem transformation。

生成：

C=\operatorname{Expand}(K,T).

這一層不宣告 candidate 正確。

Layer 3：Adversarial Layer

負責 Paper III：

CounterexampleHunter；
AssumptionAuditor；
BoundaryMutator；
ProofCorruptor；
DependencyChecker。

輸出：

\text{DISPROVED}, \text{INVALID}, \text{COUNTEREXAMPLE}, \text{UNKNOWN}

等候選狀態。

Layer 4：Verification Layer

負責 Paper IV：

symbolic verification；
numerical tests；
finite exhaustive computation；
Lean proof；
kernel check；
axiom audit；
external checker；
semantic audit。

輸出不是單一 boolean，而是：

\boxed{ \mathbf V(K). }

Layer 5：Knowledge Graph Layer

負責 Paper V：

typed nodes；
typed edges；
provenance；
version；
append-only history；
correction；
proof lattice；
open frontier；
literature links。

它是系統的持久狀態。

Layer 6：Scheduler Layer

負責 Paper VI：

frontier generation；
scoring；
budget allocation；
branch dormancy；
revival；
stopping；
portfolio scheduling。

它決定：

\boxed{ \text{what receives the next unit of verified attention}. }

5. 為什麼生成器必須是不可信元件？

ANKER 的關鍵安全假設：

\boxed{ \text{Generator is untrusted}. }

不管候選來自：

GPT；
Claude；
local model；
symbolic enumerator；
human；
evolutionary search；

都只能得到：

\text{CANDIDATE}.

不能直接得到：

\text{VERIFIED}.

因此：

LLM output
    ↓
Candidate Store
    ↓
Verifier Pipeline
    ↓
Canonical Graph

這與現代 proof-assistant 的基本分工相容：複雜生成或 tactic 層可以不可信，而最終 proof object 由較小 checker 驗證。Lean 官方也把未審查 AI-generated proof 視為高風險輸入，並提供更高等級的 comparator + external checker 驗證路徑。

6. Candidate Store 與 Canonical Store 必須分離

如果生成 candidate 後立刻進入 canonical graph：

\text{hallucination} \rightarrow \text{knowledge}.

所以至少分兩區：

Candidate Store

狀態包括：

NEW
PARSED
ILL_TYPED
PENDING
UNDER_ATTACK
UNDER_PROOF

Canonical Knowledge Store

只接受：

VERIFIED
DISPROVED
CONFLICTED
FORMALLY_VALID
TESTED
LITERATURE_LINKED

以及明確標記的：

UNKNOWN

因此：

\boxed{ \text{candidate persistence} \neq \text{knowledge admission}. }

7. 最小 Knowledge Object Schema

最小節點：

{
  "id": "CLAIM-000123",
  "type": "CLAIM",
  "status": "UNKNOWN",
  "domain": "euclidean_geometry",
  "statement": {
    "natural": "...",
    "formal": null
  },
  "parents": [],
  "operator": null,
  "fingerprint": {},
  "dependencies": [],
  "proofs": [],
  "counterexamples": [],
  "verification": [],
  "frontier": [],
  "provenance": {},
  "version": 1
}

最重要的是：

\boxed{ \text{status must remain typed}. }

8. 建議的 Status State Machine

最小狀態：

\mathcal S = \{ NEW, PARSED, VALID\_FORM, UNKNOWN, SUPPORTED, TESTED, PROVED, CROSS\_CHECKED, DISPROVED, CONFLICTED, REJECTED \}.

可有：

NEW\rightarrow PARSED\rightarrow UNKNOWN.

之後：

UNKNOWN\rightarrow PROVED,

或：

UNKNOWN\rightarrow DISPROVED.

也可能：

PROVED\rightarrow CONFLICTED

如果 semantic audit 或 checker discrepancy 發現問題。

所以：

\boxed{ \text{verification state is dynamic}. }

9. 「PROVED」還需要子型別

不能所有 proof 都叫同一個 PROVED。

例如：

PROVED_FORMAL
PROVED_FINITE_EXHAUSTIVE
PROVED_SYMBOLIC
PROVED_CROSS_FORMALISM

而：

TESTED_NUMERIC

不能混入。

因此：

\boxed{ \text{epistemic type must survive storage}. }

10. Proof Lattice Service

建立服務：

ProofService.propose(claim_id)
ProofService.check(proof_id)
ProofService.cluster(claim_id)
ProofService.axioms(proof_id)
ProofService.crosscheck(proof_id)

每個 claim 的：

\mathfrak L(T)

獨立維護。

如果已經有：

[ 10 ]

條相同 proof skeleton，scheduler 應降低：

\text{generate another similar proof}

的分數。

11. Counterexample Service

最小接口：

CounterexampleService.search(claim_id)
CounterexampleService.verify(witness_id)
CounterexampleService.minimize(witness_id)
CounterexampleService.repair(claim_id)

若找到：

x^\ast

必須建立：

COUNTEREXAMPLE node
REFUTES edge

而不是只在 log 裡寫：

found a counterexample.

這使 failure 成為可重用知識。

12. Identity Service

最核心的去重服務：

IdentityService.fingerprint(node)
IdentityService.canonicalize(node)
IdentityService.find_equivalents(node)
IdentityService.classify_variation(parent, child)
IdentityService.branch(parent, child)

其輸出至少：

SURFACE_VARIANT
REPRESENTATION_VARIANT
STRUCTURAL_VARIANT
BRANCH
DUPLICATE
UNKNOWN_RELATION

如果：

UNKNOWN\_RELATION

就不能硬合併。

13. Scheduler Service

最小 scheduler：

Scheduler.frontier(graph)
Scheduler.score(action)
Scheduler.select(portfolio, budget)
Scheduler.sleep(branch)
Scheduler.revive(branch)
Scheduler.stop(branch)

第一版使用 rule-based：

S_F.

不需要一開始就用 RL。

原因是：

\boxed{ \text{debuggable scheduler} > \text{opaque clever scheduler} }

在 MVP 階段尤其重要。

14. Literature Bridge

數學上：

\text{internally derived} \neq \text{historically novel}.

所以需要：

LiteratureService.search(claim)
LiteratureService.link(work_id)
LiteratureService.nearest_prior(claim)

狀態：

LITERATURE_UNCHECKED
NO_MATCH_FOUND
POSSIBLE_MATCH
KNOWN_RESULT
NOVELTY_REVIEW_REQUIRED

即使：

NO\_MATCH\_FOUND,

也不應立即變成：

[ NOVEL. ]

15. Renderer

Renderer 將：

G' \subseteq G

轉成人類介面。

例如：

render_paper(topic)
render_summary(claim_id)
render_proof_explanation(proof_id)
render_failure_history(branch_id)
render_reviewer_packet(claim_id)

因此：

\boxed{ \text{Paper is a projection of canonical state}. }

這與 2026 年 ARA 類工作將 narrative paper 與 machine-executable research artifact 分離的方向高度一致。

16. Runtime Event

每個動作都記：

{
  "event_id": "EV-8821",
  "action": "ASSUMPTION_ABLATION",
  "input": ["CLAIM-31"],
  "output": ["CLAIM-88"],
  "agent": "generator-A",
  "toolchain": ["lean", "python"],
  "cost": {},
  "timestamp": "...",
  "status": "COMPLETE"
}

這形成 Execution Graph：

G_X.

而 knowledge commit 形成 Epistemic Graph：

G_E.

兩者不應混在一起。

17. 三張圖

完整系統同時維持：

\boxed{ G_X,\quad G_A,\quad G_E }

其中：

$G_X$ ：Execution Graph；
$G_A$ ：Artifact Graph；
$G_E$ ：Epistemic Graph。

例如：

RUN-88
  ↓ PRODUCED
proof.lean
  ↓ SUPPORTS
PROOF-19
  ↓ PROVES
CLAIM-7

所以系統能回答兩類不同問題：

AI 做了什麼？

以及：

我們因此知道了什麼？

18. Knowledge Commit

一次真正的研究更新：

\mathcal C_t = ( \Delta V, \Delta E, P, V )

其中：

$\Delta V$ ：新增/更新節點；
$\Delta E$ ：新增關係；
(P)：provenance；
(V)：verification record。

Commit 原則：

\boxed{ \text{no silent overwrite}. }

修正必須：

NEW_NODE --CORRECTS--> OLD_NODE

19. 最小 Trust Boundary

ANKER 至少有五個信任邊界。

Boundary A：Seed Trust

Seed 是否真的可靠？

Boundary B：Formalization Trust

自然語言命題：

[ I ]

是否正確轉成：

[ F? ]

Boundary C：Proof Trust

\Pi:F

是否成立？

Boundary D：Checker Trust

kernel / verifier 是否正確？

Boundary E：World Trust

形式命題是否真的適用現實？

因此：

\boxed{ \text{formal verification only closes some boundaries}. }

20. Lean 在 MVP 中的角色

Lean 不需要負責全部研究。

它負責最適合它的部分：

theorem statement；
proof term；
type checking；
dependency；
axiom inspection；
formal counterexample certificate；
selected cross-check。

Lean 官方目前已明確區分一般 proof validation 與針對未審查 AI-generated proof 的高風險驗證；高等級方案可使用 sandboxed comparator，並以 Lean kernel 和獨立 Rust checker nanoda 等進行重播。這適合作為 ANKER 後期的 high-assurance lane，而不是每個低價值候選都使用最昂貴驗證。

21. Python 在 MVP 中的角色

Python 負責：

candidate generator；
data transform；
numerical test；
finite search；
benchmark；
scheduler；
DB adapter；
reporting。

但 Python PASS 不自動變成 formal theorem。

需要標：

verification_type = NUMERICAL_TEST

或：

verification_type = FINITE_EXHAUSTIVE

並保存 completeness assumptions。

22. Verifier Pipeline

最小 pipeline：

Candidate
   ↓
Parse
   ↓
Type / Domain Check
   ↓
Canonicalize
   ↓
Cheap Counterexample Search
   ↓
Symbolic / Numerical Test
   ↓
Formal Proof Attempt
   ↓
Kernel Check
   ↓
Optional External Check
   ↓
Semantic / Literature Audit

不是每個 candidate 都跑到底。

由 scheduler 決定：

\text{verification depth}.

23. Verification Lanes

可以設三條 lane。

Bronze

低成本：

parse；
type；
unit test；
numerical check。

Silver

中成本：

symbolic derivation；
Lean compile；
kernel check；
counterexample search。

Gold

高成本：

fresh rebuild；
comparator；
external checker；
axiom audit；
second formalization；
literature audit；
human semantic review。

因此：

\boxed{ \text{verification rigor is resource-aware}. }

24. 什麼時候升級驗證？

例如：

R(K)=\text{downstream reuse}.

若：

R(K)\gg0,

或：

Impact(K)\gg0,

就升：

Bronze\rightarrow Silver\rightarrow Gold.

也就是：

越多東西依賴的節點，越值得更嚴格驗證。

這比對所有節點平均投入相同驗證預算合理。

25. Root Dependency Priority

若：

[ K ]

有：

[ 10000 ]

個 descendants，

則其錯誤成本近似：

E_{\mathrm{propagation}}(K)

可能很高。

所以：

\boxed{ \text{verification budget should be dependency-weighted}. }

Root lemma、shared definition、canonical equivalence rule 都應優先進 high-assurance lane。

26. Frontier Queue

每個 action：

action_id
node_id
action_type
score
estimated_cost
required_verifier
dependencies
status

例如：

A-19
CLAIM-7
SEARCH_COUNTEREXAMPLE
0.82
cheap
python
READY

這讓 scheduler 可以像 job system 一樣調度研究。

27. Portfolio

每一輪不要全壓同一類 action。

第一版可使用：

35% proof / verify
20% attack / counterexample
20% structural expansion
10% literature
10% repair
5% exploration

這只是 MVP 初始值。

之後利用 observed gain 自我調整。

28. Budget

定義：

B_t = ( T_t, C_t, G_t, H_t )

可表示：

token；
CPU；
GPU；
human review。

每個 action 都估：

\hat c(a).

實際完成後記：

[ c(a). ]

Scheduler 因而能學：

\hat c\rightarrow c.

29. MVP 先不要做多模型自治

第一版最容易犯的錯誤是：

一開始就建立 20 個 AI agents。

沒有必要。

MVP：

\boxed{ 1\text{ LLM} + 1\text{ deterministic controller} + Lean + Python + DB. }

角色可以是 prompt modes，而不必真的多 agent process。

這樣更容易定位：

generator error；
scheduler error；
verifier error；
storage error。

30. MVP 技術棧

最小：

Python 3.x
SQLite
Lean 4
Mathlib
Pydantic / JSON Schema
Git
Markdown renderer

選配：

PostgreSQL
Neo4j
FastAPI
Docker
external Lean checker

不需要第一版就使用 graph DB。

若：

|V|<10^6,

SQLite / relational schema 足夠做大量 MVP 測試。

31. 最小資料表

可以先只有：

nodes
edges
events
proofs
verifications
frontier_actions

nodes

id
type
status
payload_json
fingerprint
version
created_at

edges

source
relation
target

verifications

node_id
method
status
artifact
checker_version

32. Seed Dataset

第一階段選：

100\sim500

個基礎 theorem。

來源要求：

statement 清楚；
domain 清楚；
可形式化；
易生成變種；
有反例空間；
最好已有 Lean theorem。

領域：

初等代數；
數論；
幾何；
集合；
基礎組合；
線性代數。

不先碰：

哲學；
模糊經驗科學；
高主觀領域。

33. 第一階段 Transformation Set

只做六個：

\mathcal T_0 = \{ \alpha, eq, spec, gen, conv, ablate \}.

其中：

rename；
equivalent rewrite；
specialization；
generalization；
converse；
assumption ablation。

不一開始做無限制跨 theorem composition。

因為 composition 最容易造成：

b^d

爆炸。

34. 第一階段 Error Set

只做：

ASSUMPTION_DELETE
BOUNDARY_CHANGE
QUANTIFIER_CHANGE
CONVERSE_TEST
PROOF_STEP_CORRUPTION

每個 error candidate 都要求：

\text{failure classification}.

35. 第一階段 Verification Set

PARSE
TYPE
NUMERIC
LEAN
COUNTEREXAMPLE

Gold lane 暫時只給：

[ 5% ]

高依賴節點。

36. Phase I 主要假說

最重要的不是「系統發現新定理」。

而是驗證以下工程假說。

H1：結構化去重

\text{duplicate rate} \downarrow.

H2：錯誤鄰域提高邊界辨識

\text{false-premise resistance} \uparrow.

H3：Proof Lattice 增加修復與重用

\text{proof reuse} \uparrow.

H4：Graph-centric continuation 降低長程成本

C_{\mathrm{continue}} \downarrow.

H5：Frontier Scheduler 優於 random expansion

\frac{\Delta\mathcal I}{Cost} \uparrow.

如果這五個都不成立，BKSE Runtime 的工程價值就應被大幅下修。

37. Phase I 不應以「發現未解難題」當 KPI

這點非常重要。

若第一版 KPI 是：

找到人類不知道的新數學。

系統會被錯誤激勵。

第一版 KPI 應是：

\boxed{ \text{reliable expansion quality}. }

包括：

legal variation precision；
branch detection；
counterexample verification；
proof validity；
deduplication；
replay；
scheduler efficiency。

38. Phase II：多 Proof / 多 Checker

Phase I 穩定後加入：

multiple proof prompts
proof clustering
external Lean checker
axiom audit
formalization alternatives

Lean 官方目前已為高風險 AI-generated proof 提供 comparator + external checker 的明確路徑，因此這一層已有現成可借鑑的驗證哲學。

39. Phase II：Literature Bridge

再加入：

arXiv；
OpenAlex；
Semantic Scholar；
Crossref。

但 literature search 只處理：

\text{novelty / precedent}.

不取代 formal verifier。

40. Phase II：Learned Scheduler

先累積：

10^4\sim10^5

個 action outcome。

再訓練：

f_\theta(q,G_t) \rightarrow \widehat{ESG}.

硬規則保留：

UNKNOWN != FALSE
TESTED != PROVED
INTERNAL_NEW != NOVEL
LLM_OUTPUT != VERIFIED

41. Phase III：長期 Runtime

Phase III 才開始：

[ 24/7 ]

或長週期自治。

需要：

crash recovery；
checkpoint；
budget reset；
task lease；
agent identity；
concurrent writes；
deadlock prevention；
audit；
sandbox。

到這一階段，系統才真正接近 long-running autonomous science infrastructure。

2026 年的 XScientist 已把 long-running、branching、repair、daemon scheduling 與 reproducibility artifact 視為核心問題；ScienceClaw 則展示共享 artifact DAG、lineage 與多 agent coordination 的另一種路徑。ANKER 可把這些概念接到 proposition-level epistemic graph，而非重新發明整套 orchestration。

42. 與 2026 ARA 的關係

2026 年的 Agent-Native Research Artifact（ARA）工作明確指出，傳統論文會把 branching research process 壓縮成線性敘事，並提出 machine-executable research package，包含 scientific logic、executable code、exploration graph 與 evidence。

這與 Paper V 的：

\text{Paper} = \operatorname{RenderHuman}(G)

高度收斂。

因此 ANKER 不應宣稱「paper-as-rendering」本身為首次提出。

ANKER 的差異應縮在：

\boxed{ \text{verified epistemic expansion runtime} }

也就是：

proposition identity；
structural variation；
counterexample neighborhood；
proof lattice；
frontier scheduler；

如何以一個 persistent graph LOOP 運行。

43. 與自監督 theorem discovery 的關係

2026 年已有工作從 axioms 與 inference rules 出發，交替進行 proof search 與 useful-theorem extraction，形成可被後續 proof 重用的 theorem library，並發現大量形式 theorem。

這證明：

\boxed{ \text{self-growing formal theorem libraries are technically plausible}. }

ANKER 的差異不在「AI 會自己發現 theorem」本身。

而在於把 theorem discovery 放入更完整狀態：

\text{identity} + \text{negative neighborhood} + \text{proof trust} + \text{lineage} + \text{scheduling}.

44. Runtime 的核心不變量

不管未來換什麼模型、資料庫、proof assistant，ANKER 都應保持以下 invariant。

I1

\text{candidate}\neq\text{knowledge}.

I2

\text{not proved}\neq\text{disproved}.

I3

\text{tested}\neq\text{proved}.

I4

\text{internally new}\neq\text{globally novel}.

I5

\text{formal validity}\neq\text{semantic fidelity}.

I6

\text{more samples}\neq\text{more structures}.

I7

\text{more proofs}\neq\text{more independent trust}.

I8

\text{legal expansion}\neq\text{worthwhile expansion}.

這八條比任何具體實作技術更重要。

45. Failure Taxonomy

Runtime 必須能說自己怎麼失敗。

至少：

GENERATION_ERROR
PARSE_ERROR
TYPE_ERROR
DOMAIN_ERROR
DUPLICATE
FALSE_CLAIM
PROOF_FAILURE
CHECKER_CONFLICT
SEMANTIC_MISMATCH
LITERATURE_DUPLICATE
SCHEDULER_WASTE
RESOURCE_TIMEOUT
TOOL_FAILURE
UNKNOWN

不能都變成：

FAILED

因為 failure 本身也是訓練資料。

46. Runtime 不應自動隱藏失敗

如果：

[ 100 ]

個 candidates 中：

[ 95 ]

個失敗，

但最後找到：

[ 5 ]

個成功，

報告不能只保存成功的 5 個。

完整系統應保存：

\boxed{ \text{failed branch structure}. }

這與 ARA/XScientist 類工作的探索圖理念一致，也與 Paper III 的 error neighborhood 相容。

47. 但也不能把所有失敗放進 Active Graph

區分：

G_{\mathrm{canonical}},

G_{\mathrm{archive}}.

Active graph 只保留高價值路徑。

Archive 保存完整 history。

因此：

\boxed{ \text{preserve} \neq \text{keep active}. }

48. Compression

ANKER 也可以被理解成 research-state compression。

傳統 agent 每次重新讀：

H_{1:t}.

ANKER 只讀：

\operatorname{RelevantSubgraph}(G_t,Q).

因此 token cost：

C_{\mathrm{context}}

理論上可以隨 graph indexing 改善。

這也是 Phase I 應測的核心。

49. 可重播

任何 Gold-level result 必須盡量：

\operatorname{Replay}(K)=PASS.

包括：

code；
environment；
theorem statement；
proof；
checker version；
dependencies。

對非 deterministic experiment：

[ Replay ]

可以被降級為：

[ ProtocolReproduction. ]

但必須明確標記。

50. Human Gate

以下至少預設需要 human review：

高影響 novelty claim；
semantic alignment disputed；
real-world safety implication；
public publication；
external irreversible action。

因此：

\boxed{ \text{autonomous research} \neq \text{autonomous authority}. }

51. MVP Repository Structure

建議：

anker/
├── core/
│   ├── models.py
│   ├── identity.py
│   ├── graph.py
│   └── states.py
├── generators/
│   ├── variation.py
│   └── error_mutation.py
├── verifiers/
│   ├── python_verify.py
│   ├── lean_verify.py
│   └── counterexample.py
├── proofs/
│   ├── lattice.py
│   └── clustering.py
├── scheduler/
│   ├── frontier.py
│   └── score.py
├── render/
│   └── markdown.py
├── storage/
│   ├── db.py
│   └── schema.sql
├── seeds/
├── tests/
└── README.md

這已足夠開始。

52. CLI MVP

第一版 CLI：

anker seed import seeds.json
anker expand CLAIM-001 --operator ablate
anker attack CLAIM-019
anker prove CLAIM-019 --lean
anker verify PROOF-008
anker frontier list
anker frontier run --budget 50
anker graph show CLAIM-019
anker render paper CLAIM-019

不需要 GUI。

53. 第一個 Demo

建議仍然使用直角三角形 theorem family。

原因：

statement 簡單；
結構變種多；
反例容易；
可與 algebra/vector/circle 組合；
可形式化；
人類容易檢查。

Seed：

a^2+b^2=c^2.

讓 runtime 自己：

生成表示變種；
生成 converse；
assumption/domain mutation；
找 counterexample；
生成 proof；
建 equivalence classes；
建 open frontier；
scheduler 選下一步；
render Markdown report。

如果這個流程跑不穩，就不要先碰高等數學。

54. 第二個 Demo

程式語言版：

Seed：

binary_search

變種：

ascending / descending；
duplicates；
custom comparator；
boundary cases；
iterative / recursive；
Python / Rust；
fuzzing；
property tests；
complexity benchmark。

這可以測：

\boxed{ \text{BKSE is not math-only}. }

55. 評測矩陣

至少分四類。

Knowledge Quality

duplicate precision；
variation classification；
branch detection；
counterexample validity；
proof validity。

Runtime Efficiency

token / useful node；
compute / useful node；
continuation cost；
cache reuse。

Research Utility

downstream lemma reuse；
bridge nodes；
proof compression；
resolved frontiers。

Reliability

false admission rate；
UNKNOWN→FALSE error；
TESTED→PROVED error；
novelty false positive；
replay success。

56. 最重要的 Reliability 指標

我會把：

\boxed{ FAR = \frac{\text{invalid nodes admitted to canonical graph}} {\text{all admitted nodes}} }

定義為：

False Admission Rate。

Phase I 最重要的目標之一：

FAR\rightarrow0.

因為一個會產生大量知識但大量污染 canonical graph 的系統沒有價值。

57. 第二個重要指標：Structural Yield

定義：

\boxed{ SY = \frac{ \text{verified non-redundant structural nodes} }{ \text{total executed actions} }. }

它衡量：

花多少研究動作，得到多少真正新增結構？

這比：

\text{samples generated}

重要。

58. 第三個指標：Verification Density

定義：

VD = \frac{ \text{verified relation edges} }{ \text{canonical nodes} }.

但不是越高越好。

如果所有節點被無意義重證：

VD\gg0

也可能浪費。

所以要搭配：

[ ProofDiversity, Reuse, Cost. ]

59. 第四個指標：Continuation Compression

設 document-centric 下一輪所需 context：

C_D.

Graph-centric：

C_G.

定義：

\boxed{ CCR = 1-\frac{C_G}{C_D}. }

測試研究圖是否真的降低長程 continuation cost。

60. Phase I 成功標準

不要求「震撼世界」。

只要求：

\boxed{ \begin{aligned} &FAR \text{ 足夠低};\\ &SY_{\mathrm{scheduler}}>SY_{\mathrm{random}};\\ &\text{dedup works};\\ &\text{counterexamples are replayable};\\ &\text{Lean proofs recheck};\\ &CCR>0;\\ &\text{graph can render usable reports}. \end{aligned} }

只要這些成立，Series I 就已經取得工程上的第一個支持。

61. 外部系統現在已經逼近哪裡？

截至 2026 年中，外部 autonomous-research infrastructure 已經明顯從「一次性 paper generation」往「長期、branching、reproducible artifacts」移動。

ARA 直接把 scientific logic、executable code、exploration graph 與 evidence 分層封裝，並保留 failed branches。

ScienceClaw + Infinite 使用 artifact DAG、typed metadata、parent lineage 與 provenance-aware agent coordination。

XScientist 進一步使用 Git-like protocol、daemon scheduling、quality gates、repair 與 re-execution hooks。

AutoResearchClaw 則強調 iterative challenge、self-healing execution、verifiable reporting、human intervention 與 cross-run learning。

因此 ANKER 的學術位置不應建立在：

「以前研究系統都是線性的。」

這在 2026 年已不再準確。

更精確的位置是：

\boxed{ \text{verified proposition-level expansion substrate} }

及其：

\text{identity} + \text{negative neighborhood} + \text{proof lattice} + \text{frontier scheduling}.

62. 與 RO-Crate 的兼容方向

RO-Crate 1.3 已在 2026-06-22 成為 Recommendation，提供 JSON-LD 形式的 research-object metadata。

ANKER 不應另造一個完全孤立的 package 標準。

未來可以：

\text{ANKER internal graph} \rightarrow \text{RO-Crate export}.

例如：

proof files；
datasets；
runtime logs；
rendered paper；
provenance。

這有利於外部可攜性。

63. 為什麼 Runtime 不是新的「大一統知識本體」

本文仍避免過度宣稱。

ANKER 是：

\boxed{ \text{runtime architecture} }

不是：

\text{complete ontology of all knowledge}.

對哲學、法律、社會科學等領域，命題 identity 與 semantic equivalence 比數學困難得多。

這也是 Series II 存在的理由。

64. 與 Series II 的接口

Series I 假設相對穩定的：

\text{claim identity}.

但高語義領域可能有：

\text{same symbol} \neq \text{same referent}.

因此未來需要：

SemanticState
JudgmentDomain
BaseSpace
ReferentState
TransitionHistory

作為 Knowledge Object 的附加層。

也就是：

\boxed{ \text{Series II} = \text{semantic identity guard for high-semantic domains}. }

65. Series I Phase I 最終整體圖

整套架構可以壓成：

\boxed{ \begin{aligned} \text{Seed} &\rightarrow \text{Identity}\\ &\rightarrow \text{Expansion}\\ &\rightarrow \text{Adversarial Mutation}\\ &\rightarrow \text{Proof / Counterexample}\\ &\rightarrow \text{Verification}\\ &\rightarrow \text{Proof Lattice}\\ &\rightarrow \text{Research Graph}\\ &\rightarrow \text{Frontier Scheduler}\\ &\rightarrow \text{Next Expansion}. \end{aligned} }

這就是 BKSE Runtime。

66. 最終核心 LOOP

用最短形式：

\boxed{ G_{t+1} = \operatorname{Commit} \left[ \operatorname{Verify} \left( \operatorname{Act} \left( \operatorname{Select}(F(G_t)) \right) \right) \right]. }

生成器只出現在：

\operatorname{Act}

內。

所以 AI-native research 的本體不是 LLM。

而是：

\boxed{ \text{state} + \text{operators} + \text{verification} + \text{selection} + \text{history}. }

67. 結論：從「會回答」到「會維持研究世界狀態」

Series I 一開始只是問：

如果我們拿畢氏定理這種基礎知識，讓 AI 不斷證明、變種、重組、驗證，會發生什麼？

經過七篇後，問題已經改變。

我們得到：

\text{Base Knowledge Space Expansion},

\text{Structural Variation Identity},

\text{Error Neighborhood},

\text{Proof Lattice},

\text{AI-Native Research Graph},

\text{Frontier Scheduler},

以及最終：

\boxed{ \text{ANKER Runtime}. }

真正的轉換是：

\boxed{ \text{AI answers research questions} \rightarrow \text{AI maintains a research state}. }

一個成熟的 AI-native research system 不只需要能說：

我認為 theorem (T) 是真的。

它還需要知道：

(T) 從哪裡來；
它是哪一個命題；
有哪些等價表示；
哪些假設必要；
哪些反例已找到；
哪些 proof 真正不同；
哪些 checker 驗過；
哪些 upstream assumptions 被信任；
文獻 novelty 是否檢查；
哪些 branch 已失敗；
哪些 open frontier 尚未完成；
為什麼下一步選擇研究 (Q) 而不是 (R)。

因此，本系列第一階段最終可濃縮為：

\boxed{ \text{AI-Native Research} = \text{Persistent State} + \text{Structured Expansion} + \text{Adversarial Falsification} + \text{Machine Verification} + \text{Attention Scheduling}. }

其中最珍貴的資源不是生成 token。

而是：

\boxed{ \text{verified attention}. }

如果 Phase I MVP 可以證明這套 runtime 在相同資源下，比 document-centric、random-expansion baseline 產生更多非重複、可驗證、可重用、可追溯的結構知識，那麼 BKSE 就不再只是一個關於「高品質資料」的抽象猜想。

它會成為一個可以繼續工程化的 AI-native research architecture。

參考文獻

Lean Project. Validating a Lean Proof. Lean Language Reference, 2026.

Lean Project. Comparator. Lean Prover Project, 2026.

RO-Crate Community. RO-Crate Metadata Specification 1.3. Recommendation, 2026.

Liu, J. et al. (2026). The Last Human-Written Paper: Agent-Native Research Artifacts. arXiv:2604.24658.

Wang, F. Y., Marom, L., Pal, S., et al. (2026). Autonomous Agents Coordinating Distributed Discovery Through Emergent Artifact Exchange. arXiv:2603.14312.

Luo, J. (2026). XScientist: A Git-Like Research Protocol for Long-Running Autonomous Scientific Discovery. arXiv:2607.12301.

Liu, J. et al. (2026). AutoResearchClaw: Self-Reinforcing Autonomous Research with Human-AI Collaboration. arXiv:2605.20025.

Ota, K., Osa, T., & Harada, T. (2026). Self-Supervised Theorem Discovery in a Formal Axiomatic System. arXiv:2606.28747.

Xin, R., Xi, C., Yang, J., et al. (2025). BFS-Prover: Scalable Best-First Tree Search for LLM-based Automatic Theorem Proving. ACL 2025 / arXiv:2502.03438.