Skip to content

Latest commit

 

History

History
310 lines (227 loc) · 19.6 KB

File metadata and controls

310 lines (227 loc) · 19.6 KB

Agent 验证模式

本文定义 Agent 创作、重构或实质审查算法竞赛题目时的验证契约。快速、普通、完整三种模式改变的是独立交叉验证深度,不改变 ProbHub Core 的 Schema、Judge 宿命或正式发布门禁。

模式目前由 Agent Skill 选择和执行,不是 probhub CLI 参数。不要虚构 --mode、把自然语言审查冒充 Core 证据,或让 Python Core 绑定某个 Agent 平台、模型名称或协作接口。

目录

  1. 术语与选择规则
  2. 所有模式的共同底线
  3. 快速模式
  4. 普通模式
  5. 完整模式
  6. 上下文隔离与审查角色
  7. 无法直接 stress 的题型
  8. 升级、分歧与失败处理
  9. 验证记录与交接
  10. 并行出题与正式构建

1. 术语与选择规则

每次任务同时记录:

  • requested_mode:用户明确要求的模式;未指定时为 null
  • effective_mode:Agent 实际执行的模式。
  • selection_reason:选择或升级原因,不能只写“感觉较难”。

按以下规则选择:

  1. 用户未指定时默认普通模式。
  2. 用户要求普通或完整模式时,将其视为最低验证深度,不得降级。
  3. 用户要求快速模式时,可以从快速模式开始;一旦出现硬升级信号,仍必须升级。若用户同时禁止所需的 stress 或独立审查,只能把任务标记为验证未完成,不能声称快速模式已经充分证明高风险题。
  4. Agent 只有在快速模式准入条件全部成立时,才可自行选择快速模式。
  5. 模式可以 快速 -> 普通 -> 完整 升级,不得在发现风险后静默降级。
  6. 模型档位、参数量或推理强度本身不构成独立性证据。遵守用户与工作区对模型的约束,但用上下文隔离、不同算法或关键实现、不同审查角色建立独立性。

以下任一项是硬升级信号:

  • 证明存在未闭合步骤、依赖未经验证的猜想,或主 Agent 无法逐步复述正确性理由;
  • 主解与独立解、oracle、样例或正式数据结果不一致;
  • 随机化、启发式、近似算法,或正确性依赖概率/经验参数;
  • 浮点误差、非唯一输出、复杂 Custom Checker 或 Interactor;
  • Validator、Checker、Interactor 或生成器包含难以人工穷尽的状态与协议分支;
  • 时限、内存或输出余量紧张,校准出现 warning,或正确性与性能强耦合;
  • stress 命中反例、出现基础设施异常,或有代表性的错解未被目标组稳定击杀;
  • 题目难度高、结论新颖、边界繁多,且缺少可信的不同算法或小范围 oracle;
  • 任一独立审查者给出未解决的阻断意见;
  • 用户明确要求完整模式。

2. 所有模式的共同底线

无论模式如何,都必须完成与任务阶段相符的确定性验证:

  1. 冻结并核对题面、约束、Judge 语义、样例和正式代码矩阵。
  2. 运行 probhub lint <ID>,处理错误并人工审阅 warning。
  3. 运行 probhub sample-check <ID> --no-cache;交互题使用 Core 返回的明确“不适用”结果,不能伪称样例评测通过。
  4. 运行 probhub judge <ID> --no-cache,检查退出码、最终结构化事件、逐解法宿命、数据组目标和本地校准证据。
  5. 确认首个 accepted 全域 AC;brute 不得 WA;每个声明 wrong 都必须按配置在目标组得到稳定预期结果,不能用偶然 RE/TLE 代替要求的 WA。
  6. 核对 Validator、Checker/Interactor、数据配方、数据去重、边界/定向/近上界覆盖和样例解释。
  7. 所有算法、代码、数据、答案或限制修改结束后,重新执行受影响的验证,不能沿用修改前的结果。
  8. 单题并行开发完成时执行 probhub seal <ID> --no-cache --seed 12345probhub generation-status,检查 sealed revision 与隔离 generation,并完成单题页和整卷上下文的 PDF 目检。
  9. 负责整场正式交付时,在所有题目均为有效 sealed revision 后执行一次多 ID build --no-cache,再运行 status、深度 verify-package 和最终 PDF QA。
  10. 最终交接必须区分已自动验证、已人工/Agent 审查、未验证和剩余风险;不得用“未发现问题”替代通过条件。

