夜雨聆风学习资料网

ARTICLE · 1112944

AI 提议,工具裁决:这个项目给 AI 幻觉上了道硬闸

AI 提议,工具裁决:这个项目给 AI 幻觉上了道硬闸

问一个 AI 模型「这个 Windows 系统文件的函数开头是什么指令」,它会非常自信地告诉你:教科书式的 push rbp ; mov rbp, rsp。

开发者对这个答案做了个实验:拿 71 个真实的 Windows 系统文件去验证,结果 69 个的答案都是错的——准确率 97% 的错误率。模型不是在分析,是在背课文。它见过太多教科书例子,就把「常见」当成了「事实」。

这个开发者随后做了 reverify(github.com/2akouwu/reverify,GitHub 搜索同名即可找到,PyPI 直接 pip install),一个把「AI 说的」和「实际是的」彻底分开的工具。核心理念用一句话讲:模型提议,确定性工具裁决。AI 可以提任何假设,但每一条都必须由确定性的工具去实际验证,验证不过就不算数——每条结论要么 VERIFIED、要么 REFUTED,都带着工具实际观察到的字节作为证据。

为什么「更好的模型」解决不了幻觉

市面上对付幻觉的主流思路是让模型更强:更多推理、更多引用、RAG 检索增强。这些都有用,但它们都在同一个框架里打转——模型自己验证自己。一个语言模型判断另一个语言模型的输出,本质还是概率判断,概率判断就有翻车率。

reverify 的思路反直觉:防幻觉靠的不是更聪明的模型,而是更笨的工具。笨到什么程度?笨到它是确定性的——同样输入永远同样输出,没有「我觉得」,只有「字节就在那里」。PE/ELF/Mach-O 解析、x86/x64/ARM/ARM64 反汇编、AOB 模式扫描、CPU 仿真,这套工具链是纯 Python 实现的确定性代码。模型说「offset 4096 处是 push、mov、sub 三条指令」?工具直接把那个位置的字节反汇编出来对答案,对得上就 VERIFIED,对不上就 REFUTED,裁决书里附上实际字节。

谁提议谁验证彻底分离,这才是它能做到「0 条错误结论被放过」的根子。

97% 错误率是怎么测出来的

这个数字值得展开讲,因为它不是营销数字,是可复现的实验。

模型的「先验」很顽固:问它函数开头,它答教科书式的帧指针开场。benchmark 就把这个先验盲测到真实二进制上——不读反汇编,直接假设模型会说 push rbp,然后拿 reverify 去验证这个假设。在 71 个 Windows 系统文件上:

  • 先验错误率(=模型的幻觉率):69/71,97%
  • 错误结论被 VERIFIED(安全指标,必须为 0):0 次
  • 一轮反馈后得到真实字节:71/71,100%

两个细节说明这不是 rigged 的测试:那 71 个文件里有 2 个真的以 push rbp 开头,工具正确地 VERIFIED 了它们——先验偶尔也是对的,工具不冤枉好人。整个 benchmark 在 CI 里每次 push 都跑,任何一个错误结论被 VERIFIED 都会让构建直接失败。验证器本身也被独立的裁判检验:解析器对 lief、反汇编器对 capstone 和 objdump、仿真器对 Unicorn,外加每日 2 万个畸形输入的 fuzzing,确保「错误的说法永远不会被放行」这件事本身就是被验证过的。

每条裁决还带「小票」:二进制的 SHA-256、工具版本、用了哪些引擎。报告可以交给第三方重放,不用信任何人的嘴。

不只管逆向:你改的代码也能「测过才算」

这个项目最让我意外的是它没有把自己锁死在二进制逆向这个最难的场景里。reverify equiv 命令把同一套 rigor 对准了普通源码:给一个参考实现和一个 AI 重写后的候选实现,跑同一组输入,逐个比对输出。AI 说的「我这次重构保持了行为一致」不算数,跑出来一致才算一致——不一致的时候,裁决结果里带着当时的输入和双方的输出,你直接就能看到它在哪一步分道扬镳。

这对用 AI 编程的人是个很实在的东西。现在大家都遇到过「修一个坏一个」:AI 声称改好了,你跑一遍才知道又碰坏了别的。equiv 就是把「跑一遍」自动化成裁决环节,变成开发工作流的内置步骤,而不是你手动兜底。

