基底知識空間擴張：AI 原生高品質資料生成的結構閉包假說

English Title: Base Knowledge Space Expansion: A Structural-Closure Hypothesis for AI-Native High-Quality Data Generation
Series: AI-Native Knowledge Expansion, Paper I
Author: Neo.K
Collaborator: Aletheia (GPT-5.6 Sol)
Institution: EveMissLab / 一言諾科技有限公司
Version: v0.1
Date: 2026-08-09

摘要

大型語言模型的數學能力通常被討論為模型規模、推理架構、強化學習、難題資料與形式化證明資料的函數。然而，「高品質資料」經常被不自覺地等同於「高難度資料」、「前沿研究資料」或「由專家撰寫的稀缺資料」。本文提出不同的假說：深度不要求每一個資料點本身都很深；只要可靠的基礎知識能被大量、合法、可驗證地展開，其結構閉包本身就可能形成高價值推理資料。

本文將此機制定義為「基底知識空間擴張」（Base Knowledge Space Expansion, BKSE）。對一個可靠基礎命題 (P)，不僅保存其單一敘述，而是建立由等價變換、逆向問題、條件消融、表示轉換、跨模組組合、反例鄰域、維度提升與形式驗證所形成的結構鄰域 $\mathcal E(P)$ 。資料品質因而不只由難度衡量，而應由正確性、結構變異、覆蓋密度、推導深度、可驗證性、去重程度與錯誤可檢出性共同決定。

本文進一步提出：AI 原生數學的早期突破未必首先來自更難的數學，而可能來自人類不願長期承受的大規模「認知重複」——對基礎命題反覆證明、反駁、重組、形式化與交叉驗證。這種高密度驗證與結構展開，可同時服務於資料生成、模型訓練、推理穩定性、形式化數學與自主研究系統。本文最後提出可被實驗否證的 BKSE 訓練與評測框架，並界定其與一般資料增強、表面改寫及純粹難題合成的差異。

關鍵詞： 基底知識空間；AI 原生數學；合成資料；形式化證明；結構閉包；資料品質；定理證明器；自動形式化；知識覆蓋；驗證密度

1. 問題：我們真的缺「更難的資料」嗎？

當代 AI 數學研究有一個合理但容易過度延伸的直覺：若希望模型變得更強，就應提供更難、更專業、更接近數學前沿的資料。這條路當然重要，但它隱含了一個未必成立的等價：

\text{High-quality data} \overset{?}{=} \text{Difficult data}.

本文否定這個等價。

一個資料點的「難度」只是資料品質的一個維度。對推理系統而言，同樣重要的還包括：

Q(d) = f( C, V, D, R, L, E, G ),

其中：

(C)：correctness，正確性；
(V)：structural variation，結構變異；
(D)：derivational depth，推導深度；
(R)：reusability，可重用性；
(L)：linkage，跨知識連接程度；
(E)：error detectability，錯誤可檢出性；
(G)：granularity，知識粒度。

因此，一個非常基礎的定理，只要能形成高密度、高變異、低錯誤的推理網路，也可能比一篇孤立而困難的自然語言論文提供更高的有效訓練價值。

本文的核心命題是：

\boxed{ \text{Deep intelligence does not require every datum to be deep.} }

更強地說：

\boxed{ \text{A sufficiently rich verified closure of reliable basics may itself become deep.} }

即：

深度不一定來自每一個資料點本身都很深；可靠基礎經過足夠豐富、可驗證的展開與組合，其閉包本身就可能產生深度。

2. 原始資料量與有效結構量不是同一個量

人類已經產生極大量的數學自然語言：教材、論文、題庫、講義、論壇回答、證明、翻譯、重述與評論。但「文字很多」不代表其中包含同等數量的獨立數學結構。

設原始資料集合為：

D_{\mathrm{raw}}.

若定義等價關係：

x_i\sim x_j

表示兩個樣本雖然字面不同，但承載近似相同的核心結構，則真正值得關心的數量不是：

|D_{\mathrm{raw}}|,

而是某種近似的結構商空間：

\left|D_{\mathrm{raw}}/\sim\right|.

自然語言具有極高的「表示重數」。同一個定理可能被不同語言、不同教材、不同例子與不同敘述方式重複數萬次，但完整、可機械檢查、可追溯依賴的形式證明數量可能非常有限。

形式數學的現況支持這種「表面龐大、形式結構仍稀疏」的判斷。Mathlib 已是目前規模最大的形式數學庫之一，包含超過兩百萬行形式化內容，並強調定義、定理與證明的可組合重用；然而，自動形式化研究仍普遍將高品質形式資料不足視為核心瓶頸。2025–2026 年的研究甚至仍以數千道自然語言題轉換為 Lean、或把整本教材轉成形式內容，作為重要的資料與工程進展。