多组数据的上限推导统一见 aggregate-limit-derivation.md,三种模式都必须遵守其硬门槛。模式文档只记录选择和证据边界:题面与 Validator 的累计上限必须相同;累加器类型、初始化、每组恰好累计一次、上限内接受/超限拒绝、联合边界和 accepted/Validator/Checker/Interactor 的资源校准必须实际审查。5..100000 是常见 T_max 候选区间,10N 是条件性累计候选,不是模式统一的拒绝或通过数字。constraint_reconciliation.aggregate_constraints 若为 statement_onlyaggregate_constraint_mismatchdynamic,以及人工发现没有真实累计/拒绝逻辑时,必须保留未完成状态并重跑受影响门禁。

模式不能削弱现有 Core 门禁。快速模式必须配置可用的 stress 链路,并使用固定 seed 完成 100 轮对拍;不得删除已有 stress 配置、减少到 100 轮以下或虚构跳过参数来绕过 seal

所有模式还保留以下操作边界:只修改规范源,正式产物/evidence/generation 由 Core 通过锁、快照、staging 和验证后发布写入;不要手工修复结果或把自然语言审查当作自动 evidence。外部程序必须使用共享进程控制和有界输出;取消、超时、基础设施失败或后代进程清理失败均保持未完成/失败语义。临时 submission、stress、preview 和审查快照在交接前清理,清理失败优先于“通过”结论。

3. 快速模式

快速模式使用固定 seed 完成 100 轮 stress 对拍,不调用独立审查 Agent。只有以下条件全部成立时,Agent 才可自行选择:

  • 题目简单、确定性强,主解与约束之间没有隐藏的算法分支;
  • 正确性证明短且闭合,主 Agent 能逐条检查不变量、完备性与边界;
  • 使用标准 Judge 或等价的低风险精确判定,不涉及浮点、交互、复杂构造或概率;
  • Generator、Validator、accepted 与 brute 能组成稳定的 stress 链路,brute 或可穷举 oracle 能覆盖有意义的小范围,且正式数据包含明确边界和错解定向组;
  • Validator、生成器和数据组织简单,没有高风险协议或复杂状态;
  • 资源余量充足,未出现校准 warning 或平台敏感行为;
  • 没有审查分歧、未解决反例或幸存的代表性错解。

快速模式仍执行全部共同底线,并在最终 seal 时显式固定对拍轮数:

probhub seal <ID> --no-cache --rounds 100 --seed 12345

seal 内部的 stress 必须取得最终结构化成功结果;超时、中断、基础设施失败或只完成部分轮次都不算通过。若 100 轮对拍已经表现出异常耗时、反例或不稳定性,应重新评估风险并升级模式。

结束时必须明确写出:

  • 未运行独立 Agent 交叉验证;
  • 固定 seed 的 stress 已完成 100/100 轮;
  • 选择快速模式的逐项依据;
  • 仍然存在的风险。

用户强制要求快速模式并不允许忽略已经出现的硬升级信号。无法升级时,将 verification_complete 标记为 false,说明缺失证据,不得进入“已充分验证”的交接状态。

4. 普通模式

普通模式是默认模式,包含共同底线、固定 seed 差分测试和一个盲审独立解题者。

