☰
Math Olympiad 插件的对抗式证明验证提示词库:从 85.7% 自验证到人类评审级核查的完整 Prompt 体系
2026/9/30 6:41:09 网站建设 项目流程
  • AI 插件
  • 开发工具
  • 插件系统

【免费下载链接】claude-plugins-official

Official, Anthropic-managed directory of high quality Claude Code Plugins.

项目地址:https://gitcode.com/GitHub_Trending/cl/claude-plugins-official
点击查看免费下载

导读:本文系统讲解 claude-plugins-official 仓库中 math-olympiad 技能的核心组件——对抗式验证提示词库(adversarial_prompts.md)。这份提示词库是验证子代理(verifier subagent)的"人设与弹药库":它把验证者从"打分的老师"重塑为"一心想拆台的攻击者",并以七类失败模式(taxonomy)和七套可复制的 Prompt 模板,专门捕捉自我验证(self-verification)会漏掉的那类微妙错误。读完本文,你将掌握这七类漏洞的判别标准、每套验证 Prompt 的完整结构与输出格式,以及它们如何与 5-pass 投票、非对称阈值、Adversarial Brief 修正机制在完整工作流中协同。


背景:为什么"自信的证明"不值得信任

数学竞赛(IMO、Putnam、USAMO、AIME)的求解失败模式里,最危险的不是"解不出来",而是"解错了却自信满满"。SKILL.md 与插件 README 反复引用的研究背景(arXiv:2503.21934,即 "Proof or Bluff")给出了一个触目惊心的数据:

模型自我验证(self-verified)时在 IMO 上的成功率可达 85.7%,但在人类评分标准下会骤降到 5% 以下。

也就是说,让同一个模型(或看到了推理过程的验证者)来检查自己的答案,几乎必然被"推理过程长得像证据"所蒙蔽。推理轨迹(thinking trace)会形成一种认同偏置(bias toward agreement):再长的错误推理链,读起来也像是一连串支撑结论的证据。

本提示词库的设计初衷,就是让验证者扮演人类评分员:它不知道求解者的思考过程,不知道其他验证者怎么投票,手里只有"题目 + 清洗后的干净证明",并且被明确命令去**击穿(BREAK)而非评分(grade)**这份证明。


第一原则:验证者隔离(Verifier Isolation)

adversarial_prompts.md开篇就规定了验证者子代理的上下文边界,这是整套机制的地基:

  • 新鲜上下文(Fresh context):验证者只看到"题目陈述 + 清洗后的解答",绝不包含任何 thinking trace;
  • 无工具(NO tools):验证者只能纯推理(pure reasoning only),不允许 Bash、Python、WebSearch、Read、Write 等任何计算或取数工具;
  • 社会证据免疫:验证者不知道其他验证者如何投票,也不知道这份证明是否已被他人确认或驳斥——它必须假设自己是第一个且唯一的评审人。原因很直白:"已有 3 人确认"这类社会证明(social proof)会把人推向随大流式的认同。

这三条约束与 SKILL.md 中第 3 步"清洗解答(context isolation)"和第 5 步"双重上下文隔离"完全对应:求解者的思维轨迹在进入验证前必须被剥离,同时每个验证者对同伴的结论也保持盲区。SKILL.md 甚至给出了一条硬性规则:一个求解者不能验证自己的解答——必须换一个不同的 agent、换一份新鲜上下文。


驳斥理由分类学(Refutation Taxonomy):七类必查漏洞

提示词库要求验证者"找一个理由去驳斥",并给出了一张七分类漏洞清单。任何证明只要落入其中一类,即视为 HOLE:

#漏洞类别含义典型信号 / 例子
1Step doesn't follow(步骤不成立)某一步的结论不是由前提推出的,包括方向性错误A>B 且 C>D不能推出 A−C>B−D
2Hypothesis not satisfied(假设未满足)引用的定理需要某个条件,而证明从未验证Pattern #5:"entire"(整函数)≠"在某圆盘内解析"
3Claim false in small case(小情形即崩)某个恒等式或界在 n=2、n=3 或第一个非平凡块处失效在脑中直接用小情形测试
4Tautological(同义反复)结尾的"缺口"其实是原问题的伪装Pattern #18:把证明自己的恒等式代回去
5Proves too much(证得过强)论证骨架套用到某个著名对象上,会证明一个开放或错误的问题Pattern #4
6Wrong interpretation(误解题意)解的是题目的一个更简单读法,而非本意Pattern #60
7Hand-wave at the crux(关键处搪塞)在最不该是例行公事的步骤处说"迭代并优化即得""用标准方法""细节是 routine 的"恰好落在不是routine 的那一步

