这论文搞了个 CAPRI 工具，管 LLM 改 Isabelle 证明，能查它有没有动不该动的地方。12 个失败证明跑 180 次，修复率直观看得很清楚，想用 LLM 做形式化证明的可以看看。
CAPRI 是一种面向 Isabelle 证明的契约感知修复工作流，由 Isabelle 检查证明，独立检查器执行机器可读的编辑契约。研究在四个开发项目的十二个失败证明上评估了五种工作流，每任务三份复现，共 180 次运行和 138 次有效修复。其中 144 个被 Isabelle 接受的候选修复有六个修改了受保护文本，均来自可编辑完整理论的迭代工作流。仅限证明体的接口得到 29/36 个有效修复且无契约违规，而对应完整理论工作流为 31/36。
CAPRI: Contract-Aware Proof Repair for Isabelle
We address the use of large language models (LLMs) to help discover Isabelle proofs. An Isabelle build establishes that the submitted theory is accepted, but not that an LLM changed only what the developer authorised. We present CAPRI, a contract-aware repair workflow in which Isabelle checks the proof and an independent checker enforces a machine-readable edit contract. Prompts, proposals, candidate repositories, diagnostics, verdicts, and hashes are retained for audit. We evaluate five workflows on twelve failed proofs from four developments, with three replicates per task and condition, giving 180 runs and 138 valid repairs. Of 144 terminal candidates accepted by Isabelle, six had modified protected text; all arose in iterative workflows that could edit a complete theory. A proof-body-only interface produced 29/36 valid repairs and no contract violations, compared with 31/36 for the corresponding full-theory workflow. One-shot repair produced 22/36, while a later prospectively frozen iterative workflow produced 32/36; these figures compare complete workflows rather than individual mechanisms. A separate post hoc OpenRouter campaign found no improvement in the designated Luna comparisons. A Sol configuration with matched demonstrations produced 33/36 repairs, compared with 29/36 in the frozen OpenAI Responses condition, but the difference was not statistically significant in a one-sided exact McNemar test ($p=0.0625$).