# 非適應性計算基線：二十種數學認知障礙的機械化還原

## The Non-Adaptive Computational Baseline: Mechanizing Twenty Barriers in Mathematical Problem Solving

**系列：計算基底、認知干預與廣義智能計算研究，第 2 篇／共 8 篇**  
**作者：Neo.K**  
**機構：EveMissLab／一言諾科技有限公司**  
**日期：2026-08-07**

---

## 摘要

前篇提出二十類數學問題障礙，並以搜索、表示、結構、證明與元問題五個維度描述數學問題對不同求解系統形成的困難。然而，「某問題需要直覺」、「需要發明表示法」、「需要找到中間引理」等敘述仍混合了兩個不同層次：一是問題本身需要完成的狀態轉換；二是智能體如何選擇、預測與組織這些轉換。

本文刻意拿掉後者，建立一個**非適應性計算基線**：

$$
\boxed{
\text{Non-Adaptive Computational Baseline, NACB}
}
$$

NACB 並非沒有演算法、沒有啟發式，也不等於單純逐項暴力枚舉。它允許任何事先指定且可機械執行的：

- 搜索；
- 剪枝；
- 排序；
- 動態規劃；
- clause learning；
- cache；
- 隨機抽樣；
- 形式推導；
- 表示轉換；
- 證明驗證。

但執行期間的所有此類行為都必須由既定程序生成，而不能由一個高階智能體主動重新定義「現在應該解什麼問題」、「應該使用什麼概念語言」、「哪些規則才算有效」或「為什麼原問題可能問錯」。

本文重新分析前篇二十種數學障礙，指出其中大量看似「認知型」的能力，在完全機械化後可以轉化為：

$$
\boxed{
\begin{aligned}
&\text{Enumeration},\\
&\text{Transformation Search},\\
&\text{Proof Search},\\
&\text{Verification},\\
&\text{Compression Search},\\
&\text{Resource Management}.
\end{aligned}}
$$

然而，這並不意味所有數學問題只是「給足算力即可」。可計算性、可判定性、無限搜索、表示空間大小、驗證器本身的正確性，以及不可判定問題仍構成根本界線。

本文的核心主張是：

$$
\boxed{
\text{許多被描述成「智能困難」的現象，
在固定形式系統中可以重新表達成計算空間與資源配置問題；
但這不等價於它們在所有情況下都可有效計算。}
}
$$

這為下一篇「廣義智能體的認知干預算子」建立了一個必要的零階比較基線。

---

## 關鍵詞

非適應性計算、證明搜尋、枚舉、形式驗證、計算複雜度、可判定性、暴力搜尋、數學推理、AI 數學、表示空間

---

# 1. 為什麼需要一個「拿掉智能」的基線？

當我們說：

> 「這題需要直覺。」

其實可能包含兩種完全不同的敘述。

第一種是：

> 沒有好的策略時，候選空間太大。

第二種則是：

> 存在某種不能由固定計算程序實現的特殊能力。

這兩件事不能直接畫上等號。

同樣地：

> 「需要發明一個新表示法」

也可能只是意味著：

$$
\text{現有表示空間中存在一個非常低機率、但可描述的有用表示。}
$$

如果所有有限描述都可枚舉，那麼理論上可以搜索表示法。

真正的問題可能不是：

$$
\text{能不能產生它？}
$$

而是：

$$
\text{要搜索多久？}
$$

因此本文提出一個反事實問題：

> 假設完全不允許智能體在執行中進行高階主動選擇、經驗式重構、直覺預判或問題重新定義，只允許事先指定的可計算規則，那麼前篇二十種數學困難各自會變成什麼？

---

# 2. NACB 的正式定義

定義一個非適應性計算系統：

$$
\boxed{
\mathcal N=
(
\mathcal S,
\mathcal A,
T,
\pi_0,
V,
G,
\mathcal B
)
}
$$

其中：

$$
\mathcal S
$$

是可表示的計算狀態集合；

$$
\mathcal A
$$

是可執行操作集合；

$$
T:
\mathcal S\times\mathcal A
\rightarrow
\mathcal S
$$

是狀態轉移；

$$
\pi_0:
\mathcal S
\rightarrow
\Delta(\mathcal A)
$$

是**事先固定的操作政策**；

$$
V
$$

是候選答案、證明或狀態的驗證程序；

$$
G
$$

是固定任務目標；

$$
\mathcal B=(B_T,B_S,B_C,\ldots)
$$

是時間、空間、通訊等資源預算。

其中：

$$
\Delta(\mathcal A)
$$

允許 $\pi_0$ 為確定或隨機政策。

---

# 3. 「非適應性」不等於「不會根據狀態改變行為」

這是一個重要校正。

一個 A* 搜索器會根據節點成本決定下一個節點。

一個 SAT solver 可以：

- unit propagation；
- conflict detection；
- clause learning；
- restart；
- branching heuristic。

這些表面上都「會學習」或「會調整」。

本文仍允許把它們放進 NACB。

因為只要：

$$
\pi_0
$$

和更新規則在執行前已被固定，那麼執行中的變化仍然只是：

$$
s_t\rightarrow s_{t+1}.
$$

換句話說：

$$
\boxed{
\text{state adaptation}
\neq
\text{policy-level cognitive adaptation}.
}
$$

