mlsanityData to 7 Oct 2026

Application of AI to formal methods - an analysis of current trends

arXiv 2411.14870 ↗First posted 22 Nov 2024cs.LO cs.AI cs.LGcited by 2

Not on the map. Why?

Abstract (arXiv)

Context: With artificial intelligence (AI) being well established within the daily lives of research communities, we turn our gaze toward formal methods (FM). FM aim to provide sound and verifiable reasoning about problems in computer science. Objective: We conduct a systematic mapping study to overview the current landscape of research publications that apply AI to FM. We aim to identify how FM can benefit from AI techniques and highlight areas for further research. Our focus lies on the previous five years (2019-2023) of research. Method: Following the proposed guidelines for systematic mapping studies, we searched for relevant publications in four major databases, defined inclusion and exclusion criteria, and applied extensive snowballing to uncover potential additional sources. Results: This investigation results in 189 entries which we explored to find current trends and highlight research gaps. We find a strong focus on AI in the area of theorem proving while other subfields of FM are less represented. Conclusions: The mapping study provides a quantitative overview of the modern state of AI application in FM. The current trend of the field is yet to mature. Many primary studies focus on practical application, yet we identify a lack of theoretical groundwork, standard benchmarks, or case studies. Further, we identify issues regarding shared training data sets and standard benchmarks.

Key facts. Cited by 2 papers in the map (data through 7 Oct 2026). Builds on 66 of its 262 references that are in the map. First posted on arXiv 22 Nov 2024.

Builds on

66 of 262 references.

References · 66

  1. 2017Attention Is All You Needcited by 59,932
  2. 2016OpenAI Gymcited by 1,684
  3. 2018Graph Neural Networks: A Review of Methods and Applicationscited by 1,571
  4. 2023A Survey on Evaluation of Large Language Modelscited by 1,227
  5. 2018Learning a SAT Solver from Single-Bit Supervisioncited by 198
  6. 2017Natural Language Processing: State of The Art, Current Trends and Challengescited by 114
  7. 2019Learning to Prove Theorems via Interacting with Proof Assistantscited by 107
  8. 2022Thor: Wielding Hammers to Integrate Language Models and Automated Theorem Proverscited by 97
  9. 2019Guiding High-Performance SAT Solvers with Unsat-Core Predictionscited by 61
  10. 2019Graph Representations for Higher-Order Logic and Theorem Provingcited by 55
  11. 2018GamePad: A Learning Environment for Theorem Provingcited by 48
  12. 2018TacticToe: Learning to Prove with Tacticscited by 43
38 more
  1. 2020Learning to Prove Theorems by Learning to Generate Theoremscited by 43
  2. 2021TacticZero: Learning to Prove Theorems from Scratch with Deep Reinforcement Learningcited by 37
  3. 2019Generating Correctness Proofs with Neural Networkscited by 36
  4. 2020ENIGMA Anonymous: Symbol-Independent Inference Guiding Machine (system description)cited by 26
  5. 2020First Neural Conjecturing Datasets and Experimentscited by 26
  6. 2020NLocalSAT: Boosting Local Search with Solution Predictioncited by 25
  7. 2019ENIGMA-NG: Efficient Neural and Gradient-Boosted Inference Guidance for Ecited by 24
  8. 2019Property Invariant Embedding for Automated Reasoningcited by 22
  9. 2021DeepSTL -- From English Requirements to Signal Temporal Logiccited by 22
  10. 2022Machine Learning Methods in Solving the Boolean Satisfiability Problemcited by 22
  11. 2019Hammering Mizar by Learning Clause Guidancecited by 20
  12. 2019G2SAT: Learning to Generate SAT Formulascited by 20
  13. 2022Passport: Improving Automated Formal Verification Using Identifierscited by 19
  14. 2022COOL-MC: A Comprehensive Tool for Reinforcement Learning and Model Checkingcited by 19
  15. 2022NSNet: A General Neural Probabilistic Framework for Satisfiability Problemscited by 18
  16. 2020Learning Nonlinear Loop Invariants with Gated Continuous Logic Networks (Extended Version)cited by 17
  17. 2021Contrastive Reinforcement Learning of Symbolic Reasoning Domainscited by 17
  18. 2021Neural Termination Analysiscited by 16
  19. 2021Learning to Guide a Saturation-Based Theorem Provercited by 15
  20. 2022Peano: Learning Formal Mathematical Reasoningcited by 15
  21. 2021Proving Theorems using Incremental Learning and Hindsight Experience Replaycited by 13
  22. 2020Statistically Model Checking PCTL Specifications on Markov Decision Processes via Reinforcement Learningcited by 12
  23. 2020Stateful Premise Selection by Recurrent Neural Networkscited by 11
  24. 2020Learning from Survey Propagation: a Neural Network for MAX-E-3-SATcited by 11
  25. 2023Neural Abstractionscited by 11
  26. 2019Towards Finding Longer Proofscited by 10
  27. 2021Vampire With a Brain Is a Good ITP Hammercited by 10
  28. 2023Assessing SATNet's Ability to Solve the Symbol Grounding Problemcited by 10
  29. 2019Deep Reinforcement Learning for Synthesizing Functions in Higher-Order Logiccited by 8
  30. 2020Tactic Learning and Proving for the Coq Proof Assistantcited by 8
  31. 2021Training a First-Order Theorem Prover from Synthetic Datacited by 8
  32. 2021The Role of Entropy in Guiding a Connection Provercited by 8
  33. 2021Fast and Slow Enigmas and Parental Guidancecited by 8
  34. 2022Learning MAX-SAT from Contextual Examples for Combinatorial Optimisationcited by 8
  35. 2022The Isabelle ENIGMAcited by 8
  36. 2020Prolog Technology Reinforcement Learning Provercited by 7
  37. 2021Online Machine Learning Techniques for Coq: A Comparisoncited by 7
  38. 2021Learning Theorem Proving Componentscited by 7

50 most cited of 66 All 66 (JSON)

Built on by

Cited by year (2026 to 7 Oct)

Citing papers per year: 2025: 1; 2026: 1.

2 papers.

  1. 2025An Automated Theorem Generator with Theoretical Foundation Based on Rectangular Standard Contradictioncited by 0
  2. 2026ReqFusion: A Multi-Provider Framework for Automated PEGS Analysis Across Software Domainscited by 0