Showing cs.AIShow all
2 papers · 1 filter
cs.AI2026
ImProver 2: Iteratively Self-Improving LMs for Neurosymbolic Proof Optimization
Riyaz Ahuja, Tate Rowney, Jeremy Avigad +1
Formal mathematics libraries are rapidly expanding, creating a growing need to refactor verified proofs for maintainability and to improve training data quality for neural provers.…
cs.AI2026
ImProver: Agent-Based Automated Proof Optimization
Riyaz Ahuja, Jeremy Avigad, Prasad Tetali +1
Large language models (LLMs) have been used to generate formal proofs of mathematical theorems in proofs assistants such as Lean. However, we often want to optimize a formal proof…