疑點驅動的推理資源配置：Freeze Controller、Value of Information 與自適應 Specialist Routing

Q: 9. Freeze Controller：Should I Think More?

只會選 specialist 還不夠。

Doubt-Driven Reasoning Allocation: Freeze Control, Value of Information, and Adaptive Specialist Routing

作者： Neo.K
機構： EveMissLab／一言諾科技有限公司
日期： 2026-08-11

摘要

隨著大型語言模型與形式定理證明系統的 inference-time compute 持續擴張，數學 AI 面臨的問題已不再只是「能否投入更多推理資源」，而是「何時值得投入更多資源，以及資源應投入哪一種推理活動」。現有 adaptive test-time compute 研究主要依據問題難度、不確定性或預期正確率收益，決定對單一輸入增加多少 sampling、search 或 verification；多 Agent 形式數學系統則開始將自然語言推理、形式驗證、修復與 orchestration 分離。然而，對研究級數學問題而言，尚存在一個更上游的資源配置問題：當 theorem target 尚未完全穩定時，額外計算究竟應該用於量詞與定義域分析、來源版本核對、自然語言解釋、跨框架 bridge audit，還是應停止擴張並凍結問題？

本文提出 Doubt-Driven Reasoning Allocation（DDRA），將 proof-search 前的 residual uncertainty 表示為多維 residual doubt vector：

D_t=(D_F,D_S,D_B,D_P,\ldots),

其中各維分別代表 formal-structural、source-fidelity、framework-bridge、perspective/pragmatic 等未決風險。系統維持一組認知 specialist：

\mathcal M = \{ M_{\mathrm{MPF}}, M_{\mathrm{Source}}, M_{\mathrm{Bridge}}, M_{\mathrm{NLU}}, \ldots \},

並估計每個 specialist 的成本 $C(M_i)$ 與對 residual doubt 的預期消除量。由此定義：

\operatorname{VOI}(M_i\mid D_t) = \frac{ \mathbb E[ V(D_t)-V(D_{t+1}) \mid M_i ] }{ C(M_i) },

其中 $V(D)$ 是 unresolved doubt 的加權風險函數。

本文將推理控制分為兩個問題：

\boxed{\text{Should I think more?}}

以及：

\boxed{\text{What should I think about next?}}

前者由 Freeze Controller 決定；後者由 VOI Specialist Scheduler 決定。當 residual doubt 已低於 freeze threshold，或所有剩餘 specialist 的邊際 VOI 低於停止門檻時，系統停止語義擴張並形成 frozen theorem target；反之，選擇最高 VOI specialist 進行下一步審計。

本文整理一組由先前 error-injection 與 holdout-style experiments 所衍生的結構代理實驗。結果顯示，在既定人工標註與 proxy cost model 下，adaptive routing 可以在保持 corruption coverage 的同時顯著減少不必要 specialist calls；但本文明確不將這些結果解讀為實際 token、latency 或 theorem-prover speedup。本文的主要貢獻是提出一個可與真實 telemetry 接軌的推理資源治理模型，使數學 AI 從「固定流程的 solver」轉向「依問題狀態動態分配認知資源的 orchestrator」。

關鍵詞： Reasoning Allocation、Value of Information、Test-Time Compute、Specialist Routing、Freeze Controller、Residual Doubt、Mathematical AI、Agent Orchestration、Inference-Time Compute、Formal Theorem Proving

1. 引言

大型語言模型的 reasoning 能力可以透過增加 inference-time compute 改善。常見方法包括：

repeated sampling；
best-of- $N$ ；
self-consistency；
search；
verifier reranking；
extended reasoning；
multi-agent decomposition。

然而，若所有輸入都使用相同計算量，系統會出現明顯浪費：

\boxed{ \text{easy cases are over-computed,} \qquad \text{hard cases may remain under-computed.} }

