Abstract:
Changes to theorem provers and libraries can break proof scripts whose statements remain provable, and large language models (LLMs) are now used to repair them. We study proof-only repair in Isabelle/HOL, where only the proof body may be edited, so that the prover can check whether a repair establishes the unchanged statement. We present ProofMend, a benchmark of 600 tasks mined from the Archive of Formal Proofs across three Isabelle version updates, each with a checked proof-only solution. Its evaluator replays each submission independently of the repair system and checks its edit scope, proposition, and proof dependencies. Our tool-assisted repair method, ProofScout, lets an LLM retrieve facts and test proofs in the target environment. With GPT-5.6 Sol, it repairs 88.3% of the tasks, a rate higher than that of a direct repair baseline (68.2%) and comparable to that of Codex (85.2%), at less than 40% of their estimated API cost per valid repair. Across all evaluated configurations, independent validation rejects 29 submissions that replay successfully but rely on prohibited oracles or on earlier lemmas that are false in the target environment, and 73 of Codex’s 573 self-reported successes fail validation.
Bio:
Xiaokun Luan is a Research Fellow at the School of Computing, National University of Singapore, working with Prof. Jin Song Dong. Xiaokun received a Ph.D. in Applied Mathematics from Peking University. Xiaokun's research lies at the intersection of trustworthy AI and formal methods, with a focus on reliable and safe agentic AI, and AI for formal reasoning. His work has appeared at venues including FSE, ICSE, POPL, NDSS, ICML, and ICLR, and has received an ACM SIGSOFT Distinguished Paper Award (FSE 2025) and a Best Paper Award (ICFEM 2025).
