從數學問題形式化到雙重張力：形式收斂、語義擴張與問題空間治理

From Mathematical Problem Formalization to Dual Tension: Formal Contraction, Semantic Expansion, and Problem-Space Governance

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

摘要

近年的自動形式化與形式定理證明系統，已能將愈來愈多自然語言數學敘述轉換為 Lean 等形式語言，並進一步進行自動證明。然而，形式證明系統的嚴格性並不自動保證「被形式化的問題」本身忠實於原始研究問題。當自然語言敘述包含省略前提、視角差異、語用暗示、框架轉換、來源版本差異或證明相關的隱含量詞時，一個語法上完備、型別正確且可被 theorem prover 接受的 formal statement，仍可能只是原問題的一個過早收斂投影。

本文提出一個位於形式證明上游的研究框架：Mathematical Problem Formalization（MPF）與 Natural-Language Understanding（NLU）的雙重張力系統。其中，MPF 負責形式收斂：顯式化物件、定義域、量詞、witness dependency、邊界條件、證書結構與 proof obligation；NLU 則負責受控的語義擴張：保留可能改變 theorem identity 的視角、語用、模態、來源 formulation、資訊狀態與框架轉換。兩者透過 cross-audit、doubt/tolerance controller 與 problem-space closure 協同工作。

本文進一步區分 interpretation tolerance 與 proof tolerance。在問題形成階段，允許非零的語義容錯以避免 premature closure；在 theorem target 被確認並凍結後，形式證明階段則回到零容錯。基於此，我們提出從原始問題到凍結目標的流程：

C_{\mathrm{source}} \rightarrow \mathcal C_{\mathrm{candidate}} \rightarrow C^\ast_{\mathrm{freeze}} \rightarrow \mathrm{MCDM} \rightarrow \mathrm{Proof}.

本文不宣稱已證明 MPF–NLU 雙重張力能普遍提升定理證明成功率；它被提出為一個可檢驗的研究計畫與系統架構。其主要目的，是把「問題可能被問錯、壓錯、理解錯或形式化錯」納入數學 AI 的正式控制流程，使 proof search 的嚴格性建立在更穩定的 problem identity 之上。

關鍵詞： Mathematical Problem Formalization、Autoformalization、Natural-Language Understanding、Target Fidelity、Problem-Space Governance、Premature Closure、Theorem Freezing、Formal Theorem Proving

1. 引言

形式數學的核心優勢之一，是能將證明義務轉換為可由 kernel 嚴格檢查的形式對象。當一個 Lean theorem 已被完整指定後，proof assistant 對型別、依賴、證明項與邏輯推導的要求可以非常嚴格。然而，在 AI 數學系統逐步由「證明已形式化 theorem」走向「從自然語言研究問題直接開始工作」之後，一個更上游的問題變得不可忽略：

形式證明的嚴格性，是否足以保證被證明的 formal target 就是原來真正想問的問題？

答案至少在一般情況下不能直接假定為肯定。

自然語言數學問題不是單純的字串。它通常壓縮了定義慣例、領域邊界、背景知識、角色視角、例外條件、量詞依賴、表示方式、歷史來源與研究意圖。傳統數學共同體可以依賴高度共享的背景，將大量內容省略在 theorem statement 之外；但當 AI 需要把這些敘述轉成唯一且可機器驗證的 formal target 時，這些原本由研究者默會處理的內容便可能轉化為 target-selection risk。

因此，本文主張應嚴格區分：

\boxed{ \text{Proof Formalization} \neq \text{Problem-Generation Formalization}. }

前者回答：

「這個已知 theorem target 要如何被形式化與證明？」

後者回答：

「我們究竟應該把哪一個問題凍結成 theorem target？」

本文研究的是第二個問題。

2. 現有形式化工作與仍存在的上游缺口

2.1 Autoformalization 的進展