因此本文不主張「世界上的數學很少」，而是提出更窄的命題：

\boxed{ \text{Verified structural coverage} \ll \text{natural-language repetition}. }

3. 基底知識空間擴張（BKSE）

令：

B_0=\{P_1,P_2,\ldots,P_n\}

為一組已知可靠的基礎命題。

對每個命題 (P)，定義一組合法轉換算子：

\mathcal T = \{ T_{\mathrm{eq}}, T_{\mathrm{inv}}, T_{\mathrm{repr}}, T_{\mathrm{cond}}, T_{\mathrm{gen}}, T_{\mathrm{spec}}, T_{\mathrm{counter}}, T_{\mathrm{compose}} \}.

分別代表：

等價變換；
逆向／逆命題；
表示語言轉換；
條件增加、移除與消融；
泛化；
特化；
反例與近錯誤生成；
與其他命題組合。

第一階擴張為：

B_1 = B_0 \cup \{ T(P): P\in B_0,\, T\in\mathcal T \}.

再允許跨命題組合：

B_{k+1} = B_k \cup \{T(P)\} \cup \{C(P,Q):P,Q\in B_k\}.

理想化閉包：

\boxed{ B^\ast = \bigcup_{k=0}^{\infty} B_k. }

本文不主張實際系統應窮舉 $B^\ast$ 。相反，這個定義只是指出：一個看似簡單的基礎命題周圍，可能存在遠大於其原始敘述的合法結構鄰域。

因此對單一命題 (P)，定義：

\boxed{ \mathcal E(P) = \{\text{legal verified neighbors of }P\}. }

BKSE 的目標不是產生最多樣本，而是提高：

\text{coverage}\bigl(\mathcal E(P)\bigr).

4. 變異不等於多樣性

最簡單的資料增強很容易退化成：

3,4,5 \rightarrow 6,8,10 \rightarrow 9,12,15.

這增加樣本數，卻不一定增加結構資訊。

因此：

\boxed{ \text{Variation}\neq\text{Diversity}. }

真正的結構變異應至少改變一項：

推理方向；
隱藏資訊位置；
前提集合；
表示系統；
所需中間引理；
組合模組；
可用工具；
反例結構；
維度；
證明路徑。

以畢氏定理為例：

a^2+b^2=c^2

可以生成的不只是不同邊長，而包括：

已知兩股求斜邊；
已知斜邊與一股反求另一股；
逆定理判斷直角；
銳角／直角／鈍角分類；
相似三角形證明；
面積重排證明；
內積空間表示；
座標表示；
三維正交距離；
高維正交分解；
與圓、投影、高、內切圓、外接圓組合；
條件消融；
錯誤命題與最小反例。

同一個母命題因此可以形成「局部理論生態」，而不是一列換數字的題目。

5. 錯誤鄰域也是高品質資料

若只生成正確變種，模型學到的可能只是：

什麼時候可以推出答案。

但強推理還需要：

什麼時候不可以推出。

因此對命題 (P)，定義錯誤鄰域：

N^-(P) = \{ P'_1,P'_2,\ldots \},

其中每個 $P'_i$ 都與 (P) 結構接近，但至少存在一個關鍵錯誤：

缺少必要條件；
將充分條件誤當必要條件；
量詞錯置；
定義域擴張過頭；
符號相似但對象不同；
合法推導中插入一個非法步驟；
把有限驗證誤當全稱證明。

因此高品質訓練單元不應只有：

(P,\text{proof}),

而更接近：

\boxed{ ( P, \text{proof}, \text{assumptions}, \text{counterexamples}, \text{near-misses}, \text{equivalents}, \text{dependencies} ). }

這使「錯誤可檢出性」本身成為資料品質的一部分。

6. 驗證器使大規模展開成為可能

BKSE 若沒有驗證，只會快速變成合成垃圾資料。

因此核心不是：

\text{Generate}.

而是：

\boxed{ \text{Generate} + \text{Verify}. }

至少可建立多層驗證：

V = ( V_{\mathrm{parse}}, V_{\mathrm{type}}, V_{\mathrm{symbolic}}, V_{\mathrm{formal}}, V_{\mathrm{numeric}}, V_{\mathrm{counter}}, V_{\mathrm{cross}} ).

其中：

語法／解析驗證；
型別與定義域驗證；
符號代數驗證；
theorem prover 形式證明；
數值測試；
反例搜尋；
獨立證明或跨驗證器檢查。

