Proof-Refactor: Refactoring Generated Formal Proofs into Modular Artifacts
The paper titled 'Proof-Refactor' addresses the challenges in generating formal proofs using Large Language Models (LLMs). It proposes a framework that enhances the readability and modularity of these proofs through a process-guided approach. The results indicate significant improvements in proof structure without prioritizing length as the main objective.
- ▪Large Language Models often produce formal proofs that lack readability and modularity.
- ▪The proposed framework, Proof-Refactor, decomposes proof refactoring into four phases.
- ▪Experimental results show that Proof-Refactor improves rubric-based refactoring scores significantly.
Opening excerpt (first ~120 words) tap to expand
Computer Science > Artificial Intelligence arXiv:2606.03743 (cs) [Submitted on 2 Jun 2026] Title:Proof-Refactor: Refactoring Generated Formal Proofs into Modular Artifacts Authors:Yiming Fu, Peixuan Liu, Zichen Wang, Kun yuan View a PDF of the paper titled Proof-Refactor: Refactoring Generated Formal Proofs into Modular Artifacts, by Yiming Fu and 3 other authors View PDF HTML (experimental) Abstract:While Large Language Models (LLMs) have shown strong performance in generating formal proofs, their outputs often remain less readable, modular, maintainable, and reusable than proofs in mature formal mathematics libraries.
…
Excerpt limited to ~120 words for fair-use compliance. The full article is at arXiv cs.AI.
Discussion
0 commentsMore from arXiv cs.AI
