Claude Code math-olympiad 插件实战:面向 IMO/Putnam 的对抗式验证解题工作流

原创2026-09-30 13:52:54467 阅读
文章标签:AI 插件开发工具插件系统

Claude Code math-olympiad 插件实战:面向 IMO/Putnam 的对抗式验证解题工作流

本篇技术指南围绕 claude-plugins-official 仓库中的 math-olympiad 插件 展开,讲解其核心设计——"上下文隔离 + 模式武装的对抗式验证"——如何在 IMO、Putnam、USAMO、AIME 等竞赛数学问题上对抗"自我验证被欺骗"这一已知缺陷,并完整还原安装、触发、八步工作流、模型分档参数与 LaTeX 呈现的全过程。读完本文,你将掌握一套可复制的"解 → 清洗 → 对抗验证 → 投票 → 修订 → 呈现"流水线,并理解为什么 17/18 的 2025 IMO+Putnam 题目可通过、0 误报。

为什么竞赛数学需要"对抗式验证"而不是"自我验证"

插件 README 开门见山点出问题:自我验证(self-verification)会被欺骗。一个能看到完整推理过程的验证器天然偏向"认同"——推理链条越长,看起来越像支撑证据,即使结论是错的。README 引用的 arXiv:2503.21934("Proof or Bluff")给出了残酷的对照数据:自我验证下 85.7% 的 IMO 成功率,在人类阅卷下跌至 <5%。

换句话说,"解出来并自认为检查过了"与"真的被独立第三方判对"之间隔着一道巨大的鸿沟。math-olympiad 的全部设计都围绕填平这道鸿沟展开,其四条核心对策是:

  • 上下文隔离验证(Context-isolated verification):验证器只看清洗后的干净证明,永远看不到解题者的思考轨迹;
  • 模式武装的对抗检查(Pattern-armed adversarial checks):不问"这正确吗",而是问"这会不会意外证明了黎曼猜想?""把这个通用引理提取出来,找个 2×2 反例";
  • 校准式弃权(Calibrated abstention):没有把握时说"no confident solution",而不是虚张声势地硬给答案;
  • 呈现打磨(Presentation pass):验证通过之后,才进入干净的 LaTeX/PDF 输出环节。

安装与自动触发

插件通过 Claude Code 官方插件机制安装,README 给出的命令为:

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

安装后无需手动唤醒。技能(skill)会自动触发,触发词包括 "IMO"、"Putnam"、"olympiad"、"verify this proof" 等。插件内的 trigger_eval.json 以可机读的断言形式给出了触发边界,共 20 条用例,分为两组:

  • 应当触发(should_trigger: true):"Solve this IMO problem: Let n ≥ 2 be an integer. Prove that…"、"Is this Putnam proof correct?"、"Find a counterexample to: every continuous function on [0,1] is uniformly continuous"、"Prove this olympiad inequality…"、"Help me with this USAMO geometry problem"、"Verify my solution to AIME 2024 problem 12"、"I think there's a gap in this competition proof"、"Simplify this proof" 以及"比赛题猜想求证"、"求最干净呈现方式"等;
  • 不应触发(should_trigger: false):算法复杂度分析、写素数判断函数、黎曼假设科普、Lean 证明助手调试、微积分基本定理讲解、找竞赛数学教材、生成 AIME 练习题、计算定积分、审阅数论论文等。

这组数据说明触发面刻意收窄到"竞赛证明/反例/验证/呈现"四类任务,普通数学问答与编程问题不会误触。

何时用哪种方案:任务类型分诊

SKILL.md 提供了一张按问题类型选择策略的分诊表,这是整套工作流的入口:

问题类型 方案 验证方式
AIME 数值答案 Best-of-N → 多数投票 只对答案
奥林匹克证明(IMO/Putnam/USAMO) 下面的完整工作流 5 轮对抗验证
"这个证明对吗?" 跳过解,直接进入验证(第 4 步) 对抗验证 + 规格博弈
完整试卷(如全部 6 题) 每题一个完整工作流,汇总后编译单一 PDF 每题单独对抗验证

