← Archive
lm-002124 · 2026-08

07_反例是終點還是新結構的入口

下載 MD 檔 ⬇

價值耦合智能論 07

反例是終點,還是新結構的入口?

摘要

在最基本的邏輯語境中,一個反例的功能十分清楚。若命題為:

h:xX, P(x),h:\forall x\in X,\ P(x),

只要找到:

cX,¬P(c),c\in X,\qquad \neg P(c),

就足以推出:

h=false.h=\text{false}.

然而,對研究型智能而言,把反例壓縮成單一布林輸出:

c0c\mapsto 0

可能浪費大量結構資訊。

本文提出「反例結構資訊」(Counterexample Structural Information, CSI)的概念,主張研究型反例除了否定命題之外,還可能提供:失效位置、最小失效條件、適用邊界、隱藏假設、反例家族、修正方向、表徵缺陷與可遷移方法等資訊。

因此應區分:

Refutational Value\text{Refutational Value}

與:

Generative Value.\text{Generative Value}.

本文借用 Lakatos《Proofs and Refutations》中 global counterexample、local counterexample 與 guilty lemma 的方法論,也借用 CEGAR(Counterexample-Guided Abstraction Refinement)與 CEGIS(Counterexample-Guided Inductive Synthesis)等形式方法,說明反例如何成為「下一輪模型/候選修正的方向訊號」。

本文進一步提出:

Γ(c;h)=(L,B,M,G,R,T)\Gamma(c;h) = ( L,B,M,G,R,T )

作為反例的結構資訊向量,其中:

  • (L):Localization,失效定位;
  • (B):Boundary,邊界資訊;
  • (M):Mechanism,失效機制;
  • (G):Generalization,反例家族/一般化資訊;
  • (R):Repair,修復方向;
  • (T):Transfer,可遷移結構。

並定義「反例提取率」:

CER=實際從反例提取的結構資訊反例中可利用的結構資訊.CER = \frac{ \text{實際從反例提取的結構資訊} }{ \text{反例中可利用的結構資訊} }.

終止式反駁的問題,可以因此重新描述為:

CER0.CER\approx0.

反例被正確使用於否定,但沒有被使用於生成。

本文核心結論是:

一個反例的邏輯價值可能只有一個 bit,\boxed{ \text{一個反例的邏輯價值可能只有一個 bit,} } 但它的研究價值可能遠大於一個 bit。\boxed{ \text{但它的研究價值可能遠大於一個 bit。} }

關鍵詞

反例、生成式反駁、Proofs and Refutations、Lakatos、CEGAR、CEGIS、最小反例、結構資訊、猜想修正、價值耦合智能


一、邏輯上,一個反例確實可以結束命題

先承認最簡單而重要的事。

若:

h:xX, P(x),h: \forall x\in X,\ P(x),

找到:

cXc\in X

滿足:

¬P(c),\neg P(c),

則:

h=false.h=\text{false}.

在形式邏輯層面,不需要第二個反例。

也不需要「再給原命題一次機會」。

一個有效反例已足以完成:

Refute(h).\operatorname{Refute}(h).

因此本文完全接受:

反例可以是命題真值問題的終點。\boxed{ \text{反例可以是命題真值問題的終點。} }

但前一篇已經區分:

Proposition ClosureInquiry Closure.\text{Proposition Closure} \neq \text{Inquiry Closure}.

所以現在真正要問的是:

一個足以終止命題的反例,是否同時可能是另一個研究過程的起點?


二、把反例壓縮成 0,究竟丟失了什麼?

假設研究系統只記錄:

h=0.h=0.

這表示:

原猜想是假的。

邏輯上已經足夠。

但它沒有記錄:

  • 哪一類對象使它失敗;
  • 最早在哪個尺度失敗;
  • 哪個證明步驟對反例無效;
  • 哪個隱藏假設被打破;
  • 是否只有一個特殊反例;
  • 是否存在整個反例家族;
  • 增加什麼條件可以恢復定理;
  • 原方法是否仍能證明較弱命題。

