{"total":234,"rows":[{"id":"2501.19393","title":"s1: Simple test-time scaling","created":"2025-01-31","cited_by_count":1341,"area":"lr"},{"id":"2501.04519","title":"rStar-Math: Small LLMs Can Master Math Reasoning with Self-Evolved Deep Thinking","created":"2025-01-08","cited_by_count":313,"area":"lr"},{"id":"2504.21801","title":"DeepSeek-Prover-V2: Advancing Formal Mathematical Reasoning via Reinforcement Learning for Subgoal Decomposition","created":"2025-04-30","cited_by_count":287,"area":"lr"},{"id":"2406.18629","title":"Step-DPO: Step-wise Preference Optimization for Long-chain Reasoning of LLMs","created":"2024-06-26","cited_by_count":273,"area":"lr"},{"id":"2505.24298","title":"AReaL: A Large-Scale Asynchronous Reinforcement Learning System for Language Reasoning","created":"2025-05-30","cited_by_count":250,"area":"lr"},{"id":"2408.08152","title":"DeepSeek-Prover-V1.5: Harnessing Proof Assistant Feedback for Reinforcement Learning and Monte-Carlo Tree Search","created":"2024-08-15","cited_by_count":197,"area":"lr"},{"id":"2508.03613","title":"Goedel-Prover-V2: Scaling Formal Theorem Proving with Scaffolded Data Synthesis and Self-Correction","created":"2025-08-05","cited_by_count":154,"area":"synth"},{"id":"2502.07640","title":"Goedel-Prover: A Frontier Model for Open-Source Automated Theorem Proving","created":"2025-02-11","cited_by_count":133,"area":null},{"id":"2406.03847","title":"Lean Workbook: A large-scale Lean problem set formalized from natural language math problems","created":"2024-06-06","cited_by_count":122,"area":null},{"id":"2507.15061","title":"WebShaper: Agentically Data Synthesizing via Information-Seeking Formalization","created":"2025-07-20","cited_by_count":121,"area":null},{"id":"2504.09037","title":"A Survey of Frontiers in LLM Reasoning: Inference Scaling, Learning to Reason, and Agentic Systems","created":"2025-04-12","cited_by_count":111,"area":"lr"},{"id":"2412.16075","title":"Formal Mathematical Reasoning: A New Frontier in AI","created":"2024-12-20","cited_by_count":81,"area":"lr"},{"id":"2502.00212","title":"STP: Self-play LLM Theorem Provers with Iterative Conjecturing and Proving","created":"2025-01-31","cited_by_count":79,"area":"lr"},{"id":"2410.01707","title":"Interpretable Contrastive Monte Carlo Tree Search Reasoning","created":"2024-10-02","cited_by_count":64,"area":"lr"},{"id":"2509.22819","title":"Hilbert: Recursively Building Formal Proofs with Informal Reasoning","created":"2025-09-26","cited_by_count":60,"area":"lr"},{"id":"2410.10878","title":"Herald: A Natural Language Annotated Lean 4 Dataset","created":"2024-10-09","cited_by_count":59,"area":"lr"},{"id":"2510.01346","title":"Aristotle: IMO-level Automated Theorem Proving","created":"2025-10-01","cited_by_count":58,"area":null},{"id":"2412.11936","title":"A Survey of Mathematical Reasoning in the Era of Multimodal Large Language Model: Benchmark, Method & Challenges","created":"2024-12-16","cited_by_count":55,"area":"lr"},{"id":"2411.17501","title":"The Limits of Inference Scaling Through Resampling","created":"2024-11-26","cited_by_count":53,"area":null},{"id":"2502.19328","title":"Agentic Reward Modeling: Integrating Human Preferences with Verifiable Correctness Signals for Reliable Reward Systems","created":"2025-02-26","cited_by_count":51,"area":"lr"},{"id":"2407.00379","title":"GraphArena: Evaluating and Exploring Large Language Models on Graph Computation","created":"2024-06-29","cited_by_count":49,"area":null},{"id":"2504.13139","title":"Syntactic and Semantic Control of Large Language Models via Sequential Monte Carlo","created":"2025-04-17","cited_by_count":46,"area":null},{"id":"2410.12896","title":"A Survey on Data Synthesis and Augmentation for Large Language Models","created":"2024-10-16","cited_by_count":41,"area":"synth"},{"id":"2503.24377","title":"Harnessing the Reasoning Economy: A Survey of Efficient Reasoning for Large Language Models","created":"2025-03-31","cited_by_count":36,"area":"lr"},{"id":"2410.06209","title":"LeanAgent: Lifelong Learning for Formal Theorem Proving","created":"2024-10-08","cited_by_count":35,"area":"lr"},{"id":"2507.15225","title":"Solving Formal Math Problems by Decomposition and Iterative Reflection","created":"2025-07-21","cited_by_count":35,"area":"lr"},{"id":"2410.15700","title":"InternLM2.5-StepProver: Advancing Automated Theorem Proving via Critic-Guided Search","created":"2024-10-21","cited_by_count":34,"area":null},{"id":"2412.20735","title":"HunyuanProver: A Scalable Data Synthesis Framework and Guided Tree Search for Automated Theorem Proving","created":"2024-12-30","cited_by_count":33,"area":"lr"},{"id":"2502.02871","title":"Position: Multimodal Large Language Models Can Significantly Advance Scientific Reasoning","created":"2025-02-05","cited_by_count":33,"area":"lr"},{"id":"2505.03171","title":"CombiBench: Benchmarking LLM Capability for Combinatorial Mathematics","created":"2025-05-06","cited_by_count":31,"area":"lr"},{"id":"2510.12787","title":"Ax-Prover: A Deep Reasoning Agentic Framework for Theorem Proving in Mathematics and Quantum Physics","created":"2025-10-14","cited_by_count":31,"area":"lr"},{"id":"2504.09772","title":"Two Heads are Better Than One: Test-time Scaling of Multi-agent Collaborative Reasoning","created":"2025-04-14","cited_by_count":29,"area":"lr"},{"id":"2505.21600","title":"R2R: Efficiently Navigating Divergent Reasoning Paths with Small-Large Model Token Routing","created":"2025-05-27","cited_by_count":29,"area":"lr"},{"id":"2509.06493","title":"Scaling up Multi-Turn Off-Policy RL and Multi-Agent Tree Search for LLM Step-Provers","created":"2025-09-08","cited_by_count":28,"area":"lr"},{"id":"2412.14063","title":"Rango: Adaptive Retrieval-Augmented Proving for Automated Software Verification","created":"2024-12-18","cited_by_count":27,"area":"rag"},{"id":"2504.06122","title":"Leanabell-Prover: Posttraining Scaling in Formal Reasoning","created":"2025-04-08","cited_by_count":27,"area":"lr"},{"id":"2507.08649","title":"Leanabell-Prover-V2: Verifier-integrated Reasoning for Formal Theorem Proving via Reinforcement Learning","created":"2025-07-11","cited_by_count":27,"area":"lr"},{"id":"2503.03205","title":"MA-LoT: Model-Collaboration Lean-based Long Chain-of-Thought Reasoning enhances Formal Theorem Proving","created":"2025-03-05","cited_by_count":24,"area":"lr"},{"id":"2504.07052","title":"To Backtrack or Not to Backtrack: When Sequential Search Limits Model Reasoning","created":"2025-04-09","cited_by_count":24,"area":"lr"},{"id":"2505.23754","title":"DeepTheorem: Advancing LLM Reasoning for Theorem Proving Through Natural Language and Reinforcement Learning","created":"2025-05-29","cited_by_count":24,"area":"lr"},{"id":"2502.00963","title":"PDE-Controller: LLMs for Autoformalization and Reasoning of PDEs","created":"2025-02-03","cited_by_count":23,"area":"lr"},{"id":"2502.05567","title":"ATLAS: Autoformalizing Theorems through Lifting, Augmentation, and Synthesis of Data","created":"2025-02-08","cited_by_count":23,"area":null},{"id":"2505.16582","title":"O$^2$-Searcher: A Searching-based Agent Model for Open-Domain Open-Ended Question Answering","created":"2025-05-22","cited_by_count":23,"area":"agents"},{"id":"2411.01829","title":"Formal Theorem Proving by Rewarding LLMs to Decompose Proofs Hierarchically","created":"2024-11-04","cited_by_count":22,"area":"lr"},{"id":"2504.05410","title":"Fast Controlled Generation from Language Models with Adaptive Weighted Rejection Sampling","created":"2025-04-07","cited_by_count":21,"area":null},{"id":"2505.14625","title":"TinyV: Reducing False Negatives in Verification Improves RL for LLM Reasoning","created":"2025-05-20","cited_by_count":21,"area":"lr"},{"id":"2505.23486","title":"Autoformalization in the Era of Large Language Models: A Survey","created":"2025-05-29","cited_by_count":21,"area":null},{"id":"2506.07927","title":"Solving Inequality Proofs with Large Language Models","created":"2025-06-09","cited_by_count":21,"area":"lr"},{"id":"2505.22960","title":"Revisiting Multi-Agent Debate as Test-Time Scaling: A Systematic Study of Conditional Effectiveness","created":"2025-05-29","cited_by_count":20,"area":"lr"},{"id":"2510.24592","title":"ReForm: Reflective Autoformalization with Prospective Bounded Sequence Optimization","created":"2025-10-28","cited_by_count":20,"area":"lr"},{"id":"2410.12854","title":"TPO: Aligning Large Language Models with Multi-branch & Multi-step Preference Trees","created":"2024-10-10","cited_by_count":19,"area":"lr"},{"id":"2502.05714","title":"Proving the Coding Interview: A Benchmark for Formally Verified Code Generation","created":"2025-02-08","cited_by_count":19,"area":null},{"id":"2505.20613","title":"REAL-Prover: Retrieval Augmented Lean Prover for Mathematical Reasoning","created":"2025-05-27","cited_by_count":18,"area":"lr"},{"id":"2510.15681","title":"ProofBridge: Auto-Formalization of Natural Language Proofs in Lean via Joint Embeddings","created":"2025-10-17","cited_by_count":18,"area":"rag"},{"id":"2409.02795","title":"Towards a Unified View of Preference Learning for Large Language Models: A Survey","created":"2024-09-04","cited_by_count":17,"area":"alignment"},{"id":"2502.13834","title":"Proving Olympiad Inequalities by Synergizing LLMs and Symbolic Reasoning","created":"2025-02-19","cited_by_count":17,"area":"lr"},{"id":"2506.04592","title":"Safe: Enhancing Mathematical Reasoning in Large Language Models via Retrospective Step-aware Formal Verification","created":"2025-06-05","cited_by_count":17,"area":"lr"},{"id":"2506.11487","title":"Reviving DSP for Advanced Theorem Proving in the Era of Reasoning Models","created":"2025-06-13","cited_by_count":17,"area":"lr"},{"id":"2507.06181","title":"CriticLean: Critic-Guided Reinforcement Learning for Mathematical Formalization","created":"2025-07-08","cited_by_count":16,"area":"lr"},{"id":"2509.23988","title":"LLM/Agent-as-Data-Analyst: A Survey","created":"2025-09-28","cited_by_count":16,"area":"agents"},{"id":"2506.09820","title":"CoRT: Code-integrated Reasoning within Thinking","created":"2025-06-11","cited_by_count":15,"area":"lr"},{"id":"2409.12929","title":"LogicPro: Improving Complex Logical Reasoning via Program-Guided Learning","created":"2024-09-19","cited_by_count":14,"area":"lr"},{"id":"2502.13137","title":"Theorem Prover as a Judge for Synthetic Data Generation","created":"2025-02-18","cited_by_count":14,"area":"lr"},{"id":"2504.09440","title":"Enhancing Mathematical Reasoning in Large Language Models with Self-Consistency-Based Hallucination Detection","created":"2025-04-13","cited_by_count":13,"area":"lr"},{"id":"2505.20196","title":"Temporal Sampling for Forgotten Reasoning in LLMs","created":"2025-05-26","cited_by_count":12,"area":"lr"},{"id":"2408.11172","title":"SubgoalXL: Subgoal-based Expert Learning for Theorem Proving","created":"2024-08-20","cited_by_count":11,"area":null},{"id":"2501.18310","title":"ProofAug: Efficient Neural Theorem Proving via Fine-grained Proof Structure Analysis","created":"2025-01-30","cited_by_count":11,"area":null},{"id":"2505.23703","title":"Let's Reason Formally: Natural-Formal Hybrid Reasoning Enhances LLM's Math Capability","created":"2025-05-29","cited_by_count":11,"area":"lr"},{"id":"2603.19329","title":"Goedel-Code-Prover: Hierarchical Proof Search for Open State-of-the-Art Code Verification","created":"2026-03-18","cited_by_count":11,"area":null},{"id":"2410.16930","title":"Math Neurosurgery: Isolating Language Models' Math Reasoning Abilities Using Only Forward Passes","created":"2024-10-22","cited_by_count":10,"area":"lr"},{"id":"2505.20047","title":"Grammars of Formal Uncertainty: When to Trust LLMs in Automated Reasoning Tasks","created":"2025-05-26","cited_by_count":10,"area":"lr"},{"id":"2602.16554","title":"MerLean: An Agentic Framework for Autoformalization in Quantum Computation","created":"2026-02-18","cited_by_count":10,"area":"agents"},{"id":"2605.29955","title":"Formalizing Mathematics at Scale","created":"2026-05-28","cited_by_count":10,"area":null},{"id":"2505.00016","title":"Sparks of Tabular Reasoning via Text2SQL Reinforcement Learning","created":"2025-04-23","cited_by_count":9,"area":"lr"},{"id":"2508.18914","title":"FormaRL: Enhancing Autoformalization with no Labeled Data","created":"2025-08-26","cited_by_count":9,"area":null},{"id":"2601.08198","title":"Triplets Better Than Pairs: Towards Stable and Effective Self-Play Fine-Tuning for LLMs","created":"2026-01-13","cited_by_count":9,"area":"synth"},{"id":"2606.06468","title":"Goedel-Architect: Streamlining Formal Theorem Proving with Blueprint Generation and Refinement","created":"2026-06-04","cited_by_count":9,"area":"agents"},{"id":"2608.05179","title":"Autonomous Research Agents: A Survey of AI Scientists and the Verification Gap","created":"2026-06-29","cited_by_count":9,"area":"agents"},{"id":"2502.02558","title":"Particle Trajectory Representation Learning with Masked Point Modeling","created":"2025-02-04","cited_by_count":8,"area":null},{"id":"2503.01424","title":"From Hypothesis to Publication: A Comprehensive Survey of AI-Driven Research Support Systems","created":"2025-03-03","cited_by_count":8,"area":null},{"id":"2503.10573","title":"Evaluating Mathematical Reasoning Across Large Language Models: A Fine-Grained Approach","created":"2025-03-13","cited_by_count":8,"area":"lr"},{"id":"2505.15960","title":"Efficient PRM Training Data Synthesis via Formal Verification","created":"2025-05-21","cited_by_count":8,"area":"lr"},{"id":"2505.24264","title":"Faithful and Robust LLM-Driven Theorem Proving for NLI Explanations","created":"2025-05-30","cited_by_count":8,"area":null},{"id":"2506.07971","title":"CyberV: Cybernetics for Test-time Scaling in Video Understanding","created":"2025-06-09","cited_by_count":8,"area":"lr"},{"id":"2510.15940","title":"Lean Finder: Semantic Search for Mathlib That Understands User Intents","created":"2025-10-08","cited_by_count":8,"area":null},{"id":"2510.25427","title":"RLMEval: Evaluating Research-Level Neural Theorem Proving","created":"2025-10-29","cited_by_count":8,"area":null},{"id":"2602.12279","title":"UniT: Unified Multimodal Chain-of-Thought Test-time Scaling","created":"2026-02-12","cited_by_count":8,"area":"lr"},{"id":"2412.17743","title":"YuLan-Mini: An Open Data-efficient Language Model","created":"2024-12-23","cited_by_count":7,"area":null},{"id":"2508.05242","title":"CodeBoost: Boosting Code LLMs by Squeezing Knowledge from Code Snippets with RL","created":"2025-08-07","cited_by_count":7,"area":null},{"id":"2510.00732","title":"EvolProver: Advancing Automated Theorem Proving by Evolving Formalized Problems via Symmetry and Difficulty","created":"2025-10-01","cited_by_count":7,"area":null},{"id":"2601.04525","title":"GRACE: Reinforcement Learning for Grounded Response and Abstention under Contextual Evidence","created":"2026-01-08","cited_by_count":7,"area":"lr"},{"id":"2602.02990","title":"Learning to Repair Lean Proofs from Compiler Feedback","created":"2026-02-03","cited_by_count":7,"area":"agents"},{"id":"2606.20068","title":"Process-Verified Reinforcement Learning for Theorem Proving via Lean","created":"2026-06-18","cited_by_count":7,"area":"lr"},{"id":"2411.18872","title":"A Lean Dataset for International Math Olympiad: Small Steps towards Writing Math Proofs for Hard Problems","created":"2024-11-28","cited_by_count":6,"area":null},{"id":"2502.09955","title":"Diverse Inference and Verification for Advanced Reasoning","created":"2025-02-14","cited_by_count":6,"area":"lr"},{"id":"2505.20415","title":"Enhancing Logical Reasoning in Language Models via Symbolically-Guided Monte Carlo Process Supervision","created":"2025-05-26","cited_by_count":6,"area":"lr"},{"id":"2506.07477","title":"Premise Selection for a Lean Hammer","created":"2025-06-09","cited_by_count":6,"area":null},{"id":"2509.08653","title":"Generative Data Refinement: Just Ask for Better Data","created":"2025-09-10","cited_by_count":6,"area":null},{"id":"2510.11769","title":"GAR: Generative Adversarial Reinforcement Learning for Formal Theorem Proving","created":"2025-10-13","cited_by_count":6,"area":"lr"},{"id":"2601.03764","title":"Learning Shrinks the Hard Tail: Training-Dependent Inference Scaling in a Solvable Linear Model","created":"2026-01-07","cited_by_count":6,"area":null}],"next_cursor":"100"}