{"total":74,"rows":[{"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":"2407.11214","title":"PutnamBench: Evaluating Neural Theorem-Provers on the Putnam Mathematical Competition","created":"2024-07-15","cited_by_count":165,"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":"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":"2306.01694","title":"Evaluating Language Models for Mathematics through Interactions","created":"2023-06-02","cited_by_count":70,"area":null},{"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":"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":"2408.03350","title":"miniCTX: Neural Theorem Proving with (Long-)Contexts","created":"2024-08-05","cited_by_count":37,"area":null},{"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":"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":"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":"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":"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":"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":"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":"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":"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":"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":"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":"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":"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.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":"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.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":"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},{"id":"2512.07501","title":"AutoICE: Automatically Synthesizing Verifiable C Code via LLM-driven Evolution","created":"2025-12-08","cited_by_count":0,"area":null},{"id":"2601.00125","title":"Constructing a Neuro-Symbolic Mathematician from First Principles","created":"2025-12-31","cited_by_count":0,"area":null},{"id":"2602.11481","title":"Compiler-Guided Inference-Time Adaptation: Improving GPT-5 Programming Performance in Idris","created":"2026-02-12","cited_by_count":0,"area":null},{"id":"2605.23931","title":"BODHI: Precise OS Kernel Specification Inference","created":"2026-04-22","cited_by_count":0,"area":null},{"id":"2606.26490","title":"An Empirical Study of LLM-Generated Specifications for VeriFast","created":"2026-06-25","cited_by_count":0,"area":null},{"id":"2607.09366","title":"Diversifying to Verify: When Task-Equivalent Programs Differ in Verifiability","created":"2026-07-10","cited_by_count":0,"area":null},{"id":"2608.13459","title":"CAPRI: Contract-Aware Proof Repair for Isabelle","created":"2026-08-13","cited_by_count":0,"area":null},{"id":"2609.23954","title":"Djinnlang: Higher-Level Programming by Unambiguous Specification with an LLM in the Compiler","created":"2026-09-21","cited_by_count":0,"area":null},{"id":"2609.38384","title":"LeanPolish: Verified Supervision for Lean Proof Compression","created":"2026-09-29","cited_by_count":0,"area":null},{"id":"2609.39228","title":"Fyan: A Human--AI Harness with Semantic Auditing for Document-Level Formalization","created":"2026-09-30","cited_by_count":0,"area":null},{"id":"2610.11862","title":"LEVER: Adaptive Cost-Aware Proof Search Over AND/OR Graphs","created":"2026-10-08","cited_by_count":0,"area":null}],"next_cursor":null}