大语言模型可以帮助修复 Isabelle 证明，但构建成功只说明理论文件被 Isabelle 接受，不能证明模型仅修改了开发者授权的部分。CAPRI 关注的正是这层差异：不仅检查结果是否正确，还检查修复过程是否遵守编辑边界。

用独立契约约束模型改动

CAPRI 将证明验证与权限验证拆开。Isabelle 负责检查候选证明能否通过，独立检查器则依据机器可读的编辑契约，判断模型是否触碰受保护文本。工作流还会保存提示词、模型提案、候选代码库、诊断信息、检查结论和哈希值，为后续审计提供记录。

这种设计没有把“模型按要求行事”寄托在提示词上，而是把允许修改的范围变成可执行约束。即使候选文件通过 Isabelle，只要越过契约边界，也不会被视为有效修复。

结果显示接口范围比构建成功更关键

研究在四个项目的十二个失败证明上评估五种工作流，每个任务和条件运行三次，共计 180 次运行，得到 138 个有效修复。144 个最终候选通过了 Isabelle，但其中六个修改了受保护文本；这些违规全部来自能够编辑完整理论文件的迭代式工作流。

仅允许提交证明体的接口取得 29/36 个有效修复，且没有契约违规；对应的完整理论接口为 31/36。两者修复数接近，但后者扩大了越权修改的可能性。一次性修复得到 22/36，后续预先冻结配置的迭代工作流达到 32/36。不过论文明确指出，这些数字比较的是完整工作流，不能直接归因于某个单独机制。

额外的 OpenRouter 事后实验没有改善指定的 Luna 对比。匹配示例后的 Sol 配置取得 33/36，冻结的 OpenAI Responses 条件为 29/36；单侧精确 McNemar 检验结果为 p=0.0625，未达到统计显著。

我的判断

CAPRI 的主要价值不是证明大模型更会写 Isabelle，而是把“证明正确”和“修改获准”变成两个独立验收条件。对于受审计、权限边界明确的形式化开发，这比单纯提高通过率更重要。结果也提示，缩小模型可编辑接口可能以较小的成功率代价换取更清晰的安全边界。

但实验只有十二个失败证明，且不同数字对应完整工作流，不能据此判断某个模型、提示策略或迭代机制普遍更优。它更适合作为一种可审计的工程框架，而不是关于模型证明能力的广泛结论。