2026 年的 adaptive test-time compute 研究已明確把問題寫成有限平均 budget 下的資源分配：哪些問題值得更多 sampling / reasoning，哪些問題可以低成本完成。Uncertainty-Aware Budget Allocation 以 per-question uncertainty 配置額外 sampling；Adaptive Test-Time Compute Allocation via Constrained Policy Optimization 則將 accuracy–cost trade-off 寫成 constrained optimization，再學習輸入到 compute action 的 allocation policy。ThinkBooster 更進一步將 test-time scaling strategy、scorer、quality–cost benchmark 與 deployable proxy service 整合成 runtime framework。

這些工作處理的是：

\boxed{ \text{How much compute should this input receive?} }

本文研究另一個相鄰但不同的問題：

\boxed{ \text{What kind of reasoning should receive the next unit of compute?} }

在研究級數學問題中，一個輸入可能同時存在：

theorem statement 本身的 formal uncertainty；
source formulation 是否選對的問題；
hidden quantifier / witness dependency；
framework bridge；
representation provenance；
natural-language perspective ambiguity。

因此，「多算一次」不是唯一 action。

下一個計算單位可能應該交給：

M_{\mathrm{MPF}},

也可能交給：

M_{\mathrm{SourceFidelity}},

或：

M_{\mathrm{Bridge}},

甚至：

\boxed{ \text{誰都不要叫，直接 Freeze。} }

因此本文提出：

\boxed{ \text{Doubt-Driven Reasoning Allocation}. }

2. 從 Compute Scaling 到 Cognitive Allocation

傳統 test-time compute allocation 可以抽象成：

x \rightarrow b(x),

其中 $b(x)$ 是輸入 $x$ 的 computation budget。

若 action 僅為增加 sample 數：

b(x)\in\{1,2,\ldots,B\}.

本文將 action space 擴張為：

a_t \in \{ \operatorname{Freeze}, M_1, M_2, \ldots, M_k \}.

其中 $M_i$ 不是單純不同 LLM，也可以是不同認知功能：

formal-structure auditor；
source-fidelity auditor；
NLU interpreter；
bridge auditor；
counterexample searcher；
premise retriever；
Lean prover；
CAS；
numerical experiment agent。

因此：

\boxed{ \text{Compute Quantity Allocation} \subset \text{Cognitive Resource Allocation}. }

本文的核心不是假定每個 specialist 必須由不同模型執行。

同一個 foundation model 也可以透過：

不同 system prompt；
不同 tool access；
不同 context；
不同 objective；
不同 verifier；

扮演不同 specialist。

因此 specialist 是 functional role，而不是必然等於 model identity。

3. 與多 Agent 形式數學的關係

形式數學系統已開始自然出現角色分離。

MA-LoT 使用多 Agent 結構，把自然語言長鏈推理與 Lean formal-language verification 結合。LeanMarathon 則建立一個 multi-agent harness，讓不同 contract-scoped agents 構建、審計、證明與修復共享 blueprint，並由 orchestrator 先穩定 target fidelity，再處理 proof DAG。

這些系統顯示：

\boxed{ \text{Mathematical reasoning} \neq \text{one monolithic model call}. }

本文的延伸在於：

如果已經存在多種 Agent / cognitive roles，則上層系統還需要決定「何時叫誰」。

也就是：

\boxed{ \text{Multi-Agent Architecture} \neq \text{Adaptive Agent Allocation}. }

僅僅擁有五個 agents，不等於每題都應該呼叫五個 agents。

4. Residual Doubt Vector

令問題在時間 $t$ 的狀態為：

S_t.

我們定義 residual doubt：

D_t = ( D_F, D_S, D_B, D_P, D_R, D_C, \ldots ).

可包含：

$D_F$ ：Formal-Structural Doubt；
$D_S$ ：Source-Fidelity Doubt；
$D_B$ ：Framework-Bridge Doubt；
$D_P$ ：Perspective / Pragmatic Doubt；
$D_R$ ：Representation Doubt；
$D_C$ ：Certificate / Closure Doubt。

其中：

D_j\ge0.

$D_j=0$ 不必解讀為「哲學上完全無疑問」，而是：

