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

arXiv: https://arxiv.org/abs/2411.14870 · HTML: https://mlsanity.com/paper/2411.14870/

## Key facts

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

## Builds on (most cited first, 30 of 66)

- [Attention Is All You Need](https://mlsanity.com/paper/1706.03762/) (2017)
- [OpenAI Gym](https://mlsanity.com/paper/1606.01540/) (2016)
- [Graph Neural Networks: A Review of Methods and Applications](https://mlsanity.com/paper/1812.08434/) (2018)
- [A Survey on Evaluation of Large Language Models](https://mlsanity.com/paper/2307.03109/) (2023)
- [Learning a SAT Solver from Single-Bit Supervision](https://mlsanity.com/paper/1802.03685/) (2018)
- [Natural Language Processing: State of The Art, Current Trends and Challenges](https://mlsanity.com/paper/1708.05148/) (2017)
- [Learning to Prove Theorems via Interacting with Proof Assistants](https://mlsanity.com/paper/1905.09381/) (2019)
- [Thor: Wielding Hammers to Integrate Language Models and Automated Theorem Provers](https://mlsanity.com/paper/2205.10893/) (2022)
- [Guiding High-Performance SAT Solvers with Unsat-Core Predictions](https://mlsanity.com/paper/1903.04671/) (2019)
- [Graph Representations for Higher-Order Logic and Theorem Proving](https://mlsanity.com/paper/1905.10006/) (2019)
- [GamePad: A Learning Environment for Theorem Proving](https://mlsanity.com/paper/1806.00608/) (2018)
- [TacticToe: Learning to Prove with Tactics](https://mlsanity.com/paper/1804.00596/) (2018)
- [Learning to Prove Theorems by Learning to Generate Theorems](https://mlsanity.com/paper/2002.07019/) (2020)
- [Generating Correctness Proofs with Neural Networks](https://mlsanity.com/paper/1907.07794/) (2019)
- [TacticZero: Learning to Prove Theorems from Scratch with Deep Reinforcement Learning](https://mlsanity.com/paper/2102.09756/) (2021)
- [ENIGMA Anonymous: Symbol-Independent Inference Guiding Machine (system description)](https://mlsanity.com/paper/2002.05406/) (2020)
- [First Neural Conjecturing Datasets and Experiments](https://mlsanity.com/paper/2005.14664/) (2020)
- [NLocalSAT: Boosting Local Search with Solution Prediction](https://mlsanity.com/paper/2001.09398/) (2020)
- [ENIGMA-NG: Efficient Neural and Gradient-Boosted Inference Guidance for E](https://mlsanity.com/paper/1903.03182/) (2019)
- [Property Invariant Embedding for Automated Reasoning](https://mlsanity.com/paper/1911.12073/) (2019)
- [DeepSTL -- From English Requirements to Signal Temporal Logic](https://mlsanity.com/paper/2109.10294/) (2021)
- [Machine Learning Methods in Solving the Boolean Satisfiability Problem](https://mlsanity.com/paper/2203.04755/) (2022)
- [Hammering Mizar by Learning Clause Guidance](https://mlsanity.com/paper/1904.01677/) (2019)
- [G2SAT: Learning to Generate SAT Formulas](https://mlsanity.com/paper/1910.13445/) (2019)
- [Passport: Improving Automated Formal Verification Using Identifiers](https://mlsanity.com/paper/2204.10370/) (2022)
- [COOL-MC: A Comprehensive Tool for Reinforcement Learning and Model Checking](https://mlsanity.com/paper/2209.07133/) (2022)
- [NSNet: A General Neural Probabilistic Framework for Satisfiability Problems](https://mlsanity.com/paper/2211.03880/) (2022)
- [Learning Nonlinear Loop Invariants with Gated Continuous Logic Networks (Extended Version)](https://mlsanity.com/paper/2003.07959/) (2020)
- [Contrastive Reinforcement Learning of Symbolic Reasoning Domains](https://mlsanity.com/paper/2106.09146/) (2021)
- [Neural Termination Analysis](https://mlsanity.com/paper/2102.03824/) (2021)

## Built on by (most cited first, 2 of 2)

- [An Automated Theorem Generator with Theoretical Foundation Based on Rectangular Standard Contradiction](https://mlsanity.com/paper/2511.04092/) (2025)
- [ReqFusion: A Multi-Provider Framework for Automated PEGS Analysis Across Software Domains](https://mlsanity.com/paper/2603.23482/) (2026)

## 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.