近年的 autoformalization 已開始建立從自然語言到 Lean statement 的大規模資料集與端到端系統。FMC 建立了數千個自然語言競賽問題與 Lean formalizations 的對齊資料；Mathesis 則直接研究從自然語言問題到形式 theorem proving 的端到端流程。這些工作顯示，自動形式化已不再只是少量人工示範，而開始成為可系統評測的研究領域。

然而，「能產生 Lean statement」與「能忠實保存原問題」仍是不同指標。一個 statement 可以：

語法正確；
型別正確；
可編譯；
可被 prover 證明；

但仍可能在某個 proof-relevant 層次上偏離原始問題。

2.2 Formal Conjectures 與 fidelity 問題

Formal Conjectures 提供大量研究級 conjectures 的 Lean statements，並明確把 formalization fidelity 視為需要持續審計的問題。其設計本身已反映一個重要事實：即使 statement 已被形式化，仍可能出現 subtle misformalization，而 proof 或 disproof 也可能反過來成為發現錯誤 formalization 的工具。

這表示形式化並不是一個單向流程：

\text{Informal} \rightarrow \text{Formal} \rightarrow \text{Proof}.

更合理的流程可能包含：

\text{Informal} \rightarrow \text{Formal Candidate} \rightarrow \text{Audit} \rightarrow \text{Revision} \rightarrow \text{Proof}.

2.3 長時程形式化中的 target drift

LeanMarathon 進一步指出，研究級長時程 autoformalization 的困難不只來自 hard lemmas，也來自 statement drift、dependency entanglement、context decay 與 local repair 對遠端結構的破壞。其 orchestrator 在正式證明 DAG 被處理前，先進行 target-fidelity stabilization。

本文接受這類觀察，但將問題再往前推：

\boxed{ \text{Target Fidelity} \text{ 不只是長時程 proof engineering 問題，} \text{也是 theorem target 生成本身的認識論問題。} }

2.4 Semantic gap 不等於 parser error

另一類 autoformalization 工作指出，模糊或缺失前提會形成 natural language 與 formal representation 之間的 semantic gap。這種 gap 不能全部被視為「模型還不夠會翻譯」。

有時候問題本身就沒有唯一的無損形式化，除非先補充：

說話者視角；
規則生成方式；
對象所知道的資訊；
來源版本；
「隨機」「應該」「典型」「一般」「存在」等詞的局部語義；
某個自然語言 predicate 背後真正的量詞結構。

因此，autoformalization 不應只被建模成 translation problem，也可能是一個 problem-space reconstruction problem。

3. 從 Compact Statement 到 Expanded Problem Object

令自然語言或傳統數學表述中的壓縮問題為：

C_{\mathrm{compact}}.

我們假設存在一個研究語義較完整的對象：

C_{\mathrm{expanded}},

其中可能包含：

C_{\mathrm{expanded}} = ( O,D,V,Q,R,T,I,X,B,E,A,\Delta,\ldots ).

例如：

$O$ ：Object Space；
$D$ ：Domain / Boundary；
$V$ ：Variable Roles；
$Q$ ：Quantifier Structure；
$R$ ：Representation；
$T$ ：Transformation / Provenance；
$I$ ：Invariant / Symmetry；
$X$ ：Exclusions / Exceptions；
$B$ ：Proof Obligation；
$E$ ：Equivalence / Implication；
$A$ ：Axioms / Model Assumptions；
$\Delta$ ：Perturbation / Sensitivity。

傳統 theorem statement 可以理解為某種壓縮：

\Pi: C_{\mathrm{expanded}} \rightarrow C_{\mathrm{compact}}.

問題在於，當不同研究者或不同 AI 對 compact statement 進行隱式解壓縮時：

\Pi_A^{-1}(C_{\mathrm{compact}}) \neq \Pi_B^{-1}(C_{\mathrm{compact}})

並不是不可能。

因此：

