Copertina

Formal Theorem Proving by Rewarding LLMs to Decompose Proofs Hierarchically

Fuente: arXiv

Salvato in:

Dettagli Bibliografici
Autori principali:	Dong, Kefan, Mahankali, Arvind, Ma, Tengyu
Natura:	Preprint
Pubblicazione:	2024
Soggetti:	Machine Learning
Accesso online:	Acceder al recurso
Tags:	Aggiungi Tag Nessun Tag, puoi essere il primo ad aggiungerne!!

Documenti analoghi

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

Divide-and-Conquer CoT: RL for Reducing Latency via Parallel Reasoning
di: Mahankali, Arvind, et al.
Pubblicazione: (2026)

Steering LLMs for Formal Theorem Proving
di: Kirtania, Shashank, et al.
Pubblicazione: (2025)

Neural Theorem Proving: Generating and Structuring Proofs for Formal Verification
di: Rao, Balaji, et al.
Pubblicazione: (2025)

Pseudo-Formalization for Automatic Proof Verification
di: Barkallah, Slim, et al.
Pubblicazione: (2026)

Scaling Self-Play with Self-Guidance
di: Bailey, Luke, et al.
Pubblicazione: (2026)

What are the Right Symmetries for Formal Theorem Proving?
di: Olejniczak, Krzysztof, et al.
Pubblicazione: (2026)

GAR: Generative Adversarial Reinforcement Learning for Formal Theorem Proving
di: Wang, Ruida, et al.
Pubblicazione: (2025)

An In-Context Learning Agent for Formal Theorem-Proving
di: Thakur, Amitayush, et al.
Pubblicazione: (2023)

LeanAgent: Lifelong Learning for Formal Theorem Proving
di: Kumarappan, Adarsh, et al.
Pubblicazione: (2024)

ProofAug: Efficient Neural Theorem Proving via Fine-grained Proof Structure Analysis
di: Liu, Haoxiong, et al.
Pubblicazione: (2025)

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

OptProver: Bridging Olympiad and Optimization through Continual Training in Formal Theorem Proving
di: Li, Chenyi, et al.
Pubblicazione: (2026)

BrokenMath: A Benchmark for Sycophancy in Theorem Proving with LLMs
di: Petrov, Ivo, et al.
Pubblicazione: (2025)

FVEL: Interactive Formal Verification Environment with Large Language Models via Theorem Proving
di: Lin, Xiaohan, et al.
Pubblicazione: (2024)

Goedel-Prover-V2: Scaling Formal Theorem Proving with Scaffolded Data Synthesis and Self-Correction
di: Lin, Yong, et al.
Pubblicazione: (2025)

Reward Is Enough: LLMs Are In-Context Reinforcement Learners
di: Song, Kefan, et al.
Pubblicazione: (2025)

A Theoretical Framework for Self-Play Theorem Proving Algorithms
di: Chen, Thomas, et al.
Pubblicazione: (2026)

Automated Formal Proofs of Combinatorial Identities via Wilf-Zeilberger Guidance and LLMs
di: Xiong, Beibei, et al.
Pubblicazione: (2026)

CuDIP: Enhancing Theorem Proving in LLMs via Curriculum Learning-based Direct Preference Optimization
di: Shi, Shuming, et al.
Pubblicazione: (2025)

Learning to Reason with Insight for Informal Theorem Proving
di: Li, Yunhe, et al.
Pubblicazione: (2026)

Lean Meets Theoretical Computer Science: Scalable Synthesis of Theorem Proving Challenges in Formal-Informal Pairs
di: Zhang, Terry Jingchen, et al.
Pubblicazione: (2025)

Bourbaki: Self-Generated and Goal-Conditioned MDPs for Theorem Proving
di: Zimmer, Matthieu, et al.
Pubblicazione: (2025)

FormalRewardBench: A Benchmark for Formal Theorem Proving Reward Models
di: Uluşan, Zeynel A., et al.
Pubblicazione: (2026)

miniCTX: Neural Theorem Proving with (Long-)Contexts
di: Hu, Jiewen, et al.
Pubblicazione: (2024)

BAIT: Benchmarking (Embedding) Architectures for Interactive Theorem-Proving
di: Lamont, Sean, et al.
Pubblicazione: (2024)

Non-Asymptotic Length Generalization
di: Chen, Thomas, et al.
Pubblicazione: (2025)

Configuration-to-Performance Scaling Law with Neural Ansatz
di: Zhang, Huaqing, et al.
Pubblicazione: (2026)

Goedel-Prover: A Frontier Model for Open-Source Automated Theorem Proving
di: Lin, Yong, et al.
Pubblicazione: (2025)

Discovering New Theorems via LLMs with In-Context Proof Learning in Lean
di: Kasaura, Kazumi, et al.
Pubblicazione: (2025)

QED-Nano: Teaching a Tiny Model to Prove Hard Theorems
di: LM-Provers, et al.
Pubblicazione: (2026)

MINIF2F-DAFNY: LLM-Guided Mathematical Theorem Proving via Auto-Active Verification
di: Baksys, Mantas, et al.
Pubblicazione: (2025)

Nazrin: Atomic Tactics for Graph Neural Networks for Theorem Proving in Lean 4
di: Aniva, Leni, et al.
Pubblicazione: (2026)

Random Latent Exploration for Deep Reinforcement Learning
di: Mahankali, Srinath, et al.
Pubblicazione: (2024)

Lean Copilot: Large Language Models as Copilots for Theorem Proving in Lean
di: Song, Peiyang, et al.
Pubblicazione: (2024)

Knowledge Offloading: Decomposing LLMs into Sparse Backbones and Memory Modules
di: Galliamov, Karim, et al.
Pubblicazione: (2026)

SubgoalXL: Subgoal-based Expert Learning for Theorem Proving
di: Zhao, Xueliang, et al.
Pubblicazione: (2024)

REFACTOR: Learning to Extract Theorems from Proofs
di: Zhou, Jin Peng, et al.
Pubblicazione: (2024)

Explaining an Agent's Future Beliefs through Temporally Decomposing Future Reward Estimators
di: Towers, Mark, et al.
Pubblicazione: (2024)

FormalProofBench: Can Models Write Graduate Level Math Proofs That Are Formally Verified?
di: Ravi, Nikil, et al.
Pubblicazione: (2026)