在一次代码评审中，我让 LLM 对一个看似理所当然的断言找反例：Python 里的浮点乘法是否满足结合律。LLM 很快给出一个反例：取x = 1e308，y = 10.0，z = 1e-308，左边(x * y) * z会得到inf，右边x * (y * z)会得到10.0，两边不相等。这个反例背后涉及 IEEE 754 浮点表示、溢出与下溢，属于很多开发人员并不熟悉的数值计算领域。问题不在反例本身，而是当 LLM 生成的反例远超出你的专业领域时，你既无法确认它是对的，也无法证明它是错的。
这类现象在 LLM 应用开发中越来越常见。LLM 不仅能生成代码和解释，还会生成“反例”来否定某个命题、测试预期或设计假设。恰巧，这类反例往往使用了大量专业术语，结构上又很像真实结论，很容易让评审者陷入两难：接受它，可能引入错误；拒绝它，又可能丢掉一个真实问题。这篇文章会围绕一个最小案例，说明如何把 LLM 生成的反例从“结论”降级为“可检验声明”，并建立一套用于验证、沉淀和复用的工程流程。
1. 先理解 LLM 反例为什么比普通回答更难处理
1.1 反例在软件工程中的真实定位
反例（counterexample）原本是数学和形式验证中的概念。当一个命题声称“所有 X 都满足性质 P”时，只要找到一个 X 让 P 不成立，就足以推翻整个命题。在软件工程中，反例通常表现为一个测试输入、一段并发执行序列、一个数据状态，或者一个环境配置，用来证明测试断言或系统假设并不总是成立。
举个例子，如果某个函数签名是int safeAdd(int a, int b)，实现者断言“在 a 和 b 均为正数时，返回值一定大于 a”。要推翻它，只需要给出a = Integer.MAX_VALUE、b = 1，函数在溢出后返回一个负数。这个反例的价值不在于“函数写错了”，而在于它暴露了底层数值表示的边界，提醒开发者必须处理溢出。
反例和普通 bug 报告最大的区别在于：反例往往不是“程序运行报错”，而是“程序运行结果推翻了一个假设”。因此，反例在代码审查、测试设计、数据库隔离级别分析、并发编程和协议设计中都很重要。过去判断一个反例是否正确，主要靠领域专家经验和复现实验。现在有了 LLM，生成反例的门槛极低，但验证反例的难度并没有随之下降。
1.2 LLM 反例的三个特征：专业、可执行、不可信
LLM 生成的反例通常有三个明显特征。
第一个特征是“专业腔”。LLM 在训练语料中见过大量论文、技术文档和专家讨论，因此很容易组织出包含专业术语的句子。例如一个刚接触 PostgreSQL 的前端开发者，看到 LLM 输出“在 READ COMMITTED 隔离级别下，如果使用 SELECT FOR UPDATE 先锁定行，两个事务可以顺序更新，后提交事务不会失败”，会本能地认为这个结论来自数据库专家。术语密度很高，但不代表结论一定正确。
第二个特征是“可执行”。LLM 通常会生成具体的数字、代码片段、步骤序列，而不是空泛的“可能不成立”。这反而增加了判断难度，因为看起来很具体的东西更容易被当成已经被验证过的东西。
第三个特征是“不可信”。LLM 本质上是一个概率语言模型，不是定理证明器。它生成反例时，并不会在内部“计算”这个反例是否成立，而是根据训练语料中的相关模式，生成一段在统计上最可能出现的文本。语料里浮点精度问题很多，它就可能生成一个浮点反例；语料里数据库死锁案例很多，它就可能生成一个并发反例。这段文本可能完全正确，也可能只是“看起来正确”。
1.3 当反例超出专业领域时，人工验证会失效
如果反例落在你的专业范围内，比如你长期写 SQL，看到 LLM 说“MySQL 在 RC 隔离级别下存在不可重复读”，你可以凭经验判断它是否成立。但很多反例恰恰落在你的知识盲区里。一个前端工程师可能没听过 IEEE 754，一个后端工程师可能不熟悉概率分布的特征函数，一个移动端开发者可能不了解编译器优化中的未定义行为。
此时，人工验证会退化成两种极端行为。一种是因为看不懂而盲目相信，理由是“它说得那么详细，应该没错”；另一种是看不懂就一律拒绝，理由是“我无法复现，所以它可能是幻觉”。这两种行为都不是工程判断，而是心理偏误。
正确处理方式是承认两个事实：第一，单靠人类知识和直觉无法覆盖所有领域；第二，LLM 生成的反例必须经过一个“可复现验证流程”才能被采纳。这篇文章后续的流程就是围绕这一点展开的，核心目标是把反例从“叙述”变成“可执行的证据”。
2. 一个最小案例：让 LLM 为断言生成反例
2.1 选择一条处于知识边界上的断言
为了演示完整流程，我选择一条在应用开发者看来“没什么问题”，但在数值计算领域很容易出错的断言：
Python 浮点乘法满足结合律，即对任意三个 float，都有
(a * b) * c == a * (b * c)。
在高中数学里，实数乘法满足结合律。但在计算机中，浮点数并不是实数。浮点数使用有限位二进制表示，会引入舍入；同时，当数值接近指数边界时，会发生溢出或下溢。因此，浮点乘法不满足结合律是一个真实存在的问题。
这个断言对于普通 Web 开发者来说，往往处于知识边界之外。大多数人在日常开发中不会主动思考1e308 * 10会变成inf，也不会关心1e-308是否会下溢到0。这就天然符合“反例远离专业经验”的场景。
2.2 定义生成反例的提示词
直接问 LLM“请找反例”通常只会得到一段结论，不利于后续自动验证。更好的方式是要求 LLM 输出结构化信息。下面这段提示词可以用于说明思路，实际项目中需要根据模型能力和接口做调整。
系统角色：你是严格验证者。你的任务不是给出泛泛结论，而是生成一个可以被程序验证的结构化反例。 待验证断言：Python 浮点乘法满足结合律，即对任意三个 float， 都有 (a * b) * c == a * (b * c)。 请输出 JSON： { "assertion": "字符串，原始断言", "counterexample": {"a": 数值, "b": 数值, "c": 数值}, "reason": "字符串，说明为什么该输入会让断言失效", "verification_code": "可运行的 Python 代码", "expected_output": "运行代码后预期看到的输出" }把提示词限定为 JSON 输出有两个好处。第一，后续处理环节可以直接解析字段，不用从自然语言里抽取信息。第二，强制 LLM 提供验证代码和预期输出，会让反例的可复现性前置到生成阶段。
2.3 LLM 可能返回的两类反例
调用一个 OpenAI 兼容接口，把上述提示词发给模型，可能会得到类似下面的内容。
{ "assertion": "Python 浮点乘法满足结合律", "counterexample": { "a": 1e308, "b": 10.0, "c": 1e-308 }, "reason": "左式先计算 1e308*10，结果溢出为 inf，再乘 1e-308 仍为 inf；右式先计算 10*1e-308 得到 1e-307，再乘 1e308 得到 10.0。两边结果不同，所以结合律不成立。", "verification_code": "x = 1e308; y = 10.0; z = 1e-308; print((x*y)*z, x*(y*z), (x*y)*z == x*(y*z))", "expected_output": "inf 10.0 False" }这个反例是可以执行验证的，而且验证结果确实如expected_output所示。但并不是所有 LLM 输出都这么可靠。换一个模型，或者换成另一个断言，LLM 可能给出下面这种“专业但不真实”的反例：
{ "assertion": "Python 浮点加法满足交换律", "counterexample": { "a": 0.1, "b": 0.2 }, "reason": "在 RISC-V 架构下，编译器可能使用 FMA 指令融合乘加，导致 0.1+0.2 的结果不满足 IEEE 754 单步语义。", "verification_code": "print(0.1 + 0.2 != 0.3)", "expected_output": "True" }这段内容的问题在于混淆了概念，0.1 + 0.2 != 0.3在大多数环境中确实成立，但它不是加法交换律的反例，也和 FMA 指令没有必然关系。如果开发者只看到“FMA 指令融合”和“RISC-V 架构”这些专业词，很容易被带偏。
2.4 为什么这类反例不能直接采用
上面两类反例的共同点是：它们都没有经过验证。即使第一个反例看起来正确，也必须运行验证代码才能确认。第二个反例虽然“可能碰巧输出 True”，但它的推理过程是错误的，不能作为反例证据使用。
在工程实践中，一个可执行反例至少需要包含三部分：
- 反例输入，能够唯一确定一个可构造的值或状态。
- 验证代码，能在实际环境中运行并退出。
- 预期输出，能说明代码运行后应该在哪个位置暴露矛盾。
只有三者齐全，反例才算“可检验声明”。否则，它只是一个“叙述”。正确的处理方式是把 LLM 的输出原样保存，然后进入验证流水线，而不是在评审现场用直觉判断。
3. 建立反例验证流水线：生成、检索、执行、复核
3.1 验证流水线的总体设计
单个 LLM 生成的反例不足以作为决策依据。更稳妥的方式是把“生成反例”放到一条可追踪的流水线里。流水线至少包含五个环节：
| 环节 | 主要任务 | 产出 |
|---|---|---|
| 生成反例 | 调用 LLM，输出结构化反例 | JSON 反例草稿 |
| 资料检索 | 使用 RAG 检索标准、文档、案例 | 相关证据列表 |
| 代码执行 | 在隔离环境中运行验证代码 | 实际输出与退出码 |
| 交叉验证 | 使用另一个模型独立判断 | 多模型结论 |
| 人工复核 | 由负责人综合证据作出结论 | 验证报告与结论 |
这条流水线适合用编排框架实现。LLM 应用开发中，编排框架解决的核心问题就是“多步骤、多工具、多模型”的组织方式。初学者可以先不引入复杂框架，直接用 Python 函数实现 pipeline；当步骤变多、需要重试和状态管理时，再引入 LangChain、LlamaIndex 或 Spring AI 这类编排框架。
3.2 用编排框架组装验证 Agent
下面是一个极简的 pipeline 实现，目的是展示流程，不依赖具体框架。实际项目需要根据模型网关、向量库和运行环境调整。
from typing import Any import json import subprocess def generate_counterexample(assertion: str) -> dict: # 伪代码，真实场景在这里调用 LLM 接口 # 返回结构化反例 JSON return { "assertion": assertion, "counterexample": {"a": 1e308, "b": 10.0, "c": 1e-308}, "verification_code": "x=1e308;y=10.0;z=1e-308;print((x*y)*z, x*(y*z), (x*y)*z == x*(y*z))", "expected_output": "inf 10.0 False", } def execute_script(code: str) -> dict: # 在实际环境中，建议通过 Docker 或子进程隔离执行 proc = subprocess.run( ["python", "-c", code], capture_output=True, text=True, timeout=30, ) return { "returncode": proc.returncode, "stdout": proc.stdout.strip(), "stderr": proc.stderr.strip(), } def search_kb(query: str) -> list[str]: # 伪代码，这里调用向量检索 return [] def cross_check(evidence: dict) -> str: # 调用另一个模型，独立判断反例是否成立 return "支持" # 或 "不支持" / "证据不足" def run_pipeline(assertion: str) -> dict: candidate = generate_counterexample(assertion) docs = search_kb(candidate["assertion"]) execution = execute_script(candidate["verification_code"]) model_opinion = cross_check(candidate) return { "candidate": candidate, "evidence_docs": docs, "execution": execution, "cross_check": model_opinion, "status": "verification_passed" if execution["stdout"] == candidate["expected_output"] else "verification_failed", } if __name__ == "__main__": print(json.dumps(run_pipeline("Python 浮点乘法满足结合律"), ensure_ascii=False, indent=2))这里要注意：不能把expected_output直接当作“应该正确”的基准，因为 LLM 可能在预期输出里写了错误答案。正确的逻辑是：执行结果需要和预期输出一致，且人工复核会进一步判断这个“一致”是否真的能证明断言失败。否则，LLM 只是“自己提出假设，自己验证假设”，并没有增加可信度。
3.3 用 RAG 和向量检索做资料核验
RAG（检索增强生成）在 LLM 应用中的一个重要作用，是从外部知识库中检索可靠资料，再把资料与原始问题一起交给模型。对于反例验证来说，RAG 可以用于检索浮点标准、数据库文档、并发模型说明等资料。
搭建一个反例验证知识库的常见步骤是：
- 收集资料，例如 IEEE 754 文档、Python 语言参考、数据库官方文档、论文摘要。
- 将文本切分成固定长度的块，建议 500 到 1000 字符。
- 使用 embedding 模型计算向量，存入向量数据库。
- 在验证时，用断言文本作为查询，取 TopK 相似度最高的文档。
下面是使用 Chroma 和 OpenAI 兼容 embedding 接口的示例，重点在于展示思路：
from langchain_community.vectorstores import Chroma from langchain_community.embeddings import OpenAIEmbeddings vectorstore = Chroma( collection_name="counterexample_library", embedding_function=OpenAIEmbeddings(), persist_directory="./kb", ) docs = vectorstore.similarity_search( "IEEE 754 float multiplication associativity overflow", k=3, ) for doc in docs: print(doc.page_content)如果遇到“文本向量 API 未配置”的报错，通常要检查四个地方：模型网关地址OPENAI_BASE_URL、密钥OPENAI_API_KEY、embedding 模型名，以及当前运行环境与网关之间是否有网络访问权限。报错信息中会有具体密钥名或模型名，根据提示调整即可。
需要明确，RAG 检索到的资料不能替代运行验证，但能做两件事：一是帮助人工理解反例涉及的领域背景，二是把 LLM 的“事实声明”和“公开文档”对齐，尽早发现明显矛盾。
3.4 用本地推理引擎交叉验证模型
如果刚才是用模型 A 生成反例，再用模型 A 来验证，很容易出现“自我确认偏差”。同一个模型倾向于延续自己已经生成的结论。因此，交叉验证应该使用不同来源的模型，例如不同的云服务、不同厂商的开源模型，或者本地推理引擎部署的模型。
部署本地模型时，工具选择比较丰富。在 Mac 上常用 Ollama 或 LM Studio 来跑中小尺寸模型；在资源受限的环境里，也可以使用量化模型。对于移动端场景，Maid LLM 等工具可以用来录入和检查反例，但它更适合做轻量复核，不适合做完整验证。
交叉验证的提示词也需要设计，不能直接问“这个反例对不对”，而要要求模型独立推导：
给定以下反例 JSON，请你忽略它是谁生成的，独立分析： 1. 反例中的数值是否会导致断言失败？ 2. 反例中涉及的领域知识是否准确？ 3. 如果让你构造一个反例，你会如何构造？ 4. 给出你自己的结论：支持、反对或证据不足。本地推理引擎的调用方式和 OpenAI 兼容接口类似：
ollama pull qwen2.5:7b ollama run qwen2.5:7b "请独立验证：给定反例 a=1e308, b=10, c=1e-308，计算 (a*b)*c 和 a*(b*c)，并判断是否推翻浮点乘法结合律。"交叉验证的价值在于暴露分歧。如果两个模型结论一致，并不能证明正确，但可信度会提高；如果两个模型结论不一致，说明反例的证据链还不够扎实，需要更多资料或运行实验。
3.5 输出验证报告并升级人工复核
验证流水线完成后，应该输出一份结构化报告。报告至少包含以下字段：
| 字段 | 含义 | 示例 |
|---|---|---|
| assertion | 原始待验证断言 | Python 浮点乘法满足结合律 |
| candidate | LLM 生成的反例 | {"a": 1e308, ...} |
| evidence | 检索到的资料摘要 | IEEE 754 文档片段 |
| execution_stdout | 验证代码实际输出 | inf 10.0 False |
| expected_output | LLM 给出的预期输出 | inf 10.0 False |
| cross_check | 其他模型结论 | 支持 |
| risk_level | 人工根据影响面判定 | 高风险 |
| conclusion | 最终人工结论 | 反例成立，需要修复断言 |
人工复核的价值不是再次判断专业细节，而是结合执行结果、检索资料和多模型结论，做最终决策。整个流水线的目的就是让人工从“判断一个陌生领域命题真假”的高难度任务，降级为“判断一段可执行证据链是否完整”的低难度任务。
4. 精度问题是常见的“专业外反例”来源
4.1 为什么 LLM 会提出与精度有关的反例
在 LLM 的训练语料中，浮点精度、整数溢出、舍入误差是非常多见的代码错误类型。这类问题天然容易形成反例，因为它们平时不会出现，只在极端数值下暴露。比如0.1 + 0.2 != 0.3这类案例几乎出现在每一本讲浮点误差的文章中，所以 LLM 很容易生成类似反例。
但问题也在于此。LLM 见过的浮点案例很多，它可能把不同案例的细节混淆。比如把“浮点加法不满足结合律”记成“浮点加法不满足交换律”，或者拿 CPU 指令扩展来解释并不存在的精度行为。因此，凡是 LLM 生成和精度有关的反例，都必须用实际运行结果来裁决，不能靠语料中的“常见答案”。
4.2 FP16、FP32、BF16 对比
在 LLM 训练和推理中，精度是一个绕不开的话题。FP16、FP32、BF16 都是常用的浮点格式，它们的差异经常被 LLM 用来构造反例。如果开发人员不清楚这些格式的区别，就会把模型量化问题当成业务 bug，或者反过来把真正由精度导致的问题归因到代码逻辑上。
下面是三种常见格式的对比，数值范围是近似值，实际以 IEEE 标准为准。
| 格式 | 位宽 | 指数位 | 尾数位 | 大致表示范围 | 精度特点 | 常见场景 |
|---|---|---|---|---|---|---|
| FP16 | 16 位 | 5 位 | 10 位 | 约 ±65504 | 精度低，大数容易溢出 | 部分训练加速、显存受限场景 |
| FP32 | 32 位 | 8 位 | 23 位 | 约 ±3.4e38 | 精度较高，通用计算标准 | 训练主精度、CPU/GPU 通用计算 |
| BF16 | 16 位 | 8 位 | 7 位 | 与 FP32 范围相近 | 精度低但范围大，不易溢出 | 大模型训练与推理，混合精度 |
从这张表可以看出，BF16 和 FP16 虽然都是 16 位，但设计思路完全不同。BF16 牺牲尾数位，保留了和 FP32 一样的指数位，因此在大模型中不容易溢出，但小数点后的精度很差。FP16 尾数位多一些，但在数值很大时容易溢出。
4.3 精度反例如何通过代码验证
回到前文的结合律反例。直接运行下面的 Python 代码，可以看到浮点乘法如何因为溢出而破坏结合律：
x = 1e308 y = 10.0 z = 1e-308 left = (x * y) * z right = x * (y * z) print("left:", left) print("right:", right) print("left == right:", left == right)在 CPython 3.11、x86-64 环境下，输出通常是：
left: inf right: 10.0 left == right: False这里的关键不是inf，而是left和right走了完全不同的计算路径。left先计算x * y，结果超过float64的最大值，得到无穷大；无穷大再乘任何非零数仍然是无穷大。right先计算y * z，得到一个很小的数1e-307，再乘1e308，回到10.0。同一个数学表达式，因为运算顺序不同，产生了不同的结果，这就是结合律失效的真实现象。
如果使用 FP16 格式，这个现象更加直观。Python 标准库没有内置float16，可以用 NumPy 模拟：
import numpy as np x = np.float16(65504.0) y = np.float16(2.0) print(x + y) # 运行时输出 inf，因为 FP16 范围上限约为 65504这个例子展示了“超出专业领域”的反例：很多开发人员都知道浮点有精度问题，但未必清楚 FP16 会在 65504 之后直接溢出。当 LLM 用这类格式差异构造反例时，最好的验证方式就是像这样的最小代码，而不是依赖记忆。
4.4 让 LLM 感知数值精度差异
在提示词设计上，可以直接要求 LLM 把数值计算交给代码执行环境，而不是让它自己输出最终结果。比如在系统提示中规定：
当你分析数值精度问题时，不要直接声称“结果会变成 inf”或“结果不相等”。 你必须生成一个可执行的 Python 或 NumPy 脚本，并说明脚本的预期输出。 最终结果以脚本执行结果为准。这样可以减少 LLM 在数值结果上的“编造空间”。LLM 无法在参数空间中完成精确的无穷大运算，但它可以生成正确的代码，让 CPU 或 GPU 完成实际计算。把“计算任务”和“文本生成任务”分离，是处理精度反例的一个重要原则。
5. 用知识库沉淀已验证的反例
5.1 从 LLM Wiki 范式借鉴验证知识管理
Andrej Karpathy 提出的 LLM Wiki 范式，核心思想是不要把知识硬编码在模型参数里，而是把知识放在外部 Wiki 中，让 LLM 基于 Wiki 内容进行检索和回答。这种范式对“反例库”同样适用。
一个已被验证过的反例，如果只存在于聊天记录里，下次遇到类似断言时，开发人员又要重新让 LLM 生成、重新运行验证，成本很高。更稳妥的做法是建立“反例 Wiki”，每一个反例对应一个页面，页面里记录断言、反例输入、验证代码、运行环境、验证日期和最终结论。
使用 Obsidian 这类 Markdown 工具管理反例卡片很合适，因为 Markdown 便于版本管理，Obsidian 的链接功能可以把相关反例关联起来。还可以通过插件或脚本把 Markdown 文档同步到向量库，供后续 RAG 检索。
5.2 搭建本地知识库的路径
搭建反例知识库不需要很复杂的架构。可以先按以下顺序推进：
- 用 Obsidian 建立一个
counterexamples目录，每个反例一个 Markdown 文件。 - 在每个文件中使用固定 frontmatter，记录断言、领域、验证状态、模型、日期。
- 使用 Python 脚本读取目录下的 Markdown 文件，切分文本，写入 Chroma 向量库。
- 在验证流水线中接入向量检索，用断言文本查询相关反例。
下面是一个简单的写入向量库的脚本示例：
from pathlib import Path from langchain_text_splitters import RecursiveCharacterTextSplitter from langchain_community.vectorstores import Chroma from langchain_community.embeddings import OpenAIEmbeddings text_splitter = RecursiveCharacterTextSplitter( chunk_size=800, chunk_overlap=100, ) documents = [] for md_file in Path("./counterexamples").glob("*.md"): content = md_file.read_text(encoding="utf-8") chunks = text_splitter.split_text(content) for chunk in chunks: documents.append(chunk) vectorstore = Chroma.from_texts( documents, embedding=OpenAIEmbeddings(), persist_directory="./kb", )向量库建成后，检索命中率会直接影响验证效率。文本切分过大会导致检索结果太泛，切分过小会导致上下文不完整。800 字符、100 字符重叠通常是一个可以接受的起点，实际项目需要根据资料类型调整。
5.3 ComfyUI extra_model_paths.yaml 配置示例
如果使用 ComfyUI 或其他模型管理平台来管理本地模型，可以通过extra_model_paths.yaml指定多个模型目录。这个配置常用于让推理服务识别到额外的模型路径，方便交叉验证时加载不同模型。
下面是一个示例结构，用于说明思路，实际字段需要根据所用平台版本确认：
my_models: base_path: /data/models checkpoints: checkpoints loras: loras
