---
title: "CAPRI：面向 Isabelle 的合同感知证明修复方法"
source: "arXiv AI/CL/LG（论文）"
source_tier: "t2"
url: "https://arxiv.org/abs/2608.13459v1"
permalink: "https://feed.astralor.com/items/itm_5a6590962c8963efc49c0484"
published: "2026-08-13T16:43:44.000Z"
score: 77
channel: "ai"
tags: ["CAPRI","Isabelle","合同感知修复","大语言模型"]
---

# CAPRI：面向 Isabelle 的合同感知证明修复方法

## AI 点评

> 这篇论文最值得关注的是把“允许改什么”和“改得对不对”分开验证，这种设计比单纯追求修复成功率更贴近真实工程需求。对 Isabelle 用户和做 AI 代码生成的开发者来说，CAPRI 的审计机制和受限接口思路有直接参考价值。

## 速览

CAPRI 提出一种合同感知的 Isabelle 证明修复工作流：由 Isabelle 验证证明，同时由独立检查器执行机器可读的编辑合同，确保大语言模型只修改开发者授权的内容。系统保留提示、提案、诊断、判定和哈希以供审计。研究在四个开发项目的 12 个失败证明上评估五种工作流，共 180 次运行和 138 次有效修复。其中仅允许修改证明体的接口实现了 29/36 的有效修复且无合同违规，而一次性修复为 22/36，前瞻冻结迭代工作流为 32/36。比较结果显示，证明体受限接口在安全性与有效性上均有优势。

## 关键点

- CAPRI 使用独立检查器强制执行机器可读的编辑合同，防止 LLM 修改受保护文本。
- 在所有 144 个被 Isabelle 接受的候选证明中，有 6 个修改了受保护文本，全部来自可编辑完整理论的迭代工作流。
- 仅允许修改证明体的接口获得 29/36 有效修复且无合同违规，优于同条件下的完整理论工作流的安全性表现。
- 一次性修复为 22/36，前瞻冻结迭代工作流为 32/36；Sol 配置匹配演示后为 33/36，但与冻结 OpenAI Responses 的差异未达统计显著。

## 全文

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$).

---

引用前请核对原文;本文由星际流动整理:https://feed.astralor.com/items/itm_5a6590962c8963efc49c0484