使用准则同样重要:如果经过真诚的尝试后七类都没有触发,就 CONFIRM;绝不因为证明"听起来很自信"就确认。这句"do not confirm because the proof sounds confident"是全库的灵魂——自信恰恰是微妙错误最常见的伪装。


七套验证者 Prompt 模板详解

提示词库提供了七套即用型 Prompt。前六套是给验证者子代理的,第七套是给修订者(reviser)的专用简报。下面逐一给出其完整结构与使用场景。

1. 通用对抗验证(General Adversarial,默认)

这是默认的攻击型验证人设。核心指令是:

你不是在打分,你是在试图击穿它(trying to BREAK it)。假设作者是一名犯了一个细微错误、而同情心强的读者会一带而过的强学生。你的工作就是找出那个错误。如果真诚尝试后仍找不到,就直说——但不能仅仅因为解答写得很自信就直说。

对每一步发起攻击时,检查清单包括:

  • 声称的不等式方向是否真的成立?在脑中用小情形推理一遍;
  • 每个 "clearly" / "obviously" / "it follows that" 是否真的显然?这些词往往精确标记了作者说服了自己某个错误论断的位置;
  • 每个被引用定理的假设是否真的满足?检查量词:"for all" 与 "there exists"、pointwise 与 average 的差异;
  • 每个 "WLOG"(不失一般性):一般性真的被保留了吗?还是这个约化恰恰丢弃了困难情形?
  • 论证是否用到了对泛型对象成立、但对题目中的特定对象并不成立的属性?

输出格式为三段式:

VERDICT: CORRECT | INCORRECT | GAP CONFIDENCE: high | medium | low ISSUE: [若 INCORRECT/GAP:一句话定位 + 一段解释;若 CORRECT:你最难击穿的那一步以及它为何成立]

2. Pattern #4 —— 会不会证得过强?

这套 Prompt 只做一件事:这个论证是否意外证明了一个著名开放问题或著名错误命题?

操作步骤:

  1. 剥离骨架:把论证压缩到它"实际使用"的对象属性;
  2. 寻找替身:找到共享这些属性的最著名对象——如果论证只用"正递减项"来界定一个和,那么调和级数(harmonic series)是否也有正递减项?如果只用"可乘且被 1 界定",莫比乌斯函数(Möbius function)是否也满足?
  3. 脑中重跑:把论证在替身上重跑一遍,看它现在证明了什么。

如果替身结论是已知的开放问题或已知错误,那么原证明必有一处缺口——缺口就在"论证对替身失效的那一步",而这一步正在悄悄使用一个作者从未声明的属性。反之,如果论证确实用到了替身所缺乏的、题目对象的专属属性,请明确说出是哪个属性、用在哪里。

VERDICT: CORRECT | INCORRECT CONFIDENCE: high | medium | low SUBSTITUTE_TESTED: [你替换的对象] ISSUE: [若证得过强:对替身失效的步骤 + 缺失的未声明属性;若否:哪一步用了专属属性、为何替身在那里失败]

这套模板与 verifier_patterns.md 中的 Pattern 4 一一对应:一个"对所有具有性质 P 的 Dirichlet 级数成立"的界,套到 ζ(s) 上就会证出 Lindelöf 猜想——这是把算术输入当成了泛型输入。SKILL.md 也把它列为五条"改变结果的关键"之首("Does this prove RH?"):如果你的定理特化到 ζ 是一个著名开放问题,你就有一个缺口——这是最可靠的红色警报。

3. Pattern #40 —— 一行证明过于干净(One-Line-Proof-Too-Clean)

