{"total":56,"rows":[{"id":"2302.07842","title":"Augmented Language Models: a Survey","created":"2023-02-15","cited_by_count":403,"area":"lr"},{"id":"2310.10631","title":"Llemma: An Open Language Model For Mathematics","created":"2023-10-16","cited_by_count":388,"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":"2504.11354","title":"Kimina-Prover Preview: Towards Large Formal Reasoning Models with Reinforcement Learning","created":"2025-04-15","cited_by_count":180,"area":"lr"},{"id":"2412.18319","title":"Mulberry: Empowering MLLM with o1-like Reasoning and Reflection via Collective Monte Carlo Tree Search","created":"2024-12-24","cited_by_count":175,"area":"lr"},{"id":"2304.09797","title":"Progressive-Hint Prompting Improves Reasoning in Large Language Models","created":"2023-04-19","cited_by_count":147,"area":"lr"},{"id":"2212.10535","title":"A Survey of Deep Learning for Mathematical Reasoning","created":"2022-12-20","cited_by_count":124,"area":"lr"},{"id":"2402.06332","title":"InternLM-Math: Open Math Large Language Models Toward Verifiable Reasoning","created":"2024-02-09","cited_by_count":119,"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":"2506.02355","title":"Rewarding the Unlikely: Lifting GRPO Beyond Distribution Sharpening","created":"2025-06-03","cited_by_count":80,"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":"2503.00031","title":"Efficient Test-Time Scaling via Self-Calibration","created":"2025-02-25","cited_by_count":75,"area":"lr"},{"id":"2407.10040","title":"Lean-STaR: Learning to Interleave Thinking and Proving","created":"2024-07-14","cited_by_count":68,"area":"lr"},{"id":"2407.03203","title":"TheoremLlama: Transforming General-Purpose LLMs into Lean4 Experts","created":"2024-07-03","cited_by_count":59,"area":"lr"},{"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":"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":"2502.02871","title":"Position: Multimodal Large Language Models Can Significantly Advance Scientific Reasoning","created":"2025-02-05","cited_by_count":33,"area":"lr"},{"id":"2410.08304","title":"Global Lyapunov functions: a long-standing open problem in mathematics, with symbolic transformers","created":"2024-10-10","cited_by_count":29,"area":"lr"},{"id":"2501.11110","title":"Chain-of-Reasoning: Towards Unified Mathematical Reasoning in Large Language Models via a Multi-Paradigm Perspective","created":"2025-01-19","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":"2504.06122","title":"Leanabell-Prover: Posttraining Scaling in Formal Reasoning","created":"2025-04-08","cited_by_count":27,"area":"lr"},{"id":"2407.17227","title":"LEAN-GitHub: Compiling GitHub LEAN repositories for a versatile LEAN prover","created":"2024-07-24","cited_by_count":25,"area":"lr"},{"id":"2310.10180","title":"TRIGO: Benchmarking Formal Mathematical Proof Reduction for Generative Language Models","created":"2023-10-16","cited_by_count":24,"area":"lr"},{"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":"2412.10673","title":"Proposing and solving olympiad geometry with guided tree search","created":"2024-12-14","cited_by_count":19,"area":"lr"},{"id":"2505.20613","title":"REAL-Prover: Retrieval Augmented Lean Prover for Mathematical Reasoning","created":"2025-05-27","cited_by_count":18,"area":"lr"},{"id":"2502.13834","title":"Proving Olympiad Inequalities by Synergizing LLMs and Symbolic Reasoning","created":"2025-02-19","cited_by_count":17,"area":"lr"},{"id":"2410.22480","title":"Scaling LLM Inference with Optimized Sample Compute Allocation","created":"2024-10-29","cited_by_count":16,"area":"lr"},{"id":"2402.08147","title":"VerMCTS: Synthesizing Multi-Step Programs using a Verifier, a Large Language Model, and Tree Search","created":"2024-02-13","cited_by_count":14,"area":"lr"},{"id":"2503.17726","title":"A Survey on Mathematical Reasoning and Optimization with Large Language Models","created":"2025-03-22","cited_by_count":12,"area":"lr"},{"id":"2606.03303","title":"LEAP: Supercharging LLMs for Formal Mathematics with Agentic Frameworks","created":"2026-06-02","cited_by_count":12,"area":"lr"},{"id":"2509.25454","title":"DeepSearch: Overcome the Bottleneck of Reinforcement Learning with Verifiable Rewards via Monte Carlo Tree Search","created":"2025-09-29","cited_by_count":11,"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":"2403.04017","title":"Learning Guided Automated Reasoning: A Brief Survey","created":"2024-03-06","cited_by_count":7,"area":"lr"},{"id":"2606.20068","title":"Process-Verified Reinforcement Learning for Theorem Proving via Lean","created":"2026-06-18","cited_by_count":7,"area":"lr"},{"id":"2511.02603","title":"CGES: Confidence-Guided Early Stopping for Efficient and Accurate Self-Consistency","created":"2025-11-04","cited_by_count":6,"area":"lr"},{"id":"2211.08671","title":"LEMMA: Bootstrapping High-Level Mathematical Reasoning with Learned Symbolic Abstractions","created":"2022-11-16","cited_by_count":5,"area":"lr"},{"id":"2603.19514","title":"Learning to Disprove: Formal Counterexample Generation with Large Language Models","created":"2026-03-19","cited_by_count":5,"area":"lr"},{"id":"2508.00459","title":"Thinking Machines: Mathematical Reasoning in the Age of LLMs","created":"2025-08-01","cited_by_count":4,"area":"lr"},{"id":"2312.08926","title":"Modeling Complex Mathematical Reasoning via Large Language Model based MathAgent","created":"2023-12-14","cited_by_count":3,"area":"lr"},{"id":"2404.18384","title":"Exploring the Limits of Fine-grained LLM-based Physics Inference via Premise Removal Interventions","created":"2024-04-29","cited_by_count":3,"area":"lr"},{"id":"2507.14335","title":"ProofCompass: Enhancing Specialized Provers with LLM Guidance","created":"2025-07-18","cited_by_count":3,"area":"lr"},{"id":"2503.11657","title":"Scaling Natural-Language Graph-Based Test Time Compute for Automated Theorem Proving","created":"2025-02-04","cited_by_count":2,"area":"lr"},{"id":"2509.06809","title":"Saturation-Driven Dataset Generation for LLM Mathematical Reasoning in the TPTP Ecosystem","created":"2025-09-08","cited_by_count":2,"area":"lr"},{"id":"2512.10187","title":"MINIF2F-DAFNY: LLM-Guided Mathematical Theorem Proving via Auto-Active Verification","created":"2025-12-11","cited_by_count":2,"area":"lr"},{"id":"2502.18532","title":"CuDIP: Enhancing Theorem Proving in LLMs via Curriculum Learning-based Direct Preference Optimization","created":"2025-02-25","cited_by_count":1,"area":"lr"},{"id":"2605.04064","title":"Improving Medical VQA through Trajectory-Aware Process Supervision","created":"2026-04-10","cited_by_count":1,"area":"lr"},{"id":"2605.15445","title":"From LLM-Generated Conjectures to Lean Formalizations: Automated Polynomial Inequality Proving via Sum-of-Squares Certificates","created":"2026-05-14","cited_by_count":1,"area":"lr"},{"id":"2605.30914","title":"Automating Formal Verification with Reinforcement Learning and Recursive Inference","created":"2026-05-29","cited_by_count":1,"area":"lr"},{"id":"2606.28841","title":"LAMP: Lean-based Agentic framework with MCP and Proof Repair","created":"2026-06-27","cited_by_count":1,"area":"lr"},{"id":"2501.14705","title":"The Karp Dataset","created":"2025-01-24","cited_by_count":0,"area":"lr"},{"id":"2509.01267","title":"Iterative In-Context Learning to Enhance LLMs Abstract Reasoning: The Case-Study of Algebraic Tasks","created":"2025-09-01","cited_by_count":0,"area":"lr"},{"id":"2605.17255","title":"CAM-Bench: A Benchmark for Computational and Applied Mathematics in Lean","created":"2026-05-17","cited_by_count":0,"area":"lr"},{"id":"2606.28747","title":"Self-Supervised Theorem Discovery in a Formal Axiomatic System","created":"2026-06-27","cited_by_count":0,"area":"lr"},{"id":"2610.04280","title":"Dense Neuro-Symbolic Reasoning in a Unified Geometry State","created":"2026-10-03","cited_by_count":0,"area":"lr"}],"next_cursor":null}