\boxed{ \text{Logical Precision} \neq \text{Generative / Problem-Space Completeness}. }

本文不要求所有 theorem 都必須把整個歷史與語義宇宙完全展開。那會導致無限 regress。真正需要的是 proof-relevant expansion：只展開那些會改變 theorem identity、量詞依賴、證書類型、定義域、框架或 proof obligation 的語義成分。

4. MPF：形式收斂線

我們定義 Mathematical Problem Formalization（MPF）為 proof search 之前的結構化問題建模層。

其最小向量可寫為：

\mathfrak F(C) = ( S,D,Q_s,Q_t,\mathcal G_Q, \mathcal C_T,O,R,U,X,V ).

其中：

$S$ ：statement / symbol structure；
$D$ ：domain and boundary；
$Q_s$ ：surface quantifier structure；
$Q_t$ ：transitive semantic quantifier structure；
$\mathcal G_Q$ ：quantifier dependency graph；
$\mathcal C_T$ ：certificate dependency tree；
$O$ ：proof orientation；
$R$ ：representation；
$U$ ：uniformity requirements；
$X$ ：exceptions / exclusions；
$V$ ：verification / closure condition。

4.1 Surface quantifier 與 transitive quantifier

設 theorem 表面為：

Q_s(C).

若其中 predicate 本身封裝 asymptotic、density、limit、infinite、big-O 等全域結構，真正 proof-relevant quantifier 可能為：

Q_t(C) = \operatorname{SemanticExpand}_{\mathcal R}(Q_s(C)).

一般而言：

\boxed{ Q_s(C) \neq Q_t(C). }

因此，一個形式 parser 即使準確抽出外層 $\forall,\exists$ ，仍可能錯判 counterexample certificate。

4.2 Witness dependency

例如：

\forall x\exists W_x

不能在沒有額外結構時升格成：

\exists W\forall x.

同樣：

\forall N\exists A_N \not\Rightarrow \exists A\forall N.

MPF 的重要功能之一，就是在 proof search 前固定：

\boxed{ \text{Who may depend on whom?} }

4.3 Certificate dependency tree

對某些 conjecture，所謂「找一個反例」並不等於找到一個單點。

若原命題：

\forall A\exists B\,P(A,B),

其否定為：

\exists A^\ast\forall B\,\neg P(A^\ast,B).

此時 $A^\ast$ 只是外層 witness；完整 negative certificate 還包含對所有 $B$ 的 obstruction。

因此應記錄：

\mathcal C_T(C) = \text{Certificate Dependency Tree}.

5. NLU：語義擴張線

如果只有 MPF，系統仍可能過早選定一個形式模型。

因此我們提出第二條、方向相反的線：

\boxed{ N \rightarrow \mathrm{NLU}(N) \rightarrow \{H_1,H_2,\ldots,H_k\}. }

NLU 在本文不是一般語言模型中的「理解分數」，而是 proof-relevant interpretation hypothesis generation。

其任務包括：

誰正在說話？
誰知道哪些資訊？
是否存在規則生成機制？
自然語言 predicate 是否有多種合理數學讀法？
「應該」是 probability claim 還是 decision claim？
來源是否存在多個 formulation？
一個 formal representation 是否只是 source problem 的某個 projection？
某個定義替換是否已經證明 provenance / equivalence？

因此：

\boxed{ \text{MPF tends to contract;} \qquad \text{NLU tends to expand.} }

如果只有 NLU，問題可能永遠不收斂；如果只有 MPF，問題可能 premature closure。

這就是本文所稱的 Dual Tension。

6. 雙重張力：Formal Contraction 與 Semantic Expansion

令 MPF 產生形式候選族：

\mathcal F = \{F_1,\ldots,F_m\},

NLU 產生 interpretation hypotheses：

\mathcal H = \{H_1,\ldots,H_n\}.

Cross-audit：

\operatorname{CrossAudit}(\mathcal F,\mathcal H)

