CAPRI: Contract-Aware Proof Repair for Isabelle
作者: Jim Woodcock, Gabriel Leite, Augusto Sampaio, Ran Wei
分类: cs.SE, cs.AI, cs.LO
发布日期: 2026-08-13
备注: 17 pages, 1 figure, 7 tables. Submitted to SBMF 2026. Reproducibility artefact available on Zenodo
💡 一句话要点
提出CAPRI以解决Isabelle证明中的合同意识问题
🎯 匹配领域: 支柱九：具身大模型 (Embodied Foundation Models)
关键词: 大型语言模型 形式化验证 合同意识 自动证明 软件开发 Isabelle 修复工作流
📋 核心要点
- 现有方法无法确保大型语言模型在修改证明时遵循开发者的授权，导致潜在的合同违反问题。
- CAPRI通过引入合同意识的修复工作流，结合Isabelle的证明检查和独立的合同执行，确保修改的合规性。
- 实验结果显示，使用不同工作流的有效修复率有所不同，某些工作流在合同遵循方面表现优异，提供了新的研究方向。
📝 摘要（中文）
本文探讨了利用大型语言模型（LLMs）辅助发现Isabelle证明的过程。虽然Isabelle构建可以确认提交的理论被接受，但并不能保证LLM仅修改开发者授权的部分。为此，本文提出了CAPRI，一个合同意识的修复工作流，其中Isabelle检查证明，而独立检查器强制执行机器可读的编辑合同。我们评估了五种工作流在四个开发中的十二个失败证明上的表现，进行了180次实验，得到了138个有效修复。结果显示，某些工作流在合同遵循方面表现优异，提供了对未来研究的启示。
🔬 方法详解
问题定义：本文旨在解决在使用大型语言模型辅助Isabelle证明时，如何确保模型修改的合规性问题。现有方法未能有效控制模型的修改范围，可能导致合同违反。
核心思路：CAPRI的核心思路是引入合同意识的修复工作流，通过Isabelle进行证明检查，并使用独立的检查器来执行机器可读的编辑合同，从而确保修改的合规性。
技术框架：CAPRI的整体架构包括多个模块：首先是输入的证明理论，然后是Isabelle的证明检查模块，接着是独立的合同执行模块，最后是审计记录的保留机制，确保每一步的透明性和可追溯性。
关键创新：CAPRI的主要创新在于引入了合同意识的概念，使得在使用LLM进行证明修复时，能够有效地控制和审计修改的内容，避免了传统方法中的合规性问题。
关键设计：在设计中，CAPRI使用了多种工作流，包括全理论和仅证明体的接口，实验中对不同工作流的表现进行了比较，确保了合同遵循的有效性。
🖼️ 关键图片
📊 实验亮点
实验结果显示，在180次实验中，CAPRI实现了138个有效修复，其中某些工作流在合同遵循方面表现优异。例如，使用仅证明体接口的工作流达到了29/36的有效修复率，而全理论工作流为31/36，显示出不同工作流在合同遵循上的差异。
🎯 应用场景
CAPRI的研究成果在形式化验证、自动证明和软件开发等领域具有广泛的应用潜力。通过确保修改的合规性，CAPRI可以帮助开发者在使用大型语言模型时，保持对证明过程的控制，提升软件的可靠性和安全性。未来，CAPRI的理念和方法可以扩展到其他形式化系统和自动化工具中，推动智能合约和自动验证技术的发展。
📄 摘要（原文）
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$).