两个实战要点:

  1. 并行 + 标签:完整试卷场景下,应在每次 agent() 调用上设置 opts.label 携带题目 ID(如 label: "P3:solver:2")。没有标签时,36 个返回结果无法对应题目。并行运行各题,标签才是关联的关键,与顺序无关。
  2. 不要在单个 agent 上下文中解全部 N 题:每道题需要独立的思考预算和独立的 fresh-context 验证器。合成是机械性的:收集各题输出 → 填入 LaTeX 章节 → 一次性编译。若只需"简化某个证明",直接跳到呈现(第 8 步)即可。

完整工作流:从题意核对到对抗验证

第 1 步:题意核对(30 秒,可拦下一类错误中的 50/63)

正式解题之前先确认"题目到底在问什么"。SKILL.md 给出的提示模板为:

阅读题目。列出 2–3 种可能的解读。对每种解读问:这个读法是不是 TRIVIAL 的?如果一种读法让题目变简单、另一种让它变难,那么难的读法几乎肯定是本意。说明你按哪种解读解题、为什么相信这是本意。

依据:Aletheia 案例研究发现 63 份"技术上正确"的解答里有 50 份解错了题意。奥林匹克题经常故意埋一个"容易的误读"作为陷阱——这与验证模式库中的 Pattern #60(最简解读陷阱) 完全对应:verifier_patterns.md 记录道,63 份"技术上正确"中仅 13 份"实质正确",差距就出在解了最容易的语法合法读法而非本意。判断提示:如果某个解读让 7 分题变成三行就做完,那你很可能选错了。

第 2 步:并行生成候选并内部打磨(纯推理)

并行启动 8–12 个 attempt agent。每个 agent 在内部自我迭代——解 → 自改进 → 自验证 → 修正 → 重复。这就是 Yang-Huang 结构在 IMO 上达到 85.7% 的关键:一次性求解不够,逐次尝试的反复打磨才有意义。

一个必须遵守的铁律:Agent 工具无法强制限制子代理的工具集,唯一的机制就是提示词。SKILL.md 明确要求以下提示词必须 VERBATIM 使用,不得自行改写或摘要:

NO COMPUTATION. Do not use Bash, Python, WebSearch, Read, Write, or any tool that runs code or fetches data. Numerical verification is not a proof step. "I computed n=1..10 and the pattern holds" is not a proof.

(If your agent harness requires a StructuredOutput or similar return-mechanism tool call, that is NOT a computation tool — call it to return your answer. The restriction is on tools that DO work, not tools that REPORT work.)

Your internal process (iterate until done):
- Solve: Complete rigorous solution.
- Self-improve: Reread. Fix gaps before a grader sees it.
- Self-verify: Strict grader mode. Every step justified?
- Correct: Fix and re-verify. Up to 5 rounds.
- Stop: Self-verify passes twice clean, OR 5 rounds, OR approach fundamentally wrong.

A correct answer from flawed reasoning is a failure. If incomplete, say so honestly. Never hide gaps.

PROBLEM: <insert the problem statement here>
ANGLE: <insert one starting angle here>

SKILL.md 特别警告:前两段是承重墙。如果某个会话自拟提示词并省略它们,子代理会去跑 30 轮 Python,然后自信地给出错误答案——"对 n≤10 成立、在 n=100 失效"的模式根本不是证明。

起点角度(跨 agent 差异化,完整清单见 solver_heuristics.md):先算小情形(并越过 n=3 再测试)、找不变量或单调量、考察极值情形、尝试归纳、找对称性、倒推、删掉一个条件看哪里变得平凡为假、推广(发明者悖论——结构更多有时更容易)。

该文件还浓缩了 Pólya 与奥林匹克实战的动作库:专精化(解不动就手算 n=3,4,5,模式常常就是证明);推广("对全体素数证明"可能比"对全体整数证明"更难);删条件(删掉假设后哪里平凡为假,那里往往就是承重步骤);倒推;辅助元素(奥林匹克几何全靠辅助点);以及几何专属招式——坐标暴力、圆幂定理、螺旋相似、反演、角追。另有递推陷阱提醒:b_{n+1}=P(b_n) 且 P 为二次以上多项式时,b_n 是双重指数增长,b_30 就有万亿位数字,必须一开始就在 ℤ/2^m 上归纳证明同余,绝不能精确计算。