4.1 Stress

  1. 先用约 100 轮测量吞吐,确认 Generator、Validator、accepted、brute 和 Checker 链路有效。
  2. 根据实测吞吐设置正式轮数与外层等待预算;等待预算至少为预计时间的 1.5 倍再加 60 秒。
  3. 使用固定 seed 运行正式 stress,并取得最终结构化结果。外层超时、任务中断或“暂未看到反例”都不算通过。
  4. 命中反例后先 replay,修复后把有价值的反例固化为 secret 数据,再重新执行完整验证。
  5. 不能直接 stress 时,按第 7 节提供强度相当的替代证据。

4.2 盲审独立解题者

给盲审者一个新鲜、隔离的上下文,只提供:

  • 冻结后的公开题面、完整约束、Judge 语义和公开样例;
  • 要求输出的语言、接口与资源限制;
  • 用户或工作区明确规定的协作模型约束。

不得提供或暗示:

  • 主 Agent 的算法、证明、复杂度分析或源码;
  • 官方数据、生成器、Validator/Checker/Interactor 源码;
  • brute、wrong、数据组目标、已知反例或其他审查结果;
  • 工作区路径或允许其自行浏览 live 题目目录的指令。

盲审者必须返回:

  1. 对任务和约束的独立复述;
  2. 算法与逐步正确性证明;
  3. 时间、空间复杂度和边界条件;
  4. 可编译的完整 std;
  5. 假设、无法证明处和自认为高风险的用例。

主 Agent 负责逐行审查返回代码。审查通过后,由主 Agent 而不是审查者决定是否把它落入 code/,并用 independence 记录不同算法或关键实现。必须实际编译并对样例、oracle/正式数据和 stress 输入交叉运行;只比较自然语言结论不算完成。

如果平台无法提供新鲜上下文、无法调用审查 Agent,或审查者实际读取了主解/正式数据,则普通模式的独立证据缺失。只有同时满足快速准入条件并明确改为快速模式时才可降级;否则标记验证未完成。

5. 完整模式

完整模式包含普通模式的全部内容,并增加以下两个独立角色,以及适用时的 mutation 补充检查。

5.1 独立证明与参考实现审查者

使用与盲审解题者相互隔离的新鲜上下文。提供公开题面和约束,要求其优先寻找不同算法;若不同算法不可行,至少使用不同关键实现、精确小范围 oracle 或可证明的性质检查。

输出必须包含:

  • 独立证明,以及对主结论可能失败位置的清单;
  • 完整参考实现,或明确适用范围的可信 oracle;
  • 与盲审解法相比真正不同的算法/关键实现说明;
  • 可用于穷举或定向验证的边界分类。

相同算法、变量重命名、I/O 改写或共享代码不构成独立实现。无法建立独立性时如实记录 independence: unverified,并补充 oracle 或对抗证据,不能伪称“双标程互证”。

5.2 对抗审查者

对抗审查者在规范源冻结后读取完整审查快照,包括主证明、accepted/brute/wrong、Validator、Checker/Interactor、生成器、数据组与期望矩阵。其任务不是再写一份相似标程,而是主动寻找失败:

  • 攻击证明中的必要性、充分性、单调性、贪心交换、状态压缩和边界假设;
  • 构造 Validator 接受非法输入或拒绝合法输入的例子;
  • 构造 Checker 错收、错拒、依赖官方答案错误或协议错误的输出;
  • 枚举三层错解分类,指出缺失 mutant、幸存错解和未覆盖数据组;
  • 检查整数溢出、精度、递归深度、复杂度、平台差异和资源限制;
  • 给出可重放、可固化的最小反例或定向生成策略。

主 Agent 必须验证每条阻断意见。有效问题进入规范源并重跑相应门禁;错误或不适用意见也要记录理由,不能只写“已查看”。所有分歧解决前不得把完整模式标记为完成。

5.3 条件性 mutation 检查

