{"total":57,"rows":[{"id":"2412.16075","title":"Formal Mathematical Reasoning: A New Frontier in AI","created":"2024-12-20","cited_by_count":81,"area":"lr"},{"id":"2406.08467","title":"DafnyBench: A Benchmark for Formal Software Verification","created":"2024-06-12","cited_by_count":57,"area":null},{"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":"2409.13082","title":"AutoVerus: Automated Proof Generation for Rust Code","created":"2024-09-19","cited_by_count":49,"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":"2405.17216","title":"Autoformalizing Euclidean Geometry","created":"2024-05-27","cited_by_count":27,"area":null},{"id":"2410.10135","title":"FormalAlign: Automated Alignment Evaluation for Autoformalization","created":"2024-10-14","cited_by_count":24,"area":null},{"id":"2502.00963","title":"PDE-Controller: LLMs for Autoformalization and Reasoning of PDEs","created":"2025-02-03","cited_by_count":23,"area":"lr"},{"id":"2406.14408","title":"FVEL: Interactive Formal Verification Environment with Large Language Models via Theorem Proving","created":"2024-06-20","cited_by_count":22,"area":null},{"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":"2602.06176","title":"Large Language Model Reasoning Failures","created":"2026-02-05","cited_by_count":21,"area":"lr"},{"id":"2510.24592","title":"ReForm: Reflective Autoformalization with Prospective Bounded Sequence Optimization","created":"2025-10-28","cited_by_count":20,"area":"lr"},{"id":"2501.16207","title":"From Informal to Formal -- Incorporating and Evaluating LLMs on Natural Language Requirements to Verifiable Formal Proofs","created":"2025-01-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":"2506.11487","title":"Reviving DSP for Advanced Theorem Proving in the Era of Reasoning Models","created":"2025-06-13","cited_by_count":17,"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":"2512.18436","title":"VeruSAGE: A Study of Agent-Based Verification for Rust Systems","created":"2025-12-20","cited_by_count":12,"area":"agents"},{"id":"2405.16792","title":"Laurel: Unblocking Automated Verification with Large Language Models","created":"2024-05-27","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":"2410.19940","title":"Cobblestone: A Divide-and-Conquer Approach for Automating Formal Verification","created":"2024-10-25","cited_by_count":9,"area":null},{"id":"2503.01424","title":"From Hypothesis to Publication: A Comprehensive Survey of AI-Driven Research Support Systems","created":"2025-03-03","cited_by_count":8,"area":null},{"id":"2505.24264","title":"Faithful and Robust LLM-Driven Theorem Proving for NLI Explanations","created":"2025-05-30","cited_by_count":8,"area":null},{"id":"2510.06857","title":"Autoformalizer with Tool Feedback","created":"2025-10-08","cited_by_count":7,"area":null},{"id":"2505.03418","title":"Knowledge Augmented Complex Problem Solving with Large Language Models: A Survey","created":"2025-05-06","cited_by_count":6,"area":"lr"},{"id":"2506.10558","title":"StepProof: Step-by-step verification of natural language mathematical proofs","created":"2025-06-12","cited_by_count":6,"area":null},{"id":"2511.17330","title":"Agentic Verification of Software Systems","created":"2025-11-21","cited_by_count":6,"area":"agents"},{"id":"2510.02335","title":"FormalML: A Benchmark for Evaluating Formal Subgoal Completion in Machine Learning Theory","created":"2025-09-26","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":"2604.26311","title":"DreamProver: Evolving Transferable Lemma Libraries via a Wake-Sleep Theorem-Proving Agent","created":"2026-04-29","cited_by_count":5,"area":"agents"},{"id":"2410.15748","title":"Alchemy: Amplifying Theorem-Proving Capability through Symbolic Mutation","created":"2024-10-21","cited_by_count":4,"area":null},{"id":"2410.20274","title":"Library Learning Doesn't: The Curious Case of the Single-Use \"Library\"","created":"2024-10-26","cited_by_count":4,"area":"lr"},{"id":"2502.04675","title":"Scalable Oversight for Superhuman AI via Recursive Self-Critiquing","created":"2025-02-07","cited_by_count":4,"area":"alignment"},{"id":"2502.05344","title":"RAG-Verus: Repository-Level Program Verification with LLMs using Retrieval Augmented Generation","created":"2025-02-07","cited_by_count":4,"area":"rag"},{"id":"2506.08321","title":"LeanTutor: Towards a Verified AI Mathematical Proof Tutor","created":"2025-06-10","cited_by_count":4,"area":null},{"id":"2507.11936","title":"A Survey of Deep Learning for Geometry Problem Solving","created":"2025-07-16","cited_by_count":4,"area":"lr"},{"id":"2509.25197","title":"Towards Repository-Level Program Verification with Large Language Models","created":"2025-08-31","cited_by_count":4,"area":null},{"id":"2606.26525","title":"Theory-Scale Auto-Formalization of Logics for Computer Science","created":"2026-06-25","cited_by_count":4,"area":null},{"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":"2409.11074","title":"RoMath: A Mathematical Reasoning Benchmark in Romanian","created":"2024-09-17","cited_by_count":2,"area":"lr"},{"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":"2511.11990","title":"Improving Autoformalization Using Direct Dependency Retrieval","created":"2025-11-15","cited_by_count":2,"area":"rag"},{"id":"2512.18256","title":"MSC-180: A Benchmark for Automated Formal Theorem Proving from Mathematical Subject Classification","created":"2025-12-20","cited_by_count":2,"area":null},{"id":"2605.16385","title":"Hilbert-Geo: Solving Solid Geometric Problems by Neural-Symbolic Reasoning","created":"2026-05-11","cited_by_count":2,"area":"lr"},{"id":"2606.14688","title":"Flood and Harvest: The Provable Necessity of Trivia for Generating Valuable Mathematics via the Lens of Language Generation in the Limit","created":"2026-06-12","cited_by_count":2,"area":null},{"id":"2608.15432","title":"Does the Proof Prove It That Way? Faithful Formalization of Elements Proofs","created":"2026-08-15","cited_by_count":2,"area":null},{"id":"2608.20686","title":"CDRL: Certification-Driven Reinforcement Learning for Neutrino Flavor Model Discovery","created":"2026-08-21","cited_by_count":2,"area":"lr"},{"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.28841","title":"LAMP: Lean-based Agentic framework with MCP and Proof Repair","created":"2026-06-27","cited_by_count":1,"area":"lr"},{"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":"2509.02758","title":"An Ontology-Based Approach to Optimizing Geometry Problem Sets for Skill Development","created":"2025-09-02","cited_by_count":0,"area":"lr"},{"id":"2510.01853","title":"Learning Representations Through Contrastive Neural Model Checking","created":"2025-10-02","cited_by_count":0,"area":null},{"id":"2601.17473","title":"LeanTutor: Towards a Verified AI Mathematical Proof Tutor","created":"2026-01-24","cited_by_count":0,"area":null},{"id":"2602.10512","title":"Exponential Sample Complexity Separation between Flat and Hierarchical Agentic Theorem Provers","created":"2026-02-11","cited_by_count":0,"area":"agents"},{"id":"2605.22885","title":"ImProver 2: Iteratively Self-Improving LMs for Neurosymbolic Proof Optimization","created":"2026-05-21","cited_by_count":0,"area":null},{"id":"2609.15194","title":"Semiotic Relations and Proof Methods: A Cross-Genre Study of Argument Structure with Large Language Models","created":"2026-09-14","cited_by_count":0,"area":null},{"id":"2610.02792","title":"Law And Order: Tax Law Autoformalization","created":"2026-10-02","cited_by_count":0,"area":null}],"next_cursor":null}