因此:

Compress(c)=FALSE\operatorname{Compress}(c) = \text{FALSE}

是一種極度有損的資訊壓縮。

本文將這種損失稱為:

Counterexample Information Loss\boxed{ \text{Counterexample Information Loss} }

三、Lakatos 的核心正是在反例之後繼續追問

《Proofs and Refutations》所展示的數學發展模式,不是:

ConjectureCounterexampleEnd.\text{Conjecture} \rightarrow \text{Counterexample} \rightarrow \text{End}.

而更接近:

Primitive ConjectureProofGlobal CounterexampleRe-examine ProofLocal CounterexampleGuilty LemmaImproved Conjecture.\text{Primitive Conjecture} \rightarrow \text{Proof} \rightarrow \text{Global Counterexample} \rightarrow \text{Re-examine Proof} \rightarrow \text{Local Counterexample} \rightarrow \text{Guilty Lemma} \rightarrow \text{Improved Conjecture}.

這個結構極其重要。

「global counterexample」否定整體命題。

但真正的研究動作,是重新檢查原證明,找出:

哪一個 lemma\text{哪一個 lemma}

對這個反例失效。

也就是找到:

guilty lemma\boxed{ \text{guilty lemma} }

再把新發現的限制條件寫進修正版命題。

所以:

global failure\text{global failure}

被轉換成:

local diagnosis.\text{local diagnosis}.

這就是從「反駁」進入「生成」的第一步。


四、反例的第一層額外資訊:失效定位

本文把第一項結構資訊記為:

L(c;h)=Localization.L(c;h) = \text{Localization}.

也就是:

反例到底打中了哪一層?

假設:

h=l1l2l3T.h = l_1\land l_2\land l_3\Rightarrow T.

反例 (c) 使整個證明失敗,不代表:

l1,l2,l3l_1,l_2,l_3

全部錯。

更可能只有:

l2(c)=false.l_2(c)=\text{false}.

那麼:

L(c;h)=l2.L(c;h)=l_2.

這個結果和單純:

h=falseh=\text{false}

相比,多出了「可修正性」。

因為現在知道應該修哪裡。


五、第二層:邊界資訊

反例還可以告訴我們:

命題在哪裡開始不成立?

例如原命題聲稱:

xX, P(x).\forall x\in X,\ P(x).

反例分析後可能發現:

xX,P(x)\forall x\in X', \quad P(x)

仍然成立,其中:

XX.X'\subset X.

或者存在參數:

λ.\lambda.

命題在:

λ<λc\lambda<\lambda_c

成立,而:

λλc\lambda\geq\lambda_c

開始失效。

此時反例不只否定。

它在幫助研究者估計:

Validity Boundary\boxed{ \text{Validity Boundary} }

本文記為:

B(c;h).B(c;h).

六、第三層:失效機制

知道「在哪裡錯」還不夠。

還可以問:

為什麼錯?

定義:

M(c;h)=Failure Mechanism.M(c;h) = \text{Failure Mechanism}.

例如某猜想失效可能是因為:

  • 非單連通;
  • 對稱性破缺;
  • 極限交換不合法;
  • 某種退化情況;
  • 非緊致性;
  • 邊界項沒有消失;
  • 整數條件被忽略;
  • 遞迴在特殊狀態不收斂。

如果知道機制:

M,M,

就可能從:

false theorem\text{false theorem}

生成:

conditional theorem.\text{conditional theorem}.

所以:

機制資訊比單純反例座標更深。\boxed{ \text{機制資訊比單純反例座標更深。} }

七、第四層:反例不是點,也可能形成家族

一個反例:

c1c_1

可能只是一個特殊例外。

但如果進一步搜尋得到:

C={c1,c2,},\mathcal C = \{c_1,c_2,\ldots\},

