神经交互证明

如何让计算受限但可信的 verifier 学会与更强、不可信的 prover 交互，从而可验证地解决给定决策问题。

• 场景：作者认为大模型输出难信任，限制高风险使用；传统验证扩展不到当今最强系统（第1节）。交互式证明允许受限但可信的 verifier 借助更强但不可信的 prover，并限制被误导的机会。
• 现有不足：作者认为 Anil 等（2021）的协议所得证明系统形式强度有限，且只用于小模型；Irving 等（2018）与 Wäldchen 等（2024）理论更强，但只用于很简单的问题。近期语言模型工作或未按协议训练，或只训 Anil 协议，或限于问答。
• 假设：作者受 Gowal 等（2019）启发，认为 verifier 若能学习协议，这类思想更能扩展到真实机器学习系统（第1.3节）。
• 本文提出：统一的 prover-verifier game 框架、含零知识在内的新协议、新旧协议的理论比较，以及图同构与代码验证实验。
• 威胁模型：
  • 任务：输入 x 来自分布 P，verifier 最终输出是否 x 属于正例集 S，并与真标签比较。例1是规格说明与代码是否匹配。
  • 不对称：verifier 计算受限但可信，且单独不能解题；任一 prover 能解题。双方目标不完全一致（Definition 6）。
  • 交互：按 messaging game 的通道与轮次交换消息；某个 verifier 在特殊通道输出接受或拒绝。
  • 有效性：completeness 要求正例被接受的概率至少 1−εc；soundness 要求对任意 prover，负例被拒绝的概率至少 1−εs，且 εc+εs<1（Definition 2）。

神经 prover-verifier 与辩论

• Anil 等（2021）提出神经网络之间的 prover-verifier game。作者认为其证明系统形式强度有限，且只用于小模型和小问题。
• Irving 等（2018）的 debate 与 Wäldchen 等（2024）的 Merlin-Arthur classifier 使用两个相互竞争的 prover。作者认为二者理论更强，但仍只用于很简单的问题。
• Michael 等（2023）与 Khan 等（2024）研究辩论能否帮助监督不可靠专家。论文只作背景描述，未在此展开与本文的数值对比。

语言模型上的可扩展监督

• Kenton 等（2024）在问答之外比较多 prover 的 debate 与单 prover 的 consultancy，并考虑计算不对称。该文发现 debate 优于 consultancy，但相对 verifier 基线收益有限；该文作者假设原因之一是未用协议训练模型。
• Kirchner 等（2024）用多轮强化学习训练 Anil 等（2021）的协议。该文报告 helpful prover 的准确率与 verifier 对对抗攻击的鲁棒性在训练中上升，主要关注输出对人类的可读性。本文作者指出该协议有理论限制。
• Arnesen 等（2024）比较多种协议，并用 Direct Preference Optimisation 的变体训练 prover，但限于问答。该文发现优化 prover 会提高 debate 中的 verifier 准确率，而 consultancy 不会。

证明系统理论

• Goldwasser 等（1985）定义交互式证明；Shamir（1992）给出 IP=PSPACE。Ben-Or 等（1988）等把设定扩到多 prover。
• Brown-Cohen 等（2024）研究 doubly efficient debate：在适当假设下，多项式时间计算可用常数次人类判断查询来验证。
• Goldwasser 等（2020）的 PAC verification 与 Amit 等（2024）的 self-proving models 关注证明模型或输出正确。作者指出这两项使用手工证明系统，而非学习得到的协议。

基线与数据集：实验基线包括 Anil 等的 adp、Irving 等的 debate、Wäldchen 等的 mac，以及单独训练的 verifier、随机 prover。数据为合成图同构，以及由 APPS（Hendrycks 等，2021）构造的代码验证集。

作者把本文与上述近期实证工作区分开：本文同时考察不同协议的理论含义；并认为相对手工证明系统，让 verifier 学习协议更可能扩展到真实系统。

作者把神经交互式证明写成 prover-verifier game（PVG）：智能体学习发消息，均衡被要求对应有效证明系统，而不是手工指定证明步骤。

决策问题与证明系统