的目標不是找到「語言的唯一真義」，而是排除那些：

與來源明顯衝突；
丟失 proof-relevant dependency；
改變 theorem strength；
偷換 framework；
漏掉 boundary；
造成 representation coverage failure；

的候選。

最終保留一個 tolerable fixed region：

\boxed{ \mathcal R^\ast = \{F_1,\ldots,F_r\}. }

這裡我們刻意不宣稱一定存在唯一 semantic fixed point。

更一般地，問題可能只收斂到一個局部穩定的 semantic–formal neighborhood。

7. Interpretation Tolerance 與 Proof Tolerance

我們引入：

\tau_{\mathrm{interpret}}

作為 theorem target 凍結前允許的 interpretation tolerance。

若某 interpretation $H_i$ 與 formal candidate $F$ 的差異：

d(F,H_i)\le\tau_{\mathrm{interpret}},

系統可以暫時保留該分支。

但這個容錯只存在於問題形成階段。

一旦 theorem target 被 freeze：

C^\ast_{\mathrm{freeze}},

則：

\boxed{ \tau_{\mathrm{proof}}=0. }

至少在 logical correctness 的意義下，proof kernel 仍採嚴格驗證。

因此本文強調：

\boxed{ \text{Interpretation Tolerance} \neq \text{Proof Tolerance}. }

這避免兩種極端：

極端 A：過早形式化

\tau_{\mathrm{interpret}}=0

太早被使用，導致 legitimate alternative interpretations 被剪掉。

極端 B：永久語義漂移

\tau_{\mathrm{interpret}}\rightarrow\infty

導致 theorem target 永遠無法 freeze。

真正需要的是一個控制器。

8. Doubt/Tolerance Controller

令：

D(C) = (D_F,D_S,D_B,D_P,\ldots)

表示 residual doubt vector，例如：

$D_F$ ：formal-structural doubt；
$D_S$ ：source-fidelity doubt；
$D_B$ ：framework-bridge doubt；
$D_P$ ：perspective / pragmatic doubt。

若：

D(C)>\theta,

系統不應直接把它解讀成「拒絕回答」。

而是：

\boxed{ D>\theta \Rightarrow \operatorname{ExpandDomain}. }

可能的擴張為：

D_{t+1}^{\mathrm{problem}} = D_t^{\mathrm{problem}} \cup \Delta D_{\mathrm{semantic}} \cup \Delta D_{\mathrm{perspective}} \cup \Delta D_{\mathrm{framework}} \cup \Delta D_{\mathrm{ontology}}.

反之，當所有 load-bearing ambiguity 已被處理：

D(C)\le\theta_{\mathrm{freeze}},

則：

\boxed{ \operatorname{Freeze}(C) = C^\ast_{\mathrm{freeze}}. }

因此：

\boxed{ \text{Doubt} \rightarrow \text{Expansion / Audit} \rightarrow \text{Closure}, }

而不是：

\text{Doubt} \rightarrow \text{Refusal}.

9. Bridge Audit：跨框架推論的通行費

數學與應用推理經常在不同框架間跳躍。

例如：

F_i \xrightarrow{B_{ij}} F_j.

這種轉換不一定錯，但必須記錄 bridge condition。

例：

\text{frequency} \rightarrow \text{single-case probability},

\text{posterior probability} \rightarrow \text{behavior recommendation},

\text{simulation} \rightarrow \text{theorem claim}.

本文稱：

\boxed{ \mathcal B = \text{Bridge Ledger}. }

每個 bridge 應記錄：

source framework；
target framework；
required assumptions；
preserved invariants；
lost information；
validity status。

若 bridge 尚未被支付其 proof / assumption cost：

\boxed{ \text{Unpaid Bridge} \neq \text{False Conclusion}, }

但表示目前 reasoning chain 尚未 closure。

10. 從 Problem Space 到 Frozen Theorem Target

