Image de couverture de livre

Inference-Time Diversity in RL-Trained Lean Theorem Provers: A Diagnostic Study

Fuente: arXiv

Enregistré dans:

Détails bibliographiques
Auteur principal:	Burton, Zachary
Format:	Preprint
Publié:	2026
Sujets:	Artificial Intelligence
Accès en ligne:	Acceder al recurso
Tags:	Ajouter un tag Pas de tags, Soyez le premier à ajouter un tag!

Documents similaires

SorryDB: Can AI Provers Complete Real-World Lean Theorems?
par: Letson, Austin, et autres
Publié: (2026)

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

3D-Prover: Diversity Driven Theorem Proving With Determinantal Point Processes
par: Lamont, Sean, et autres
Publié: (2024)

Theorem Prover as a Judge for Synthetic Data Generation
par: Leang, Joshua Ong Jun, et autres
Publié: (2025)

OptProver: Bridging Olympiad and Optimization through Continual Training in Formal Theorem Proving
par: Li, Chenyi, et autres
Publié: (2026)

Vibe Coding an LLM-powered Theorem Prover
par: Hou, Zhe
Publié: (2026)

PhysProver: Advancing Automatic Theorem Proving for Physics
par: Zhang, Hanning, et autres
Publié: (2026)

EconProver: Towards More Economical Test-Time Scaling for Automated Theorem Proving
par: Li, Mukai, et autres
Publié: (2025)

Proof Recommendation System for the HOL4 Theorem Prover
par: Dekhil, Nour, et autres
Publié: (2024)

Awakening the Sleeping Agent: Lean-Specific Agentic Data Reactivates General Tool Use in Goedel Prover
par: Chung, Jui-Hui, et autres
Publié: (2026)

Seed-Prover: Deep and Broad Reasoning for Automated Theorem Proving
par: Chen, Luoxin, et autres
Publié: (2025)

Goedel-Prover: A Frontier Model for Open-Source Automated Theorem Proving
par: Lin, Yong, et autres
Publié: (2025)

MPS-Prover: Advancing Stepwise Theorem Proving by Multi-Perspective Search and Data Curation
par: Liang, Zhenwen, et autres
Publié: (2025)

BFS-Prover: Scalable Best-First Tree Search for LLM-based Automatic Theorem Proving
par: Xin, Ran, et autres
Publié: (2025)

EvolProver: Advancing Automated Theorem Proving by Evolving Formalized Problems via Symmetry and Difficulty
par: Tian, Yuchen, et autres
Publié: (2025)

DeepSeek-Prover: Advancing Theorem Proving in LLMs through Large-Scale Synthetic Data
par: Xin, Huajian, et autres
Publié: (2024)

Steamroller Problems: An Evaluation of LLM Reasoning Capability with Automated Theorem Prover Strategies
par: McGinness, Lachlan, et autres
Publié: (2024)

Distilling LLM Feedback for Lean Theorem Proving
par: Narozniak, Gaetan, et autres
Publié: (2026)

DreamProver: Evolving Transferable Lemma Libraries via a Wake-Sleep Theorem-Proving Agent
par: Zhang, Youyuan, et autres
Publié: (2026)

Leanabell-Prover-V2: Verifier-integrated Reasoning for Formal Theorem Proving via Reinforcement Learning
par: Ji, Xingguang, et autres
Publié: (2025)

Ax-Prover: A Deep Reasoning Agentic Framework for Theorem Proving in Mathematics and Quantum Physics
par: Breen, Benjamin, et autres
Publié: (2025)

Scaling up Multi-Turn Off-Policy RL and Multi-Agent Tree Search for LLM Step-Provers
par: Xin, Ran, et autres
Publié: (2025)

STP: Self-play LLM Theorem Provers with Iterative Conjecturing and Proving
par: Dong, Kefan, et autres
Publié: (2025)

Compile to Compress: Boosting Formal Theorem Provers by Compiler Outputs
par: Li, Guchan, et autres
Publié: (2026)

HunyuanProver: A Scalable Data Synthesis Framework and Guided Tree Search for Automated Theorem Proving
par: Li, Yang, et autres
Publié: (2024)

Proceedings 19th International Workshop on the ACL2 Theorem Prover and Its Applications
par: Gamboa, Ruben, et autres
Publié: (2025)

LeanConjecturer: Automatic Generation of Mathematical Conjectures for Theorem Proving
par: Onda, Naoto, et autres
Publié: (2025)

LeanSearch v2: Global Premise Retrieval for Lean 4 Theorem Proving
par: Gao, Guoxiong, et autres
Publié: (2026)

QaRL: Rollout-Aligned Quantization-Aware RL for Fast and Stable Training under Training--Inference Mismatch
par: Gu, Hao, et autres
Publié: (2026)

Goedel-Prover-V2: Scaling Formal Theorem Proving with Scaffolded Data Synthesis and Self-Correction
par: Lin, Yong, et autres
Publié: (2025)

HybridProver: Augmenting Theorem Proving with LLM-Driven Proof Synthesis and Refinement
par: Hu, Jilin, et autres
Publié: (2025)

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

TaoBench: Do Automated Theorem Prover LLMs Generalize Beyond MathLib?
par: Taylor, Alexander K, et autres
Publié: (2026)

InternLM2.5-StepProver: Advancing Automated Theorem Proving via Critic-Guided Search
par: Wu, Zijian, et autres
Publié: (2024)

Leanabell-Prover: Posttraining Scaling in Formal Reasoning
par: Zhang, Jingyuan, et autres
Publié: (2025)

PutnamBench: Evaluating Neural Theorem-Provers on the Putnam Mathematical Competition
par: Tsoukalas, George, et autres
Publié: (2024)

Clarifying Before Reasoning: A Coq Prover with Structural Context
par: Lu, Yanzhen, et autres
Publié: (2025)

Mitigating Legibility Tax with Decoupled Prover-Verifier Games
par: Kim, Yegon, et autres
Publié: (2026)

ProofCompass: Enhancing Specialized Provers with LLM Guidance
par: Wischermann, Nicolas, et autres
Publié: (2025)

Diverse Inference and Verification for Advanced Reasoning
par: Drori, Iddo, et autres
Publié: (2025)