• 对象：概率决策问题 (X, S, P)。例1中 X 是规格说明–代码对，S 是代码满足规格的对。
• 交互：prover 与 verifier 的消息空间分别为 M^p、M^v。序列长度 T 由 verifier 决定，末条消息 mT 为接受或拒绝。
• 逐样本损失：verifier 要降低 ℓ(σ,x):=𝔼_σ[m_T≠ y]，即决策与标签不一致的概率。经验风险 LER 对数据集取平均；最坏情况损失 LWC 取数据集上的最大损失。
• 零知识：对每个 verifier 变体，存在同属弱策略类的模拟器，使正例上的消息分布统计接近。作者还采用更强条件：对任意标签都要求统计接近。

广义 PVG 与协议

• 博弈：np 个 prover 与 nv 个 verifier 在通道上发消息，只能看见自己所在通道，且不能在通道成员之外识别发送者。输入 x 作为共同观察。
• 四条要求：决策 verifier 要输出真标签；verifier 单独不能解题；任一 prover 能解题；双方目标不完全一致（Definition 6）。
• adp 的反例：Proposition 7 给出一个决策问题和 adp 博弈，其中存在 εc=0 的有效协议，但 verifier 领导的 Stackelberg 均衡对该有效性既非必要也非充分。作者以此转向新协议。
• nip：一个 prover、一个 verifier，按轮交替发消息。损失把正例与负例的最坏情况分开：prover 最小化 L^p(σ)=L^WC(σ∣ y=1)−L^WC(σ∣ y=0)，verifier 最小化两项之和。定理8陈述：在存在有效证明系统时，策略是有效 IP 当且仅当它是该博弈的近似 verifier 领导 Stackelberg 均衡。

Table 1 的协议对照如下。

Swipe horizontally to read the table

协议	Prover/Verifier	轮数	复杂度	零知识
adp	1/1	2	NP	否
debate	2/1	T	PSPACE	否
mac	2/1	2	MA	否
nip	1/1	T	PSPACE	否
mnip	2/1	T	NEXP	否
zk-nip	1/3	T	PSPACE	是
zk-mnip	2/3	T	NEXP	是

作者称在 prover 为全部图灵机、verifier 为概率多项式时间时，由定理8和 Shamir（1992）可得 nip 对应 PSPACE；论文写 Irving 等证明 debate 对应 PSPACE。附录 C 写 adp 在确定性 verifier 与零 soundness 误差下的对应，其强度受 εs=0 则问题属于 NP 这一事实限制。

最坏情况与均衡求解

• 经验风险何时够用：Proposition 9 给出两条件——最坏情况一致收敛，以及经验风险最小化者的经验最坏损失离经验最坏最小化者不远。满足时，足够大的数据集上，经验风险最小化者的真实最坏损失接近最优最坏损失。
• 对手：可增加策略空间为 S×(X\S) 的对手。Proposition 10 陈述：原 nip 的近似 verifier 领导均衡，当且仅当存在对手策略使三方策略成为新博弈的近似 verifier-prover 领导均衡。这要求对手能输出任意 x。
• Stackelberg：作者把求解写成双层优化，并用时间尺度分离；内层更快更新 prover。大参数下逆 Hessian 不可行时，可改用 LOLA，或在 LOLA 与 LookAhead 之间插值。论文给出这些更新形式，实验未使用它们。

多 prover 与零知识

• mnip：两个 prover 损失相同，交互期间不能通信，但可事先约定联合策略和共享随机信号。soundness 要求 verifier 对任意一对替代 prover 稳健。定理11把有效 MIP 对应到近似 verifier 领导的相关 Stackelberg 均衡。
• zk-nip：增加试图提取知识的 v2 和模拟器 v3，二者损失相反；并把模拟器损失加进 prover 损失。作者要 prover 在保持有效性的前提下再降低泄漏，并提到可用词典序目标实现。定理12只给一个方向：若策略是近似 verifier-prover 领导均衡，则它是有效的 εk 统计零知识 IP。v2、v3 的子博弈是零和，纳什均衡即可。
• zk-mnip：Table 1 列为两个 prover、三个 verifier、NEXP 且为零知识。正文未单独给出与定理12对应的陈述。

实验中的学习与判定

• 图任务：独立 PPO。成功看留出测试集上 verifier 决策是否匹配同构标签。
• 代码任务：八轮 expert iteration；每轮用此前全部 rollout 从头微调。另一方案在退火比例的 rollout 中把 verifier 猜测换成真标签。
• 判定：mT 与 y 比较。代码标签来自人类正确解，以及仍能编译但至少失败一个测试的改动解。附录 D.2.2 给出 nip 的系统提示词，此处不列措辞。

实验设置