近期研究已經顯示，定理證明器可被用作合成數學資料的判定器；也有工作透過 proof-state exploration 大量生成訓練資料，提高自動定理證明表現。這些結果支持「生成—驗證閉環」的工程可行性，但本文將其研究對象向更基礎處擴張：不是只對難題或既有 benchmark 生成證明資料，而是有系統地擴張整個基礎知識鄰域。

7. AI 的特殊優勢：驗證密度而不只是智力

人類研究者必須分配注意力。

設理論圖：

G=(V,E)

包含大量局部推理節點。人類通常只能詳細檢查：

S_H\subset V.

AI 系統則可以在資源允許時逼近：

S_{AI}\approx V,

並且對每個節點執行多種操作：

v_i \rightarrow \{ \text{prove}, \text{disprove}, \text{formalize}, \text{rederive}, \text{perturb}, \text{test} \}.

因此 AI 的一項重要研究優勢可定義為：

\boxed{ \text{Verification Density}. }

這不是聲稱 AI 永遠比人類聰明，而是指出兩者成本函數不同。人類會合理地覺得第 10,000 個微小邊界條件「不值得再查」；自動系統則可以將這類工作制度化。

由此可提出：

AI 原生數學未必首先來自更高的智力，也可能先來自對大規模、反覆、精細甚至令人類嫌煩的邏輯清理工作的極高耐受性。

8. 有效結構資料量

傳統資料集主要以：

token 數；
文件數；
題目數；
proof 數；

衡量規模。

本文提出一個概念性指標：

\boxed{ E(D) = \sum_{s\in\mathcal S} w(s) C(s) V(s) R(s) }

其中：

(s)：近似獨立結構；
(C(s))：結構覆蓋；
(V(s))：有效變異；
(R(s))：驗證可靠性；
(w(s))：資訊或任務權重。

稱：

E(D) = \text{Effective Structural Dataset Size}.

因此：

|D_1|>|D_2|

不必然表示：

E(D_1)>E(D_2).

一個包含大量自然語言近義重複的巨大 corpus，其有效結構量可能小於一個規模較小、但包含高密度形式變種、反例與證明依賴的資料集。

此量目前只是理論指標，不是已建立的標準 metric。後續必須研究如何近似估計結構等價、覆蓋與驗證可靠性。

9. BKSE 與一般 synthetic data 的差別

BKSE 不等於普通合成資料。

普通流程常為：

P \rightarrow \text{LLM generates }P'_1,\ldots,P'_n.

BKSE 則要求：

\boxed{ \text{Invariant} + \text{Transformation} + \text{Verification}. }

每個生成物至少必須回答：

哪個核心結構被保留？
哪個結構被改變？
此轉換是否合法？
新命題與母命題是等價、強化、弱化、特化、泛化，還是分叉？
如何驗證？
是否與資料庫既有節點重複？
是否產生新的可研究鄰域？

因此一個 BKSE 節點更適合表示成：

claim_id
parent_ids
transformation
assumptions
statement
proof
verification
counterexamples
equivalence_class
novelty_status
frontier

它首先是一個機器可操作的研究節點，而不只是問答對。

10. AI-Native Research Loop

BKSE 可以自然形成自主研究循環：

P_0 \rightarrow \operatorname{Expand} \rightarrow \operatorname{Attack} \rightarrow \operatorname{Verify} \rightarrow \operatorname{Deduplicate} \rightarrow \operatorname{Select} \rightarrow P_1.

其中 Select 不應只按「難度」排序，而應同時考慮：

J = \lambda_1 N + \lambda_2 C + \lambda_3 V - \lambda_4 R_d - \lambda_5 C_e,

其中可分別表示：

(N)：novelty；
(C)：coverage gain；
(V)：verification value；
$R_d$ ：redundancy；
$C_e$ ：compute cost。

這可以避免組合爆炸。

如果沒有選擇器：

|B_k|

會快速失控；因此 BKSE 的核心工程問題不是「能不能生成很多」，而是：

\boxed{ \text{Which frontier is worth expanding next?} }

11. 可否證的實驗設計

本文提出一個最小實驗。

11.1 基礎資料集

選擇 100–500 個中學到大學基礎命題，例如：

代數恆等式；
初等數論；
歐氏幾何；
基礎組合；
微積分基本命題；
線性代數基本命題。

11.2 三組資料

Group A：Raw Repetition

只收集大量自然語言教材、解釋與重述。

Group B：Hard-Problem Expansion

主要加入競賽／高難度題。

Group C：BKSE

對同一基礎命題做：

結構變種；
條件消融；
多證法；
反例；
錯誤鄰域；
Lean／其他形式驗證；
等價類去重；
跨命題組合。

控制 token budget：

|D_A| \approx |D_B| \approx |D_C|.

