在一次代码评审中我让 LLM 对一个看似理所当然的断言找反例Python 里的浮点乘法是否满足结合律。LLM 很快给出一个反例取x 1e308y 10.0z 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.10.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: x1e308;y10.0;z1e-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_outputTrue, textTrue, timeout30, ) 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_asciiFalse, indent2))这里要注意不能把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_namecounterexample_library, embedding_functionOpenAIEmbeddings(), persist_directory./kb, ) docs vectorstore.similarity_search( IEEE 754 float multiplication associativity overflow, k3, ) 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 请独立验证给定反例 a1e308, b10, c1e-308计算 (a*b)*c 和 a*(b*c)并判断是否推翻浮点乘法结合律。交叉验证的价值在于暴露分歧。如果两个模型结论一致并不能证明正确但可信度会提高如果两个模型结论不一致说明反例的证据链还不够扎实需要更多资料或运行实验。3.5 输出验证报告并升级人工复核验证流水线完成后应该输出一份结构化报告。报告至少包含以下字段字段含义示例assertion原始待验证断言Python 浮点乘法满足结合律candidateLLM 生成的反例{a: 1e308, ...}evidence检索到的资料摘要IEEE 754 文档片段execution_stdout验证代码实际输出inf 10.0 Falseexpected_outputLLM 给出的预期输出inf 10.0 Falsecross_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 标准为准。格式位宽指数位尾数位大致表示范围精度特点常见场景FP1616 位5 位10 位约 ±65504精度低大数容易溢出部分训练加速、显存受限场景FP3232 位8 位23 位约 ±3.4e38精度较高通用计算标准训练主精度、CPU/GPU 通用计算BF1616 位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_size800, chunk_overlap100, ) documents [] for md_file in Path(./counterexamples).glob(*.md): content md_file.read_text(encodingutf-8) chunks text_splitter.split_text(content) for chunk in chunks: documents.append(chunk) vectorstore Chroma.from_texts( documents, embeddingOpenAIEmbeddings(), 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 LLM生成的反例如何验证？从浮点数精度到可执行证据链
在一次代码评审中我让 LLM 对一个看似理所当然的断言找反例Python 里的浮点乘法是否满足结合律。LLM 很快给出一个反例取x 1e308y 10.0z 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.10.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: x1e308;y10.0;z1e-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_outputTrue, textTrue, timeout30, ) 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_asciiFalse, indent2))这里要注意不能把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_namecounterexample_library, embedding_functionOpenAIEmbeddings(), persist_directory./kb, ) docs vectorstore.similarity_search( IEEE 754 float multiplication associativity overflow, k3, ) 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 请独立验证给定反例 a1e308, b10, c1e-308计算 (a*b)*c 和 a*(b*c)并判断是否推翻浮点乘法结合律。交叉验证的价值在于暴露分歧。如果两个模型结论一致并不能证明正确但可信度会提高如果两个模型结论不一致说明反例的证据链还不够扎实需要更多资料或运行实验。3.5 输出验证报告并升级人工复核验证流水线完成后应该输出一份结构化报告。报告至少包含以下字段字段含义示例assertion原始待验证断言Python 浮点乘法满足结合律candidateLLM 生成的反例{a: 1e308, ...}evidence检索到的资料摘要IEEE 754 文档片段execution_stdout验证代码实际输出inf 10.0 Falseexpected_outputLLM 给出的预期输出inf 10.0 Falsecross_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 标准为准。格式位宽指数位尾数位大致表示范围精度特点常见场景FP1616 位5 位10 位约 ±65504精度低大数容易溢出部分训练加速、显存受限场景FP3232 位8 位23 位约 ±3.4e38精度较高通用计算标准训练主精度、CPU/GPU 通用计算BF1616 位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_size800, chunk_overlap100, ) documents [] for md_file in Path(./counterexamples).glob(*.md): content md_file.read_text(encodingutf-8) chunks text_splitter.split_text(content) for chunk in chunks: documents.append(chunk) vectorstore Chroma.from_texts( documents, embeddingOpenAIEmbeddings(), 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