mutation 的算法、算子、预算和 evidence 语义以 mutation-testing.md 为准。完成独立证明、对抗审查并冻结题面、Validator、标程和正式数据后,主 Agent 只需判断是否适用:仅 judge.type: standard 且首个 accepted 为 C++ 时可运行;Checker、Interactor、浮点判定和非 C++ 标程记录 not_applicable,不把跳过当作失败或通过。

适用且有明确时间预算时,按权威 reference 选择参数并运行,例如:

probhub mutation <ID> --jobs 2 --no-cache

mutation 是补充证据,不是完整模式的统一硬门禁,也不接入普通模式、sealbuild。运行前记录可接受的墙钟和资源预算,命令返回后必须读取结构化 evidence,而不是只看 score:

  • raw_plannedexcludedplannedselectedexecuted 必须互相一致;
  • infrastructure-failedcancelled、超时或发布失败不计为 killed,且 mutation 子检查未完成;
  • no_candidates 表示没有可执行候选,不表示题目已获得 mutation 保证;
  • survived 必须由主 Agent 阅读源码位置、变换和命中范围后分类;mutation 子任务的编译、执行、取消、超时或发布失败都保持未完成语义。

对 survivor 的处置只有三种:补数据或修复题目后重跑;确认等价、不适用或越界未定义行为并按稳定 ID 写出具体 exclusion 理由;无法判断时保留 residual risk。不能为了提高 score 批量排除,也不能把“全部已知变异被击杀”写成“没有未知错解”。

完整模式交接必须记录 mutation 的适用性、命令、requested/effective jobs、候选计数、分类、人工处置和剩余风险。若适用 mutation 未完成,verification_complete 不得无条件写成 true;若用户明确接受缺口,需在交接中保留 mutation: incomplete 及原因。

6. 上下文隔离与审查角色

独立性是流程属性,不是模型标签。执行审查时遵守:

  1. 使用新鲜会话或不继承主任务历史的上下文;只传递该角色允许看到的材料。
  2. 在共享文件系统环境中,明确禁止盲审者浏览工作区,并只向其提供隔离副本或消息内的公开材料。该隔离是协作纪律,不是安全边界;若发生泄漏,证据作废。
  3. 审查者默认只读,不直接修改 live 题目文件、workspace.yaml、生成物或正式数据。
  4. 主 Agent 统一审查、选择并落盘代码和反例,避免并发覆盖规范源。
  5. 不让不同角色互看答案后再声称独立。需要讨论分歧时,先保存各自原始结论,再由主 Agent 汇总。
  6. 遵守用户和项目对模型、推理强度、并发数和工具的限制;不得为了“多样性”擅自换用被禁止或更低档模型。
  7. 审查者不可用时,不得虚构角色、结果、运行记录或通过状态。

7. 无法直接 stress 的题型

Stress 是手段,不是唯一证据。替代方案必须有可判定 oracle,并在验证记录中说明覆盖边界。

7.1 Custom Checker 与非唯一输出

  • 用小范围穷举或独立构造器生成多个合法答案;
  • 对 Checker 提交合法、次优、越界、格式异常和伪造 witness,确认不会错收/错拒;
  • 独立核对官方答案或最优值,不让 Checker 与标程共享同一错误假设;
  • 能使用 Core custom stress 时仍应使用 Checker 语义比较。

7.2 浮点题

  • 使用更高精度或不同数值方法建立 oracle;
  • 覆盖接近误差阈值、极值、退化和消去误差用例;
  • 同时检查绝对/相对误差、NaN、Infinity 和输出格式;
  • 统计随机测试只能补充,不能替代误差界证明。

7.3 交互题

  • 对 Interactor 状态机、查询上限、终止条件和非法协议分支做独立审查;
  • 使用多种 accepted/wrong 策略覆盖成功、失败、超限、空闲和提前退出;
  • 核对双向 transcript、idle limit、输出预算和后代进程清理;
  • 对可缩小状态空间的版本做穷举或模型检查。

