# 價值耦合智能論 07
# 反例是終點，還是新結構的入口？

## 摘要

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

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

只要找到：

$$
c\in X,\qquad \neg P(c),
$$

就足以推出：

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

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

$$
c\mapsto 0
$$

可能浪費大量結構資訊。

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

因此應區分：

$$
\text{Refutational Value}
$$

與：

$$
\text{Generative Value}.
$$

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

本文進一步提出：

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

作為反例的結構資訊向量，其中：

- \(L\)：Localization，失效定位；
- \(B\)：Boundary，邊界資訊；
- \(M\)：Mechanism，失效機制；
- \(G\)：Generalization，反例家族／一般化資訊；
- \(R\)：Repair，修復方向；
- \(T\)：Transfer，可遷移結構。

並定義「反例提取率」：

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

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

$$
CER\approx0.
$$

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

本文核心結論是：

$$
\boxed{
\text{一個反例的邏輯價值可能只有一個 bit，}
}
$$

$$
\boxed{
\text{但它的研究價值可能遠大於一個 bit。}
}
$$

---

## 關鍵詞

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

---

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

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

若：

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

找到：

$$
c\in X
$$

滿足：

$$
\neg P(c),
$$

則：

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

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

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

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

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

因此本文完全接受：

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

但前一篇已經區分：

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

所以現在真正要問的是：

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

---

## 二、把反例壓縮成 0，究竟丟失了什麼？

假設研究系統只記錄：

$$
h=0.
$$

這表示：

> 原猜想是假的。

邏輯上已經足夠。

但它沒有記錄：

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

因此：

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

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

本文將這種損失稱為：

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

---

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

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

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

而更接近：

$$
\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」否定整體命題。

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

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

對這個反例失效。

也就是找到：

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

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

所以：

$$
\text{global failure}
$$

被轉換成：

$$
\text{local diagnosis}.
$$

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

---

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

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

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

也就是：

> 反例到底打中了哪一層？

假設：

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

反例 \(c\) 使整個證明失敗，不代表：

$$
l_1,l_2,l_3
$$

全部錯。

更可能只有：

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

那麼：

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

這個結果和單純：

$$
h=\text{false}
$$

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

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

---

## 五、第二層：邊界資訊

反例還可以告訴我們：

> 命題在哪裡開始不成立？

例如原命題聲稱：

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

反例分析後可能發現：

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

仍然成立，其中：

$$
X'\subset X.
$$

或者存在參數：

$$
\lambda.
$$

命題在：

$$
\lambda<\lambda_c
$$

成立，而：

$$
\lambda\geq\lambda_c
$$

開始失效。

此時反例不只否定。

它在幫助研究者估計：

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

本文記為：

$$
B(c;h).
$$

---

## 六、第三層：失效機制

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

還可以問：

> 為什麼錯？

定義：

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

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

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

如果知道機制：

$$
M,
$$

就可能從：

$$
\text{false theorem}
$$

生成：

$$
\text{conditional theorem}.
$$

所以：

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

---

## 七、第四層：反例不是點，也可能形成家族

一個反例：

$$
c_1
$$

可能只是一個特殊例外。

但如果進一步搜尋得到：

$$
\mathcal C
=
\{c_1,c_2,\ldots\},
$$

甚至可參數化成：

$$
c(\lambda),
$$

那麼研究問題便從：

> 命題是假的。

轉變為：

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

本文把這一層稱為：

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

即：

$$
c
\rightarrow
\mathcal C.
$$

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

---

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

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

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

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

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

### Level 1

找到一個失敗案例。

### Level 2

理解它為什麼失敗。

### Level 3

找到失敗條件。

### Level 4

形成反例類別。

### Level 5

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

因此：

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

---

## 九、第五層：修復資訊

反例最大的生成價值之一，是提供：

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

例如反例顯示：

$$
h:
A\Rightarrow B
$$

太強。

可能修成：

$$
A\land C\Rightarrow B.
$$

或者：

$$
A\Rightarrow B'
$$

其中：

$$
B'\subset B.
$$

或者：

$$
h
$$

其實只在某個：

$$
X'
$$

上成立。

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

$$
\neg h.
$$

它還可能產生：

$$
h'.
$$

這就是：

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

---

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

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

因此：

$$
c
$$

同時發揮：

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

這個案例很重要，因為它顯示：

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

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

---

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

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

> 為什麼原論證是錯的。

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

$$
\text{Refutation Success}
$$

可能很高，

但：

$$
\text{Explanatory Yield}
$$

仍然很低。

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

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

---

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

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

而是：

$$
\text{Representation}
$$

本身不適合。

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

那麼反例可能要求：

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

也就是：

> 不是修理 theorem，而是修改 object language。

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

所以反例還可能生成：

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

而不只是：

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

---

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

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

### Monster-barring

說：

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

### Concept revision

問：

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

前者有時合理。

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

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

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

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

所以真正問題不是：

> 能不能改定義？

而是：

$$
\boxed{
\text{改定義是在暴露結構，還是在逃避反例？}
}
$$

---

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

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

$$
\text{CEGAR}
$$

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

基本流程可以抽象成：

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

如果抽象模型產生一個：

$$
\text{spurious counterexample},
$$

系統不是說：

> 驗證失敗，所以結束。

