一句话定义：反例搜索（Counterexample Search）是在给定猜想后，主动寻找满足前提却违反结论的具体例子；一旦找到并经形式化验证，猜想即被推翻。
展开讲清原理：数学猜想常写成“对所有满足条件 X 的对象，都有性质 Y”。证明它要覆盖无穷多情况；推翻它只需一个对象，满足 X 但不满足 Y。生活化比方：有人说“所有天鹅都是白的”，你不需要研究所有天鹅的基因，只要找到一只黑天鹅。反例搜索就是组织各种方法去找这只黑天鹅。
在 AI for Math 里，大语言模型擅长根据猜想生成候选构造、参数化思路、边界条件；但它的输出不可信，必须交给验证器。验证器可以是穷举搜索、SAT/SMT 求解器、数值检查，或 Lean/Coq 这类证明助手。OpenAI 的推理模型反驳离散几何猜想，就是先由模型提出反例构造，再由数学家形式化验证，而不是直接生成一篇传统证明。这条路径把“生成”和“验证”分开：模型负责猜，机器负责判。
和相邻概念的区别：
- 证明搜索：目标证明“对所有”成立，通常更难、更开放。
- 定理证明：给定命题，构造形式化证明。
- 反例搜索：目标证明“存在一个”不成立，是存在性搜索。
- 猜想自动生成：提出新猜想，不负责判真假。
| 维度 | 反例搜索 | 证明搜索 |
|---|---|---|
| 目标 | 找一个违反猜想的实例 | 证明猜想对所有实例成立 |
| 逻辑 | 存在量词 | 全称量词 |
| 成功条件 | 一个可验证的反例 | 完整证明 |
| 常见工具 | 搜索、SAT/SMT、数值、LLM 提议 | 证明助手、归纳、策略搜索 |
| 风险 | 候选多、验证必须严格 | 搜索空间大、易卡住 |
对从业者与普通人的实际意义：对 AI 从业者，这是一个可复用的工作流：让模型当“候选生成器”，让形式化工具当“裁判”。它不追求模型自己永远正确，而是把错误限制在可验证的一步。对普通人，遇到“所有人都……”“所有情况都……”的论断，先问：有没有一个反例？找到反例，比争论更省力。注意：反例必须经过严格验证，模型说“找到了”不算数；具体工具与模型能力以官方页面为准。