CAPRI: Contract-Aware Proof Repair for Isabelle

Jim Woodcock, Gabriel Leite, Augusto Sampaio +1

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 change…