7.4 随机化、启发式或大规模题

  • 固定 seed 只用于复现,不等于正确性证明;
  • 用可穷举的小规模版本、独立确定性 oracle、性质测试和 metamorphic relations 交叉验证;
  • 对所有随机分支、失败概率和退化输入给出可审计论证;
  • 若只能提供经验成功率,完整模式仍应标记验证未完成,不能承诺 accepted 一定正确。

8. 升级、分歧与失败处理

维护 escalation_history,每次记录原模式、目标模式、触发证据和处理结果。

  • 快速模式发现任一硬升级信号:至少升级到普通;特殊 Judge、概率正确性或证明分歧直接升级完整。
  • 普通模式的盲审解法与主解不同:先用最小反例、oracle 和逐步证明定位,不以多数投票决定正确性;无法解决时升级完整。
  • Stress 基础设施失败:先修 Generator、Validator、Checker 或进程控制;不得把失败轮次计为通过。
  • 审查代码无法编译、只给伪代码或缺少证明:要求补齐;仍不满足时该角色未完成。
  • 对抗审查者给出反例:主 Agent 必须实际 replay 或构造测试验证,不能仅凭文字接受或驳回。
  • 发生任何规范源修改:旧审查快照和受影响证据失效;重新冻结、重跑并生成新的 checkpoint/seal。
  • 用户停止任务或禁止必要验证:保留已完成证据,列出缺口并设置 verification_complete: false

9. 验证记录与交接

在任务笔记或最终交接中记录以下结构;当前不要把它写入 probhub.yaml 或伪装成 Core Schema 字段:

verification:
  requested_mode: null
  effective_mode: normal
  selection_reason:
    - default mode
  escalation_history: []
  reviewers:
    - role: blind_solver
      context: statement-constraints-samples-only
      artifact: code/std_independent.cpp
      independence: algorithm
      verdict: passed
  commands:
    - command: probhub judge L10 --no-cache
      exit_code: 0
      result: all_expectations_met
    - command: probhub stress L10 --rounds 3000 --seed 12345
      exit_code: 0
      result: passed
  mutation:
    applicability: applicable
    command: probhub mutation L10 --jobs 2 --no-cache
    status: reviewed
    requested_jobs: 2
    effective_jobs: 2
    raw_planned: 12
    selected: 12
    executed: 12
    killed: 11
    survived: 1
    compile_invalid: 0
    infrastructure_failed: 0
    survivor_disposition:
      - id: cpp-token-v1:comparison-boundary:42:17:0123456789abcdef
        result: excluded
        reason: Validator guarantee makes the changed branch unreachable
  disagreements: []
  residual_risks:
    - target Linux time limit still requires final calibration
  verification_complete: true
  delivery_state: SEALED

至少记录:

  • requested/effective mode 与选择理由;
  • 全部升级历史;
  • 审查角色、允许上下文、产物、独立性依据和结论;
  • 证明/实现/Checker 分歧及其解决证据;
  • Judge、stress、oracle、seal/build、验包和 PDF QA 的命令与结构化结果;
  • 完整模式 mutation 的 applicability、候选/执行计数、requested/effective jobs、survivor 处置和未完成原因;
  • 自动验证与人工/Agent 判断的边界;
  • 未完成项、平台边界和剩余风险。

verification_complete: true 只表示所选有效模式的契约已执行,不表示本地结果能够保证目标 Linux/DOMjudge 行为,也不替代 Core 的 Manifest、status 或 package verification。

10. 并行出题与正式构建

并行、checkpoint、seal、generation 和正式批量 build 的权威流程见 generations.md。本模式只保留交接边界:每个任务使用冻结审查快照并只修改自己的题目目录;完成所选验证模式后执行 seal,记录 delivery_state: SEALED,不等待其他题;整场交付再由一个任务执行多 ID build。任何 generation、发布或清理失败都必须保留未完成状态,不能冒充 FORMALLY_BUILTQA_DONE