本文所排除的是例如：

> 「這套問題表示法不好，我重新發明一種表示空間。」

> 「這個 proof objective 本身可能問錯了，我改問另一個問題。」

> 「我過去的搜索風格一直失敗，因此我要修改自己判定『好方法』的標準。」

除非這些行為本身已經作為普通可枚舉操作，被寫進 $\pi_0$ 所允許的程序。

---

# 4. NACB 可以很強

因此 NACB 不應被理解為：

$$
\text{for i in range(N): test(i)}
$$

而可以包含非常先進的計算程序。

例如：

$$
\boxed{
\text{generate}
+
\text{rank}
+
\text{search}
+
\text{prune}
+
\text{verify}
}
$$

只要 ranking function、search rule、pruning rule 與 verifier 都事先固定。

這一區分對 AI 數學尤其重要。

現代形式證明系統通常同時依賴 proof generation、premise retrieval、搜索以及 kernel verification；例如 LeanSearch v2 的研究顯示，更好的 global premise retrieval 可以直接提高固定 prover loop 的證明成功率，說明「找到哪些既有引理值得拿來用」本身就是一個獨立搜索瓶頸。

而 2026 年的 Pythagoras-Prover 則進一步顯示，proof length、training data 與 inference compute 都會強烈影響形式證明效果；換言之，單純存在一個可驗證 proof 並不代表「找到它」的計算成本很小。

---

# 5. 第一類：小尺度暴力搜尋不能終結全稱命題

設：

$$
P(n)
$$

為一個可判定 predicate。

NACB 可以執行：

$$
P(1),P(2),P(3),\ldots
$$

若存在反例：

$$
\exists n:\neg P(n),
$$

而枚舉是公平的，則某些情況下：

$$
\text{finite counterexample}
\Rightarrow
\text{eventual discovery}.
$$

然而若：

$$
\forall n\,P(n),
$$

則即使已經驗證：

$$
P(1)=P(2)=\cdots=P(10^{100})=1,
$$

仍然不能單靠這些計算推出：

$$
\forall n\,P(n).
$$

因此障礙轉化成：

$$
\boxed{
\text{finite enumeration}
\not\Rightarrow
\text{universal certification}.
}
$$

NACB 若要完成全稱命題，必須：

1. 找到一個有限證明；
2. 找到有限 certificate；
3. 或使用另一個已證定理把無限集合壓縮成有限推理。

---

# 6. 第二類：無法靠知名題型匹配

對智能體而言：

> 「看出這是 Pell equation」

可能像是一個瞬間洞見。

對 NACB 而言，不存在「看出」。

但若有可枚舉轉換族：

$$
\mathcal R=
\{
R_1,R_2,\ldots
\},
$$

系統可以嘗試：

$$
R_1(P),R_2(P),R_3(P),\ldots
$$

並檢查轉換後問題是否進入某個已知可解類別。

因此：

$$
\boxed{
\text{pattern recognition}
\rightarrow
\text{transformation-space search}.
}
$$

困難沒有消失。

它只是從：

$$
\text{「不知道是哪一類問題」}
$$

改寫成：

$$
\text{「要在多少候選轉換中才能命中有效轉換？」}
$$

---

# 7. 第三類：需要多個不自然結構相連

若正確路徑為：

$$
P
\xrightarrow{R_a}
P_1
\xrightarrow{R_b}
P_2
\xrightarrow{R_c}
P_3,
$$

而每一層有平均 $b$ 個候選操作，深度為 $d$，最粗略的完整搜索可能接近：

$$
O(b^d).
$$

因此所謂：

> 「跨兩個領域的非直覺洞見」

在固定操作語言下可以被翻譯成：

$$
\boxed{
\text{deep composition search}.
}
$$

真正的難點是 branch factor 和 depth。

---

# 8. 第四類：大量數值證據不能代替證明

這一點對 NACB 反而很乾淨。

定義兩個不同 verifier：

$$
V_{\mathrm{instance}}(P,n)
$$

和：

$$
V_{\mathrm{proof}}(\pi,P).
$$

前者只回答：

$$
P(n)?
$$

後者回答：

$$
\pi\vdash P?
$$

因此：

$$
\boxed{
\underbrace{\forall n\le N,\;V_{\mathrm{instance}}(P,n)=1}_{\text{finite computation}}
}
$$

不會被 verifier 自動當成：

$$
\boxed{
V_{\mathrm{proof}}(\pi,\forall nP(n))=1.
}
$$

這裡「證據」與「證明」在形式層面可完全分離。

---

# 9. 第五類：高度誘惑的假證明

「誘惑」本身不屬於 NACB。

若 proof checker 正確，則：

$$
V(\pi,P)=
\begin{cases}
1,&\pi\text{ 合法證明}\\
0,&\text{其他}.
\end{cases}
$$

形式錯誤不是心理陷阱，而只是驗證失敗。

因此：

$$
\boxed{
\text{cognitive proof trap}
\rightarrow
\text{verification problem}.
}
$$

然而這裡必須再加一道重要限制：

$$
\boxed{
\text{verified formal derivation}
\neq
\text{intended theorem correctly formalized}.
}
$$