在目前 theorem identity 與 proof obligation 下，此維度沒有剩餘的 load-bearing unresolved issue。

因此 residual doubt 是 operational state，而不是主觀信念的完整哲學模型。

5. Doubt Value Function

不同 doubt dimensions 的危險性不一定相同。

例如：

一個 minor notation ambiguity；
一個量詞 swap；
一個錯 source formulation；

其後果不同。

因此定義：

V(D) = \sum_j \lambda_jD_j.

其中：

\lambda_j\ge0

是 risk weight。

更一般可以：

V: \mathbb R_{\ge0}^m \rightarrow \mathbb R_{\ge0}.

而不要求線性。

例如若 source-fidelity doubt 與 formal doubt 同時高時風險超線性增加，可使用：

V(D) = \sum_j\lambda_jD_j + \sum_{i<j}\gamma_{ij}D_iD_j.

這反映：

\boxed{ \text{doubt dimensions may interact}. }

6. Specialist Model

令 specialist set：

\mathcal M = \{M_1,\ldots,M_k\}.

每個 specialist 至少具有兩種估計。

6.1 Cost

C(M_i\mid S_t)>0.

成本可以是：

tokens；
wall-clock latency；
API cost；
tool calls；
proof nodes；
human supervision；
energy；
mixed operational cost。

初期可以使用 proxy cost，未來應改用 runtime telemetry。

6.2 Expected doubt transition

呼叫：

M_i

使：

D_t \rightarrow D_{t+1}.

定義：

R_i(D_t) = \mathbb E[ D_t-D_{t+1} \mid M_i,S_t ].

這是一個向量。

例如 MPF：

R_{\mathrm{MPF}} \approx ( r_F, r_S, r_B,\ldots )

一般期望：

r_F

較高，

但不必假定：

r_S=r_B=0.

一個 specialist 可能順帶消除多種 doubt。

7. Value of Information

本文定義 specialist 的基本 VOI：

\boxed{ \operatorname{VOI}(M_i\mid D_t) = \frac{ \mathbb E[ V(D_t)-V(D_{t+1}) \mid M_i ] }{ C(M_i\mid S_t) }. }

若使用線性 $V$ ：

\operatorname{VOI}(M_i\mid D_t) = \frac{ \sum_j \lambda_j \mathbb E[\Delta D_j\mid M_i] }{ C(M_i) }.

這表示：

每一單位認知成本，預期消掉多少 proof-relevant unresolved risk。

因此 routing：

\boxed{ M_t^\ast = \arg\max_{M_i} \operatorname{VOI}(M_i\mid D_t). }

8. VOI 不等於 Accuracy Predictor

這裡必須區分。

一般 inference allocation 可能估：

P(\text{correct}\mid x,b).

而本文主要估：

\mathbb E[\Delta D\mid M_i,D].

兩者可能相關，但不相同。

例如：

Case A

MPF specialist 不直接提高 theorem proof probability，

但可以發現：

\forall x\exists y

被誤寫成：

\exists y\forall x.

它的價值是阻止 proof search 進入錯 target。

Case B

Source Fidelity specialist 完全不會做代數證明，

但可以發現：

AI 正在證 source 中較強的另一個 variant。

因此：

\boxed{ \text{Value of a reasoning module} \neq \text{its standalone solving accuracy}. }

這是 specialist orchestration 的重要原則。

9. Freeze Controller：Should I Think More?

只會選 specialist 還不夠。

如果每輪都必須選一個 $M_i$ ：

M_t^\ast = \arg\max_i\operatorname{VOI},

系統仍可能永遠推理。

因此 action set 必須包含：

\boxed{ \operatorname{Freeze}. }

我們提出兩種基本停止條件。

9.1 State-Based Freeze

若：

V(D_t) \le \theta_D,

則：

\operatorname{Freeze}(S_t)=1.

即 residual doubt 已低於可接受 threshold。

9.2 Marginal-Value Freeze

即使：

V(D_t)>\theta_D,