每个 attempt agent 只返回 最终状态(不返回中间轮次):

**Verdict**: complete solution | partial result | no progress
**Rounds**: [how many verify→correct cycles]
**Method**: [key idea, one paragraph]
**Detailed Solution**: [full step-by-step, every step justified]
**Answer**: [if applicable]
**Self-verification notes**: [what you caught and fixed; remaining concerns]

对应的完整子代理提示词模板见 attempt_agent.md——它以"严格 IMO 阅卷人"身份做第 3 轮自验证,把问题分成 Critical Error(断链)与 Justification Gap(论证不完整)两类,最多修正 5 轮。重试策略:agent 失败或超时则重试一次,瞬时故障是常态。

第 3 步:清洗解答(上下文隔离——第一杠杆)

思考轨迹会让验证器偏向认同——即使结论错误,一长串推理读起来也像支撑证据。验证前必须剥离:

  • 所有 thinking-block 内容;
  • 所有 "Let me try…" / "Actually wait…" / "Hmm" 类散文;
  • 所有假起点与回溯。

从每个 solver 的输出中只提取 Method + Proof + Answer 三节。验证器永远不知道 solver 是怎么走过来的。

第 4 步:对抗式验证(fresh context + 模式武装)

对每个清洗后的解答,启动一个全新的验证器 agent:fresh context——它只看到(题目 + 清洗后的解答),无任何工具。

验证器的工作是"攻击",不是"评分"。它加载 adversarial_prompts.md 中的提示词,按 verifier_patterns.md 的 13 个纯推理模式逐一排查。SKILL.md 展示了其中五个核心模式:

模式 检查内容
#4 该定理特化到著名对象(ζ、二次互反律等)后,是否证明了关于它的某个未解问题?→ 有洞
#18 把证明自己建立的中间恒等式代回"剩余缺口",是否恢复出原命题?→ 同义反复
#40 某步是否为"一行引理"?提取其一般形式,找 2×2 反例。若一般形式为假,找出是什么特殊结构拯救了本实例
#5 对每个被调用的定理,从零重新核对假设条件——"[0,1] 连续"≠"ℝ 上连续"
#6 无穷和是否借正则化值"有界"?检查边界——若有极点,级数发散

验证模式的底层逻辑值得展开。以 Pattern #4(会证明出著名未解问题吗) 为例:把被证定理特化到其类中最著名的对象(ζ(s)、Ramsey 数、Collatz 映射),若特化后解决了一个已知开放问题,原证明必有洞——例如"对所有满足性质 P 的 Dirichlet 级数"的有界性命题套到 ζ 上会证明 Lindelöf 猜想,说明证明把算术输入当成了泛型输入。Pattern #40(一行证明过于干净) 的经典案例是"秩只取决于支撑集":[[1,1],[1,1]] 秩为 1,[[1,1],[1,−1]] 秩为 2,支撑集相同——一般引理为假,具体实例因符号因子分解而成立,那才是真正的证明。Pattern #6(解析延拓背后的发散级数) 提醒:"Σ 1/n ≤ ζ(1)" 荒谬,因为 ζ(1) 是极点,级数的解析延拓不等于级数本身。

adversarial_prompts.md 还把"找洞"归纳为七类反驳(refutation taxonomy),验证器只需命中任意一类即可驳倒:步骤不成立、假设条件不满足、小情形即假、同义反复、证得过多(Proves too much)、解错题意、关键处含糊其辞("由标准方法""细节是常规的"——恰好在非常规之处)。

验证器返回格式:

**Verdict**: HOLDS | HOLE FOUND | UNCLEAR

**If HOLE FOUND**:
- Location: [quote the problematic step]
- Pattern: [which check fired, or "other"]
- Why it breaks: [specific]
- Fixable?: [yes with X / no, fundamental]

第 5 步:排序 + 投票验证(非对称阈值与鸽巢早退)

