---
title: "CAPRI: Contract-Aware Proof Repair for 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","Contract-Aware Repair","Large Language Models"]
---

# CAPRI: Contract-Aware Proof Repair for Isabelle

## AI commentary

> What stands out most is the separation of 'what is allowed to change' from 'whether the change is correct' — a design that is closer to real engineering needs than merely optimizing repair success rates. For Isabelle users and AI code generation developers, CAPRI's auditing mechanism and restricted interface approach offer directly relevant insights.

## At a glance

CAPRI presents a contract-aware proof repair workflow for Isabelle, where Isabelle checks the proof and an independent checker enforces a machine-readable edit contract to ensure large language models only modify developer-authorized content. The system retains prompts, proposals, candidate repositories, diagnostics, verdicts, and hashes for audit. The study evaluates five workflows on twelve failed proofs from four developments, with three replicates per task and condition, totaling 180 runs and 138 valid repairs. A proof-body-only interface achieved 29/36 valid repairs with zero contract violations, compared to 31/36 for the corresponding full-theory workflow. One-shot repair produced 22/36, while a later prospectively frozen iterative workflow produced 32/36. The results indicate that restricting edits to the proof body provides a favorable balance of effectiveness and safety.

## Key points

- CAPRI uses an independent checker to enforce a machine-readable edit contract, preventing LLMs from modifying protected text.
- Of 144 terminal candidates accepted by Isabelle, six had modified protected text, all arising from iterative workflows that could edit a complete theory.
- A proof-body-only interface produced 29/36 valid repairs with no contract violations, outperforming the full-theory workflow in safety under comparable settings.
- One-shot repair achieved 22/36, and a prospectively frozen iterative workflow achieved 32/36; the Sol configuration with matched demonstrations reached 33/36, but the difference from the frozen OpenAI Responses condition was not statistically significant.

## Full text

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

---

Verify against the original before citing; curated by Astral Feed: https://feed.astralor.com/items/itm_5a6590962c8963efc49c0484