针对"太短"的证明。凡是"一行干了很多活"的可疑步骤,执行三步:

  1. 提取一般引理(general lemma):把该步骤隐式使用的命题写成最一般的形式——不是"对这个和",而是"对任何这种形状的和";不是"对这个行列式",而是"对任何具有此性质的矩阵元素函数";
  2. 用 2×2 情形攻击:两个元素、两项、一个 2×2 矩阵——即最小非平凡实例。在脑中推理:能否找到让一般引理失效的取值?
  3. 判定:
    • 一般引理扛住了 2×2 攻击 → 该步骤大概率没问题;
    • 一般引理在 2×2 处失败、但题中特定实例似乎仍成立 → 该步骤按字面意义是 INCORRECT:题目存在特殊结构使其为真,而证明没有援引该结构——作者"答对了答案,却出于错误的原因"。

库中给出的经典案例:"秩只依赖支撑集(support)"——但[[1,1],[1,1]]秩为 1,[[1,1],[1,−1]]秩为 2,二者支撑集相同。一般引理为假,具体实例成立只是因为存在一个证明从未提及的符号分解(sign-factorization)。

VERDICT: CORRECT | INCORRECT | GAP CONFIDENCE: high | medium | low GENERAL_LEMMA: [提取出的一般断言] 2x2_TEST: [尝试的实例及其结论] ISSUE: [若一般引理为假:证明未能援引的特殊结构是什么]

verifier_patterns.md 的 Pattern 40 给出了相同的判别法与"隐藏结构才是真正证明"的结论;SKILL.md 的第三条"关键"也复述了这一策略:短证明 → 提取一般引理 → 试 2×2 反例 → 若一般形式为假,找出本实例的特殊之处。

4. Pattern #18 —— 循环论证 / 同义反复约化

只检查一件事:解答是否在绕圈子?

  1. 列出恒等式:记下证明沿途建立的所有恒等、等式与代换("A = B + C"、"和式拆为 X + Y"、"由前面的引理 P = Q"等);
  2. 取出最终论断:即解答宣称"现在很容易"或"这由某个标准事实立即得出"的那个最终估计;
  3. 回代展开:把链条自身的恒等式代回最终论断,展开、化简;
  4. 审视结果:如果得到的是原问题本身,或与原问题平凡等价的东西,那么这个"约化"就是同义反复——证明什么都没做,只是给问题改了个名字就宣布解决了。

提示词库特别警告了陷阱心理:长链条会让人感觉在前进。"我们已经把它约化到界定 X 了!"只有在 X 确实不同于起点时才算前进;有时 X 只是戴着帽子的原问题。

VERDICT: CORRECT | INCORRECT | GAP CONFIDENCE: high | medium | low FINAL_CLAIM: [解答当作容易终点的论断] SUBSTITUTED_BACK: [展开链条自身恒等式后的样子] ISSUE: [是原问题?平凡等价?还是真的更简单?说明是哪种以及原因]