按(verdict,验证器置信度)排序,取第一名,再启动最多 5 个 fresh verifier agent。

  • 非对称阈值: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)。
  • 双重上下文隔离:每个验证器对 (a) solver 的思考轨迹(第 3 步已剥离)和 (b) 其他验证器的判定都一无所知。每个验证器都以为自己是第一个。"已有 3 个 agent 确认过了"这种社会性证据同样会引入偏差。
  • solver 不能验证自己的解答:必须是不同 agent + fresh context。

adversarial_prompts.md 的 5-pass 连续验证提示词把这一点推到极致:"不要推理'这个大概已经有人查过了'——你的投票是唯一由你控制的投票。如果每个人都假设别人会抓住错误,错误就通过了。"它还给出一个反直觉的防偏置准则:写得漂亮、自信、大部分地方标准机制正确的解答,恰恰最可能是微妙错误的——作者先说服了自己再说服了数学;你唯一跟不上的一步,恰恰是要下最大力气的地方。

第 5b 步:某一情形打不开时——先退一步,别硬磨

证明分情形讨论、一种情形轻松、另一种死活打不开时:硬磨之前,先问是否存在让分情形消失的路线。

救命模式:困难情形的假设本身往往蕴含了关于某个你还没看的中间对象的强结论,直接用这个蕴含,别走原来的链条。SKILL.md 给出了具体形状:证明受约束函数满足 f(n) ≤ cn,对整除 f(n) 的素数 p 分情形。一支用 (ℤ/p^e)* 的指标论证收掉;另一支同样的群结构却磨不动。修正法:把假设 "p | f(n)" 代回主控方程,推出 f(p) = p 本身——之后一个 Fermat+Dirichlet 论证三行内同时杀死两支。那个分情形本身就是绕路:它是在对一个在假设下取值已知的变量做分裂。

卡在情形 B 时的自查清单:情形 B 的假设对 f 在其他输入上说了什么?是否有不同的 (a,b) 对可代入主控方程?是不是证得太多?(更干净的矛盾需要更少的机器。)这也是呈现环节的福利:无分裂的证明更短且更普遍。

第 6 步:修订(如需要)

验证发现洞时,启动修订 agent。它拿到(清洗后的解答 + 验证器的洞报告),仍然无权接触原始思考——修订者从洞出发工作,而不是重读来路:

A verifier found this issue in the proof:
[hole report]