• 数据：图同构为 Erdős-Rényi 合成的 10,000 张图，每张约十个顶点；训练/测试 80:20（第6.1节、附录 D.1）。代码验证基于 APPS；Table 2 写 4,877 题、每题两解，训练/测试 90:10。插入 bug 的中位 Levenshtein 距离为 7（附录 D.2.1）。
• 模型：图任务用 GIN、一层 transformer 和前馈头；prover 的 GIN 为五层，verifier 默认为两层，并改变宽度与层数。代码任务 prover 为 GPT-4o，verifier 为 GPT-4o-mini；bug 也由 GPT-4o-mini 插入。
• 协议：图任务直接比较 adp、debate、nip、mnip，对照为随机 prover，并考察 zk-nip。代码任务作者称测试了上文各协议，基线是单独训练的 verifier。附录 E.2 有 adp、debate、mac、nip、mnip 的转录。
• 训练：图任务独立 PPO，5,000 步、10 个 seed；裁剪 ε=0.2，γ=0.95，λ=0.95，熵系数 0.001，学习率 0.003。代码任务八轮 expert iteration，每轮用此前全部 rollout 从头微调，并按 10% 分批加入数据。
• 指标：留出集测试准确率；每测试点 10 次 rollout 中 verifier 总是猜错的比例；precision 与 recall。第6节写误差条为 10 个 seed 的一个标准差。
• 判定：决策对照真标签。主指标不是 LLM 裁判。附录 E.2.1 另用 GPT-4o-mini 分析转录。

主结果

正文没有写出 Figure 3 各柱的精确准确率，下表只保留正文中的原表述。

协议	相对单独 verifier 的测试准确率（Figure 3a）	总是猜错的比例（Figure 3b）
nip	作者称提升约 11%，与 mnip 同为最大	未报告
mnip	作者称提升约 11%，与 nip 同为最大	作者称最好，数值未报告
debate	未报告；作者称各协议都有改进	未报告
adp	未报告	未报告
mac	未报告	未报告
单独 verifier	基线，绝对准确率未报告	未报告

• 作者称所有被测协议的最终测试准确率都高于单独 verifier，nip 与 mnip 的提升最大（Figure 3a）。此处“约 11%”是提升幅度的原文说法，不是绝对准确率。
• 作者称多数协议的总是猜错比例优于单独 verifier，mnip 最好（Figure 3b）。Figure 3c 上，作者称 nip 与 mnip 的假阴性率低于其他协议，同时真阳性率高；正文未给 precision、recall 数字。
• 作者称 debate 与单独 verifier 的 precision 相对 recall 偏高，并把原因归到 expert iteration：只纳入 verifier 猜对的 rollout，放大了初始低接受率。

图同构：协议、规模与零知识

• 协议：作者称 nip 有利，verifier 与 prover 交互后对有效实例的分类达到原文所称 near-perfectly；adp、debate、mnip 未见提升（Figure 2a）。作者的解释是：存在较简单的做法，由 verifier 选一个节点、prover 在另一图返回相似节点；adp 中 verifier 不向 prover 发消息，多 prover 更难学。
• 模型规模：作者称更大模型能解该任务、更小不能；相对随机 prover，非随机 prover 带来能力增益，且在 verifier 单独不能解、学会交互后能解时最明显（Figure 2b）。正文未给准确率数字。
• zk-nip：作者改变 prover 损失中 Lv3 项的系数，称消息序列似然差与该系数大致负相关，并认为系数增大时训练收敛到信息泄漏更低的均衡（Figure 2c）。正文未给差值。

代码验证的训练方案

• 稳定化 expert iteration：prover 仍按原方案训练；verifier 在退火比例的 rollout 中把猜测换成真标签。该比例从 80% 线性降到 0%（附录 D.2.3）。
• 作者称这减轻了普通 expert iteration 的 mode collapse（Figure 4a），并使单独 verifier 的平均准确率高得多；作者假设是因为更接近标准监督微调。
• 作者称该方案对各交互协议的平均准确率影响小，有的升、有的降；每个协议的最差情况都改善，debate 尤其突出（Figure 4b、4c）。这些曲线的精确值未在正文给出。

其他消融与分析