甚至可參數化成:

c(λ),c(\lambda),

那麼研究問題便從:

命題是假的。

轉變為:

所有失敗案例的共同結構是什麼?

本文把這一層稱為:

G(c;h)=Generalization of Counterexamples.G(c;h) = \text{Generalization of Counterexamples}.

即:

cC.c \rightarrow \mathcal C.

這時反例本身開始變成新的數學對象。


八、尋找「一般反例」本身就是更高階能力

數學教育研究對 proof-by-counterexample 的分析也顯示,學習者的反例能力並非只有「偶然找到一個例子」這一層。

有些更高階的推理能夠從單一例子進一步形成:

general set of counterexamples.\text{general set of counterexamples}.

這意味著反駁能力本身就可以分層:

Level 1

找到一個失敗案例。

Level 2

理解它為什麼失敗。

Level 3

找到失敗條件。

Level 4

形成反例類別。

Level 5

由反例類別生成修正版定理。

因此:

反例發現反例理解.\boxed{ \text{反例發現} \neq \text{反例理解}. }

九、第五層:修復資訊

反例最大的生成價值之一,是提供:

R(c;h)=Repair Direction.R(c;h) = \text{Repair Direction}.

例如反例顯示:

h:ABh: A\Rightarrow B

太強。

可能修成:

ACB.A\land C\Rightarrow B.

或者:

ABA\Rightarrow B'

其中:

BB.B'\subset B.

或者:

hh

其實只在某個:

XX'

上成立。

所以反例的輸出不必只有:

¬h.\neg h.

它還可能產生:

h.h'.

這就是:

Counterexample-guided conjecture repair.\boxed{ \text{Counterexample-guided conjecture repair}. }

十、數學教育中已直接觀察到這種修正過程

一項針對小學生猜想與證明的研究中,學生原本以為已證明自己的猜想;當研究者提供反例後,他們沒有只停在「原猜想錯了」,而是重新檢查舊證明、理解失敗原因、找出仍適用於反例的證明部分,最後形成更完整的猜想。

因此:

cc

同時發揮:

Refutation+Diagnosis+Revision.\text{Refutation} + \text{Diagnosis} + \text{Revision}.

這個案例很重要,因為它顯示:

生成式使用反例不需要先假設研究者是頂尖數學家。

它是一種可以被培養、被工作流化的認知操作。


十一、2026 年的教師研究也顯示「找到反例」和「解釋反例」不同

近期針對準小學教師的研究發現,多數參與者能成功辨識錯誤論證並提出反例,但只有少部分反例真正解釋:

為什麼原論證是錯的。

這提供了一個很有價值的區分:

Refutation Success\text{Refutation Success}

可能很高,

但:

Explanatory Yield\text{Explanatory Yield}

仍然很低。

所以「會反駁」不能直接推出:

會提取反例結構.\text{會提取反例結構}.

十二、第六層:反例可能暴露表示本身有問題

有些時候,問題不是命題需要多加一個條件。

而是:

Representation\text{Representation}

本身不適合。

例如我們把一類對象用錯誤分類方式表達,使某些反例看起來像怪物。

那麼反例可能要求:

Reframe(X).\operatorname{Reframe}(X).

也就是:

不是修理 theorem,而是修改 object language。

數學史中大量新的定義、分類與不變量,正是為了使原本混亂的例外變得可以被系統描述。

所以反例還可能生成:

新的概念空間\boxed{ \text{新的概念空間} }

而不只是:

新的命題.\text{新的命題}.

十三、這就是為什麼「怪物」有時候很重要

面對極端反例,研究者可以採取兩種不同策略:

Monster-barring

說:

這種對象根本不應算在我們的定義裡。

Concept revision

問:

為什麼它會讓我們現在的概念系統失效?

前者有時合理。

因為真正研究對象可能確實需要精確定義。

但如果每次反例都透過定義排除:

Coutside domain,\mathcal C \rightarrow \text{outside domain},

就可能錯過新的分類結構。

所以真正問題不是:

能不能改定義?

而是:

改定義是在暴露結構,還是在逃避反例?\boxed{ \text{改定義是在暴露結構,還是在逃避反例?} }

十四、CEGAR:工程上把「反例→修正模型」變成演算法

形式驗證中的 Counterexample-Guided Abstraction Refinement:

CEGAR\text{CEGAR}

提供了一個極其漂亮的工程類比。

基本流程可以抽象成:

M0Model CheckcAnalyzeM1.M_0 \rightarrow \text{Model Check} \rightarrow c \rightarrow \text{Analyze} \rightarrow M_1 \rightarrow \cdots.

如果抽象模型產生一個:

spurious counterexample,\text{spurious counterexample},

系統不是說:

驗證失敗,所以結束。

而是分析:

這個反例暴露了目前 abstraction 的哪個缺陷?

然後:

Refine(M0,c)=M1.\operatorname{Refine}(M_0,c) = M_1.

換句話說:

反例不是錯誤訊息,而是模型精煉訊號。\boxed{ \text{反例不是錯誤訊息,而是模型精煉訊號。} }

十五、CEGAR 最重要的思想是「失敗指向哪裡要增加解析度」

抽象模型的目的本來就是:

忽略部分細節.\text{忽略部分細節}.

所以它可能產生虛假的錯誤路徑。

這時真正的問題不是:

模型有反例,因此模型沒用。

而是:

哪些被抽象掉的差異,現在證明不能再忽略?

因此反例在這裡實際提供:

ΔA\Delta \mathcal A

即:

abstraction refinement direction.\text{abstraction refinement direction}.

這和數學猜想修正幾乎具有同一個資訊結構:

counterexamplelocate missing distinctionrefine representation.\text{counterexample} \rightarrow \text{locate missing distinction} \rightarrow \text{refine representation}.

十六、CEGIS:反例甚至可以直接縮小候選空間

Counterexample-Guided Inductive Synthesis:

CEGIS\text{CEGIS}

則把這件事做得更直接。

其基本循環是:

Synthesize candidateVerifyCounterexampleUpdate examplesSynthesize again.\text{Synthesize candidate} \rightarrow \text{Verify} \rightarrow \text{Counterexample} \rightarrow \text{Update examples} \rightarrow \text{Synthesize again}.

候選:

ptp_t

被反例:

ctc_t

推翻後,不只是被丟掉。

ctc_t 被加入約束集合:

Et+1=Et{ct}.E_{t+1} = E_t\cup\{c_t\}.

下一個候選:

pt+1p_{t+1}

因此必須滿足:

Et+1.E_{t+1}.

所以反例的功能是:

縮小下一輪搜索空間。\boxed{ \text{縮小下一輪搜索空間。} }

十七、這裡出現了一個關鍵概念:反例的「頻寬」

不是所有反例都同樣有用。

假設兩個反例:

c1,c2.c_1,\qquad c_2.

兩者都能否定:

h.h.

但:

c1c_1

可能只是特殊噪聲;

而:

c2c_2

能揭示:

  • 一整類失效條件;
  • 某個核心變量;
  • 某種邊界結構。

因此可以有:

I(c2;H)>I(c1;H).I(c_2;H) > I(c_1;H).

也就是:

相對於目前候選空間,某些反例包含更高資訊增益。

CEGIS 相關研究甚至直接討論:

oracle 提供的反例類型與反饋「vocabulary/bandwidth」會影響學習與收斂能力。

因此研究型智能不能只問:

有反例嗎?\text{有反例嗎?}

還要問:

哪一個反例最有信息?\boxed{ \text{哪一個反例最有信息?} }

十八、最小反例為什麼常常有價值?

數學證明中常見:

minimal counterexample\text{minimal counterexample}

策略。

假設命題是假。