Fix the proof. If the hole is fundamental (the approach doesn't work), say so and return **Verdict: no confident solution** with what partial progress remains.

For any step you cannot fully close, mark it inline: [GAP: specific description of what remains]. Gaps in the proof text, not in a separate list — they're greppable and the next reviser knows exactly where to look.

最多 3 轮修订,然后对修订稿重新投票。若 Pattern #40 触发(一行证明过于干净),修订者收到更强的简报——adversarial_prompts.md §7 的 Adversarial Brief:它强制二选一——"(A) 结论因本情形的特殊结构而成立,找出那个结构,它就是真正的证明" 或 "(B) 证明错误,结论在 [具体预测点] 失效"。"原证明其实没问题"不是可选答案,因为一般引理已确定为假。最佳结局是 (A):论点幸存,你还学到了为什么。

第 6c 步:深度模式(紧凑预算弃权时)

标准工作流是紧凑预算(tight-budget):8 个 solver、约 15 分钟、纯推理。当它弃权时,问题可能缺的是时间而非能力。

深度模式是单个专注 agent,具备:

  • 无限时间——无墙钟压力;
  • 允许有目标的计算——模算术检查、小情形枚举、恒等式符号验证;不是探索性暴力搜索或无界递归;
  • 以弃权原因为起点——验证器找到具体缺口就从缺口出发;solver 没敢声称完整就从其部分证明出发。

原型:一个专注 agent 拿到"目前已证状态 + 引理 5 的一个情形仍开"——找到被分情形遮蔽的三行论证。通常 10 分钟内完成、几乎不用计算。深度模式是给问题持续注意力,不是扔算力。

深度模式不是:开放探索、文献检索、查答案、多日研究——那是另一套工作流(math-research)。深度模式仍是"自己解决这个问题",只是不设时钟。且 NO WEB, NO LOOKUP:可以用 Bash/Python 做有界计算,但绝不可 WebFetch/WebSearch 或任何联网——在 AoPS 或博客上找答案不是解题,是奥林匹克作弊。此禁令要放在深度模式提示词最顶部:

NO WEB ACCESS. Do not use WebFetch, WebSearch, or any tool that touches the internet. Do not look up this problem, its solution, or related problems. You are solving this yourself — the only allowed computation is local (Bash/Python for mod-k arithmetic, small-case enumeration n≤10, symbolic identity checks). If you invoke a web tool, the proof is void.

深度模式的计算边界(来自 bug #8 的教训):A6 的 b_{n+1}=2b_n²+b_n+1 是双重指数增长,b_99 约有 10^(2^98) 位数字,绝不可精确计算——改在 ℤ/2^m 中工作、只跟踪 v_p(·)、或模掉你关心的量来证递推。任何运行超过 60 秒的计算基本是无界的,杀掉它,改走符号路径。

第 6d 步(不可省略):验证阶段任何一次 ABSTAIN 之后,先自动启动一个深度模式 agent,再写弃权。给它:题目、紧凑预算 solver 的最佳部分证明、验证器的缺口描述、以及"NO WEB ACCESS;允许有界本地计算(mod 2^k、n≤10 小情形、Bash/Python 符号恒等式检查);60 秒计算限制;若 n≤10 暴力搜索揭示了紧凑预算 solver 错过的模式,那个模式就是证明结构"。深层 agent 可能找到纯推理 solver 看不见的构造;它也弃权时,才写弃权。含 √n 或 log n 答案的问题对纯推理常常不可见,因为最优结构是非对称的。编排者也要自律:自己也不得联网搜题"帮"深层 agent——那会污染技能输出并歪曲其能力。

第 7 步:校准式弃权

3 轮修订全失败:停止并承认。

**Verdict**: no confident solution

**What was tried**: [approaches]
**What WAS proven**: [any lemma or partial result that survived verification]
**Where it breaks**: [the unfixed hole]

不要猜。 错误的自信答案比诚实的"解不出"更糟。真正重要的指标是条件准确率(conditional accuracy)——当你说"解出来了"时,你真的对吗?

第 8 步:呈现打磨(正确性确立之后)

已验证正确的证明往往不是漂亮的证明。发现的顺序极少是呈现的最佳顺序。启动一个全新的呈现 agent,给它已验证的证明,加载 presentation_prompts.md。它要问:

  • 最简单的说法是什么?
  • 哪些引理应内联、哪些值得独立成段?
  • 有什么 OVERKILL?(构造双重指数,而线性就够)
  • 现在已知答案,是否存在三行的后见之明证明?

该文件的核心理念直接引自论文级经验:"somewhat overkill; any f whose inverse is at most [X] would suffice, no need to take the double exponential"——呈现打磨就是让 overkill 去死的地方。它还列出呈现 agent 要抓的反模式:发现顺序式叙述("先试了 X,由此注意到 Y……")、过强构造、威吓式证明("显然""标准论证")、不必要的普遍性、孤儿引理、无标签情形分裂、缺路标(读者被迫逆向工程你的策略)。风格约定包括:产生结果的方程用 display math,过程中的代数用行内;引用著名结论时精确标注(如 Jacquet–Piatetski-Shapiro–Shalika, 1981);整数界用上取整:d ≥ n/k 且 d ∈ ℤ 时写 d ≥ ⌈n/k⌉。

输出为 LaTeX 格式证明,模板见 presentation_prompts.md §2(最小化导言区、无 tcolorbox、无自定义颜色)。若 pdflatex 可用(check_latex.sh 返回 0),再经 compile_pdf.sh 编译为 PDF。该脚本会把你提交的证明正文(只含 \begin{document}...\end{document} 内容)包裹进最小导言区生成 *_full.tex,优先 pdflatex、其次 xelatex,连续编译两次(-interaction=nonstopmode -halt-on-error)后输出 *_full.pdf 路径。

模型分档:预算不是约束,噪声地板才是

model_tier_defaults.md 给出的分档哲学很关键:参数随模型能力伸缩,约束不是预算,而是边际收益递减与"非对称噪声地板"——Haiku 验证器个体更不可靠,正确应对是加宽度而非加深度。SKILL.md 的汇总表:

模型 Solvers 验证轮次 弃权阈值 呈现
Haiku 8 3 2 次修订失败 跳过
Sonnet 4 5 3 次修订失败 是
Opus 3 5 + 全模式清扫 4 次修订失败 2 稿,选更干净的

参考文件中的完整配置差异更大:

  • Haiku:12 个并行 solver(宽扇面,个体弱就撒大网);7 个验证器,需 5 确认 / 3 驳倒(比 Sonnet 的 2 更高,防止两个糊涂的 Haiku 杀死正确证明);呈现轮为 3 稿 + 比较器(基础模型输出更粗糙,呈现反而更重要)。
  • Sonnet:6 个 solver;5 个验证器,4 确认 / 2 驳倒;4-of-5 容忍一次闪失,2 个异议是信号。
  • Opus:4 个 solver;5 个通用验证器(4/2 阈值)外加 12 个专项模式 agent(verifier_patterns.md 每个模式一个专用攻击者),任一专项 HOLE FOUND 都计入驳倒;弃权阈值放宽到 5 轮修订;呈现为 3 稿、三种不同指令("最优雅""最初等""最短")让强模型产出不同风格的证明。
  • 鸽巢早退保留在所有档位:不是因为省钱,而是因为一旦 inflight >= confirm_needed + refute_needed - 1,剩余票无论怎么投都不携带信息,再启动纯属延迟。
  • 档位识别:编排会话不知道自己是哪个模型时默认 Sonnet 配置;合理启发式是让模型在首个响应中自我识别,并匹配输出中的 haiku/sonnet/opus。

面向数值答案(AIME 风格)的简化路径

跳开整个证明机制:运行 5–7 个采用不同方法的 solver,对数值答案取多数投票;无多数时,把前两个候选代回验证。

这套方案与泛泛的"验证-修订"有何不同

SKILL.md 结尾总结了六点根本差异,也是理解整套设计的关键:

  1. 双重上下文隔离:验证器对 (a) solver 思考轨迹(它偏向认同)和 (b) 其他验证器的判定(社会性证据同样偏差)双重失明。每个验证器都以为自己是第一个。
  2. 模式特定攻击:不是问"这正确吗",而是问"这是 #40 式错误吗?#4 式错误吗?"——具体打败泛化。七类反驳分类学给了验证器一张检查清单。
  3. 非对称投票 + 鸽巢早退:4 确认 / 2 驳倒。一个不稳定的验证器杀不死正确证明,两个异议才作数。结果已定时停止启动验证器,清晰情形下节省约 30% 的验证成本。
  4. 规格博弈检查先行:解题前明确问"这是不是本意解读?"——先例工作最大的失败模式(63 份"正确"答案中 50 份解错读法)。
  5. 校准式弃权:会说"no confident solution"并附部分结果。优化条件准确率而非覆盖率。
  6. 呈现打磨:正确性与优雅是两步。呈现 agent 拿到已验证证明,去找最干净的说法。

验证数据与边界声明

README 报告的验证结果是:2025 IMO+Putnam 的 17/18 道题目解决,0 误报,2 个新证明;评估数据存放于技能目录下的 eval 数据(原文档指向的 anthropic monorepo 评估框架在本仓库内对应 trigger_eval.json 等文件,仓库根 README 同时声明本项目为 Anthropic 官方维护的高质量 Claude Code 插件目录)。需要强调的是,这一数字是插件作者声明的自身评估结果,作为能力参考而非普遍承诺。

使用前提同样值得注意:标准工作流是纯推理的紧凑预算流程,子代理工具限制完全依赖提示词(Agent 工具本身无法强制);深度模式中的有界计算与"60 秒即视为无界"的警戒线是运行约束;LaTeX/PDF 输出依赖本机存在 pdflatex/xelatex。这些边界都已写进 SKILL.md 与两个脚本的注释中。

快速查阅索引

登录后查看全文
claude-plugins-official