剩餘疑點也可能成本極高、影響極低。

如果：

\max_i \operatorname{VOI}(M_i\mid D_t) \le \theta_{\mathrm{VOI}},

則可以 conditional freeze。

因此：

\boxed{ \operatorname{Freeze} \iff \left[ V(D_t)\le\theta_D \right] \lor \left[ \max_i\operatorname{VOI}_i \le\theta_{\mathrm{VOI}} \right], }

但第二種 freeze 必須記錄 remaining debt。

10. Hard Constraints：不是所有風險都可用低 VOI 忽略

純 VOI 最大化可能出現危險。

例如一個 quantifier corruption 的發現成本很高，但若漏掉，其 consequence 非常大。

因此定義 load-bearing set：

\mathcal L(D_t).

若：

D_j\in\mathcal L

且：

D_j>\theta_j^{\mathrm{hard}},

則禁止 freeze。

即：

\boxed{ \operatorname{FreezeEligible} = \operatorname{SoftStop} \land \operatorname{HardClosure}. }

其中：

\operatorname{HardClosure} = \bigwedge_{j\in\mathcal L} [ D_j\le\theta_j^{\mathrm{hard}} ].

這使系統不會因成本太高就跳過 theorem identity 的核心風險。

11. Risk-Aware VOI

更一般地，可以把 catastrophic target error 直接放入價值函數。

若 specialist $M_i$ 有機率發現 fatal corruption：

p_i^{\mathrm{fatal}},

漏掉此 corruption 的 expected loss：

L_{\mathrm{fatal}},

則：

\operatorname{VOI}_{\mathrm{risk}}(M_i) = \frac{ \mathbb E[\Delta V] + p_i^{\mathrm{fatal}}L_{\mathrm{fatal}} }{ C(M_i) }.

如此，「平常不太有用，但偶爾能抓到致命 target error」的 specialist 不會被簡單平均效益淘汰。

12. Adaptive Routing Algorithm

基本 runtime：

INPUT: source problem / candidate target

1. SURFACE AUDIT
2. estimate residual doubt D_t
3. check hard closure
4. if freeze eligible:
       FREEZE
   else:
       estimate VOI(M_i | D_t)
       choose argmax VOI
       run specialist
       update state and D_t
       repeat
5. output frozen target
6. hand off to MCDM / Proof Router

形式化：

S_0 \rightarrow D_0 \rightarrow M_0^\ast \rightarrow S_1 \rightarrow D_1 \rightarrow \cdots \rightarrow C^\ast_{\mathrm{freeze}}.

13. Specialist Roles

本文至少區分四個 proof-search 前 specialist。

13.1 Surface Auditor

成本最低。

檢查：

明顯 domain omission；
source 與 target 的 literal mismatch；
顯式 boundary；
已充分指定的 clean target。

若 Surface 已足夠：

\boxed{ \text{do not call deeper specialists}. }

13.2 MPF Specialist

檢查：

domain；
quantifier；
hidden/transitive quantifier；
witness dependency；
uniformity；
asymptotic semantics；
certificate tree。

13.3 Source-Fidelity Specialist

檢查：

source formulation family；
target-strength relation；
definition provenance；
representation equivalence；
benchmark target identity。

13.4 Bridge Specialist

檢查：

probability $\rightarrow$ decision；
simulation $\rightarrow$ theorem；
empirical observation $\rightarrow$ universal mathematical claim；
one model/framework $\rightarrow$ another。

14. 為何不是 Always-Dual？

一個直覺安全策略是：

每題全部跑 Surface + MPF + NLU + Source + Bridge。

稱為：

\operatorname{AlwaysDual}.

其優勢是高 coverage。

但成本：

C_{\mathrm{Always}} = \sum_{i=1}^{k}C(M_i)

每題都支付。

若大量問題其實 Surface 就可 freeze：

\boxed{ \text{Always-Dual creates systematic over-expansion}. }

所以真正目標不是：

\max\text{analysis depth},

而是：

\boxed{ \min C_{\mathrm{audit}} }