不是任意拿一個反例,而是在某種良序下選擇「最小」反例:

c=argmincCμ(c).c^* = \arg\min_{c\in\mathcal C} \mu(c).

最小性會額外提供結構條件。

因為所有:

μ(c)<μ(c)\mu(c)<\mu(c^*)

的案例都不是反例。

所以最小反例同時包含:

failure+all smaller success.\text{failure} + \text{all smaller success}.

這經常讓研究者能夠建立遞降、刪除或還原結構,最後導出矛盾。

因此:

好的反例不只是反例,還攜帶鄰域信息。\boxed{ \text{好的反例不只是反例,還攜帶鄰域信息。} }

十九、反例應該被看成一個「差分訊號」

假設候選理論:

TtT_t

經反例 ctc_t 後更新成:

Tt+1.T_{t+1}.

我們可以把反例理解為:

ΔTt=F(ct,Tt).\Delta T_t = F(c_t,T_t).

如果只記錄:

ΔTt=accept(Tt),\Delta T_t = -\text{accept}(T_t),

那麼它只是終止訊號。

但如果可以推導:

ΔTt=(Δscope,Δlemma,Δrepresentation,Δconstraint),\Delta T_t = ( \Delta\text{scope}, \Delta\text{lemma}, \Delta\text{representation}, \Delta\text{constraint} ),

反例就變成:

模型更新梯度的離散類比。\boxed{ \text{模型更新梯度的離散類比。} }

它告訴我們:

往哪裡改。


二十、本文提出反例結構資訊向量

因此定義:

Γ(c;h)=(L,B,M,G,R,T).\Gamma(c;h) = ( L,B,M,G,R,T ).

其中:

(L):Localization

反例定位了哪一個失效部分?

(B):Boundary

它揭示了什麼成立/失效邊界?

(M):Mechanism

失敗的機制是什麼?

(G):Generalization

是否能產生反例家族或失效分類?

(R):Repair

它指向哪些合理修正版?

(T):Transfer

其中是否存在可遷移到其他問題的工具、方法或表示?

所以傳統反例只讀:

bool(c)=0.\operatorname{bool}(c)=0.

生成式智能則嘗試讀:

Γ(c;h).\Gamma(c;h).

二十一、再提出「反例提取率」

定義:

CER=Iextracted(c)Iavailable(c).CER = \frac{ I_{\mathrm{extracted}}(c) }{ I_{\mathrm{available}}(c) }.

稱為:

Counterexample Extraction Rate

若智能找到反例後只說:

命題錯了。

則可能:

CER0.CER\approx0.

若它進一步:

  • 找失效引理;
  • 找邊界;
  • 找家族;
  • 修正命題;
  • 保存方法;

則:

CER.CER\uparrow.

因此第 05 篇的「終止式反駁」現在可以更精確地寫成:

TRPCER\boxed{ TRP\uparrow \quad\Longleftrightarrow\quad CER\downarrow }

至少在仍存在可回收結構的問題中如此。


二十二、還需要一個「反例生成收益」

假設反例導致新的候選集合:

Ht+1.\mathcal H_{t+1}.

可以定義:

CGR=Ht+1valuable1+Htvaluable.CGR = \frac{ |\mathcal H_{t+1}^{\mathrm{valuable}}| }{ 1+|\mathcal H_t^{\mathrm{valuable}}| }.

稱為:

Counterexample Generative Return

這不是要求每個反例都必須產生很多猜想。

而是測量:

反例是否讓後續研究空間變得更有結構?

有些好反例甚至會:

Ht+1<Ht|\mathcal H_{t+1}|<|\mathcal H_t|

但品質更高。

所以更精確的 CGR 應按:

hHU(h)\sum_{h\in\mathcal H}U(h)

而不只是數量計算。


二十三、反例的價值和當前知識狀態有關

同一個反例:

cc

對不同智能體,資訊量可能不同。

如果智能已經知道失效機制:

I(cH1)0.I(c\mid H_1)\approx0.

但另一個智能不知道:

I(cH2)0.I(c\mid H_2)\gg0.

因此反例價值應寫成:

I(cHt).I(c\mid H_t).

這表示:

反例沒有絕對固定的研究價值。\boxed{ \text{反例沒有絕對固定的研究價值。} }

它和:

  • 已知知識;
  • 當前候選;
  • 搜索歷史;
  • 研究目標;

耦合。


二十四、因此也存在「好反例選擇」問題

如果智能可以主動尋找反例,就不應只最大化:

P(find any failure).P(\text{find any failure}).

更好的目標可能是:

c=argmaxcE[I(c;H)+R(c)+B(c)].c^* = \arg\max_c \mathbb E[ I(c;H) + R(c) + B(c) ].

也就是尋找:

最能區分候選、暴露機制、縮小搜索空間的反例。

這和 active learning 的思想非常接近。

不是問最多問題。

而是問:

最有信息的問題。\boxed{ \text{最有信息的問題。} }

二十五、AI 數學系統可以加入 Counterexample Curator

因此研究 Agent 不只需要:

  • Generator;
  • Verifier;
  • Reviser。

還可以加入:

Counterexample Curator

它的職責不是單純找更多反例,而是:

  1. 去除重複反例;
  2. 尋找最小反例;
  3. 聚類反例家族;
  4. 找共同失效機制;
  5. 評估信息量;
  6. 將反例轉換成修正條件;
  7. 保存可遷移結構。

這樣:

VV

不再只輸出:

fail.\text{fail}.

而輸出:

(c,Γ(c;h)).(c,\Gamma(c;h)).

二十六、這能直接改善前面的生成—驗證—修復循環

第 04 篇提出:

GVRG.G\rightarrow V\rightarrow R\rightarrow G.

現在可以把它細化成:

GVCRG,G \rightarrow V \rightarrow C \rightarrow R \rightarrow G,

其中:

C=Counterexample Analysis.C=\text{Counterexample Analysis}.

也就是:

Generator

生成候選。

Verifier

判斷是否成立。

Counterexample Analyzer

若失敗,提取反例結構。

Reviser

利用結構資訊修正。

Generator

重新展開。

因此真正完整的迴圈更像:

GenerateFalsifyExplain FailureRepairRegenerate\boxed{ \text{Generate} \rightarrow \text{Falsify} \rightarrow \text{Explain Failure} \rightarrow \text{Repair} \rightarrow \text{Regenerate} }

二十七、這也重新定義了「反駁型智能」

現在可以區分三種智能。

第一種:弱反駁型

找不到好的反例。

FR.F_R\downarrow.

第二種:終止式反駁型

很會找反例,但:

CER,TRP.CER\downarrow, \qquad TRP\uparrow.

第三種:生成式反駁型

同時具有:

FR,CER,CGR.F_R\uparrow, \qquad CER\uparrow, \qquad CGR\uparrow.

第三種才是真正適合研究的強反駁智能。

所以:

反駁能力越高,越需要反例後生成能力配套。\boxed{ \text{反駁能力越高,越需要反例後生成能力配套。} }

二十八、終止式反駁其實把高維反例降成一維

我們現在可以重新理解第 05 篇。

反例本來可能是:

Γ(c)Rk\Gamma(c) \in \mathbb R^k

的高維結構信號。

終止式策略執行:

Γ(c){0,1}.\Gamma(c) \mapsto \{0,1\}.

只保留:

pass/fail.\text{pass/fail}.

這是一個巨大的資訊降維。

因此:

終止式反駁不只是過早停止,\boxed{ \text{終止式反駁不只是過早停止,} } 也是過度壓縮失敗資訊。\boxed{ \text{也是過度壓縮失敗資訊。} }

二十九、但反例也不能被過度神化

仍然必須限制。

