Sage: Formalization with Semantic Correction
cs.LG, cs.AI, cs.CL, cs.LO
Submitted: 2026-09-16
Updated: 2026-09-30
Terminology
Sources
- Faults in Our Formal Benchmarking: Dataset Defects and Evaluation Failures in Lean Theorem Proving
- Goedel-Prover-V2: Scaling Formal Theorem Proving with Scaffolded Data Synthesis and Self-Correction
- FIMO: A Challenge Formal Dataset for Automated Theorem Proving
- Process-Driven Autoformalization in Lean 4
- DeepSeek-Prover-V2: Advancing Formal Mathematical Reasoning via Reinforcement Learning for Subgoal Decomposition
- Code Generation with AlphaCodium: From Prompt Engineering to Flow Engineering
- Aria: An Agent For Retrieval and Iterative Auto-Formalization via Dependency Graph
- Lean Workbook: A large-scale Lean problem set formalized from natural language math problems
- Beyond Compilation: Evaluating Faithful Natural-Language-to-Lean Statement Formalization
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: Local-Consistency Optimisation for Bayesian Neural Networks
- Understanding Diffusion Models via Ratio-Based Function Approximation with SignReLU Networks