subject to：

\boxed{ P(\text{accept corrupted target}) \le\epsilon. }

15. 與 Adaptive Test-Time Compute 的關係

Uncertainty-aware allocation 已顯示，固定 sampling budget 平均分配到所有問題並非理想策略；依 uncertainty 配置 budget 可以改善有限計算資源下的 reasoning performance。

Constrained Policy Optimization 類方法則可寫成：

\max_\pi \mathbb E[\operatorname{Accuracy}]

subject to：

\mathbb E[C]\le B.

本文可類比寫為：

\min_\pi \mathbb E[ \mathcal R_{\mathrm{target}} + \alpha C ]

或：

\max_\pi \mathbb E[ \operatorname{TargetFidelity} ]

subject to：

\mathbb E[C_{\mathrm{audit}}] \le B.

差異是 action 不只是 budget level：

a\neq\text{more samples}.

而是：

a\in\{ \operatorname{Freeze}, M_{\mathrm{MPF}}, M_{\mathrm{Source}}, M_{\mathrm{Bridge}}, \ldots \}.

因此 DDRA 可以理解為：

\boxed{ \text{structured test-time compute allocation over cognitive roles}. }

16. 與 Selective Verification 的關係

近期 selective verification 工作指出，在 search 中平均驗證所有 intermediate hypotheses 會浪費 verifier calls；應優先驗證較具資訊價值的狀態。

本文的精神相似：

\boxed{ \text{not every unresolved branch deserves verification}. }

但我們把 allocation point 放得更上游：

selective verification：選擇哪個 reasoning state 要驗證；
DDRA：選擇哪個 problem-understanding / formalization specialist 值得先投入。

兩者未來可以組合：

\text{Problem-Space VOI} \rightarrow \text{Proof-State VOI}.

17. EXP-0005：Freeze Controller 的結構代理結果

在先前開發集的結構模擬中，我們比較：

Surface-only；
Always-MPF；
Always-Dual；
Adaptive Controller。

以每個 audit module invocation 為一個 proxy cost unit。

結果顯示，在該人工建立 development set 上：

Surface-only 成本最低，但漏掉大量深層 target corruption；
Always-MPF 能抓 formal-structure corruption，但漏掉 source-fidelity 與 bridge 類；
Always-Dual coverage 完整，但存在大量 unnecessary module calls；
Adaptive Controller 在相同人工 coverage 下，用顯著更少 module invocations 完成 audit。

其中 Adaptive 相較 Always-Dual 的 module-call proxy 約降低：

57.7\%.

但：

\boxed{ 57.7\% \text{ is not measured compute saving}. }

它只表示在人工 annotation 與 unit-cost assumption 下，啟動的分析模組較少。

18. EXP-0006：Holdout-Style Generalization

為避免控制器只記住 development cases，後續換用新的 Formal Conjectures 問題類型：

Erdős 12；
Erdős 26；
Erdős 56；
Open Quantum Problem 13；
Open Quantum Problem 35；
OEIS A6697。

這些案例新增：

optimization-target replacement；
representation-coverage failure；
definition substitution / provenance gap。

固定 controller policy 後的 holdout-style 結構測試顯示，routing taxonomy 可以自然把：

quantifier / uniformity $\rightarrow$ MPF；
source identity / provenance $\rightarrow$ Source Fidelity；
explicit boundary $\rightarrow$ Surface；
representation coverage $\rightarrow$ MPF / Source Fidelity。

但也暴露 rule-based controller 的保守性：

一些 case 會同時啟動兩個 specialist，即使一個 specialist 已可能足夠。

這直接導向 VOI scheduler。

19. EXP-0007：VOI Specialist Scheduler

在下一步 simulation 中，為 specialist 指定 proxy costs：

C_{\mathrm{Surface}}=1,

C_{\mathrm{MPF}}=2,

C_{\mathrm{Source}}=1.3,

C_{\mathrm{Bridge}}=1.2.

並以人工 residual-doubt profiles 估計各 specialist 的 expected doubt reduction。