有些反例就是:

  • 特殊例外;
  • 噪聲;
  • 已知邊界;
  • 沒有新資訊;
  • 由錯誤輸入造成;
  • 對主問題沒有後續價值。

因此不能要求:

c,CER=1.\forall c,\quad CER=1.

也不能:

每發現一個反例就開一個新研究計畫。

真正合理的是計算:

Uanalyze(c).U_{\mathrm{analyze}}(c).

若:

Uanalyze0,U_{\mathrm{analyze}}\leq0,

直接停止完全合理。

所以本文不是:

counterexample worship.\text{counterexample worship}.

而是:

counterexample valuation.\boxed{ \text{counterexample valuation}. }

三十、結論:一個反例的邏輯價值可能只有一個 bit,但研究價值可能遠大於一個 bit

若命題:

hh

只有真與假:

{1,0},\{1,0\},

一個有效反例確實足以提供:

h=0.h=0.

從真值判定角度看,工作完成。

但研究不是只存:

Truth(h).\operatorname{Truth}(h).

研究還關心:

Structure(h).\operatorname{Structure}(h).

所以反例可能同時提供:

Γ(c;h)=(L,B,M,G,R,T).\Gamma(c;h) = ( L,B,M,G,R,T ).

因此:

反例的邏輯輸出可以只有 FALSE,\boxed{ \text{反例的邏輯輸出可以只有 FALSE,} } 反例的研究輸出卻可以是一整個新模型。\boxed{ \text{反例的研究輸出卻可以是一整個新模型。} }

Lakatos 的證明與反駁,把反例從結束符號變成猜想改進工具。

CEGAR 把反例變成 abstraction refinement 的方向。

CEGIS 把反例變成下一輪 synthesis 的約束。

研究型智能也應該做同樣的事:

不要只問「它證明我錯了嗎?」\boxed{ \text{不要只問「它證明我錯了嗎?」} }

而要繼續問:

「它究竟教了我什麼?」\boxed{ \text{「它究竟教了我什麼?」} }

這使第二部下一篇自然進入:

價值耦合智能論 08

失敗回收率:一個智能能從錯誤中帶走多少東西

第 07 篇已經證明反例可能包含大量結構資訊。

下一篇將把問題從:

反例\text{反例}

擴大到:

所有失敗研究路徑\text{所有失敗研究路徑}

並正式建立:

Failure Salvage Rate\boxed{ \text{Failure Salvage Rate} }

來測量:

一個智能究竟能從失敗的理論、證明、程式、實驗與搜索路徑中,保存多少可用結構?


參考資料(本篇重新查核)

  1. Lakatos, Imre. Proofs and Refutations: The Logic of Mathematical Discovery. Cambridge University Press.
  2. Lakatos, Appendix 1: the method of proofs and refutations, including global counterexamples, local counterexamples and the “guilty lemma”.
  3. Komatsu, K. (2010). Counter-examples for refinement of conjectures and proofs in primary school mathematics. The Journal of Mathematical Behavior 29(1), 1–10.
  4. Students’ proof schemes for mathematical proving and disproving of propositions (2016), Journal of Mathematical Behavior.
  5. “It won’t work every time”: Prospective elementary teachers’ counterexamples for students’ false arguments about fractions (2026), Journal of Mathematical Behavior.
  6. Clarke, E. M., Grumberg, O., Jha, S., Lu, Y., & Veith, H. Counterexample-Guided Abstraction Refinement; later JACM formulation of CEGAR.
  7. Hajdu & Micskei (2020). Efficient Strategies for CEGAR-Based Model Checking. Journal of Automated Reasoning.
  8. Jha & Seshia (2017). A Theory of Formal Synthesis via Inductive Learning. Acta Informatica.
  9. Polgreen, Reynolds & Seshia (2021/2022). Satisfiability and Synthesis Modulo Oracles.
  10. Research and talks on CEGIS-T / counterexample feedback vocabulary and bandwidth.