• 训练集规模：Figure 5 作者称 NIP 测试准确率在规模 10,000 出现相变。
• verifier 的 GIN 深度：Figure 6 作者称 adp、debate、mnip 的性能随深度未见变化。
• 未训练的难度分层：Figure 8 作者称与 prover 交互的准确率在各 APPS 难度上都高于单独 verifier，且难度升高时准确率下降；正文未给数字。
• 逐点准确率直方图：Figure 9、10 作者称两种训练方案下，单独 verifier 的分布都收到两端；多数交互协议的分布相对不变。稳定化训练下，debate 从双峰散开，总是猜错的比例下降。正文未给比例。
• 转录分析：附录 E.2.1 用 GPT-4o-mini 判断是否守角色、是否跟进前文、是否引用以及引用是否完全准确，并画随轮次变化的比例。正文未给这些比例。
• 作者对 debate 偏低的主要假设是：有 prover 专门论证拒绝，且指出一处缺陷比论证整段代码无缺陷更容易，再加上单独 verifier 不愿接受可能有 bug 的代码。

作者指出的局限与后续方向

• 图同构实验的训练没有使用第4.1、4.2节中更进一步的方法；代码验证也没有用基于强化学习的学习。作者认为这使实证结果离理论对应更远（Discussion）。
• 协议只在两个领域评测。作者称这两个领域远不能代表当代 AI 系统可解决的任务范围（Discussion）。
• 未评测全部协议变体，例如同时发消息与顺序发消息的 debate，以及训练中 prover 自己选择论证哪一方结果的 open protocols（Discussion，引用 Kenton 等，2024）。
• 作者提出可利用该博弈框架和代码库开发、评测新协议，并认为新协议的理论或实证表现可能不同于本文协议（Discussion）。
• 作者提出另一方向：发展学习理论结果，而不是只基于图灵机等抽象计算模型的复杂度结果，以刻画学习智能体的计算能力与数据量如何影响弱智能体验证强智能体（Discussion）。

实验覆盖范围

• 实验有两个域：10,000 张合成图上的同构判定，以及 Table 2 所写 4,877 道、每题两解的代码验证题；后者由 APPS 构造。
• 图任务比较 adp、debate、nip、mnip，并以随机 prover 作对照；zk-nip 只改变 Lv3 系数。训练为独立 PPO，10 个 seed、5,000 步。
• 代码任务的 prover 为 GPT-4o、verifier 为 GPT-4o-mini，训练为八轮 expert iteration。附录 E.2 给出 adp、debate、mac、nip、mnip 的转录。
• 最差情况指标对每个测试点采样 10 次 rollout。第6节的误差条为 10 个 seed 的一个标准差。
• 正文未给出 Figure 3 各协议的精确准确率、precision 和 recall；Table 1 列出 zk-mnip，正文未报告其实验数字。主判定使用标签和测试用例，论文未报告评审与人工的一致性。

作者研究计算受限但可信的 verifier 如何学会与更强、不可信的 prover 交互，以便可验证地解决决策问题，并把它放在可扩展监督的背景下。

• 问题：大模型输出难直接信任，传统验证又难扩展。作者用交互式证明的 completeness 与 soundness 作为目标，要求 verifier 有标签数据、单独不能解题，而 prover 能解题且双方目标不完全一致。
• 框架：广义 prover-verifier game 统一已有协议。nip 把正例与负例的最坏情况损失分开；定理8陈述有效 IP 与近似 verifier 领导 Stackelberg 均衡等价。mnip 对应多 prover 证明，zk-nip 把模拟器损失加入 prover，以约束信息泄漏。Proposition 7 说明放宽假设后，adp 的均衡与有效性不再对应。
• 图同构：10,000 张约十顶点的合成图上，作者称 nip 有利，其他被比较协议未见提升，并把原因归到该任务的简单交互算法与协议限制。更大 verifier 能解、更小不能；zk-nip 中作者称泄漏相关的似然差随 prover 系数大致下降。
• 代码验证：GPT-4o 为 prover、GPT-4o-mini 为 verifier，数据为 4,877 题、每题两解。作者称各协议相对单独 verifier 都有改进，nip 与 mnip 的准确率提升约 11%，且 mnip 的总是猜错比例最好。普通 expert iteration 下 debate 与单独 verifier 偏向拒绝；把部分猜测换成真标签后，作者称各协议最差情况改善，debate 尤其突出。
• 作者的结论：这些结果加入了作者所称仍属初步的证据，即此类技术可能变得更可用，并可能受益于 AI 能力继续提高。作者同时认为当前训练未贴近理论分析，领域和协议变体也未评全，因而还不能把复杂度理论中的保证直接当成机器学习系统上的安全保证。