{"total":119,"rows":[{"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":"2406.01297","title":"When Can LLMs Actually Correct Their Own Mistakes? A Critical Survey of Self-Correction of LLMs","created":"2024-06-03","cited_by_count":240,"area":null},{"id":"2308.03188","title":"Automatically Correcting Large Language Models: Surveying the landscape of diverse self-correction strategies","created":"2023-08-06","cited_by_count":238,"area":"lr"},{"id":"2407.11214","title":"PutnamBench: Evaluating Neural Theorem-Provers on the Putnam Mathematical Competition","created":"2024-07-15","cited_by_count":165,"area":null},{"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":"2310.00656","title":"LEGO-Prover: Neural Theorem Proving with Growing Libraries","created":"2023-10-01","cited_by_count":109,"area":null},{"id":"2507.15855","title":"Winning Gold at IMO 2025 with a Model-Agnostic Verification-and-Refinement Pipeline","created":"2025-07-21","cited_by_count":82,"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":"2306.01694","title":"Evaluating Language Models for Mathematics through Interactions","created":"2023-06-02","cited_by_count":70,"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":"2411.17501","title":"The Limits of Inference Scaling Through Resampling","created":"2024-11-26","cited_by_count":53,"area":null},{"id":"2310.04870","title":"Lemur: Integrating Large Language Models in Automated Program Verification","created":"2023-10-07","cited_by_count":49,"area":null},{"id":"2409.13082","title":"AutoVerus: Automated Proof Generation for Rust Code","created":"2024-09-19","cited_by_count":49,"area":null},{"id":"2308.09895","title":"Knowledge Transfer from High-Resource to Low-Resource Programming Languages for Code LLMs","created":"2023-08-19","cited_by_count":45,"area":null},{"id":"2502.03671","title":"Advancing Reasoning in Large Language Models: Promising Methods and Approaches","created":"2025-02-05","cited_by_count":43,"area":"lr"},{"id":"2307.10236","title":"Look Before You Leap: An Exploratory Study of Uncertainty Measurement for Large Language Models","created":"2023-07-16","cited_by_count":41,"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":"2408.03350","title":"miniCTX: Neural Theorem Proving with (Long-)Contexts","created":"2024-08-05","cited_by_count":37,"area":null},{"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":"2505.23135","title":"VERINA: Benchmarking Verifiable Code Generation","created":"2025-05-29","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":"2506.19923","title":"Prover Agent: An Agent-Based Framework for Formal Mathematical Proofs","created":"2025-06-24","cited_by_count":31,"area":"agents"},{"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":"2312.07622","title":"Mathematical Language Models: A Survey","created":"2023-12-12","cited_by_count":24,"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":"2405.01787","title":"Towards Neural Synthesis for SMT-Assisted Proof-Oriented Programming","created":"2024-05-03","cited_by_count":20,"area":null},{"id":"2305.14699","title":"Can Transformers Learn to Solve Problems Recursively?","created":"2023-05-24","cited_by_count":17,"area":null},{"id":"2502.13834","title":"Proving Olympiad Inequalities by Synergizing LLMs and Symbolic Reasoning","created":"2025-02-19","cited_by_count":17,"area":"lr"},{"id":"2504.13828","title":"Generative AI Act II: Test Time Scaling Drives Cognition Engineering","created":"2025-04-18","cited_by_count":15,"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":"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":"2606.03303","title":"LEAP: Supercharging LLMs for Formal Mathematics with Agentic Frameworks","created":"2026-06-02","cited_by_count":12,"area":"lr"},{"id":"2311.03739","title":"Leveraging Large Language Models for Automated Proof Synthesis in Rust","created":"2023-11-07","cited_by_count":11,"area":null},{"id":"2405.16792","title":"Laurel: Unblocking Automated Verification with Large Language Models","created":"2024-05-27","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":"2410.19605","title":"CoqPilot, a plugin for LLM-based generation of proofs","created":"2024-10-25","cited_by_count":11,"area":null},{"id":"2412.15184","title":"Data for Mathematical Copilots: Better Ways of Presenting Proofs for Machine Learning","created":"2024-12-19","cited_by_count":11,"area":null},{"id":"2511.18760","title":"HERMES: Towards Efficient and Verifiable Mathematical Reasoning in LLMs","created":"2025-11-24","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":"2310.13021","title":"AI for Mathematics: A Cognitive Science Perspective","created":"2023-10-19","cited_by_count":10,"area":null},{"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":"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":"2410.19940","title":"Cobblestone: A Divide-and-Conquer Approach for Automating Formal Verification","created":"2024-10-25","cited_by_count":9,"area":null},{"id":"2312.04556","title":"Large Language Models for Mathematicians","created":"2023-12-07","cited_by_count":7,"area":null},{"id":"2502.15441","title":"On the Effectiveness of Large Language Models in Writing Alloy Formulas","created":"2025-02-21","cited_by_count":7,"area":null},{"id":"2504.02902","title":"Beyond Accuracy: The Role of Calibration in Self-Improving Large Language Models","created":"2025-04-03","cited_by_count":7,"area":"synth"},{"id":"2506.03332","title":"Helpful Agent Meets Deceptive Judge: Understanding Vulnerabilities in Agentic Workflows","created":"2025-06-03","cited_by_count":7,"area":"agents"},{"id":"2507.06804","title":"Towards Solving More Challenging IMO Problems via Decoupled Reasoning and Proving","created":"2025-07-07","cited_by_count":7,"area":"lr"},{"id":"2605.17283","title":"OProver: A Unified Framework for Agentic Formal Theorem Proving","created":"2026-05-17","cited_by_count":7,"area":"agents"},{"id":"2406.15540","title":"Specify What? Enhancing Neural Specification Synthesis by Symbolic Methods","created":"2024-06-21","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":"2505.15740","title":"HybridProver: Augmenting Theorem Proving with LLM-Driven Proof Synthesis and Refinement","created":"2025-05-21","cited_by_count":6,"area":null},{"id":"2506.07477","title":"Premise Selection for a Lean Hammer","created":"2025-06-09","cited_by_count":6,"area":null},{"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":"2512.04680","title":"Generative AI for Self-Adaptive Systems: State of the Art and Research Roadmap","created":"2025-12-04","cited_by_count":5,"area":null},{"id":"2402.13577","title":"BBA: Bi-Modal Behavioral Alignment for Reasoning with Large Vision-Language Models","created":"2024-02-21","cited_by_count":4,"area":"lr"},{"id":"2502.07728","title":"Verifying LLM-Generated Code in the Context of Software Verification with Ada/SPARK","created":"2025-02-11","cited_by_count":4,"area":null},{"id":"2502.15507","title":"Steering LLMs for Formal Theorem Proving","created":"2025-02-21","cited_by_count":4,"area":null},{"id":"2510.25626","title":"Are Language Models Efficient Reasoners? A Perspective from Logic Programming","created":"2025-10-29","cited_by_count":4,"area":"lr"},{"id":"2603.01896","title":"Agentic Code Reasoning","created":"2026-03-02","cited_by_count":4,"area":"lr"},{"id":"2605.23109","title":"Inductive Deductive Synthesis: Enabling AI to Generate Formally Verified Systems","created":"2026-05-22","cited_by_count":4,"area":null},{"id":"2401.12131","title":"NeuroSynt: A Neuro-symbolic Portfolio Solver for Reactive Synthesis","created":"2024-01-22","cited_by_count":3,"area":null},{"id":"2408.09237","title":"QEDCartographer: Automating Formal Verification Using Reward-Free Reinforcement Learning","created":"2024-08-17","cited_by_count":3,"area":"deeprl"},{"id":"2504.04945","title":"A Llama walks into the 'Bar': Efficient Supervised Fine-Tuning for Legal Reasoning in the Multi-state Bar Exam","created":"2025-04-07","cited_by_count":3,"area":"lr"},{"id":"2508.18587","title":"A Case Study on the Effectiveness of LLMs in Verification with Proof Assistants","created":"2025-08-26","cited_by_count":3,"area":null},{"id":"2509.23675","title":"PAT-Agent: Autoformalization for Model Checking","created":"2025-09-28","cited_by_count":3,"area":"agents"},{"id":"2605.17475","title":"Event-B Agent: Towards LLM Agent for Formal Model Synthesis and Repair","created":"2026-05-17","cited_by_count":3,"area":"agents"},{"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},{"id":"2505.04528","title":"Beyond Theorem Proving: Formulation, Framework and Benchmark for Formal Problem-Solving","created":"2025-05-07","cited_by_count":2,"area":null},{"id":"2509.14274","title":"Discovering New Theorems via LLMs with In-Context Proof Learning in Lean","created":"2025-09-16","cited_by_count":2,"area":null},{"id":"2510.10066","title":"OBsmith: LLM-Powered JavaScript Obfuscator Testing","created":"2025-10-11","cited_by_count":2,"area":null},{"id":"2602.04892","title":"Doc2Spec: Synthesizing Formal Programming Specifications from Natural Language via Grammar Induction","created":"2026-01-30","cited_by_count":2,"area":null},{"id":"2607.03656","title":"AutoCedar: An Agentic Framework for Verifier-Guided Access Control Policy Synthesis","created":"2026-07-04","cited_by_count":2,"area":"agents"},{"id":"2608.09277","title":"P$^{3}$: Joint Program-and-Proof Planning for Verified Code Generation","created":"2026-08-10","cited_by_count":2,"area":null},{"id":"2307.09998","title":"Controlling Equational Reasoning in Large Language Models with Prompt Interventions","created":"2023-07-19","cited_by_count":1,"area":"lr"},{"id":"2402.08365","title":"Learning Better Representations From Less Data For Propositional Satisfiability","created":"2024-02-13","cited_by_count":1,"area":null},{"id":"2511.13043","title":"Spark-Prover-X1: Formal Theorem Proving Through Diverse Data Training","created":"2025-11-17","cited_by_count":1,"area":null},{"id":"2512.02080","title":"The 4/$\\delta$ Bound: Designing Predictable LLM-Verifier Systems for Formal Method Guarantee","created":"2025-11-30","cited_by_count":1,"area":null},{"id":"2512.14252","title":"G\\\"odel's Poetry","created":"2025-12-16","cited_by_count":1,"area":null},{"id":"2603.19715","title":"Neuro-Symbolic Proof Generation for Scaling Systems Software Verification","created":"2026-03-20","cited_by_count":1,"area":null},{"id":"2606.06133","title":"TLA-Prover: Verifiable TLA+ Specification Synthesis via Preference-Optimized Low-Rank Adaptation","created":"2026-06-04","cited_by_count":1,"area":"alignment"},{"id":"2606.09450","title":"TheoremBench: Evaluating LLMs on Theorem Proving in Formal Mathematics","created":"2026-06-08","cited_by_count":1,"area":null},{"id":"2606.18098","title":"IsabeLLM: Automated Theorem Proving Applied to Formally Verifying Consensus","created":"2026-06-16","cited_by_count":1,"area":null},{"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":"2607.04562","title":"Heaviside Continuity of Rolling Coefficients for Eliminating Epistemic Entropy in Large Language Models","created":"2026-07-06","cited_by_count":1,"area":null},{"id":"2607.06341","title":"Harnessing Code Agents for Automatic Software Verification","created":"2026-07-07","cited_by_count":1,"area":"agents"},{"id":"2607.07779","title":"From Solvers to Research: Large Language Model-Driven Formal Mathematics at the Research Frontier","created":"2026-07-08","cited_by_count":1,"area":null},{"id":"2607.22511","title":"CausalSmith: A Formally Grounded, Self-Improving Agentic Framework for Automated Research in Causal Inference","created":"2026-07-24","cited_by_count":1,"area":"agents"},{"id":"2310.17064","title":"math-PVS: A Large Language Model Framework to Map Scientific Publications to PVS Theories","created":"2023-10-25","cited_by_count":0,"area":null},{"id":"2410.18107","title":"In-Context Code-Text Learning for Bimodal Software Engineering","created":"2024-10-08","cited_by_count":0,"area":null}],"next_cursor":"100"}