2026 年對多個 Lean theorem-proving benchmarks 的審計發現，machine-checked proof 仍不能保證 formal statement 忠實表達原本 informal problem；研究甚至找出 vacuous theorem、錯誤形式化與 benchmark evaluation defect。

因此 verifier 只能保證：

$$
\pi\vdash F,
$$

不能自動保證：

$$
F=\text{我們原本想證明的命題}.
$$

這個差異將在後續「智能干預」與「問題重構」部分再次出現。

---

# 10. 第六類：局部與全局互相欺騙

NACB 不會被「欺騙」。

如果：

$$
P(U_i)
$$

與：

$$
P\left(\bigcup_iU_i\right)
$$

都是明確可計算對象，那就分別計算。

難點只在：

$$
\boxed{
\text{全局對象是否有限可表示、有限可驗證？}
}
$$

如果整體涉及：

$$
n\rightarrow\infty,
$$

則問題重新落入：

- 極限證明；
- 無限量詞；
- compact certificate；
- structural proof。

因此局部—全局障礙被改寫成：

$$
\boxed{
\text{representation size}
+
\text{global verification}.
}
$$

---

# 11. 第七類：找到不變量，但不是有用的不變量

設候選函數語言：

$$
\mathcal F=
\{f_1,f_2,\ldots\}.
$$

可以枚舉並驗證：

$$
f_j(Tx)=f_j(x).
$$

因此尋找 invariant 本身可以轉成：

$$
\boxed{
\text{function-space enumeration}.
}
$$

但若找到：

$$
10^8
$$

個 invariant，真正問題仍然是：

$$
f_j\Rightarrow P?
$$

因此還需要第二層：

$$
V(
f_j\Rightarrow P
).
$$

所以：

$$
\boxed{
\text{useful invariant search}
=
\text{invariant enumeration}
+
\text{implication proof search}.
}
$$

---

# 12. 第八類：正確中間命題更難想到

設形式語言中的合法公式可枚舉為：

$$
Q_1,Q_2,Q_3,\ldots
$$

NACB 可以搜索：

$$
P_{\mathrm{premise}}
\vdash Q_i
$$

以及：

$$
Q_i\vdash P_{\mathrm{target}}.
$$

甚至：

$$
Q_{i_1},Q_{i_2},\ldots,Q_{i_k}
$$

的多 lemma 組合。

因此：

$$
\boxed{
\text{lemma invention}
\rightarrow
\text{formula-space search}.
}
$$

形式上不需要「靈感」。

但公式空間的增長速度足以令實際搜索不可承受。

---

# 13. 第九類：發明新的表示法

只要表示方式可以被有限描述：

$$
r\in\Sigma^\ast,
$$

它就可以被枚舉：

$$
r_1,r_2,r_3,\ldots
$$

例如：

$$
r_1(P)=\text{graph encoding},
$$

$$
r_2(P)=\text{matrix encoding},
$$

$$
r_3(P)=\text{generating function}.
$$

理論上：

$$
\boxed{
\text{representation invention}
\rightarrow
\text{representation-space enumeration}.
}
$$

但這裡有一個巨大代價：

對每個 $r_i$，還需要判斷：

$$
\operatorname{Useful}(r_i,P)?
$$

而「有用」本身通常又需要解一部分原問題才能知道。

因此表示搜索具有高度自指性：

$$
\boxed{
\text{為了知道表示是否值得用，
往往必須先使用它進行昂貴計算。}
}
$$

---

# 14. 第十類：表面領域與核心領域不同

對純形式計算而言：

$$
\text{number theory},
\quad
\text{graph theory},
\quad
\text{linear algebra}
$$

最終都可編碼成符號與規則。

學科名稱本身不是計算邊界。

若存在：

$$
R:
\mathcal P_{\mathrm{number}}
\rightarrow
\mathcal P_{\mathrm{graph}},
$$

且 $R$ 可描述，NACB 即可枚舉或直接使用 $R$。

因此：

$$
\boxed{
\text{cross-domain insight}
\rightarrow
\text{cross-representation transformation}.
}
$$

這也說明：

> 「跨領域」很可能主要是智能體的知識組織問題，而不一定是基礎計算模型中的原生分類。

---

# 15. 第十一類：對稱性陷阱

若 NACB 完整枚舉：

$$
x\in X,
$$

它不會因為：

$$
P
$$

具有對稱性，就心理上偏好對稱解。

因此：

$$
\text{symmetry bias}=0
$$

是可能的。

但代價是：

$$
|X|
$$

全部都要算。

若利用群作用 $G$：

$$
X/G
$$

進行 quotient search，可以大幅壓縮。

所以：

$$
\boxed{
\text{不使用偏好}
\Rightarrow
\text{避免錯誤先驗},
}
$$

但也可能意味：

$$
\boxed{
\text{失去巨大的搜索壓縮}.
}
$$

---

# 16. 第十二類：證明不存在

有限空間：

$$
X=\{x_1,\ldots,x_N\}
$$

可以直接驗證：

$$
\forall i,\neg P(x_i).
$$

但若 $X$ 無限，持續找不到：

$$
x
$$

只說明：

$$
\text{目前尚未找到}.
$$

而不是：

$$
\nexists x.
$$

因此最好把不存在轉成有限證書：

$$
\exists \pi:
\pi\vdash\neg\exists xP(x).
$$

即：