得到：

\operatorname{VOI}(M_i) = \frac{\mathbb E[\Delta D]}{C_i}.

在相同 holdout-style sample 上，VOI routing 能避免部分 rule-based 的保守 double-routing。

代理結果：

Always-Dual：48 module calls；
Rule-Based Adaptive：26；
VOI Scheduler：24。

VOI scheduler 的 weighted proxy cost 相對 Always-Dual 約降低：

51.8\%.

相對 Rule-Based Adaptive 約降低：

11.2\%.

與利用 gold information 才能定義的 oracle lower bound 相比，proxy overhead 約：

4.3\%.

再次強調：

\boxed{ \text{這些全部是 controller simulation，} \text{不是實際 LLM / Lean 性能結果。} }

20. 一個重要結果：Routing 可以是序列，而不是一次分類

有些問題：

D_F\gg0, \qquad D_S\gg0.

此時可能：

M_{\mathrm{Source}} \rightarrow M_{\mathrm{MPF}} \rightarrow \operatorname{Freeze}.

例如 representation fidelity 問題：

Source specialist 先判定某 representation 是否可能忠實；
MPF 再檢查 symmetry / quantifier coverage 是否完整。

因此：

\boxed{ \text{Routing} \neq \text{one-shot classification}. }

更像：

D_t \rightarrow M_t \rightarrow D_{t+1} \rightarrow M_{t+1}.

也就是 closed-loop reasoning control。

21. Problem-Level Scheduler 與 Proof-Level Scheduler

本文主要處理 proof search 前。

但完整數學 AI 可以有兩級 scheduler。

Level A：Problem-Space Scheduler

決定：

target 是否穩定；
該叫哪個 semantic/formal specialist；
是否 Freeze。

Level B：Proof-Space Scheduler

Target freeze 後決定：

Lean search；
premise retrieval；
counterexample；
CAS；
numerical experiment；
natural-language lemma planning；
ATP。

因此：

\boxed{ \text{Problem-Space Governance} \rightarrow \text{Proof-Space Governance}. }

這避免 proof-level agent 被要求替上游 target corruption 買單。

22. 與 MCDM 的接口

MCDM 類 difficulty router 用來評估 frozen problem 的研究障礙向量。

因此順序應是：

C^\ast_{\mathrm{freeze}} \rightarrow \mathrm{MCDM} \rightarrow \mathrm{ResearchRouter}.

而不是：

C_{\mathrm{raw}} \rightarrow \mathrm{MCDM}.

因為如果 candidate target 本身不穩定：

\mathrm{MCDM}(C_1) \neq \mathrm{MCDM}(C_2).

甚至：

\operatorname{Var} [ \mathrm{MCDM}(C_i) ] \gg0

可以成為 target-instability diagnostic。

因此 DDRA 位於 MCDM 的上游。

23. 可學習的 Routing Policy

目前的 $C(M_i)$ 與 $R_i(D)$ 可以人工指定。

但真正 Runtime 應由 telemetry 學習：

\widehat C_t(M_i)

以及：

\widehat R_t(M_i\mid X,D).

其中 $X$ 包含：

problem domain；
theorem form；
source type；
model version；
prompt version；
tool availability。

於是：

\widehat{\operatorname{VOI}}_t(M_i) = \frac{ \widehat{\mathbb E}[\Delta V] }{ \widehat C_t(M_i) }.

這將是本系列下一篇 self-calibrating orchestration 的核心。

24. 評測指標

未來真實 benchmark 至少應保存：

24.1 Target Safety

\text{Corruption Recall},

\text{False Freeze Rate},

\text{Clean Freeze Rate}.

24.2 Routing Efficiency

N_{\mathrm{module\ calls}},

\text{tokens},

\text{latency},

\text{tool calls}.

24.3 Proof-Downstream Effect

\text{proof branches},

\text{premise retrieval count},

\text{Lean elaboration failures},

\text{proof search nodes},

\text{proof success}.

