ProofCoder把证明搜索交给智能体：Rocq验证成功率从47%升到60%，推理成本约减半
核心概要
面向Rocq软件验证的证明合成系统ProofCoder不再让外部控制器规定何时检索前提、回退或修补，而是让模型在每次工具调用前写下对当前证明状态的判断，并据此决定继续、查证还是回退到某一行。在AutoRocq基准的280个验证引理上，最佳配置把证明成功率从AutoRocq的47%提高到60%，推理成本约为后者一半；去掉连续推理后，智能体解出的引理更少、成本更高，回退次数多出四到六倍。
深度剖析
ProofCoder把交互式定理证明改造成类似编码智能体的编辑—反馈循环，模型自己决定何时检索、查看证明状态、修改脚本或回退到更早位置。 此前的LLM证明系统把模型放在控制器驱动的搜索循环里，由外部算法决定何时检索上下文、回退或修补；AutoRocq虽已让模型选择规划、生成策略和查询环境的工具，但仍受半约束协议限制。 在AutoRocq基准的280个验证引理上，最佳配置的证明成功率从AutoRocq的47%提高到60%，推理成本约为其一半。
证明脚本被当作可编辑的产物，智能体通过少量工具读写它，并在每次动作前用自然语言说明自己对当前目标与失败原因的判断。 工具接口把只读操作与唯一的写操作分开：check_state重放到指定策略行返回证明状态，call_command执行Search、Print、Locate等Rocq命令，read_proof_file读取工作区文件，edit_proof保留前n行并追加新片段。 实验在SV-COMP的200个引理与Linux内核Verker的80个引理上进行，使用claude-sonnet-4.5和gpt-6-sol两个模型，温度设为0，单次尝试以20万非缓存token为主要预算。
消融显示连续推理与局部修补是收益的主要来源，其中局部修补的影响更大。 去掉连续推理后，策略级配置在SV-COMP上从119个引理降到115个、在Verker上从46降到40，成本在两个数据集上都翻倍以上；把局部修补换成失败即从头重启，整证明配置在SV-COMP上从120降到81、在Verker上从48降到24。 这些消融使用gpt-6-sol运行，并与同一OpenCode基础设施下的其他ProofCoder变体对照，以隔离框架差异。
启示与展望
结果覆盖AutoRocq基准中按项数复杂度选取的200个SV-COMP引理和80个Verker内核引理，使用claude-sonnet-4.5与gpt-6-sol两个模型，单次尝试以20万非缓存token为主预算，并设5M token与30分钟上限。作者把在更多证明助手和验证相关语言上评估、以及更丰富的验证器交互与多智能体协作证明搜索列为后续工作。
SV-COMP子集没有标准证明，因此不能确定全部引理可证，作者只确认其中88个在原AutoRocq评测中被AutoRocq或其基线解出。ProofCoder与AutoRocq使用不同的智能体框架，上下文管理与工具调用序列化等差异可能影响表现。在Verker上使用claude-sonnet-4.5时，ProofCoder两个配置解出的循环不变式引理都少于AutoRocq，且仍有少量引理仅由AutoRocq解出。