$$
\boxed{
\text{infinite non-existence}
\rightarrow
\text{finite certificate search}.
}
$$

如果不存在這樣的可得 certificate，枚舉程序可能永遠不能停止。

---

# 17. 第十三類：分類全部解

若：

$$
|\mathcal E|<\infty,
$$

可全部列舉。

但若：

$$
|\mathcal E|
$$

巨大甚至無限，一個更有用的輸出是：

$$
\mathcal E=
\{G(\theta):\theta\in\Theta\}.
$$

此時需要搜索：

$$
G_1,G_2,\ldots
$$

以及驗證：

$$
\operatorname{Im}G_i=\mathcal E.
$$

因此分類問題變成：

$$
\boxed{
\text{solution enumeration}
+
\text{compression/generator search}.
}
$$

---

# 18. 第十四類：相變點

對參數：

$$
\lambda
$$

可以執行：

$$
\lambda_1,\lambda_2,\ldots
$$

的數值掃描。

若發現行為在：

$$
\lambda\approx1.732
$$

附近改變，只得到：

$$
\lambda_c\approx1.732.
$$

它不等於：

$$
\lambda_c=\sqrt3,
$$

更不等於：

$$
\text{證明 }\sqrt3\text{ 是唯一臨界點}.
$$

因此需區分：

$$
\boxed{
\text{transition detection},
\quad
\text{exact identification},
\quad
\text{criticality proof}.
}
$$

三者可以具有完全不同成本。

---

# 19. 第十五類：邊界案例

這類問題在 NACB 下反而可能比較容易管理。

只要 domain 已明確定義：

$$
X,
$$

並且枚舉或 verifier 覆蓋全部條件，就不存在：

> 「我覺得 $x=0$ 應該沒差。」

但是：

$$
\boxed{
\text{系統不會主動發現定義域本身漏寫了 }x=0.
}
$$

所以：

- 已形式化邊界：計算問題；
- 未形式化邊界：規格問題。

這兩者不能混在一起。

---

# 20. 第十六類：量詞順序

形式語言中：

$$
\forall x\exists y\,P(x,y)
$$

和：

$$
\exists y\forall x\,P(x,y)
$$

是不同 syntax tree。

若 inference rules 正確，proof checker 不會因語義「感覺接近」而交換兩者。

因此：

$$
\boxed{
\text{quantifier confusion}
\rightarrow
\text{formal syntax/inference verification}.
}
$$

這是形式化相對自然語言推理的一項重要優勢。

---

# 21. 第十七類：lemma 的逆否與多方向使用

若已有：

$$
A\Rightarrow B,
$$

形式邏輯允許導出：

$$
\neg B\Rightarrow\neg A.
$$

所以 NACB 可以把整個推理空間視為 graph：

$$
G_{\mathrm{proof}}
=
(V_{\mathrm{statement}},E_{\mathrm{inference}}).
$$

求證：

$$
P
$$

變成某種：

$$
\boxed{
\text{reachability/search problem}.
}
$$

難點不在「看不出逆否」的心理障礙，而在：

$$
|V|,
\quad
|E|,
\quad
\text{branching},
\quad
\text{search depth}.
$$

---

# 22. 第十八類：必須排除大量錯路

形式化後就是搜索樹：

$$
\mathcal T.
$$

每一分支：

$$
H_i
$$

繼續展開，直到：

$$
H_i\vdash\bot
$$

或達到資源界限。

沒有預判時，可能：

$$
\boxed{
\text{expand almost everything}.
}
$$

因此「研究經驗可以少走很多錯路」在 NACB 中被翻譯為：

$$
\boxed{
\text{better branch ordering or pruning policy}.
}
$$

但若 policy 固定，它仍屬 NACB。

---

# 23. 第十九類：最短證明與最容易發現證明不同

若按 proof length 枚舉所有合法 proof terms：

$$
|\pi|=1,2,3,\ldots
$$

第一個成功的：

$$
\pi^\ast
$$

滿足：

$$
\pi^\ast
=
\arg\min_{\pi:V(\pi,P)=1}
|\pi|.
$$

所以最短 proof 在理論上可由枚舉定義。

但：

$$
\boxed{
\text{minimum description}
\neq
\text{minimum discovery cost}.
}
$$

最短證明可能藏在一個極難命中的 proof prefix 後面。

較長但結構局部明顯的證明反而更容易找到。

近期形式證明工作也持續顯示長 proof traces 和 inference compute 是實際瓶頸，而並非只有「有沒有合法 proof」這個二元問題。

---

# 24. 第二十類：題目本身需要被質疑

這是 NACB 最特殊的一類。

如果目標固定：

$$
G=P,
$$

那麼系統只會求解 $P$。

它不會突然問：

> 為什麼要證 $P$？

除非我們預先定義一個 problem-neighborhood operator：

$$
\mathcal N(P)
=
\{
P_1,P_2,\ldots
\}.
$$

例如允許產生：

- weaker assumptions；
- stronger conclusions；
- equivalent forms；
- removed conditions；
- alternative constants；
- dual statements。

此時「質疑問題」仍然可以被計算化成：

$$
\boxed{
\text{problem-space enumeration}.
}
$$

但新的核心問題立刻出現：

> 誰決定 $\mathcal N(P)$ 的生成規則？