24.4 Regret

若存在 oracle 或 hindsight estimate：

R_T = \sum_{t=1}^{T} [ V(a_t^\ast)-V(a_t) ].

24.5 Over-Expansion

\operatorname{OER} = \frac{ \text{unnecessary specialist calls} }{ \text{all specialist calls} }.

25. 三個核心 Hypotheses

H1：Adaptive Freeze

相較 Always-Dual：

\mathbb E[C_{\mathrm{audit}}]

應下降，而 target-corruption miss rate 不顯著上升。

H2：VOI Routing

相較固定 rule-based routing：

\operatorname{VOI\ Scheduler}

應降低 over-expansion。

H3：Downstream Search

若上游 target audit 避免了 wrong target / wrong certificate route：

\mathbb E[ C_{\mathrm{proof}} \mid \mathrm{DDRA} ] < \mathbb E[ C_{\mathrm{proof}} \mid \mathrm{DirectProof} ].

但這是 empirical hypothesis，不是本文已證結果。

26. 失敗模式

26.1 Wrong Doubt Estimation

若：

D_t

估錯，

則 VOI 全部跟著錯。

26.2 Wrong Specialist Capability Model

若：

R_i(D)

估得太樂觀，會過度調用某 specialist。

26.3 Cheap-but-Useless Bias

若成本權重過重：

\arg\max\operatorname{VOI}

可能偏向便宜但只能消除小疑點的 specialist。

因此需 hard closure / fatal-risk term。

26.4 Endless Audit

若：

\theta_D

過低，

系統可能永遠不 Freeze。

26.5 Premature Freeze

若：

\theta_D

過高，

則重新產生 Paper 02 的 premature closure。

26.6 Correlated Specialists

兩個 specialists 可能高度冗餘：

R_i\approx R_j.

若 scheduler 不考慮 conditional marginal value，可能重複付費。

更完整應估：

\operatorname{VOI} ( M_j \mid D, M_i\text{ already run} ).

27. 從 Solver 到 Orchestrator

傳統 AI solver：

\boxed{ \text{Problem} \rightarrow \text{Answer}. }

Agent system：

\boxed{ \text{Problem} \rightarrow \text{Agents} \rightarrow \text{Answer}. }

本文提出的 adaptive orchestrator：

\boxed{ \text{Problem} \rightarrow D_t \rightarrow \text{Choose Specialist} \rightarrow D_{t+1} \rightarrow \cdots \rightarrow \operatorname{Freeze}. }

因此上層 AI 真正需要回答：

\boxed{ \text{Who should think?} }

\boxed{ \text{What should they think about?} }

以及：

\boxed{ \text{When should everyone stop thinking?} }

28. 認知資源治理

這使推理系統可以分層：

\begin{array}{ll} L_0 &: \text{Solver / Worker}\\ L_1 &: \text{Specialist Reasoner}\\ L_2 &: \text{Adaptive Orchestrator}\\ L_3 &: \text{Epistemic Governor} \end{array}

$L_0$ 解局部問題。

$L_1$ 專門處理某種認知功能。

$L_2$ 決定 specialist allocation。

$L_3$ 管理：

target 是否值得 Freeze；
哪些 unresolved risks 不可忽略；
推理預算怎麼分；
哪些認知活動目前沒有邊際價值。

因此：

\boxed{ \text{Tool Routing} \subset \text{Reasoning Routing} \subset \text{Problem-Space Governance}. }

本文主要建立中間層：

\boxed{ \text{Reasoning Routing}. }

29. 討論

Adaptive test-time compute 已經提出一個重要觀念：

inference compute 應是可分配資源，而不是固定常數。

本文再推一步：

reasoning type 本身也應是可分配資源。

對數學 AI 而言，額外的一千 tokens 可以拿來：

繼續同一路推 proof；
回頭檢查量詞；
找 source；
檢查 provenance；
反例搜尋；
形式驗證。

這些 action 的 information gain 完全不同。

因此真正的 inference-time intelligence 不只是：