11.3 評測

測量：

未見過的結構變種；
長鏈推理正確率；
必要／充分條件辨識；
反例搜尋能力；
proof repair；
autoformalization；
theorem proving；
對錯誤前提的拒絕能力；
跨表示轉換；
OOD 組合能力。

核心假說：

\boxed{ \operatorname{Perf}(D_C) > \operatorname{Perf}(D_A) }

並且在某些任務上：

\operatorname{Perf}(D_C) \ge \operatorname{Perf}(D_B),

即使 BKSE 的原始母命題難度較低。

若結果不成立，BKSE 的強版本即被削弱。

12. 研究邊界

本文不主張：

基礎資料可以取代前沿數學；
所有知識都可無損形式化；
合成資料必然優於人類資料；
數值測試等同一般數學證明；
形式證明器永遠無錯；
只要生成足夠多變種就會自動產生新數學；
結構等價可以在任意程式或任意語義系統中完美判定；
一個形式系統的驗證等同跨所有公理系統的真理；
BKSE 已經是一個完成的訓練演算法。

本文只提出一個較窄的研究假說：

\boxed{ \text{Reliable basics have underexploited structural neighborhoods.} }

而 AI、形式工具與自動驗證，使得大規模探索這些鄰域第一次變得具有實際工程可能性。

13. 與現有研究的關係

近年的研究已經提供若干重要拼圖：

Mathlib 顯示大規模形式知識庫可以形成高度可組合、可重用的數學基礎；
autoformalization 研究正試圖把大量非形式數學轉換成可驗證形式；
FormaRL 等工作直接指出形式化資料稀缺，並嘗試利用 compiler / consistency feedback 在少量標註甚至無標註條件下改進形式化；
Theorem Prover as a Judge 將 theorem prover 用作合成資料的嚴格判定器；
proof-state synthetic data 工作則顯示，擴張中間證明狀態本身可以提高自動定理證明能力；
Formal Conjectures 類專案則顯示，甚至「只有形式化命題、尚無證明」的研究節點本身也可以成為獨立資源。

BKSE 與這些工作的差別在於研究單位。

現有工作通常從：

\text{problem} \rightarrow \text{formalize / solve / synthesize proof data}

出發。

BKSE 則從：

\text{reliable knowledge atom} \rightarrow \text{verified structural neighborhood}

出發。

它研究的不是單一答案，而是知識原子周圍可被系統探索的閉包。

14. 結論

人類已經產生大量數學文字，但我們尚不能因此推論，人類已經充分探索了基礎數學知識的可驗證結構鄰域。

同一個基礎命題可以被：

\text{證明} \rightarrow \text{逆向} \rightarrow \text{消融} \rightarrow \text{反駁} \rightarrow \text{泛化} \rightarrow \text{重組} \rightarrow \text{形式化} \rightarrow \text{交叉驗證}.

這些操作產生的並非單純重複，而可能形成高密度的推理結構。

因此本文提出：

\boxed{ \text{High-quality data} \neq \text{hard data only}. }

以及：

\boxed{ \text{High-quality AI reasoning data} \supset \text{verified structural expansion of reliable basics}. }

如果此假說成立，AI 原生數學的第一階段不必等待 AI 自己解出最難的未解問題。它可以先完成一項人類從未大規模完成的工作：

對已知可靠知識進行近乎工業化的展開、反駁、重組、形式化、去重與交叉驗證。

這種工作看似基礎、重複，甚至令人類感到無聊；但正因為如此，它可能是最適合 AI 的研究生產層之一。

下一篇將進一步處理本系列的第二個核心問題：

\boxed{ \text{What counts as a genuinely different variation?} }

亦即：如何區分表面改寫、參數替換、結構變種與真正的新命題，並建立可計算的「結構覆蓋」與「變種合法性」框架。

參考文獻（初版）

Lean Community. Mathlib: A Foundation for Formal Mathematics Research and Verification. Lean.
Weng, K. et al. (2025). Autoformalization in the Era of Large Language Models: A Survey. arXiv:2505.23486.
Huang, Y. et al. (2025). FormaRL: Enhancing Autoformalization with no Labeled Data. arXiv:2508.18914.
Leang, J. O. J. et al. (2025). Theorem Prover as a Judge for Synthetic Data Generation. arXiv:2502.13137.
Lai, J. et al. (2025). LLM-based Automated Theorem Proving Hinges on Scalable Synthetic Data Generation. arXiv:2505.12031.
Xie, J. et al. (2025). FMC: Formalization of Natural Language Mathematical Competition Problems. arXiv:2507.11275.
Google DeepMind. Formal Conjectures: A Collection of Formalised Statements of Conjectures in Lean.