如果這些規則仍是固定的，它只是更大的 NACB。

若系統能自己改變「哪些鄰近問題值得生成」的判準，就開始進入下一篇要處理的認知干預層。

---

# 25. 二十種障礙在 NACB 下的壓縮

前述二十項在拿掉主動智能干預後，可以大致映射到六種基礎類別。

| 原障礙 | NACB 主要形式 |
|---|---|
| 小尺度搜索不足 | Enumeration / Proof Search |
| 無標準題型 | Transformation Search |
| 多結構連接 | Deep Transformation Search |
| 數值證據不足 | Verification / Proof Search |
| 假證明誘惑 | Verification |
| 局部—全局 | Global Representation / Verification |
| useful invariant | Function Search + Proof Search |
| 中間 lemma | Formula Search |
| 新表示法 | Representation Search |
| 跨領域 | Transformation Search |
| 對稱陷阱 | Coverage vs Compression |
| 不存在 | Certificate Search |
| 分類全部解 | Compression / Generator Search |
| 相變 | Enumeration + Exact Proof |
| 邊界案例 | Coverage / Specification |
| 量詞 | Formal Verification |
| 多方向 lemma | Graph Search |
| 排除錯路 | Tree Search |
| 最短證明 | Ordered Proof Enumeration |
| 質疑問題 | Problem-Space Search |

這個表不是數學上的等價定理，而是一套**機械化還原 taxonomy**。

---

# 26. 六個基礎計算類別

## 26.1 枚舉

$$
\boxed{
\mathcal E_{\mathrm{num}}
}
$$

對一個可生成空間：

$$
X=\{x_1,x_2,\ldots\},
$$

逐步產生候選。

其價值是：

$$
\text{coverage}.
$$

代價是：

$$
\text{scale}.
$$

---

## 26.2 轉換搜索

$$
\boxed{
\mathcal E_{\mathrm{trans}}
}
$$

在操作空間：

$$
R_1,R_2,\ldots
$$

中搜索：

$$
P\rightarrow R_i(P).
$$

它涵蓋：

- 重寫；
- 代換；
- 新座標；
- graph encoding；
- domain translation。

---

## 26.3 證明搜索

$$
\boxed{
\mathcal E_{\mathrm{proof}}
}
$$

在 formal derivation space 中尋找：

$$
\pi
$$

使：

$$
V(\pi,P)=1.
$$

proof generation 與 proof verification 必須分離。

實際系統中 premise retrieval 也可以成為主要瓶頸：LeanSearch v2 的結果顯示，在固定 prover 下改善前提檢索即可明顯提高證明成功率。

---

## 26.4 驗證

$$
\boxed{
\mathcal V
}
$$

理想化為：

$$
V(x)\in\{0,1\}.
$$

驗證通常比發現更結構化，但它也不是完全免費。

而且：

$$
\boxed{
\text{kernel correctness}
\neq
\text{specification correctness}.
}
$$

2026 年 ACL Industry Track 的 T² 工作也顯示，單純 compile success 可能高估 theorem generation 的 semantic correctness；作者使用依賴後續 theorem 是否仍能成立的測試方式，得到明顯更低的 semantic accuracy。

所以 verifier 本身也有不同層次。

---

## 26.5 壓縮搜索

$$
\boxed{
\mathcal E_{\mathrm{comp}}
}
$$

大量答案：

$$
x_1,x_2,\ldots
$$

可能需要被壓成：

$$
G(\theta),
$$

或一個 theorem：

$$
T.
$$

從純計算角度，一個高品質 invariant、分類定理或公式都可視為：

$$
\boxed{
\text{a compact representation of a large state family}.
}
$$

這不是在宣稱「所有數學洞見就是資料壓縮」，而是指出**壓縮率**提供了一個很有用的計算觀點。

---

## 26.6 資源管理

即使問題可計算：

$$
f(x)
$$

仍可能有：

$$
T(n)=2^{2^n}
$$

或其他不可實際承受的資源需求。

因此：

$$
\boxed{
\text{computable}
\neq
\text{feasibly computable}.
}
$$

時間：

$$
T(n),
$$

空間：

$$
S(n),
$$

通訊：

$$
C(n),
$$

以及平行性都需要獨立考慮。

---

# 27. 暴力搜尋的重新定義

「暴力搜尋」經常被當成低階甚至負面方法。

本文採更中性的定義：

$$
\boxed{
\mathcal C_{\mathrm{brute}}
=
\text{explicit realization of candidate state space under weak structural priors}.
}
$$

中文可表述為：

> **在很少依賴問題特定結構先驗的情況下，顯式實現候選狀態空間的能力。**

因此暴力搜尋不是「沒有能力」。

它具有一個非常重要的特性：

$$
\boxed{
\text{coverage}.
}
$$

如果：

- 空間有限；
- verifier 正確；
- 資源足夠；

那完整 enumeration 可以提供其他 heuristic 方法未必具有的覆蓋保證。

---

# 28. 「暴力」與「聰明算法」不是本體上的二分

例如動態規劃、A*、SAT solving 或 theorem proving 本身都可能同時具有：

$$
\text{enumeration}
+
\text{pruning}
+
\text{memoization}
+
\text{heuristics}.
$$

因此更正確的軸不是：

