LeanPolish: Verified Supervision for Lean Proof Compression
cs.LG
Submitted: 2026-09-29
Updated: 2026-09-29
Code: https://github.com/paulinebourigault/leanpolish
Sources
- Learn from Failure: Fine-Tuning LLMs with Trial-and-Error Data for Intuitionistic Propositional Logic Proving
- Learning to superoptimize programs
- Meta Large Language Model Compiler: Foundation Models of Compiler Optimization
- Herald: A Natural Language Annotated Lean 4 Dataset
- APOLLO: Automated LLM and Lean Collaboration for Advanced Formal Reasoning
- Formal Mathematics Statement Curriculum Learning
- Learning Performance-Improving Code Edits
- BFS-Prover: Scalable Best-First Tree Search for LLM-based Automatic Theorem Proving
Related papers
- Polynomial-Augmented Neural Networks (PANNs) with Weak Orthogonality Constraints for Enhanced Function and PDE Approximation
- AIRL-S: Unifying Reinforcement Learning and Search-Based Test-Time Scaling via Adversarial Inverse Reinforcement Learning
- Transformers as Bayesian In-Context Experimenters: Smoothness-Adaptive Efficient ATE Estimation
- Convergence issues in Relational Concept Analysis based on AOC-posets
- Beliefs Beyond Posteriors: The Predictive Cost of ELBO Binding
- Understanding Diffusion Models via Ratio-Based Function Approximation with SignReLU Networks