而是分析：

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

然後：

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

換句話說：

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

---

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

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

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

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

這時真正的問題不是：

> 模型有反例，因此模型沒用。

而是：

> 哪些被抽象掉的差異，現在證明不能再忽略？

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

$$
\Delta \mathcal A
$$

即：

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

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

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

---

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

Counterexample-Guided Inductive Synthesis：

$$
\text{CEGIS}
$$

則把這件事做得更直接。

其基本循環是：

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

候選：

$$
p_t
$$

被反例：

$$
c_t
$$

推翻後，不只是被丟掉。

\(c_t\) 被加入約束集合：

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

下一個候選：

$$
p_{t+1}
$$

因此必須滿足：

$$
E_{t+1}.
$$

所以反例的功能是：

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

---

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

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

假設兩個反例：

$$
c_1,\qquad c_2.
$$

兩者都能否定：

$$
h.
$$

但：

$$
c_1
$$

可能只是特殊噪聲；

而：

$$
c_2
$$

能揭示：

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

因此可以有：

$$
I(c_2;H)
>
I(c_1;H).
$$

也就是：

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

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

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

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

$$
\text{有反例嗎？}
$$

還要問：

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

---

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

數學證明中常見：

$$
\text{minimal counterexample}
$$

策略。

假設命題是假。

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

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

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

因為所有：

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

的案例都不是反例。

所以最小反例同時包含：

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

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

因此：

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

---

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

假設候選理論：

$$
T_t
$$

經反例 \(c_t\) 後更新成：

$$
T_{t+1}.
$$

我們可以把反例理解為：

$$
\Delta T_t
=
F(c_t,T_t).
$$

如果只記錄：

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

那麼它只是終止訊號。

但如果可以推導：

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

反例就變成：

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

它告訴我們：

> 往哪裡改。

---

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

因此定義：

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

其中：

### \(L\)：Localization

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

### \(B\)：Boundary

它揭示了什麼成立／失效邊界？

### \(M\)：Mechanism

失敗的機制是什麼？

### \(G\)：Generalization

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

### \(R\)：Repair

它指向哪些合理修正版？

### \(T\)：Transfer

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

所以傳統反例只讀：

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

生成式智能則嘗試讀：

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

---

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

定義：

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

稱為：

# Counterexample Extraction Rate

若智能找到反例後只說：

> 命題錯了。

則可能：

$$
CER\approx0.
$$

若它進一步：

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

則：

$$
CER\uparrow.
$$

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

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

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

---

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

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

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

可以定義：

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

稱為：

# Counterexample Generative Return

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

而是測量：

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

有些好反例甚至會：

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

但品質更高。

所以更精確的 CGR 應按：

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

而不只是數量計算。

---

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

同一個反例：

$$
c
$$

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

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

$$
I(c\mid H_1)\approx0.
$$

但另一個智能不知道：

$$
I(c\mid H_2)\gg0.
$$

因此反例價值應寫成：

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

這表示：

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

它和：

- 已知知識；
- 當前候選；
- 搜索歷史；
- 研究目標；

耦合。

---

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

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

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

更好的目標可能是：

$$
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. 保存可遷移結構。

這樣：

$$
V
$$

不再只輸出：

$$
\text{fail}.
$$

而輸出：

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

---

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

第 04 篇提出：

$$
G\rightarrow V\rightarrow R\rightarrow G.
$$

現在可以把它細化成：

$$
G
\rightarrow
V
\rightarrow
C
\rightarrow
R
\rightarrow
G,
$$

其中：

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

也就是：

### Generator

生成候選。

### Verifier

判斷是否成立。

### Counterexample Analyzer

若失敗，提取反例結構。

### Reviser

利用結構資訊修正。

### Generator

重新展開。

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

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

---

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

現在可以區分三種智能。

### 第一種：弱反駁型

找不到好的反例。

$$
F_R\downarrow.
$$

### 第二種：終止式反駁型

很會找反例，但：

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

### 第三種：生成式反駁型

同時具有：

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

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

所以：

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

---

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

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

反例本來可能是：

$$
\Gamma(c)
\in
\mathbb R^k
$$

的高維結構信號。

終止式策略執行：

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

只保留：

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

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

因此：

$$
\boxed{
\text{終止式反駁不只是過早停止，}
}
$$

$$
\boxed{
\text{也是過度壓縮失敗資訊。}
}
$$

---

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

仍然必須限制。

有些反例就是：

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

因此不能要求：

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

也不能：

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

真正合理的是計算：

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

若：

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

直接停止完全合理。

所以本文不是：

$$
\text{counterexample worship}.
$$

而是：

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

---

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

若命題：

$$
h
$$

只有真與假：

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

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

$$
h=0.
$$

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

但研究不是只存：

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

研究還關心：

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

所以反例可能同時提供：

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

因此：

$$
\boxed{
\text{反例的邏輯輸出可以只有 FALSE，}
}
$$

$$
\boxed{
\text{反例的研究輸出卻可以是一整個新模型。}
}
$$

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

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

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

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

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

而要繼續問：

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

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

# 價值耦合智能論 08
# 失敗回收率：一個智能能從錯誤中帶走多少東西

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

下一篇將把問題從：

$$
\text{反例}
$$

擴大到：

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

並正式建立：

$$
\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.