$$
\text{brute}
\leftrightarrow
\text{intelligent}.
$$

而是：

$$
\boxed{
\text{weakly structured exhaustive realization}
\leftrightarrow
\text{strongly structured selective realization}.
}
$$

兩端都仍然是 computation。

---

# 29. 可計算性是第一道真正不能靠更多算力消失的界線

到目前為止，大量障礙都可以被改寫為：

> 搜索空間太大。

但是存在另一種問題：

$$
\boxed{
\text{不存在對所有輸入皆正確停止的一般判定算法}.
}
$$

最典型為 Halting Problem。

不存在一般算法：

$$
H(M,x)
$$

能對所有程式 $M$ 和輸入 $x$ 正確判斷：

$$
M(x)
$$

是否最終停機。

這與：

$$
T(n)=10^{10^{100}}
$$

不是同一種困難。

後者是：

$$
\text{非常昂貴但仍有算法}.
$$

前者是：

$$
\text{不存在這樣的通用判定算法}.
$$

因此最少應區分：

$$
\boxed{
\text{tractable}
\subset
\text{computable but intractable}
\subsetneq
\text{all mathematically expressible decision problems}.
}
$$

---

# 30. 半判定與公平枚舉

另一個容易被忽略的修正是：

> 「一直枚舉就一定找得到答案」

並不總成立。

若候選集可遞歸枚舉，且 witness 存在：

$$
\exists xP(x),
$$

在公平枚舉下可能最終找到 witness。

但對：

$$
\forall xP(x)
$$

或：

$$
\nexists xP(x)
$$

並不一定能有限停止。

因此需區分：

$$
\boxed{
\text{decidable},
\quad
\text{semi-decidable},
\quad
\text{undecidable}.
}
$$

這是後續任何「給無限算力就全部算完」敘述必須守住的邏輯邊界。

---

# 31. 無限資源也不能被隨意使用

「假設無限算力」本身還需要非常謹慎。

因為：

$$
\text{arbitrarily large finite resources}
$$

與：

$$
\text{completed actual infinity}
$$

不是同一個計算模型。

如果對每個有限 $N$ 都可以計算：

$$
f_N,
$$

並不代表有一台普通機器可以在有限時間執行真正無限步計算。

因此本文使用的極限語言只表示：

$$
B_T,B_S\rightarrow\text{arbitrarily large finite values},
$$

而不自動引入超圖靈計算。

---

# 32. NACB 的一個通用程序

可以寫出一個極端抽象的 NACB：

$$
s_0=P.
$$

在每一輪：

$$
\mathcal C_t
=
\operatorname{Generate}(s_t),
$$

產生：

- candidate；
- transformation；
- lemma；
- representation；
- proof prefix。

再：

$$
\mathcal C_t'
=
\operatorname{Filter}_{\pi_0}(\mathcal C_t).
$$

接著：

$$
V(c)
$$

驗證每個候選。

成功則：

$$
\operatorname{Return}(c).
$$

否則：

