Image de couverture de livre

Premise Selection for a Lean Hammer

Fuente: arXiv

Enregistré dans:

Détails bibliographiques
Auteurs principaux:	Zhu, Thomas, Clune, Joshua, Avigad, Jeremy, Jiang, Albert Qiaochu, Welleck, Sean
Format:	Preprint
Publié:	2025
Sujets:	Machine Learning Artificial Intelligence Logic in Computer Science
Accès en ligne:	Acceder al recurso
Tags:	Ajouter un tag Pas de tags, Soyez le premier à ajouter un tag!

Documents similaires

ImProver 2: Iteratively Self-Improving LMs for Neurosymbolic Proof Optimization
par: Ahuja, Riyaz, et autres
Publié: (2026)

Magnushammer: A Transformer-Based Approach to Premise Selection
par: Mikuła, Maciej, et autres
Publié: (2023)

LeanArchitect: Automating Blueprint Generation for Humans and AI
par: Zhu, Thomas, et autres
Publié: (2026)

Combining Textual and Structural Information for Premise Selection in Lean
par: Petrovčič, Job, et autres
Publié: (2025)

Lean-auto: An Interface between Lean 4 and Automated Theorem Provers
par: Qian, Yicheng, et autres
Publié: (2025)

DSLean: A Framework for Type-Correct Interoperability Between Lean 4 and External DSLs
par: Rowney, Tate, et autres
Publié: (2026)

Hint-Based SMT Proof Reconstruction
par: Clune, Joshua, et autres
Publié: (2026)

Lean Copilot: Large Language Models as Copilots for Theorem Proving in Lean
par: Song, Peiyang, et autres
Publié: (2024)

LeanAgent: Lifelong Learning for Formal Theorem Proving
par: Kumarappan, Adarsh, et autres
Publié: (2024)

Discovering New Theorems via LLMs with In-Context Proof Learning in Lean
par: Kasaura, Kazumi, et autres
Publié: (2025)

Herald: A Natural Language Annotated Lean 4 Dataset
par: Gao, Guoxiong, et autres
Publié: (2024)

REAL-Prover: Retrieval Augmented Lean Prover for Mathematical Reasoning
par: Shen, Ziju, et autres
Publié: (2025)

Lean Meets Theoretical Computer Science: Scalable Synthesis of Theorem Proving Challenges in Formal-Informal Pairs
par: Zhang, Terry Jingchen, et autres
Publié: (2025)

Machine Learning for Quantifier Selection in cvc5
par: Jakubův, Jan, et autres
Publié: (2024)

BAIT: Benchmarking (Embedding) Architectures for Interactive Theorem-Proving
par: Lamont, Sean, et autres
Publié: (2024)

Canonical for Automated Theorem Proving in Lean
par: Norman, Chase, et autres
Publié: (2025)

Approximating Pareto Frontiers in Stochastic Multi-Objective Optimization via Hashing and Randomization
par: Li, Jinzhao, et autres
Publié: (2026)

Lean Refactor: Multi-Objective Controllable Proof Optimization via Agentic Strategy Search
par: Lu, Jialin, et autres
Publié: (2026)

PiShield: A PyTorch Package for Learning with Requirements
par: Stoian, Mihaela Cătălina, et autres
Publié: (2024)

LeanCat: A Benchmark Suite for Formal Category Theory in Lean (Part I: 1-Categories)
par: Xu, Rongge, et autres
Publié: (2025)

Llemma: An Open Language Model For Mathematics
par: Azerbayev, Zhangir, et autres
Publié: (2023)

Inference of Abstraction for a Unified Account of Reasoning and Learning
par: Kido, Hiroyuki
Publié: (2024)

SFT-GRPO Data Overlap as a Post-Training Hyperparameter for Autoformalization
par: Su, Xiaole, et autres
Publié: (2026)

THEIA: Learning Complete Kleene Three-Valued Logic in a Pure-Neural Modular Architecture
par: Li, Augustus Haoyang
Publié: (2026)

Towards Compositional Interpretability for XAI
par: Tull, Sean, et autres
Publié: (2024)

Constraint-aware Learning of Probabilistic Sequential Models for Multi-Label Classification
par: Buleshnyi, Mykhailo, et autres
Publié: (2025)

P2C: Path to Counterfactuals
par: Dasgupta, Sopam, et autres
Publié: (2025)

Autonomous Code Evolution Meets NP-Completeness
par: Yu, Cunxi, et autres
Publié: (2025)

The Logical Expressiveness of Temporal GNNs via Two-Dimensional Product Logics
par: Sälzer, Marco, et autres
Publié: (2025)

Comparing Neural Network Encodings for Logic-based Explainability
par: Carvalho, Levi Cordeiro, et autres
Publié: (2025)

Expressive Temporal Specifications for Reward Monitoring
par: Adalat, Omar, et autres
Publié: (2025)

Abduction of Domain Relationships from Data for VQA
par: Chowdhury, Al Mehdi Saadat, et autres
Publié: (2025)

Symbolic Knowledge Extraction and Injection with Sub-symbolic Predictors: A Systematic Literature Review
par: Ciatto, Giovanni, et autres
Publié: (2025)

On Trustworthy Rule-Based Models and Explanations
par: Siala, Mohamed, et autres
Publié: (2025)

Fully Geometric Multi-Hop Reasoning on Knowledge Graphs with Transitive Relations
par: Zhapa-Camacho, Fernando, et autres
Publié: (2025)

Regional, Lattice and Logical Representations of Neural Networks
par: Preto, Sandro, et autres
Publié: (2025)

Neural DNF-MT: A Neuro-symbolic Approach for Learning Interpretable and Editable Policies
par: Baugh, Kexin Gu, et autres
Publié: (2025)

Proceedings The 13th International Workshop on Theorem proving components for Educational software
par: Narboux, Julien, et autres
Publié: (2025)

Neural Logic Networks for Interpretable Classification
par: Perreault, Vincent, et autres
Publié: (2025)

Halting Recurrent GNNs and the Graded $μ$-Calculus
par: Bollen, Jeroen, et autres
Publié: (2025)