因此本文提出的完整上游流程為：

\boxed{ \text{NLU} \leftrightarrow \text{MPF} \rightarrow \text{Cross Audit} \rightarrow \text{Doubt/Tolerance} \rightarrow \text{Problem-Space Closure} \rightarrow C^\ast_{\mathrm{freeze}}. }

只有此後才進入：

\boxed{ C^\ast_{\mathrm{freeze}} \rightarrow \text{Difficulty / Research Routing} \rightarrow \text{Formal Proof}. }

如果使用本文作者群先前提出的 MCDM 類 difficulty router，則更完整為：

\boxed{ C_{\mathrm{source}} \rightarrow \mathcal C_{\mathrm{candidate}} \rightarrow C^\ast_{\mathrm{freeze}} \rightarrow \mathrm{MCDM} \rightarrow \mathrm{ResearchRouter} \rightarrow \mathrm{FormalProver}. }

其核心哲學不是增加無限前處理，而是：

\boxed{ \text{在 proof search 成本被大量支付以前，} \text{先確定正在解的是值得解且身份穩定的問題。} }

11. 與現有 Autoformalization 的關係

本文並不主張現有 autoformalization 系統「不夠形式」。

相反地，Lean、Coq 等 proof assistants 的 kernel 正是本文後端可靠性的基礎。

本文主張的是：

\boxed{ \text{Formal rigor at the proof layer} \not\Rightarrow \text{problem fidelity at the generation layer}. }

因此 MPF–NLU Dual Tension 更適合作為：

\boxed{ \text{an upstream control layer} }

而不是 theorem prover 的替代品。

它與現有研究的關係可以概括為：

Autoformalizer：將 natural-language mathematics 轉成 formal objects；
Formal benchmark：提供可驗證的 theorem targets；
Prover：搜尋證明；
本文框架：在 target 被視為固定之前，管理 candidate problem space。

12. 可檢驗假說

本文不把框架本身當作已證實優勢，而提出以下 empirical hypotheses：

H1：Target Corruption Detection

與直接 formalization 相比：

\mathrm{MPF+NLU}

應提高 proof-relevant target corruption 的偵測率。

H2：Premature Closure Reduction

在有自然語言歧義或來源 formulation 差異的問題上：

P( \text{wrong target freeze} \mid \mathrm{DualTension} ) < P( \text{wrong target freeze} \mid \mathrm{MPF-only} ).

H3：Search-Space Efficiency

若 target corruption 原本會導致大量錯誤 proof search，則上游治理可能降低：

\text{abandoned branches}, \quad \text{tokens}, \quad \text{premise retrieval}, \quad \text{proof nodes}, \quad \text{wall time}.

但：

\boxed{ \text{Search-space reduction} \neq \text{intrinsic theorem-complexity reduction}. }

H4：Controlled Expansion

相較於「永遠增加語義分析」：

\text{Adaptive Doubt Controller}

應在保持 target fidelity 的同時降低 unnecessary semantic expansion。

13. 失敗模式與限制

13.1 Over-expansion

NLU 可能產生大量 mathematically irrelevant interpretations。

因此 semantic expansion 必須是 proof-relevant 的，而不是哲學上所有可能世界的枚舉。

13.2 Wrong doubt model

若：

D(C)

本身被錯估，控制器可能在真正危險時 freeze，或在簡單問題上無限懷疑。

13.3 Source ambiguity may be irreducible

某些歷史 conjecture 可能真的存在版本差異，沒有唯一「正確原始意圖」。

此時合理輸出可能不是單一 theorem，而是：

\mathcal C^\ast = \{C_1^\ast,\ldots,C_k^\ast\}.

13.4 Formal equivalence may be expensive

判斷兩個 formulation 是否等價，本身可能需要一個重大 theorem。

因此 Source Fidelity 不能假設所有 equivalence audit 都廉價。

