{"total":55,"rows":[{"id":"2306.15626","title":"LeanDojo: Theorem Proving with Retrieval-Augmented Language Models","created":"2023-06-27","cited_by_count":427,"area":"rag"},{"id":"2109.00110","title":"MiniF2F: a cross-system benchmark for formal Olympiad-level mathematics","created":"2021-08-31","cited_by_count":391,"area":null},{"id":"2105.04165","title":"Inter-GPS: Interpretable Geometry Problem Solving with Formal Language and Symbolic Reasoning","created":"2021-05-10","cited_by_count":383,"area":null},{"id":"2102.06203","title":"Proof Artifact Co-training for Theorem Proving with Language Models","created":"2021-02-11","cited_by_count":132,"area":"offlinerl"},{"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":"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":"2404.09939","title":"A Survey on Deep Learning for Theorem Proving","created":"2024-04-15","cited_by_count":57,"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":"2101.06223","title":"LIME: Learning Inductive Bias for Primitives of Mathematical Reasoning","created":"2021-01-15","cited_by_count":46,"area":null},{"id":"2210.15889","title":"Towards Data-and Knowledge-Driven Artificial Intelligence: A Survey on Neuro-Symbolic Computing","created":"2022-10-28","cited_by_count":35,"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":"2107.11864","title":"Neural Circuit Synthesis from Specification Patterns","created":"2021-07-25","cited_by_count":17,"area":null},{"id":"2102.03824","title":"Neural Termination Analysis","created":"2021-02-07","cited_by_count":16,"area":null},{"id":"2106.03906","title":"Learning to Guide a Saturation-Based Theorem Prover","created":"2021-06-07","cited_by_count":15,"area":null},{"id":"2401.02949","title":"Graph2Tac: Online Representation Learning of Formal Math Concepts","created":"2024-01-05","cited_by_count":15,"area":null},{"id":"2307.00928","title":"Learning Differentiable Logic Programs for Abstract Visual Reasoning","created":"2023-07-03","cited_by_count":12,"area":"lr"},{"id":"2101.11981","title":"Embedding Symbolic Temporal Knowledge into Deep Sequential Models","created":"2021-01-28","cited_by_count":11,"area":"offlinerl"},{"id":"2303.11730","title":"Abstract Visual Reasoning: An Algebraic Approach for Solving Raven's Progressive Matrices","created":"2023-03-21","cited_by_count":9,"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":"2408.14915","title":"Can Transformers Do Enumerative Geometry?","created":"2024-08-27","cited_by_count":8,"area":null},{"id":"2311.01230","title":"Multi-Operational Mathematical Derivations in Latent Space","created":"2023-11-02","cited_by_count":6,"area":null},{"id":"2110.10054","title":"Generating Symbolic Reasoning Problems with Transformer GANs","created":"2021-10-19","cited_by_count":5,"area":null},{"id":"2101.09142","title":"A Study of Continuous Vector Representationsfor Theorem Proving","created":"2021-01-22","cited_by_count":4,"area":null},{"id":"2110.01639","title":"An energy-based model for neuro-symbolic reasoning on knowledge graphs","created":"2021-10-04","cited_by_count":4,"area":null},{"id":"2305.08676","title":"An Ensemble Approach for Automated Theorem Proving Based on Efficient Name Invariant Graph Neural Representations","created":"2023-05-15","cited_by_count":4,"area":null},{"id":"2108.10821","title":"Graph Contrastive Pre-training for Effective Theorem Reasoning","created":"2021-08-24","cited_by_count":3,"area":null},{"id":"2109.10476","title":"Self-Supervised Learning to Prove Equivalence Between Straight-Line Programs via Rewrite Rules","created":"2021-09-22","cited_by_count":3,"area":null},{"id":"2203.04699","title":"Gym-saturation: an OpenAI Gym environment for saturation provers","created":"2022-03-09","cited_by_count":3,"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":"2406.11563","title":"Intersymbolic AI: Interlinking Symbolic AI and Subsymbolic AI","created":"2024-06-17","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":"2503.04772","title":"Generating Millions Of Lean Theorems With Proofs By Exploring State Transition Graphs","created":"2025-02-16","cited_by_count":3,"area":null},{"id":"2207.11649","title":"OCTAL: Graph Representation Learning for LTL Model Checking","created":"2022-07-24","cited_by_count":2,"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":"2402.02104","title":"Learning Structure-Aware Representations of Dependent Types","created":"2024-02-03","cited_by_count":2,"area":null},{"id":"2402.15524","title":"Graph Pruning for Enumeration of Minimal Unsatisfiable Subsets","created":"2024-02-19","cited_by_count":2,"area":null},{"id":"2403.03401","title":"BAIT: Benchmarking (Embedding) Architectures for Interactive Theorem-Proving","created":"2024-03-06","cited_by_count":2,"area":null},{"id":"2411.14870","title":"Application of AI to formal methods - an analysis of current trends","created":"2024-11-22","cited_by_count":2,"area":null},{"id":"2206.06986","title":"Exploring Representation of Horn Clauses using GNNs (Extended Technical Report)","created":"2022-06-14","cited_by_count":1,"area":null},{"id":"2207.06679","title":"Learning to Prove Trigonometric Identities","created":"2022-07-14","cited_by_count":1,"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":"2411.05820","title":"Guiding Genetic Programming with Graph Neural Networks","created":"2024-11-03","cited_by_count":1,"area":null},{"id":"2411.15194","title":"Guiding Word Equation Solving using Graph Neural Networks (Extended Technical Report)","created":"2024-11-19","cited_by_count":1,"area":null},{"id":"2504.19188","title":"Hierarchical Attention Generates Better Proofs","created":"2025-04-27","cited_by_count":1,"area":null},{"id":"2510.21999","title":"Foundation of Intelligence: Review of Math Word Problems from Human Cognition Perspective","created":"2025-10-24","cited_by_count":1,"area":null},{"id":"2605.22257","title":"What are the Right Symmetries for Formal Theorem Proving?","created":"2026-05-21","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":"2107.09766","title":"Learning Heuristics for Template-based CEGIS of Loop Invariants with Reinforcement Learning","created":"2021-07-16","cited_by_count":0,"area":null},{"id":"2208.14641","title":"Generating Intermediate Steps for NLI with Next-Step Supervision","created":"2022-08-31","cited_by_count":0,"area":null},{"id":"2308.13474","title":"OCTAL: Graph Representation Learning for LTL Model Checking","created":"2023-08-19","cited_by_count":0,"area":null},{"id":"2403.14690","title":"Incorporating Graph Attention Mechanism into Geometric Problem Solving Based on Deep Reinforcement Learning","created":"2024-03-14","cited_by_count":0,"area":"deeprl"},{"id":"2507.03314","title":"Partial Label Learning for Automated Theorem Proving","created":"2025-07-04","cited_by_count":0,"area":null},{"id":"2510.01853","title":"Learning Representations Through Contrastive Neural Model Checking","created":"2025-10-02","cited_by_count":0,"area":null},{"id":"2602.18767","title":"Nazrin: An Atomic Neural Proof Automation Tactic in Lean 4","created":"2026-02-21","cited_by_count":0,"area":null},{"id":"2604.02350","title":"Differentiable Symbolic Planning: A Neural Architecture for Constraint Reasoning with Learned Feasibility","created":"2026-02-19","cited_by_count":0,"area":null}],"next_cursor":null}