{"total":142,"rows":[{"id":"2307.15818","title":"RT-2: Vision-Language-Action Models Transfer Web Knowledge to Robotic Control","created":"2023-07-28","cited_by_count":3080,"area":"mllm"},{"id":"2303.18223","title":"A Survey of Large Language Models","created":"2023-03-31","cited_by_count":2576,"area":null},{"id":"2303.03378","title":"PaLM-E: An Embodied Multimodal Language Model","created":"2023-03-06","cited_by_count":2071,"area":"mllm"},{"id":"2206.14858","title":"Solving Quantitative Reasoning Problems with Language Models","created":"2022-06-29","cited_by_count":1392,"area":"lr"},{"id":"2203.14465","title":"STaR: Bootstrapping Reasoning With Reasoning","created":"2022-03-28","cited_by_count":940,"area":"lr"},{"id":"2306.15626","title":"LeanDojo: Theorem Proving with Retrieval-Augmented Language Models","created":"2023-06-27","cited_by_count":427,"area":"rag"},{"id":"2310.10631","title":"Llemma: An Open Language Model For Mathematics","created":"2023-10-16","cited_by_count":388,"area":"lr"},{"id":"2210.12283","title":"Draft, Sketch, and Prove: Guiding Formal Theorem Provers with Informal Proofs","created":"2022-10-21","cited_by_count":291,"area":null},{"id":"2405.00451","title":"Monte Carlo Tree Search Boosts Reasoning via Iterative Preference Learning","created":"2024-05-01","cited_by_count":241,"area":"lr"},{"id":"2405.14333","title":"DeepSeek-Prover: Advancing Theorem Proving in LLMs through Large-Scale Synthetic Data","created":"2024-05-23","cited_by_count":234,"area":"synth"},{"id":"2205.11491","title":"HyperTree Proof Search for Neural Theorem Proving","created":"2022-05-23","cited_by_count":197,"area":null},{"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":"2204.06031","title":"A Review on Language Models as Knowledge Bases","created":"2022-04-12","cited_by_count":157,"area":null},{"id":"2304.09797","title":"Progressive-Hint Prompting Improves Reasoning in Large Language Models","created":"2023-04-19","cited_by_count":147,"area":"lr"},{"id":"2206.03126","title":"Signal Propagation in Transformers: Theoretical Perspectives and the Role of Rank Collapse","created":"2022-06-07","cited_by_count":141,"area":null},{"id":"2406.16838","title":"From Decoding to Meta-Generation: Inference-time Algorithms for Large Language Models","created":"2024-06-24","cited_by_count":137,"area":null},{"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":"2212.10535","title":"A Survey of Deep Learning for Mathematical Reasoning","created":"2022-12-20","cited_by_count":124,"area":"lr"},{"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":"2206.04301","title":"Unveiling Transformers with LEGO: a synthetic reasoning task","created":"2022-06-09","cited_by_count":106,"area":null},{"id":"2507.23726","title":"Seed-Prover: Deep and Broad Reasoning for Automated Theorem Proving","created":"2025-07-31","cited_by_count":101,"area":"lr"},{"id":"2205.10893","title":"Thor: Wielding Hammers to Integrate Language Models and Automated Theorem Provers","created":"2022-05-22","cited_by_count":98,"area":null},{"id":"2501.05707","title":"Multiagent Finetuning: Self Improvement with Diverse Reasoning Chains","created":"2025-01-10","cited_by_count":95,"area":"lr"},{"id":"2502.03438","title":"BFS-Prover: Scalable Best-First Tree Search for LLM-based Automatic Theorem Proving","created":"2025-02-05","cited_by_count":84,"area":null},{"id":"2310.04353","title":"An In-Context Learning Agent for Formal Theorem-Proving","created":"2023-10-06","cited_by_count":82,"area":"agents"},{"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":"2205.12910","title":"NaturalProver: Grounded Mathematical Proof Generation with Language Models","created":"2022-05-25","cited_by_count":72,"area":null},{"id":"2407.10040","title":"Lean-STaR: Learning to Interleave Thinking and Proving","created":"2024-07-14","cited_by_count":68,"area":"lr"},{"id":"2404.12534","title":"Lean Copilot: Large Language Models as Copilots for Theorem Proving in Lean","created":"2024-04-18","cited_by_count":58,"area":null},{"id":"2510.01346","title":"Aristotle: IMO-level Automated Theorem Proving","created":"2025-10-01","cited_by_count":58,"area":null},{"id":"2404.09939","title":"A Survey on Deep Learning for Theorem Proving","created":"2024-04-15","cited_by_count":57,"area":null},{"id":"2309.04295","title":"FIMO: A Challenge Formal Dataset for Automated Theorem Proving","created":"2023-09-08","cited_by_count":55,"area":null},{"id":"2303.04488","title":"Magnushammer: A Transformer-Based Approach to Premise Selection","created":"2023-03-08","cited_by_count":50,"area":null},{"id":"2407.00695","title":"Learning Formal Mathematics From Intrinsic Motivation","created":"2024-06-30","cited_by_count":45,"area":null},{"id":"2512.17260","title":"Seed-Prover 1.5: Mastering Undergraduate-Level Theorem Proving via Learning from Experience","created":"2025-12-19","cited_by_count":44,"area":null},{"id":"2402.08957","title":"MUSTARD: Mastering Uniform Synthesis of Theorem and Proof Data","created":"2024-02-14","cited_by_count":43,"area":"lr"},{"id":"2305.16366","title":"Decomposing the Enigma: Subgoal-based Demonstration Learning for Formal Theorem Proving","created":"2023-05-25","cited_by_count":37,"area":"diffusion"},{"id":"2410.06209","title":"LeanAgent: Lifelong Learning for Formal Theorem Proving","created":"2024-10-08","cited_by_count":35,"area":"lr"},{"id":"2412.06176","title":"AlphaVerus: Bootstrapping Formally Verified Code Generation through Self-Improving Translation and Treefinement","created":"2024-12-09","cited_by_count":35,"area":"synth"},{"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":"2410.15756","title":"Automated Proof Generation for Rust Code via Self-Evolution","created":"2024-10-21","cited_by_count":33,"area":null},{"id":"2405.10313","title":"How Far Are We From AGI: Are LLMs All We Need?","created":"2024-05-16","cited_by_count":31,"area":null},{"id":"2506.19923","title":"Prover Agent: An Agent-Based Framework for Formal Mathematical Proofs","created":"2025-06-24","cited_by_count":31,"area":"agents"},{"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":"2411.08027","title":"LLMPhy: Parameter-Identifiable Physical Reasoning Combining Large Language Models and Physics Engines","created":"2024-11-12","cited_by_count":30,"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":"2310.18021","title":"FormalGeo: An Extensible Formalized Framework for Olympiad Geometric Problem Solving","created":"2023-10-27","cited_by_count":27,"area":null},{"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":"2309.15806","title":"Lyra: Orchestrating Dual Correction in Automated Theorem Proving","created":"2023-09-27","cited_by_count":25,"area":null},{"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":"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":"2402.04858","title":"CodeIt: Self-Improving Language Models with Prioritized Hindsight Replay","created":"2024-02-07","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":"2411.01829","title":"Formal Theorem Proving by Rewarding LLMs to Decompose Proofs Hierarchically","created":"2024-11-04","cited_by_count":22,"area":"lr"},{"id":"2403.04571","title":"Machine learning and information theory concepts towards an AI Mathematician","created":"2024-03-07","cited_by_count":20,"area":"lr"},{"id":"2406.14219","title":"Proving Olympiad Algebraic Inequalities without Human Demonstrations","created":"2024-06-20","cited_by_count":20,"area":null},{"id":"2412.10673","title":"Proposing and solving olympiad geometry with guided tree search","created":"2024-12-14","cited_by_count":19,"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":"2206.06315","title":"JiuZhang: A Chinese Pre-trained Language Model for Mathematical Problem Understanding","created":"2022-06-13","cited_by_count":15,"area":null},{"id":"2211.15864","title":"Peano: Learning Formal Mathematical Reasoning","created":"2022-11-29","cited_by_count":15,"area":"lr"},{"id":"2212.10079","title":"A Survey on Pretrained Language Models for Neural Code Intelligence","created":"2022-12-20","cited_by_count":13,"area":null},{"id":"2305.18577","title":"Towards Constituting Mathematical Structures for Learning to Optimize","created":"2023-05-29","cited_by_count":13,"area":null},{"id":"2506.06034","title":"MATP-BENCH: Can MLLM Be a Good Automated Theorem Prover for Multimodal Problems?","created":"2025-06-06","cited_by_count":13,"area":"mllm"},{"id":"2507.20199","title":"StepFun-Prover Preview: Let's Think and Verify Step by Step","created":"2025-07-27","cited_by_count":13,"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":"2510.19099","title":"What Makes a Good Curriculum? Disentangling the Effects of Data Ordering on LLM Mathematical Reasoning","created":"2025-10-21","cited_by_count":11,"area":"lr"},{"id":"2410.04753","title":"ImProver: Agent-Based Automated Proof Optimization","created":"2024-10-07","cited_by_count":10,"area":"agents"},{"id":"2505.10962","title":"MPS-Prover: Advancing Stepwise Theorem Proving by Multi-Perspective Search and Data Curation","created":"2025-05-16","cited_by_count":10,"area":null},{"id":"2605.29955","title":"Formalizing Mathematics at Scale","created":"2026-05-28","cited_by_count":10,"area":null},{"id":"2408.10210","title":"A Survey on Symbolic Knowledge Distillation of Large Language Models","created":"2024-07-12","cited_by_count":9,"area":"distill"},{"id":"2408.10268","title":"Generating Streamlining Constraints with Large Language Models","created":"2024-08-16","cited_by_count":7,"area":null},{"id":"2308.15605","title":"Benchmarks for Detecting Measurement Tampering","created":"2023-08-29","cited_by_count":6,"area":null},{"id":"2405.06677","title":"ATG: Benchmarking Automated Theorem Generation for Generative Language Models","created":"2024-05-05","cited_by_count":6,"area":null},{"id":"2410.11133","title":"3D-Prover: Diversity Driven Theorem Proving With Determinantal Point Processes","created":"2024-10-14","cited_by_count":6,"area":null},{"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":"2506.07477","title":"Premise Selection for a Lean Hammer","created":"2025-06-09","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":"2211.08671","title":"LEMMA: Bootstrapping High-Level Mathematical Reasoning with Learned Symbolic Abstractions","created":"2022-11-16","cited_by_count":5,"area":"lr"},{"id":"2410.02992","title":"Learning to Better Search with Language Models via Guided Reinforced Self-Training","created":"2024-10-03","cited_by_count":5,"area":"synth"},{"id":"2503.04763","title":"MiniF2F in Rocq: Automatic Translation Between Proof Assistants -- A Case Study","created":"2025-02-11","cited_by_count":5,"area":null},{"id":"2504.17017","title":"Neural Theorem Proving: Generating and Structuring Proofs for Formal Verification","created":"2025-04-23","cited_by_count":5,"area":null},{"id":"2510.26094","title":"Lean4Physics: Comprehensive Reasoning Framework for College-level Physics in Lean4","created":"2025-10-30","cited_by_count":5,"area":null},{"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":"2603.25681","title":"Self-Improvement of Large Language Models: A Technical Overview and Future Outlook","created":"2026-03-26","cited_by_count":5,"area":"synth"},{"id":"2211.16740","title":"Explicit Knowledge Transfer for Weakly-Supervised Code Generation","created":"2022-11-30","cited_by_count":4,"area":"distill"},{"id":"2311.07618","title":"Large Language Models' Understanding of Math: Source Criticism and Extrapolation","created":"2023-11-12","cited_by_count":4,"area":null},{"id":"2410.15748","title":"Alchemy: Amplifying Theorem-Proving Capability through Symbolic Mutation","created":"2024-10-21","cited_by_count":4,"area":null},{"id":"2512.24796","title":"LeanCat: A Benchmark Suite for Formal Category Theory in Lean (Part I: 1-Categories)","created":"2025-12-31","cited_by_count":4,"area":null},{"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":"2512.10317","title":"Translating Informal Proofs into Formal Proofs Using a Chain of States","created":"2025-12-11","cited_by_count":3,"area":null},{"id":"2606.04883","title":"Optimizing the Cost-Quality Tradeoff of Agentic Theorem Provers in Lean","created":"2026-06-03","cited_by_count":3,"area":"agents"},{"id":"2606.05632","title":"Evaluation of LLMs for Mathematical Formalization in Lean","created":"2026-06-04","cited_by_count":3,"area":null},{"id":"2312.14188","title":"Enhancing Neural Theorem Proving through Data Augmentation and Dynamic Sampling Method","created":"2023-12-20","cited_by_count":2,"area":null}],"next_cursor":"100"}