13.5 No universal semantic closure guarantee

本文不證明所有 natural-language mathematical problem 都可在有限時間收斂到唯一 formal target。

因此：

\boxed{ \text{Problem-Space Closure} }

在本文中是一個工程／研究控制目標，而不是一般數學定理。

14. 討論：從解題 AI 到 Problem-Space Governance

傳統 automated theorem proving 的核心問題可以寫成：

\boxed{ \text{Given }C,\text{ find proof }P. }

本文把更上游的問題加入：

\boxed{ \text{Given source }N, \text{ determine which }C \text{ should be proved.} }

因此，數學 AI 的角色開始由：

\text{Solver}

擴張到：

\text{Problem Modeler}

再到：

\boxed{ \text{Problem-Space Governor}. }

所謂治理，不是替代數學家決定什麼問題「值得問」，而是系統化管理：

哪些假設已明示；
哪些仍不確定；
哪些 interpretation 已排除；
哪些 framework bridge 尚未支付；
哪些 target 已足夠穩定；
何時可以把語義容錯關閉，交給零容錯 formal proof。

在此意義下，一個成熟的數學 AI 不只需要容忍：

「我的答案可能錯。」

它還應容忍：

「我目前正在回答的問題模型可能錯。」

因此本文的核心原則可濃縮為：

\boxed{ \text{好的數學 AI 不只驗證答案，} \text{也治理問題被固定成答案目標之前的空間。} }

15. 結論

本文提出 MPF–NLU Dual Tension 作為形式證明上游的 problem-space governance framework。

其核心結構為：

\boxed{ \text{Formal Contraction} \leftrightarrow \text{Semantic Expansion}. }

MPF 將問題收斂為可檢查的 domain、quantifier、dependency、certificate 與 proof obligation；NLU 則防止這種收斂在 source meaning 尚未穩定前過早完成。

透過：

\text{Cross Audit}, \quad \text{Bridge Ledger}, \quad \text{Doubt/Tolerance Control},

系統從：

C_{\mathrm{source}}

建立 candidate family：

\mathcal C_{\mathrm{candidate}},

最終才形成：

C^\ast_{\mathrm{freeze}}.

因此：

\boxed{ \text{Understand the problem} \rightarrow \text{stabilize the target} \rightarrow \text{prove the target}. }

本文不宣稱這個框架已被大規模實證證明。相反地，它提出了一組可由 error injection、blind evaluation、runtime telemetry 與 formal prover benchmark 檢驗的研究假說。

後續工作將進一步研究：target corruption taxonomy、theorem-freeze control、reasoning-resource allocation、specialist orchestration、self-calibrating routing 與 runtime telemetry。這些部分將在本系列後續論文中分別展開。

參考文獻

Firsching, M., Lezeau, P., Mercuri, S., et al. Formal Conjectures: An Open and Evolving Benchmark for Verified Discovery in Mathematics. arXiv:2605.13171, 2026.
The Formal Conjectures Authors. Formal Conjectures Repository. Google DeepMind, Lean 4 / mathlib project, 2025–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.
Xie, J., Liu, C., Yuan, Y., et al. FMC: Formalization of Natural Language Mathematical Competition Problems. arXiv:2507.11275, 2025.
Yu, X., Zhong, J., Feng, Z., et al. Mathesis: Towards Formal Theorem Proving from Natural Languages. arXiv:2506.07047, 2025.
Lu, W., Du, L., Li, S., et al. Automated Formalization via Conceptual Retrieval-Augmented LLMs. arXiv:2508.06931, 2025.

研究狀態聲明

本文中的 MPF–NLU Dual Tension、Interpretation Tolerance、Doubt/Tolerance Controller、Bridge Ledger、Problem-Space Closure 與相關符號體系，均屬本文提出的研究框架與可檢驗假說；除非另有明確引用，不應被理解為現有數學或自動定理證明領域已建立的標準定理。