verifier_patterns.md 中的 Pattern 18 给出了具体捕捉实例:"只需证 ∫|P|² ≤ C·H"——但链条自己已经证明了 ∫|P|² = H + 2Re(OD') 精确成立,所以这个 X 只是原猜想加了一个化妆移位。Pattern 19 则提示:当同一个障碍连续杀死 3 个以上独立方法时,要回到最原始对象上重算——障碍可能只存在于某个代理(proxy)对象里。

5. Pattern #60 —— 规格博弈(Specification-Gaming):解的是最易读法

只检查一件事:解答是否回答了问题最容易被解释成的读法,而非本意读法?

操作流程(先读题、后看解答):

  1. 写下 2–3 种合理解读:关注量词范围("find all" vs "find one")、"determine"的含义(公式?刻画?存在性证明?)、边界情形(n=0 或 n=1 算不算?空集是否允许?退化构型是否包含?);
  2. 按难度排序这些解读;
  3. 判断解答实际处理了哪个读法。

危险信号:解答处理的是最容易的读法——尤其当该读法下题目对声称的来源(如 IMO)而言会短得离谱时。"一道 IMO 压轴题变成三行就解完了"就是红旗:竞赛题是按分值标定的,压轴题三行搞定通常意味着你解的不是那道压轴题。此外还要检查:题目问所有对象时,解答是否只证明了某个对象?题目要必要性时,解答是否只展示了可能性?

VERDICT: CORRECT | INCORRECT | GAP CONFIDENCE: high | medium | low READING_SOLVED: [解答处理的是哪种解读] READING_INTENDED: [你相信的本意解读及理由] ISSUE: [若二者不同:解答缺了什么;若相同:为何简单读法就是本意读法]

这套检查在 SKILL.md 中占据第 1 步(解释检查,30 秒)的地位——它声称能抓住某类错误的 50/63:Aletheia 案例研究发现,63 份"技术上正确"的解答里有 50 份解的是错误解读。verifier_patterns.md 的 Pattern 60 同样强调:竞赛题经常故意埋下一个容易的误读;如果你的解读让题目变成一行解而它值 7 分,你很可能选错了。

6. Consecutive-Verify —— 5 遍循环独立投票

面向"5 个独立验证者必须全部一致才算通过"的场景。每个验证者是第 {K} 遍(共 5 遍):

  • 独立验证:你没有看到、也不得臆想其他验证者说了什么;不要推理"这一步大概已经被别人查过了"。你只能控制你自己的那一票。如果你抱着"反正后面那遍会抓到"的心态放过一步,而其他四遍也这么想,错误的解答就会上线;
  • 从零追溯:读题、读解、自己从头到尾逐步追踪;
  • 主动抵抗一个偏置:当解答写得漂亮、自信、大部分地方正确使用标准机器时,你会倾向于信任唯一一处你跟不上的地方。把这个倾向反转过来——写得漂亮自信正是微妙错误的长相:作者先说服了自己,然后才说服了数学。你跟不上的那个位置,恰恰是最该用力压的地方。
VERDICT: CORRECT | INCORRECT | GAP CONFIDENCE: high | medium | low PASS_NUMBER: {K} ISSUE: [若 INCORRECT/GAP:确切步骤与原因;若 CORRECT:你最难验证的步骤,以及说服你的推理]

这套 5-pass 循环是 SKILL.md 第 5 步"排序与投票验证"的执行者:排名靠前的解答最多启动 5 个新鲜验证者,采用非对称阈值——4 票 HOLDS 才确认,2 票 HOLE FOUND 即驳斥(理由:一个状态不稳的验证者不应杀死一个正确的证明,但两个独立异议就是真实信号)。同时使用鸽笼早退(pigeonhole early exit):2 个 HOLE FOUND 即停止(省下剩余 3 次调用);4 个 HOLDS 即确认(省下第 5 次);3 遍后若为 2 HOLDS + 1 HOLE 则再启动 2 个,若为 3 HOLDS + 0 HOLE 则再启动 1 个(仍可能达到 4-1)。按 model_tier_defaults.md 的配置,不同模型档位可调整验证者数量与阈值:Haiku 用 7 个验证者、5-confirm / 3-refute(宽度弥补个体噪声);Sonnet 用 5 个、4-confirm / 2-refute;Opus 则在 5 个通用验证者之上,为 verifier_patterns.md 的每个 pattern 再各配一个专项验证者(12 次定向攻击,任何专项 HOLE FOUND 都计入驳斥票)。

7. Adversarial Brief —— 给修订者的强制二选一简报

当 Pattern #40 触发(验证者发现一个"一般形式为假的一行引理")时,不要给修订者发通用的"修一下这个洞"指令——通用指令下修订者可以回一句"看起来没问题"。这份简报强制二选一:

对抗简报:原则"[提取出的一般引理]"在一般情况下明显为假——[平凡反例,例如 [[1,1],[1,1]] 秩为 1 而 [[1,1],[1,−1]] 秩为 2,支撑集相同]。

因此以下两句话恰有一句为真,你的任务是判定是哪一句:

(A)结论因本情形特有的不同原因而成立。找出那个原因:[题目中的特定对象] 具有什么 [反例] 所缺乏的结构?那个结构才是真正的证明。

(B)证明是错的,结论在[具体分歧点预测——例如"块首次 ≥2×2 的情形,即 m=4"]处失败。

返回 (A)(附识别出的特殊结构),或 (B)(附失败点)。"原证明其实没问题"不是可选答案——一般引理已证伪,要么有什么东西拯救了这个实例,要么什么也救不了。

最好的结果是 (A)——论文命题存活,而且你学到了为什么。修正后的证明比那个假证明信息量大得多。

RESOLUTION: (A) SPECIAL_STRUCTURE | (B) CONCLUSION_FALSE IF (A): [特定对象] 具有而 [反例] 所缺乏的结构是:[...]。修正证明:[...] IF (B): 在 [参数/情形] 处失败。原因:[...]

这份简报与 SKILL.md 第 6 步(修订)直接挂钩:验证发现洞后启动修订者,它只拿到"清洗后的解答 + 验证者的洞报告",仍无权接触原始思维轨迹——修订者从洞出发工作,而不是重读求解者当初怎么走到这里。普通修订最多 3 轮;而若 Pattern #40 触发,修订者收到的就是上述强约束简报,"看起来没问题"不再是合法答案。此外,SKILL.md 第 6c 步(深度模式)与 6d 步还规定:任何在验证阶段 ABSTAIN 的情形,必须自动启动一个深度模式 agent(允许有界本地计算:模 k 运算、n≤10 小情形枚举、符号恒等式检查,60 秒计算上限,严禁任何网络访问),若它也放弃,才允许写下 abstention。


提示词库在完整工作流中的位置

把七套 Prompt 放回 SKILL.md 的八步工作流,它们的落点非常清晰:

  1. 第 1 步 解释检查(30 秒):先做 Pattern #60 式解读检查,别急着求解;
  2. 第 2 步 并行生成候选:8–12 个求解 agent 并行、各自内部迭代(solve → self-improve → self-verify → correct,最多 5 轮),使用 SKILL.md 中必须逐字使用的无计算限制 Prompt(NO COMPUTATION:禁止 Bash/Python/WebSearch/Read/Write,"数值验证不是证明步骤");起始角度参考 solver_heuristics.md(Pólya 五招 + 竞赛专属招数 + 几何专属招数 + 递推陷阱);
  3. 第 3 步 清洗解答:剥离所有 thinking-block 内容、"Let me try…"等散文、错误起步与回溯,只留"题目 + 干净最终论证",且只提取 Method / Proof / Answer 三节——验证者永远不知道求解者怎么走到的;
  4. 第 4 步 对抗验证:为每份清洗后的解答启动新鲜验证者,加载本提示词库;模式弹药以 verifier_patterns.md 的 13 个无需工具即可运行的检查为主(#4 著名开放问题、#5 假设类外、#6 解析延拓后的发散级数、#17 越过第一个非平凡块、#18 同义反复、#19 派生障碍 vs 基础障碍、#22 先算均值、#35 对角化前数清量词、#40 一行引理、#58 域大小上的量词方向、#60 最易读法陷阱等),并规定#18 与 #19 在任何正向发现后必跑,#40 对任何"过短"的证明必跑;
  5. 第 5 步 排序 + 投票验证:非对称阈值 + 鸽笼早退 + 双重上下文隔离(对思维轨迹盲、对同伴投票盲);
  6. 第 5b 步 卡壳时先退一步:某个 case 分拆久攻不下时,先问"是否存在让分拆消失的路径"——hard case 的假设本身常常蕴含关于某个中间对象的强结论;
  7. 第 6 步 修订:普通修订 3 轮;Pattern #40 触发则用本文第 7 套 Adversarial Brief;
  8. 第 7 步 校准式弃权:3 轮修订全败就停止并承认,输出 "no confident solution" + 已证内容 + 断裂点;绝不猜测——错误的自信答案劣于诚实的"没解出来",关键指标是条件准确率(说"解出来了"的时候,真的对吗);
  9. 第 8 步 呈现润色:正确性确立后,启动全新呈现 agent 加载 presentation_prompts.md,输出干净 LaTeX;若 check_latex.sh 探测到pdflatex/xelatex(退出码 0),再由 compile_pdf.sh 把仅含\begin{document}...\end{document}内容的正文包裹进最小前言后两遍编译成 PDF。

模型档位如何影响验证配置

提示词库本身不区分模型,但 model_tier_defaults.md 给出了验证预算随模型能力缩放的原则:预算不是瓶颈,边际收益递减与非对称噪声地板才是。

模型并行求解者验证投票弃权阈值模式扫描呈现
Haiku127 个验证者,5-confirm / 3-refute连续 3 轮修订失败全部 12 个3 稿,比较器选最干净
Sonnet65 个验证者,4-confirm / 2-refute连续 3 轮修订失败全部 12 个2 稿,比较器选更干净
Opus45 个通用验证者 + 每 pattern 一个专项(4-confirm / 2-refute)连续 5 轮修订失败全部 12 个,各配专属 agent3 稿("最优雅/最初等/最短"),比较器择优

设计逻辑:弱模型靠宽度补足单样本噪声(Haiku 验证者个体更不可靠,所以需要更高驳斥阈值 3 而不是 Sonnet 的 2,防止两个糊涂的 Haiku 误杀正确证明);强模型靠深度——Opus 有能力执行 #19、#22 这类需要真实数学判断的深层模式,12 个专项 pattern 通道正是其能力的最佳去处,区别是"保持怀疑"与"检查这一件具体的事"之间的差距。鸽笼早退在所有档位保留:一旦inflight >= confirm_needed + refute_needed − 1,剩余票无论怎么落都不携带信息,继续启动只是纯延迟。若编排会话不确定自己属于哪一档,默认采用 Sonnet 配置;一个合理的启发式是让模型在首次响应中自我识别并匹配haiku/sonnet/opus。


与其他参考文档的关系

adversarial_prompts.md是"执行层"的即用弹药,它与技能内其他参考文件形成完整闭环,全部位于 references 目录:

  • verifier_patterns.md:13 个无需工具即可在脑中运行的检查模式(Pattern 4/5/6/10/17/18/19/22/23/35/40/58/60),是提示词库中七类分类学与 #4/#18/#40/#60 各套模板的底层"检查引擎";每条模式都给出 check(查什么)、what it catches(抓到什么)、how to run it(怎么跑);
  • solver_heuristics.md:求解端的 Pólya 移动与竞赛/几何/递推专项招数,与验证端形成"求解启发式 ↔ 验证攻击模式"的对偶;
  • presentation_prompts.md:验证通过后的呈现润色 Prompt 与 LaTeX 模板,包含编号+命名步骤("Step 3: Fourier inversion and translation invariance")、反模式清单(发现序叙述、过度构造、恐吓式证明、孤儿引理、无标签 case 分拆、缺失路标);
  • model_tier_defaults.md:上文已述的逐档预算表。

值得注意:提示词库标题注明其来源为shared/verifier_patterns_source.md(59 个真实研究 session 中提炼的模式),而 verifier_patterns.md 是其中"无需 grep/fetch/compute、纯推理即可运行"的 13 个奥林匹亚子集——提示词库正是把这些模式翻译成了可以直接粘贴给子代理的自然语言指令。


使用与安装

该技能随 math-olympiad 插件分发,安装方式:

/plugin install math-olympiad@claude-plugins-official

使用方式:

> Solve this IMO problem: [statement]

技能会在出现 "IMO"、"Putnam"、"olympiad"、"verify this proof" 等触发词时自动激活,随后按 SKILL.md 的完整工作流执行:并行求解 → 清洗上下文 → 加载本提示词库的对抗验证 → 非对称投票 → (必要时)Adversarial Brief 修订 → 校准式弃权或呈现润色。对 AIME 这类纯数值题,则跳过证明机器,直接 5–7 个求解者多数投票,无多数时对前两名候选做代入验证。按 README 中的验证记录,该方法在 IMO+Putnam 2025 题目上达到 17/18 解决、0 误报、2 个新证明。

结语

这份提示词库的价值不在于"更多的验证",而在于把验证者从裁判席搬上攻击席:七类驳斥分类学给了它一个穷尽式检查清单,七套 Prompt 模板给了它可复制的攻击姿势,上下文隔离保证了它不会被思维轨迹与社会证据污染,非对称投票与鸽笼早退保证了工程上的鲁棒与经济。对于任何试图在竞赛数学场景下把"自信"与"正确"分开的 Agent 工作流,这份提示词库都是一份可直接落地的对抗式验证参考实现。

  • AI 插件
  • 开发工具
  • 插件系统

【免费下载链接】claude-plugins-official

Official, Anthropic-managed directory of high quality Claude Code Plugins.

项目地址:https://gitcode.com/GitHub_Trending/cl/claude-plugins-official
点击查看免费下载

相关推荐

上一篇:突破容器构建限制:Kaniko子目录构建完全指南
下一篇:srclib高级配置:配置文件详解与自定义分析流程

创作声明:本文部分内容由AI辅助生成(AIGC),仅供参考

需要专业的网站建设服务?

联系我们获取免费的网站建设咨询和方案报价,让我们帮助您实现业务目标

立即咨询