CAPRI: Contract-Aware Proof Repair for Isabelle
CAPRI adds an edit contract around LLM proof repair, catching changes Isabelle alone would accept.
The workflow keeps Isabelle as the proof checker while a separate checker enforces what parts of the theory the model was allowed to modify. In the evaluation, six Isabelle-accepted terminal candidates changed protected text, all from iterative workflows with full-theory edit access. A proof-body-only interface avoided contract violations while producing 29 valid repairs out of 36. The paper reports 180 runs across five workflows and includes retained prompts, diagnostics, verdicts, hashes, and a Zenodo reproducibility artefact. ArXiv · AI/CL/LG's note
The workflow keeps Isabelle as the proof checker while a separate checker enforces what parts of the theory the model was allowed to modify. In the evaluation, six Isabelle-accepted terminal candidates changed protected text, all from iterative workflows with full-theory edit access. A proof-body-only interface avoided contract violations while producing 29 valid repairs out of 36. The paper reports 180 runs across five workflows and includes retained prompts, diagnostics, verdicts, hashes, and a Zenodo reproducibility artefact. ArXiv · AI/CL/LG's note
score 5