$$
s_{t+1}
=
\operatorname{Update}(s_t,\mathcal C_t').
$$

這裡即使：

$$
\operatorname{Filter}
$$

非常複雜，只要它事先固定，仍屬 NACB。

---

# 33. NACB 可以模擬「看起來很像智能」的行為

例如我們可以預先寫：

> 如果發現十次 symmetry search 都失敗，就改用 asymmetric search。

形式上：

$$
c_{\mathrm{sym}}\ge10
\Rightarrow
a_{t+1}=a_{\mathrm{asym}}.
$$

它看起來像：

> 「系統反思後改變策略。」

但只要規則預先存在，它仍只是：

$$
T(s_t).
$$

這揭露了一個本系列很重要的方法論問題：

$$
\boxed{
\text{行為看起來具有智能}
\not\Rightarrow
\text{必須引入新的計算本體}.
}
$$

因此下一篇討論「認知干預」時，我們要特別避免用表面行為定義智能。

---

# 34. 那麼下一篇的「智能干預」究竟還剩什麼？

如果所有固定規則都能放進 NACB，那智能干預不能簡單定義成：

> 會剪枝。

因為固定 SAT solver 也會。

也不能只是：

> 會使用記憶。

cache 也會。

更不能只是：

> 會根據結果修改後續行動。

普通 feedback controller 就會。

因此下一篇真正需要研究的是：

$$
\boxed{
\text{高階策略空間本身的條件式修改}.
}
$$

例如：

$$
\pi_t
\rightarrow
\pi_{t+1},
$$

以及：

$$
\mathcal R_t
\rightarrow
\mathcal R_{t+1},
$$

$$
G_t
\rightarrow
G_{t+1},
$$

甚至：

$$
V_t
\rightarrow
V_{t+1}.
$$

也就是：

> 不只是狀態在變，而是「產生狀態的計算組織方式」也成為可修改對象。

---

# 35. 一個重要的層級區分

因此我們可以先得到：

### Level 0：狀態轉換

$$
s_t\rightarrow s_{t+1}.
$$

---

### Level 1：固定政策下的操作選擇

$$
a_t=\pi_0(s_t).
$$

---

### Level 2：政策更新

$$
\pi_t\rightarrow\pi_{t+1}.
$$

---

### Level 3：表示與問題空間更新

$$
(\mathcal S,\mathcal R,G)
\rightarrow
(\mathcal S',\mathcal R',G').
$$

---

### Level 4：修改「如何修改自己」的規則

$$
\Psi_t\rightarrow\Psi_{t+1}.
$$

NACB 的核心參照點主要位於：

$$
\boxed{
\text{Level 0--1}
}
$$

並允許 Level 2–4 的行為**被事先固定模擬**，但不把這種固定模擬自動稱為「智能主動干預」。

---

# 36. NACB 不等於現實計算機的全部能力

還要避免另一個錯誤：

> 「NACB = 今日電腦。」

不是。

NACB 是理論比較基線。

實際現代電腦／AI 系統通常是混合體：

$$
\boxed{
\text{fixed algorithms}
+
\text{learned policies}
+
\text{external memory}
+
\text{adaptive models}
+
\text{human intervention}.
}
$$

所以這裡不是在分類硬體，而是在拆解功能來源。

---

# 37. 一個新的觀點：數學中的「洞見」可能對應搜索空間的巨大降維

假設原始候選數：

$$
|X|=2^n.
$$

找到一個 structural invariant 後只需研究：

$$
|X'|=n^3.
$$

則洞見帶來：

$$
\frac{|X|}{|X'|}
=
\frac{2^n}{n^3}.
$$

倍的狀態空間壓縮。

這使我們可以暫時把某些洞見理解成：

$$
\boxed{
\text{computationally valuable state-space transformations}.
}
$$

但此處仍不能說：

$$
\text{insight}=\text{compression}.
$$

因為：

- 哪種壓縮保留目標資訊？
- 哪種表示具有可證明性？
- 為什麼選這個壓縮？

仍然是後續智能干預要處理的問題。

---

# 38. 一個更精確的 NACB 有效成本

對問題 $P$，可以暫時定義：

$$
C_{\mathrm{NACB}}(P)
=
C_E
+
C_T
+
C_\Pi
+
C_V
+
C_K
+
C_R,
$$

其中：

$$
C_E=\text{enumeration cost},
$$

$$
C_T=\text{transformation-search cost},
$$

$$
C_\Pi=\text{proof-search cost},
$$

$$
C_V=\text{verification cost},
$$

$$
C_K=\text{compression-search cost},
$$

$$
C_R=\text{resource-management overhead}.
$$

這不是要求所有問題真的線性相加，而是作為 bookkeeping model。

它至少迫使我們問：

> 一個系統看似「只用了三步」得到答案時，有多少成本其實藏在預計算、索引、定理庫或離線搜索裡？

---

# 39. 驗證能力也不是絕對可靠的終點

形式驗證具有巨大價值，但仍需區分三層：

$$
V_1:
\text{syntax validity},
$$

$$
V_2:
\text{formal derivation validity},
$$

$$
V_3:
\text{semantic/specification fidelity}.
$$

可能有：

$$
V_2=1,
$$

但：

$$
V_3=0.
$$

即：

> 證明形式上完全合法，但證錯了問題。

NTP4VC 在真實軟體 verification conditions 上的研究也顯示，即使神經 theorem proving 在競賽數學有進展，真實 program verification 的 proof obligations 仍然形成明顯瓶頸。

因此：

$$
\boxed{
\text{verification itself has a hierarchy}.
}
$$

---

# 40. NACB 的真正作用

本文不主張：

> 「智能其實不存在，全部只是暴力搜尋。」

也不主張：

> 「只要算力無限，數學全部可解。」

本文只建立一個對照實驗：

$$
\boxed{
\text{如果移除高階智能體干預，
有多少表面上的認知困難仍可被改寫成明確計算任務？}
}
$$

答案是：

> 很多。

但：

$$
\boxed{
\text{可寫成計算任務}
\neq
\text{可有效完成}
\neq
\text{可判定}.
}
$$

這三者必須始終分開。

---

# 41. 本文提出的六個工作命題

## 命題一：機械化還原命題

對前篇大量認知障礙，在給定有限形式語言與驗證規則後，可重新描述為：

$$
\boxed{
\text{state-space generation/search/verification problems}.
}
$$

此命題不宣稱其計算成本可接受。

---

## 命題二：認知描述與計算描述非互斥

一句：

> 「需要直覺。」

和一句：

> 「正確操作在候選空間中的先驗概率極低。」

可以同時成立。

因此：

$$
\boxed{
\text{cognitive explanation}
\neq
\text{computational explanation},
}
$$

但兩者可以描述同一現象的不同層級。

---

## 命題三：固定啟發式仍屬計算基線

若 heuristic：

$$
h(s)
$$

在執行前已指定，則：

$$
a_t
=
\arg\min_a h(T(s_t,a))
$$

仍屬 NACB。

因此：

$$
\boxed{
\text{heuristic search}
\not\Rightarrow
\text{cognitive intervention}.
}
$$

---

## 命題四：驗證與發現非對稱

通常可以存在：

$$
C_{\mathrm{verify}}(\pi,P)
\ll
C_{\mathrm{discover}}(P),
$$

但並非所有問題都如此。

因此：

$$
\boxed{
\text{proof verification}
\neq
\text{proof discovery}.
}
$$

---

## 命題五：更多計算資源不能消除不可判定性

$$
\boxed{
\text{resource amplification}
\neq
\text{computability-class transition}.
}
$$

若不改變計算模型，更多有限時間與記憶不會使 Halting Problem 變成一般可判定。

---

## 命題六：NACB 是比較基線，不是智能的否定模型

其功能是給後續定義：

$$
\Delta_{\mathcal I}(P)
=
C_{\mathrm{NACB}}(P)
-
C_{\mathrm{intervened}}(P)
$$

提供參考。

只有先知道：

> 不加主動智能干預時需要多少計算，

才有可能問：

> 某個認知能力究竟節省、增加或重組了多少計算？

---

# 42. 從 NACB 通向下一篇

現在我們終於可以更精確地問：

> 智能體到底加入了什麼？

如果只是：

- 儲存資訊；
- 依固定規則檢索；
- 依固定 heuristic 排序；
- 依既定規則剪枝；
- 使用 proof checker；
- 執行預定 transformation；

這些全部可以留在：

$$
\mathcal N.
$$

因此真正值得研究的是：

$$
\boxed{
\text{可改變計算政策、表示、目標、記憶重建方式與自身策略評價的干預算子。}
}
$$

下一篇將建立：

$$
\mathcal I
=
\{
I_{\mathrm{attention}},
I_{\mathrm{memory}},
I_{\mathrm{intuition}},
I_{\mathrm{prediction}},
I_{\mathrm{experience}},
I_{\mathrm{representation}},
I_{\mathrm{goal}},
I_{\mathrm{concept}},
I_{\mathrm{meta}},
\ldots
\}.
$$

並重新問同一組二十種問題：

> 加入人類、動物、現代 AI 與假想未來 AI 可能具有的廣義認知能力後，搜索空間究竟如何改變？

---

# 43. 結論

前篇將數學難度拆成多種認知障礙。

本文則進一步發現：

其中許多障礙，一旦移除智能體的心理／認知描述，可以重新表達為：

$$
\boxed{
\text{枚舉}
+
\text{轉換}
+
\text{證明搜尋}
+
\text{驗證}
+
\text{壓縮}
+
\text{資源限制}.
}
$$

例如：

$$
\text{「想不到 lemma」}
$$

可以改寫成：

$$
\text{formula-space search}.
$$

$$
\text{「看不出新表示」}
$$

可以改寫成：

$$
\text{representation-space search}.
$$

$$
\text{「找不到跨領域連結」}
$$

可以改寫成：

$$
\text{transformation composition search}.
$$

$$
\text{「證明不存在很難」}
$$

則可以改寫成：

$$
\text{finite obstruction/certificate search}.
$$

這並沒有消滅數學困難。

相反地，它揭示出困難的一個更基礎形態：

$$
\boxed{
\text{很多所謂「不會想」，
在計算層可以表達成「有效路徑在巨大可實現空間中極難找到」。}
}
$$

但這個結果同時保留三道不可忽略的界線：

$$
\boxed{
\text{可描述}
\neq
\text{可計算},
}
$$

$$
\boxed{
\text{可計算}
\neq
\text{可行計算},
}
$$

以及：

$$
\boxed{
\text{形式驗證成功}
\neq
\text{問題語義一定正確}.
}
$$

所以 NACB 不是「所有智能最終都只是暴力搜尋」的結論。

它是一個控制組。

只有建立這個控制組後，我們才可以在下一篇真正測量：

$$
\boxed{
\text{Attention、Memory Reconstruction、Intuition、Experience、
Prediction、Abstraction、Metacognition 等認知干預，
究竟增加、刪除、排序、重寫或重新定義了哪些計算。}
}
$$

---

## 參考文獻與近期相關工作

1. Gao et al., **LeanSearch v2: Global Premise Retrieval for Lean 4 Theorem Proving**, 2026。研究顯示全局 premise retrieval 品質會直接影響固定 prover loop 的證明成功率。

2. Leang et al., **Pythagoras-Prover: Advancing Efficient Formal Proving via Augmented Lean Formalisation**, 2026。強調 proof length、training/inference compute 與 verified proof data 對形式證明效率的重要性。

3. Xu et al., **Neural Theorem Proving for Verification Conditions: A Real-World Benchmark**, 2026。將 theorem proving 置於真實軟體 verification conditions，顯示從競賽題到實際 verification 仍存在顯著能力差距。

4. Pham et al., **TheoremBench: Evaluating LLMs on Theorem Proving in Formal Mathematics**, 2026。使用更長、dependency-rich 的經典定理評估 proof systems。

5. Ammanamanchi, Bhat, Biderman, **Faults in Our Formal Benchmarking: Dataset Defects and Evaluation Failures in Lean Theorem Proving**, 2026。指出 machine verification 並不自動保證 formalized statement 正確代表 intended problem。

6. Kim, Han, Hwang, **Benchmarking Testing in Automated Theorem Proving**, ACL Industry Track, 2026。提出後續 theorem testing 來測量生成 theorem 的 semantic correctness，顯示 compilation success 與更強 semantic metric 間仍有明顯落差。

---

**版本：v1.0**

**系列定位：計算控制組／機械化基線論文。**

**上一篇：**《數學難度不是計算量：二十種問題障礙與 AI 數學難度譜系》

**下一篇：**《廣義智能體的認知干預算子：從注意、記憶重建到元認知的計算控制理論》