CAPRI：Isabelle 的合同感知证明修复

我们解决了使用 大语言模型 (LLM) 来帮助发现 Isabelle 证明的问题。 Isabelle 构建表明所提交的理论已被接受，但 LLM 并不仅更改开发人员授权的内容。我们提出了 CAPRI，一种合同感知修复工作流程，其中 Isabelle 检查校样，并由独立检查员强制执行机器可读的编辑合同。保留提示、建议、候选存储库、诊断、结论和哈希以供审计。我们评估来自四个开发的 12 个失败证明的五个工作流程，每个任务和条件进行 3 个重复，给出 180 次运行和 138 次有效修复。在伊莎贝尔接受的 144 名最终候选人中，有 6 名修改了受保护的文本；所有这些都出现在可以编辑完整理论的迭代工作流程中。仅证明主体接口产生了 29/36 的有效修复且没有违反合同，而相应的全理论工作流程为 31/36。一次性修复产生了 22/36，而后来的前瞻性冻结迭代工作流程产生了 32/36；这些数字比较了完整的工作流程而不是单个机制。一项单独的事后 OpenRouter 活动发现与指定的 Luna 比较没有任何改进。具有匹配演示的 Sol 配置产生了 33/36 的修复，而冻结 OpenAI 响应条件下的修复为 29/36，但在单侧精确 McNemar 测试中，差异并不具有统计显着性 ($p=0.0625$)。