两件配套的事:账本和滚动交接

工具光会裁决还不够,reverify 在 agent 工作流上还做了两个设计,恰好踩中长任务的两大痛点。

验证账本(ledger)。 每个二进制一份 JSON 账本,按内容哈希做键(改个文件名账本还在),每轮验证后落盘。关键在「负记忆」:被否决的假设记成 KNOWN FALSE,新开的会话不会把同一个错误假设再提一遍——这恰恰是普通会话摘要最先丢掉的信息。上下文重置、崩掉、换进程,都能从账本原地满血复活,而且复活的全是验证过的事实。

滚动交接(rollover)。 长任务跑着跑着上下文满了,现有 agent 的处理方式是模型自己总结一遍接着跑——总结就是有损压缩,压几次精度就垮。reverify 的做法是让模型主动请求 rollover:开全新会话,新会话的开局不是模型写的总结,而是账本里的事实清单加一份有界的交接说明。事实部分(已确认的、已知为假的)直接从账本来,模型自己的判断和笔记打上「未验证」的标签跟着走。幻觉没法搭着交接的便车混进下一个上下文。它还有个 drift 检测:如果最近几轮模型都在复读已经确认过的东西,说明在原地打转,自动触发 fresh start。

CHANGELOG 里那个细节我印象很深:有个用户反馈交接收据显示正常但会话实际涨到了 90 万 token——doctor 子命令后来专门加了对这种「交接没人消费」情况的检测。这种把自家机制当攻击面来审计的写法,在个人项目里不多见。

用起来是什么样

三种形态:CLI 工具、MCP server、Python 库。装法两档:

  • pip install reverify——纯 Python 核心,零编译依赖,开箱即用
  • pip install "reverify[full]"——升级到 capstone(反汇编)、unicorn(CPU 仿真)、lief(二进制解析)、Z3(定理证明),还有 [angr] 可选装函数边界和调用图分析

没装引擎也能跑,核心实现是自带的纯 Python 版本,性能差些但功能等价。reverify backends 随时查当前激活的是哪套。

MCP 这条线对用 Claude Code、Cursor 的人最省事:配置成 MCP server 之后,agent 调 re_verify_claim 提交假设、拿回带证据的裁决,re_ledger 在上下文被清空后恢复事实清单。MIT 协议,Python 3.8+ 就能跑。

冷静说边界

它的验证域是「可确定性验证的东西」。 二进制结构、指令序列、代码等价性——这些有 ground truth 可查。但「这个需求的实现方案合不合理」「这段文案写得好不好」,没有确定性工具能裁决,reverify 帮不上。它是给事实性工作上的闸,不是给判断性工作。

逆向场景需要授权。 README 和 SECURITY.md 写得明白:恶意软件分析、CTF、互操作研究、自有软件分析,这些是目标场景。拿它去碰没有授权的软件,工具再好也改变不了性质。

项目很年轻。 我看代码的时候是 0.11.0 版本,2026 年 9 月 7 日还在提交。迭代快意味着 API 会动,今天写的集成代码可能下个版本就要改。好处是它有独立的 OpenSSF Scorecard 评级、CI 全平台跑 benchmark、SLSA 构建溯源——工程纪律在同龄项目里算严的。

维护者是个人开发者。 看仓库的提交节奏是单人在推,bus factor 为 1。不过 MIT 协议加「验证器被独立裁判检验」的设计,就算项目停了,这套方法论已经写在代码里了。

我的态度

这个项目真正值得记的不是某个功能,是那个立场:在 AI 输出和「事实」之间,放一个不服从模型的确定性裁判。幻觉问题的终点可能真的不是更强的模型,而是一套足够笨、足够硬的验证工具。

Claude Code 和 Cursor 重度用户建议直接把 MCP server 配上——成本是几分钟配置,收益是从此你的 agent 说每句「事实」之前都得先过闸。

项目地址:github.com/2akouwu/reverify(GitHub 搜索 reverify 即可),PyPI 包名就是 reverify。

你被 AI 幻觉坑过最狠的一次是什么?有什么想法可以随时留言沟通。

喜欢就先收藏,万一找不到了呢!⭐

相关学习资料