{"total":263,"rows":[{"id":"2303.18223","title":"A Survey of Large Language Models","created":"2023-03-31","cited_by_count":2576,"area":null},{"id":"2206.14858","title":"Solving Quantitative Reasoning Problems with Language Models","created":"2022-06-29","cited_by_count":1392,"area":"lr"},{"id":"2307.03109","title":"A Survey on Evaluation of Large Language Models","created":"2023-07-06","cited_by_count":1242,"area":null},{"id":"2211.10435","title":"PAL: Program-aided Language Models","created":"2022-11-18","cited_by_count":652,"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":"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":"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":"2212.09597","title":"Reasoning with Language Model Prompting: A Survey","created":"2022-12-19","cited_by_count":252,"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":"2210.06774","title":"Re3: Generating Longer Stories With Recursive Reprompting and Revision","created":"2022-10-13","cited_by_count":193,"area":null},{"id":"2302.12433","title":"ProofNet: Autoformalizing and Formally Proving Undergraduate-Level Mathematics","created":"2023-02-24","cited_by_count":192,"area":null},{"id":"2310.15164","title":"LINC: A Neurosymbolic Approach for Logical Reasoning by Combining Language Models with First-Order Logic Provers","created":"2023-10-23","cited_by_count":168,"area":"lr"},{"id":"2210.07128","title":"Language Models of Code are Few-Shot Commonsense Learners","created":"2022-10-13","cited_by_count":160,"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":"2410.14157","title":"Beyond Autoregression: Discrete Diffusion for Complex Reasoning and Planning","created":"2024-10-18","cited_by_count":135,"area":"lr"},{"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":"2304.02015","title":"How well do Large Language Models perform in Arithmetic tasks?","created":"2023-03-16","cited_by_count":130,"area":"lr"},{"id":"2209.07686","title":"Text and Patterns: For Effective Chain of Thought, It Takes Two to Tango","created":"2022-09-16","cited_by_count":128,"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":"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":"2303.04910","title":"Baldur: Whole-Proof Generation and Repair with Large Language Models","created":"2023-03-08","cited_by_count":119,"area":null},{"id":"2211.09066","title":"Teaching Algorithmic Reasoning via In-context Learning","created":"2022-11-15","cited_by_count":112,"area":"lr"},{"id":"2310.00656","title":"LEGO-Prover: Neural Theorem Proving with Growing Libraries","created":"2023-10-01","cited_by_count":109,"area":null},{"id":"2502.03544","title":"Gold-medalist Performance in Solving Olympiad Geometry with AlphaGeometry2","created":"2025-02-05","cited_by_count":97,"area":null},{"id":"2405.06624","title":"Towards Guaranteed Safe AI: A Framework for Ensuring Robust and Reliable AI Systems","created":"2024-05-10","cited_by_count":96,"area":"wm"},{"id":"2305.11391","title":"A Survey of Safety and Trustworthiness of Large Language Models through the Lens of Verification and Validation","created":"2023-05-19","cited_by_count":93,"area":null},{"id":"2402.09371","title":"Transformers Can Achieve Length Generalization But Not Robustly","created":"2024-02-14","cited_by_count":86,"area":null},{"id":"2303.10868","title":"Retrieving Multimodal Information for Augmented Generation: A Survey","created":"2023-03-20","cited_by_count":85,"area":null},{"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":"2412.16075","title":"Formal Mathematical Reasoning: A New Frontier in AI","created":"2024-12-20","cited_by_count":81,"area":"lr"},{"id":"2401.00812","title":"If LLM Is the Wizard, Then Code Is the Wand: A Survey on How Code Empowers Large Language Models to Serve as Intelligent Agents","created":"2024-01-01","cited_by_count":79,"area":"agents"},{"id":"2403.01632","title":"SynCode: LLM Generation with Grammar Augmentation","created":"2024-03-03","cited_by_count":69,"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":"2303.04864","title":"nl2spec: Interactively Translating Unstructured Natural Language to Temporal Logics with Large Language Models","created":"2023-03-08","cited_by_count":60,"area":null},{"id":"2410.10878","title":"Herald: A Natural Language Annotated Lean 4 Dataset","created":"2024-10-09","cited_by_count":59,"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":"2403.18120","title":"Don't Trust: Verify -- Grounding LLM Quantitative Reasoning with Autoformalization","created":"2024-03-26","cited_by_count":55,"area":"lr"},{"id":"2303.04488","title":"Magnushammer: A Transformer-Based Approach to Premise Selection","created":"2023-03-08","cited_by_count":50,"area":null},{"id":"2406.01940","title":"Process-Driven Autoformalization in Lean 4","created":"2024-06-04","cited_by_count":45,"area":"lr"},{"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":"2311.03755","title":"Multilingual Mathematical Autoformalization","created":"2023-11-07","cited_by_count":39,"area":null},{"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":"2401.12491","title":"Assessing and Understanding Creativity in Large Language Models","created":"2024-01-23","cited_by_count":35,"area":null},{"id":"2405.01379","title":"Verification and Refinement of Natural Language Explanations through LLM-Symbolic Theorem Proving","created":"2024-05-02","cited_by_count":35,"area":null},{"id":"2410.12112","title":"Planning Anything with Rigor: General-Purpose Zero-Shot Planning with LLM-based Formalized Programming","created":"2024-10-15","cited_by_count":35,"area":null},{"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":"2206.01962","title":"Formal Specifications from Natural Language","created":"2022-06-04","cited_by_count":33,"area":null},{"id":"2406.07222","title":"Reliable Evaluation and Benchmarks for Statement Autoformalization","created":"2024-06-11","cited_by_count":32,"area":null},{"id":"2309.01933","title":"Provably safe systems: the only path to controllable AGI","created":"2023-09-05","cited_by_count":29,"area":null},{"id":"2301.02195","title":"Towards Autoformalization of Mathematics and Code Correctness: Experiments with Elementary Proofs","created":"2023-01-05","cited_by_count":27,"area":null},{"id":"2405.17216","title":"Autoformalizing Euclidean Geometry","created":"2024-05-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":"2405.14414","title":"Proving Theorems Recursively","created":"2024-05-23","cited_by_count":26,"area":null},{"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":"2312.07622","title":"Mathematical Language Models: A Survey","created":"2023-12-12","cited_by_count":24,"area":null},{"id":"2410.10135","title":"FormalAlign: Automated Alignment Evaluation for Autoformalization","created":"2024-10-14","cited_by_count":24,"area":null},{"id":"2209.13020","title":"Law Informs Code: A Legal Informatics Approach to Aligning Artificial Intelligence with Humans","created":"2022-09-14","cited_by_count":23,"area":null},{"id":"2405.20671","title":"Position Coupling: Improving Length Generalization of Arithmetic Transformers Using Task Structure","created":"2024-05-31","cited_by_count":23,"area":null},{"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":"2211.07524","title":"Towards a Mathematics Formalisation Assistant using Large Language Models","created":"2022-11-14","cited_by_count":22,"area":null},{"id":"2409.14274","title":"Proof Automation with Large Language Models","created":"2024-09-22","cited_by_count":22,"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":"2502.02362","title":"Premise-Augmented Reasoning Chains Improve Error Identification in Math reasoning with LLMs","created":"2025-02-04","cited_by_count":22,"area":"lr"},{"id":"2503.18492","title":"VeriSafe Agent: Safeguarding Mobile GUI Agent via Logic-based Action Verification","created":"2025-03-24","cited_by_count":22,"area":"agents"},{"id":"2305.19213","title":"The Magic of IF: Investigating Causal Reasoning Abilities in Large Language Models of Code","created":"2023-05-30","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":"2510.04520","title":"Aria: An Agent For Retrieval and Iterative Auto-Formalization via Dependency Graph","created":"2025-10-06","cited_by_count":21,"area":"agents"},{"id":"2510.15981","title":"ProofFlow: A Dependency Graph Approach to Faithful Proof Autoformalization","created":"2025-10-13","cited_by_count":21,"area":null},{"id":"2510.24592","title":"ReForm: Reflective Autoformalization with Prospective Bounded Sequence Optimization","created":"2025-10-28","cited_by_count":20,"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.12189","title":"Mitigating Content Effects on Reasoning in Language Models through Fine-Grained Activation Steering","created":"2025-05-18","cited_by_count":18,"area":"lr"},{"id":"2506.07047","title":"Mathesis: Towards Formal Theorem Proving from Natural Languages","created":"2025-06-08","cited_by_count":18,"area":null},{"id":"2506.11085","title":"LeanExplore: A search engine for Lean 4 declarations","created":"2025-06-04","cited_by_count":18,"area":null},{"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":"2601.03298","title":"130k Lines of Formal Topology in Two Weeks: Simple and Cheap Autoformalization for Everyone?","created":"2026-01-06","cited_by_count":18,"area":null},{"id":"2507.06181","title":"CriticLean: Critic-Guided Reinforcement Learning for Mathematical Formalization","created":"2025-07-08","cited_by_count":16,"area":"lr"},{"id":"2508.04440","title":"StepFun-Formalizer: Unlocking the Autoformalization Potential of LLMs through Knowledge-Reasoning Fusion","created":"2025-08-06","cited_by_count":16,"area":"lr"},{"id":"2602.17016","title":"M2F: Automated Formalization of Mathematical Literature at Scale","created":"2026-02-19","cited_by_count":15,"area":null},{"id":"2511.03108","title":"miniF2F-Lean Revisited: Reviewing Limitations and Charting a Path Forward","created":"2025-11-05","cited_by_count":14,"area":null},{"id":"2401.08664","title":"Adapting Large Language Models for Education: Foundational Capabilities, Potentials, and Challenges","created":"2023-12-27","cited_by_count":13,"area":null},{"id":"2212.01944","title":"Automaton-Based Representations of Task Knowledge from Generative Language Models","created":"2022-12-04","cited_by_count":12,"area":null},{"id":"2301.09723","title":"Mathematics, word problems, common sense, and artificial intelligence","created":"2023-01-23","cited_by_count":12,"area":"lr"},{"id":"2310.18239","title":"Fine-Tuning Language Models Using Formal Methods Feedback","created":"2023-10-27","cited_by_count":12,"area":"alignment"},{"id":"2402.13321","title":"Rigor with Machine Learning from Field Theory to the Poincar\\'e Conjecture","created":"2024-02-20","cited_by_count":12,"area":null},{"id":"2507.07399","title":"Generalized Tree Edit Distance (GTED): A Faithful Evaluation Metric for Statement Autoformalization","created":"2025-07-10","cited_by_count":12,"area":null},{"id":"2606.03303","title":"LEAP: Supercharging LLMs for Formal Mathematics with Agentic Frameworks","created":"2026-06-02","cited_by_count":12,"area":"lr"},{"id":"2606.05400","title":"LeanMarathon: Toward Reliable AI Co-Mathematicians through Long-Horizon Lean Autoformalization","created":"2026-06-03","cited_by_count":12,"area":null},{"id":"2402.16269","title":"From Large Language Models and Optimization to Decision Optimization CoPilot: A Research Manifesto","created":"2024-02-26","cited_by_count":11,"area":null},{"id":"2408.05506","title":"Your Context Is Not an Array: Unveiling Random Access Limitations in Transformers","created":"2024-08-10","cited_by_count":11,"area":null},{"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":"2310.07957","title":"A New Approach Towards Autoformalization","created":"2023-10-12","cited_by_count":10,"area":null}],"next_cursor":"100"}