Cover Image

ImProver 2: Iteratively Self-Improving LMs for Neurosymbolic Proof Optimization

Fuente: arXiv

Saved in:

Bibliographic Details
Main Authors:	Ahuja, Riyaz, Rowney, Tate, Avigad, Jeremy, Welleck, Sean
Format:	Preprint
Published:	2026
Subjects:	Artificial Intelligence Computation and Language Machine Learning Logic in Computer Science
Online Access:	Acceder al recurso
Tags:	Add Tag No Tags, Be the first to tag this record!

Similar Items

DSLean: A Framework for Type-Correct Interoperability Between Lean 4 and External DSLs
by: Rowney, Tate, et al.
Published: (2026)

Premise Selection for a Lean Hammer
by: Zhu, Thomas, et al.
Published: (2025)

LeanArchitect: Automating Blueprint Generation for Humans and AI
by: Zhu, Thomas, et al.
Published: (2026)

REAL-Prover: Retrieval Augmented Lean Prover for Mathematical Reasoning
by: Shen, Ziju, et al.
Published: (2025)

Elenchus: Generating Knowledge Bases from Prover-Skeptic Dialogues
by: Allen, Bradley P.
Published: (2026)

Proof Recommendation System for the HOL4 Theorem Prover
by: Dekhil, Nour, et al.
Published: (2024)

Sound and Complete Neurosymbolic Reasoning with LLM-Grounded Interpretations
by: Allen, Bradley P., et al.
Published: (2025)

DeepSeek-Prover-V1.5: Harnessing Proof Assistant Feedback for Reinforcement Learning and Monte-Carlo Tree Search
by: Xin, Huajian, et al.
Published: (2024)

Proof of Thought : Neurosymbolic Program Synthesis allows Robust and Interpretable Reasoning
by: Ganguly, Debargha, et al.
Published: (2024)

Lean-auto: An Interface between Lean 4 and Automated Theorem Provers
by: Qian, Yicheng, et al.
Published: (2025)

STP: Self-play LLM Theorem Provers with Iterative Conjecturing and Proving
by: Dong, Kefan, et al.
Published: (2025)

Llemma: An Open Language Model For Mathematics
by: Azerbayev, Zhangir, et al.
Published: (2023)

A Neurosymbolic Approach to Natural Language Formalization and Verification
by: Bayless, Sam, et al.
Published: (2025)

3D-Prover: Diversity Driven Theorem Proving With Determinantal Point Processes
by: Lamont, Sean, et al.
Published: (2024)

PutnamBench: Evaluating Neural Theorem-Provers on the Putnam Mathematical Competition
by: Tsoukalas, George, et al.
Published: (2024)

A Neurosymbolic Approach to Loop Invariant Generation via Weakest Precondition Reasoning
by: King, Daragh, et al.
Published: (2025)

Hint-Based SMT Proof Reconstruction
by: Clune, Joshua, et al.
Published: (2026)

A Proof-Producing Compiler for Blockchain Applications
by: Avigad, Jeremy, et al.
Published: (2025)

Compile to Compress: Boosting Formal Theorem Provers by Compiler Outputs
by: Li, Guchan, et al.
Published: (2026)

Reasoning in Neurosymbolic AI
by: Tran, Son, et al.
Published: (2025)

Self-Supervised Transformers as Iterative Solution Improvers for Constraint Satisfaction
by: Xu, Yudong W., et al.
Published: (2025)

Vibe Coding an LLM-powered Theorem Prover
by: Hou, Zhe
Published: (2026)

ScenicProver: A Framework for Compositional Probabilistic Verification of Learning-Enabled Systems
by: Vin, Eric, et al.
Published: (2025)

Proceedings 19th International Workshop on the ACL2 Theorem Prover and Its Applications
by: Gamboa, Ruben, et al.
Published: (2025)

Hierarchical Attention Generates Better Proofs
by: Chen, Jianlong, et al.
Published: (2025)

A Certified Proof Checker for Deep Neural Network Verification in Imandra
by: Desmartin, Remi, et al.
Published: (2024)

Aligning with Logic: Measuring, Evaluating and Improving Logical Preference Consistency in Large Language Models
by: Liu, Yinhong, et al.
Published: (2024)

Defining implication relation for classical logic
by: Fu, Li
Published: (2013)

Neurosymbolic Decision Trees
by: Möller, Matthias, et al.
Published: (2025)

NeuroNL2LTL: A Neurosymbolic Framework for Natural Language Translation of Linear Temporal Logic
by: Quansah, Paapa Kwesi, et al.
Published: (2026)

ProofWala: A Framework for Multilingual Proof Data Synthesis and Theorem-Proving
by: Thakur, Amitayush, et al.
Published: (2025)

Lean Refactor: Multi-Objective Controllable Proof Optimization via Agentic Strategy Search
by: Lu, Jialin, et al.
Published: (2026)

Can Proof Assistants Verify Multi-Agent Systems?
by: Mendez, Julian Alfredo, et al.
Published: (2025)

Translating Informal Proofs into Formal Proofs Using a Chain of States
by: Wang, Ziyu, et al.
Published: (2025)

ProofFlow: A Dependency Graph Approach to Faithful Proof Autoformalization
by: Cabral, Rafael, et al.
Published: (2025)

Investigations into Proof Structures
by: Wernhard, Christoph, et al.
Published: (2023)

Theorem Provers: One Size Fits All?
by: Oates, Harrison, et al.
Published: (2025)

MerLean-Prover: A Recursive Looping Harness for Lean 4 Theorem Proving
by: Li, Jinzheng, et al.
Published: (2026)

Modeling Next-Token Prediction as Left-Nested Intuitionistic Implication
by: Tarau, Paul
Published: (2026)

Where to Search: Measure the Prior-Structured Search Space of LLM Agents
by: Song, Zhuo-Yang
Published: (2025)