\boxed{ \text{think longer}. }

更是：

\boxed{ \text{think in the right place}. }

而更成熟時，還包括：

\boxed{ \text{know when not to think further}. }

30. 結論

本文提出 Doubt-Driven Reasoning Allocation，將數學 AI 的 proof-search 前資源治理建模為 residual doubt 上的 sequential decision problem。

核心狀態：

D_t.

核心 action：

a_t \in \{ \operatorname{Freeze}, M_1,\ldots,M_k \}.

核心選擇準則：

\boxed{ \operatorname{VOI}(M_i\mid D_t) = \frac{ \mathbb E[ V(D_t)-V(D_{t+1}) ] }{ C(M_i) }. }

核心停止原則：

\boxed{ \text{Freeze when residual risk is sufficiently closed,} }

或：

\boxed{ \text{when no remaining reasoning action has adequate marginal value,} }

但 load-bearing target risks 必須滿足 hard closure。

因此：

\boxed{ \text{Should I think more?} }

由 Freeze Controller 回答，

而：

\boxed{ \text{What should I think about next?} }

由 VOI Scheduler 回答。

這使數學 AI 從固定 pipeline：

\text{Formalize} \rightarrow \text{Prove}

轉向：

\boxed{ \text{Observe} \rightarrow \text{Estimate Doubt} \rightarrow \text{Allocate Reasoning} \rightarrow \text{Update} \rightarrow \text{Freeze} \rightarrow \text{Prove}. }

本文的結構代理實驗只證明該控制流程可以被工程化與量測，而不證明它已在真實模型上降低 inference 或 formal-proof 成本。下一篇將進一步研究如何從 runtime telemetry 自動學習 specialist cost、能力與 routing policy，使 orchestrator 從固定規則提升為 self-calibrating meta-orchestrator。

參考文獻

Nguyen, M., Gupta, S., Le, H. Uncertainty-Aware Budget Allocation for Adaptive Test-Time Reasoning. arXiv:2605.26849, 2026.
Zhai, Z., Li, B., Xiao, B., Li, M., Wang, X. Adaptive Test-Time Compute Allocation for Reasoning LLMs via Constrained Policy Optimization. arXiv:2604.14853, 2026.
Qu, S. Adaptive Test-Time Compute Allocation via Learned Heuristics over Categorical Structure. arXiv:2602.03975, 2026.
Smirnov, V., Nguyen, C., Senichev, S., et al. ThinkBooster: A Unified Framework for Seamless Test-Time Scaling of LLM Reasoning. arXiv:2606.06915, 2026.
Zhang, Y., Sun, Y., Suzuki, T., Lee, J. D., Liu, F. LeanMarathon: Toward Reliable AI Co-Mathematicians through Long-Horizon Lean Autoformalization. arXiv:2606.05400, 2026.
Wang, R., Pan, R., Li, Y., et al. MA-LoT: Multi-Agent Lean-based Long Chain-of-Thought Reasoning Enhances Formal Theorem Proving. arXiv:2503.03205, 2025.
Chen, J., Chen, W., Du, J., et al. Seed-Prover 1.5: Mastering Undergraduate-Level Theorem Proving via Learning from Experience. arXiv:2512.17260, 2025.
Firsching, M., Lezeau, P., Mercuri, S., et al. Formal Conjectures: An Open and Evolving Benchmark for Verified Discovery in Mathematics. arXiv:2605.13171, 2026.

研究狀態聲明

本文提出的 Doubt-Driven Reasoning Allocation、Residual Doubt Vector、Freeze Controller、Specialist VOI、Hard Closure 與相關 routing 架構，屬於本文提出的研究框架。

本文所述 EXP-0005～EXP-0007 數值來自人工 annotation、結構代理成本與 controller simulation；它們不應被引用為實際 LLM token savings、wall-clock speedup、Lean proof-node reduction 或通用性能提升。這些 empirical claims 必須由獨立 Agent、固定模型版本、真實 runtime telemetry 與 formal prover logs 重新驗證。