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

Atif Mashkoor; Jannik Dunkelau; Sebastian Stock

REVIEW 3 major objections 8 minor 257 references

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

T0 review · 3 major / 8 minor · reviewed 2026-08-12 · deepseek-v4-flash

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗ Review JSON

Pith's one-line read A systematic map of 189 studies finds AI in formal methods is heavily concentrated in theorem proving and SAT solving, leaving model checking and synthesis behind.

desk verdict A useful, transparent mapping of AI-for-FM that deserves review, but the search query's blind spot around 'verification' should be stress-tested before the field-wide proportions are taken at face value. read the letter →

arxiv 2411.14870 v2 pith:CLFA2E7V submitted 2024-11-22 cs.LO cs.AIcs.LG

Sebastian Stock , Jannik Dunkelau , Atif Mashkoor This is my paper · ORCID

classification cs.LOcs.AIcs.LG

keywords formalmethodsartificialintelligencemachinelearningsystematicmappingstudytheoremprovingSATsolvingmodelcheckingbenchmarks

verification ladder T0 review T1 audit T2 compute T3 formal

The pith

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The reading

This paper maps the 2019-2023 literature on applying artificial intelligence to formal methods. After searching four databases and five rounds of snowballing, the authors retained 189 primary studies and classified them by AI technique, formal-methods area, contribution type, and dataset availability. They report that theorem proving (85 studies) and SAT solving (45 studies) together make up most of the field, while model checking (18), synthesis (19), and SMT (13) receive much less attention. They also find that most studies are practical methodologies, that shared benchmarks and training data are scarce outside theorem proving, and that many studies do not share their data. The paper's conclusion is that the field is growing but immature, with reproducibility and comparability at risk.

What carries the argument

The load-bearing object is the systematically constructed corpus plus its classification scheme. The authors build the corpus with a search query that requires at least one AI term and one formal-methods term to co-occur in title, abstract, and keywords, applied to IEEE, Scopus, ACM, and Web of Science, followed by five snowballing rounds to closure, reducing 540 candidates to 189 studies. They then tag each study along four axes: formal-methods area, AI technique, contribution type (methodology, tool, benchmark, training data, and so on), and publication venue. The central claims about research gaps are read off the cross-tabulations of these axes.

What would settle it

Re-run the systematic search with an expanded term set that includes community-specific vocabulary such as "B method," "neural guidance," "termination analysis," "loop invariant," "CADP," and "NuSMV," and compare the resulting distribution: if theorem proving and SAT no longer dominate, or if model checking and synthesis shares rise substantially, the paper's concentration claim and its gap list would need revision.

Watch

Extended reading notes

Core claim

On the authors' own terms, the central finding is a quantitative concentration: AI has been applied to formal methods mostly in theorem proving and SAT/SMT-style solving, and the rest of formal methods is comparatively neglected. Of 189 studies from 2019-2023, 85 target theorem proving and 45 target SAT, together 68.8 percent of the corpus, while model checking (18), synthesis (19), and SMT (13) lag behind. Neural networks dominate the AI side (70 primary uses, with more in multi-technique studies), followed by reinforcement learning (32). Only 21 data set contributions exist, 15 of them in theorem proving, and among 124 studies that use external data the sources are highly heterogeneous, with 65 studies generating random samples or not mentioning their data source. The authors infer that the field is yet to mature: little theoretical groundwork, few case studies or benchmarks, and an ad-hoc dataset culture that endangers reproducibility.

Load-bearing premise

The 189-study sample is representative of the 2019-2023 AI-for-formal-methods literature, which depends on the hand-picked search terms plus snowballing catching all relevant work.

Editorial extensions

If this is right

If the concentration is real, the field's next bottleneck is not more theorem-proving AI but shared benchmarks and training data for model checking, synthesis, and SMT.
The near absence of case studies and benchmarks means new AI-for-formal-methods methods are rarely compared on common ground, so reported gains may not transfer across research groups.
The paper's suggested directions—unified benchmark environments, data-mining studies, LLM and generative-AI applications, and AI-enforced model checking—are where it predicts the most room for growth.
If dataset ad hocery continues, reproducibility failures could undermine trust in AI-assisted verification, since formal methods sell exactly on verifiable guarantees.
AI is mostly used as a support function whose outputs are still checked by formal tools; replacing the tools outright is rare and would require AI outputs to carry formal guarantees.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

A re-run with community-specific terms such as "B method," "neural guidance," or "invariant generation" might shift the distribution; the paper itself acknowledges this construct-validity risk but does not quantify it.
Because the query requires AI and formal-methods terms in title, abstract, and keywords, the corpus likely undercounts studies that mention only a concrete algorithm and a concrete tool; correcting this could change the SAT and theorem-proving dominance.
The 2019-2023 window probably undercounts evolutionary-algorithm work in model checking, which the authors note was more prominent before deep learning took off; the gap may be a period effect rather than a permanent neglect.
If the trend holds, LLM-based autoformalization and synthesis papers should rise sharply after 2023, making the paper's "gap" list a testable prediction.

Share X Bluesky LinkedIn Reddit HN

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, and a circularity audit.

Desk Editor's Note

read the letter

This is the first broad quantitative map of AI applied to formal methods in 2019–2023, and the released corpus (189 classified studies plus a 457-entry dataset) is a real community resource. The finding that theorem proving and SAT dominate while model checking, synthesis, and SMT lag is the kind of concrete baseline the field needs, and the gap analysis on missing benchmarks and shared datasets is actionable.

What earns credit: the study follows the Petersen SMS guidelines, the search protocol is fully documented, the snowballing is extensive (five rounds, 89 to 540 candidates), and the authors openly discuss construct-validity threats. The classification effort is labor-intensive and the dataset is a step up from prior narrower surveys.

The main soft spot is the one the stress test flags: the FM half of the query omits "verification", "program verification", "refinement", "temporal logic", "proof assistant", and similar terms, and the query requires an FM term in title, abstract, and keywords. A paper titled simply "neural program verification" cannot enter the initial 89-study baseline; it can only be recovered by snowballing, which starts from a TP/SAT-heavy seed and may not reach verification-centric communities. So the reported proportions—especially the low counts for model checking and synthesis—could be an artifact of query construction rather than a true property of the literature. The authors acknowledge the limitation in Section 7 but never quantify the missed fraction or test sensitivity. That is a genuine weakness, not a manufactured one.

It is not fatal. The direction of the headline result (TP is the biggest area) is likely robust, and the dataset lets others re-run and re-classify. A careful referee should ask for a sensitivity analysis: re-run the initial query with "verification" and related terms added, or at least measure how many snowballed papers failed the original query and whether they cluster in certain FM subfields. An inter-rater reliability metric for the classification would also strengthen the revision, though the dual-review-plus-tiebreak process is a reasonable start.

Who gets value: AI4FM researchers, program committees, and anyone writing a grant proposal or survey. I would cite it as the current baseline, with a caveat about the query. It deserves peer review, not desk rejection—the artifact is valuable and the flaws are addressable. My recommendation is to send it out and push for the sensitivity analysis before publication.

Referee Report

3 major / 8 minor

Summary. The manuscript reports a systematic mapping study (SMS) of research applying artificial intelligence to formal methods (FM) over the period 2019–2023. Following published SMS guidelines, the authors query four databases with a two-sided search-term set (Fig. 2), apply inclusion and exclusion criteria, perform five rounds of forward and backward snowballing, and arrive at 189 primary studies. They classify the corpus by FM subfield, AI technique, contribution type, venue, and dataset availability, and publicly release the underlying data on GitHub. The headline results are that theorem proving (85 studies) and SAT solving (45) dominate, while model checking (18), synthesis (19), and SMT (13) are less represented; that neural networks are the most common AI technique; and that the field lacks shared benchmarks and training datasets.

Significance. If the corpus is representative, the paper provides a useful quantitative baseline for the AI-for-FM community: it follows an established SMS methodology, fully discloses the search query and inclusion/exclusion criteria, reports the search process transparently in Fig. 1, and ships the full dataset publicly. The relative underrepresentation of model checking, synthesis, and SMT, and the identified gaps in benchmarks and datasets, are concrete and falsifiable claims that other groups could reproduce. However, the central quantitative claim is only as strong as the completeness and balance of the recovered corpus, and the manuscript's own §7 identifies the restrictive initial query as a threat to construct validity. The absence of a quantified sensitivity analysis and the lack of an inter-rater reliability metric make the headline proportions provisional rather than established.

major comments (3)

[§4.1, Fig. 2] The FM half of the search query omits 'verification', 'refinement', 'temporal logic', 'invariant', 'proof assistant', and common tool names such as Coq, Isabelle, TLA+, or Alloy, while the unified query in Fig. 2c requires at least one FM term in the title, abstract, AND keywords. A verification-centric paper whose title and keywords use only community-specific terminology therefore cannot enter the baseline of 89 studies; it can only be recovered by snowballing, which starts from a TP/SAT-heavy seed. Since §5.2.2 (Fig. 11a) uses the resulting 189 studies to conclude that model checking, synthesis, and SMT are underrepresented, this threat is load-bearing for the paper's central claim. Section 7 acknowledges the issue but does not quantify the missed fraction or check whether the snowballed corpus is balanced across FM subfields. I ask for a sensitivity analysis: rerun the initial search with supplementary FM terms (e.g., verification, invariant, temporal logic, proof assistant, refinement) and report how the subfield proportions change, or demonstrate by citation or community sampling that the snowballing closure reaches the omitted communities.
[§4.3] Exclusion criteria EC 6 through EC 10 were added after the search was under way, and some are labeled 'During initial skim' while others are labeled 'Snowballing'. This creates a risk of criterion drift and of applying different filters to database-search results versus snowballed candidates. Because these criteria plausibly remove many entries from SAT and the 'other FM' categories, the reported counts in Fig. 11a and Table A1 depend on decisions that are not fully documented. Please report the number of studies excluded by each individual criterion and provide a sensitivity analysis with the post hoc criteria removed.
[§4.3, §5] The manual classification into FM subfields and contribution types is performed by two authors with a third as tiebreaker, but no inter-rater reliability metric (e.g., Cohen's kappa) is reported. The central numbers—85 TP versus 18 MC—are the output of this classification, so without an agreement measure or a random-sample re-classification check, the quantitative conclusions are not independently verifiable. I request the agreement statistic or a second, independent classification of a random subset.

minor comments (8)

[§4.3] EC 9 writes '2Sat'; this should be '2-SAT'.
[Table A1] The entry 'Termination anlysis' is a typo for 'Termination analysis'.
[§7] The threats-to-validity discussion cites [30] (Zhou et al., 'Graph neural networks: a review of methods and applications') as the baseline for the threats-to-validity framework; this reference does not appear to be such a framework and should be corrected or replaced.
[§5.2.2 and Fig. 12a] The text says premise selection has 27/85 entries, while Fig. 12a says 26/85; with 20 FOL and 7 HOL entries, 27 is correct, so Fig. 12a should be updated.
[Table A1 and Fig. 11a] The subcategory counts for SAT (49) and TP (89) exceed the unique totals of 45 and 85; the table should state explicitly that a study can appear in multiple subcategories and that row counts are not disjoint.
[§5.2.4 and §6.2] The dataset count is presented as '21' in §5.2.4 and as '19+2' in §6.2; the clarification should be moved to the first occurrence to avoid apparent inconsistency.
[Fig. 5] The venue-area counts sum to more than 189 because venues can be assigned to multiple areas; this should be stated in the caption.
[§5.2.1 and §6.2] Section 5.2.1 reports only two 'data mining approaches', while §6.2 says 'only three applied data mining techniques'; these numbers should be reconciled or the counting clarified.

Circularity Check

0 steps flagged · score 0.0 of 10

No circularity: the mapping study's conclusions are descriptive counts from an explicitly assembled corpus; the acknowledged term-selection bias is a validity threat, not a circular derivation.

full rationale

This manuscript reports a systematic mapping study, so its 'results' are descriptive counts of a corpus assembled through an explicit search query, inclusion/exclusion criteria, and five snowballing rounds. No claimed result is derived by construction from the query: the FM-term list includes 'formal method', 'specification', 'model check*', 'SAT', 'SMT', and 'prove*', while the AI-term list is likewise broad, and the final 189-study set was filtered by human judgment (IC/EC) and extended by snowballing. The central finding that theorem proving and SAT dominate, while model checking and synthesis are less represented, is a reading of the resulting Table A1, not a term that was programmed into the query as an output. The paper does not fit any parameter and then rename it a prediction; it does not invoke a uniqueness theorem from the authors' prior work; and it does not adopt an unverified ansatz via self-citation. The self-citations that appear (e.g., Refs. [125], [132], and [221] by author Dunkelau) are merely counted primary studies within the corpus and are not load-bearing: removing them would not change the qualitative distribution. Section 7 explicitly acknowledges the construct-validity limitation that the term-based query cannot cover every FM sub-community and relies on snowballing to recover missed work; this is a legitimate methodological threat to generalizability, not a circularity. Accordingly, the appropriate finding is no significant circularity.

Assumptions & free parameters 4 free parameters · 3 assumptions · 0 invented entities

The mapping's conclusions rest on the completeness of the corpus and the consistency of manual classification. The search parameters (keyword sets, year window) are hand-chosen, and the screening criteria include post hoc additions. These choices determine every reported count, so they function as free parameters in the 'derivation' of the field map. No new entities are invented, and the paper does not rely on unproved mathematical theorems.

free parameters (4)

Five-year window 2019-2023
Hand-chosen restriction to the recent publication peak; all content analyses apply only to this window, and 2023 is incomplete because the search ran in Q4 2023.
AI keyword set
The disjunction in Fig. 2b was selected based on the authors' experience, not derived from data or a benchmark; it determines which papers enter the initial corpus.
FM keyword set
The disjunction in Fig. 2a was similarly hand-chosen; the paper notes that relevant papers often use specific jargon (e.g., 'B method'), which is not fully covered.
Contribution type taxonomy
The 10 contribution categories in Section 2.4 are defined by the authors; the classification of each study into these categories is a hand-coded choice and affects RQ 1.3 and RQ 2 results.

assumptions (3)

domain assumption The systematic mapping study guidelines (Petersen et al., Kitchenham et al.) are a valid method for mapping a research field.
The entire study is structured around these guidelines (Section 2.1, Section 4).
domain assumption The four databases (IEEE, Scopus, ACM, Web of Science) provide adequate coverage of the AI-FM literature, especially when complemented by snowballing.
Section 4.2; the paper acknowledges WoS result variation and Springer was excluded, so coverage completeness relies on this assumption.
domain assumption The manual screening and classification of 1492 initial entries (then 540) by two authors is sufficiently consistent to produce reliable counts.
Section 4.3; the paper reports that disagreements were discussed and one tiebreaker was used for two cases, but no inter-rater agreement metric (e.g., Cohen's kappa) is reported.

how reviews work

0 comments

Cite this review

Pith. "Pith review of Application of AI to formal methods - an analysis of current trends." pith.science (2026). https://pith.science/paper/CLFA2E7V

@misc{pith2026241114870,
  author       = {Pith},
  title        = {Pith review of: Application of AI to formal methods - an analysis of current trends},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/CLFA2E7V}},
  note         = {Machine review of arXiv:2411.14870}
}

read the original abstract

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.

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

257 extracted references · 48 canonical work pages

[1]

Journal of Management Analytics 6, 1–29 (2019) https://doi.org/ 10.1080/23270012.2019.1570365

Lu, Y.: Artificial intelligence: a survey on evolution, models, applications and future trends. Journal of Management Analytics 6, 1–29 (2019) https://doi.org/ 10.1080/23270012.2019.1570365

arXiv 2019
[2]

Discover Artificial Intelligence 3 (2023) https://doi.org/10.1007/s44163-023-00089-x

Elahi, M., Afolaranmi, S.O., Martinez Lastra, J.L., Perez Garcia, J.A.: A comprehensive literature review of the applications of AI techniques through the lifecycle of industrial equipment. Discover Artificial Intelligence 3 (2023) https://doi.org/10.1007/s44163-023-00089-x

work page doi:10.1007/s44163-023-00089-x 2023
[3]

Annals of Translational Medicine 11(5) (2023) https:// doi.org/10.21037/atm-22-3773

Jiang, X., Xie, M., Ma, L., Dong, L., Li, D.: International publication trends in the application of artificial intelligence in ophthalmology research: an updated bibliometric analysis. Annals of Translational Medicine 11(5) (2023) https:// doi.org/10.21037/atm-22-3773

work page doi:10.21037/atm-22-3773 2023
[4]

Mathematics 11(11) (2023) https://doi.org/10.3390/ math11112420

Chang, K.-H.: Artificial intelligence and information processing: A system- atic literature review. Mathematics 11(11) (2023) https://doi.org/10.3390/ math11112420

2023
[5]

AI Perspectives 2 (2020) https://doi.org/10.1186/ s42467-020-00005-4

Barenkamp, M., Rebstadt, J., Thomas, O.: Applications of AI in classi- cal software engineering. AI Perspectives 2 (2020) https://doi.org/10.1186/ s42467-020-00005-4

2020
[6]

IEEE Access 9, 140896–140920 (2021) https://doi.org/10.1109/ACCESS.2021.3119746

Shafiq, S., Mashkoor, A., Mayr-Dorn, C., Egyed, A.: A literature review of using machine learning in software development life cycle stages. IEEE Access 9, 140896–140920 (2021) https://doi.org/10.1109/ACCESS.2021.3119746

arXiv 2021
[7]

(eds.): Software Engi- neering Body of Knowledge vol

Abran, A., Moore, J.W., Bourque, P., Dupuis, R. (eds.): Software Engi- neering Body of Knowledge vol. 25. IEEE Computer Society, Los Alamitos, CA, USA (2004). https://www.computer.org/education/bodies-of-knowledge/ software-engineering

2004
[8]

Information and Software Technology 64, 1–18 (2015) https://doi.org/10.1016/j.infsof.2015.03.007

Petersen, K., Vakkalanka, S., Kuzniarz, L.: Guidelines for conducting systematic mapping studies in software engineering: An update. Information and Software Technology 64, 1–18 (2015) https://doi.org/10.1016/j.infsof.2015.03.007

doi:10.1016/j.infsof.2015.03.007 2015

Show all 257 references

[9]

In: Proceedings of the 14th International Conference on Evaluation and Assessment in Software Engineering

Kitchenham, B.A., Budgen, D., Brereton, O.P.: The value of mapping studies – a participant-observer case study. In: Proceedings of the 14th International Conference on Evaluation and Assessment in Software Engineering. EASE’10, pp. 25–33. BCS Learning & Development Ltd., Swind...

2010 doi
[10]

Technical report, Keele University (2007)

Kitchenham, B., Charters, S., et al.: Guidelines for performing sys- tematic literature reviews in software engineering. Technical report, Keele University (2007). https://legacyfileshare.elsevier.com/promis misc/ 525444systematicreviewsguide.pdf 36

2007
[11]

ACM Computing Surveys 41, 1–36 (2009) https: //doi.org/10.1145/1592434.1592436

Woodcock, J., Larsen, P.G., Bicarregui, J., Fitzgerald, J.: Formal methods: Practice and experience. ACM Computing Surveys 41, 1–36 (2009) https: //doi.org/10.1145/1592434.1592436

2009
[12]

ACM Computing Surveys 28(4), 626–643 (1996) https://doi.org/10.1145/ 242223.242257

Clarke, E.M., Wing, J.M.: Formal methods: State of the art and future direc- tions. ACM Computing Surveys 28(4), 626–643 (1996) https://doi.org/10.1145/ 242223.242257

1996
[14]

(eds.): Hand- book of Model Checking

Clarke, E.M., Henzinger, T.A., Veith, H., Bloem, R., et al. (eds.): Hand- book of Model Checking. Springer, Cham (2018). https://doi.org/10.1007/ 978-3-319-10575-8

2018
[15]

Courier Dover Publications, USA (2015)

Gallier, J.H.: Logic for Computer Science: Foundations of Automatic Theorem Proving, 2nd edn. Courier Dover Publications, USA (2015). https://store. doverpublications.com/products/9780486780825

2015
[16]

Texts in Theoretical Computer Science

Bertot, Y., Cast´ eran, P.: Interactive Theorem Proving and Program Devel- opment, 1st edn. Texts in Theoretical Computer Science. An EATCS Series. Springer, Berlin, Heidelberg (2013). https://doi.org/10.1007/978-3-662-07964-5

2013 doi
[17]

(eds.): Handbook of Satisfiabil- ity, 2nd edn

Biere, A., Heule, M., Maaren, H. (eds.): Handbook of Satisfiabil- ity, 2nd edn. Frontiers in Artificial Intelligence and Applications, vol
[18]

In: Clarke, E.M., Hen- zinger, T.A., Veith, H., Bloem, R

Barrett, C., Tinelli, C.: Satisfiability Modulo Theories. In: Clarke, E.M., Hen- zinger, T.A., Veith, H., Bloem, R. (eds.) Handbook of Model Checking, pp. 305–343. Springer, Cham (2018). https://doi.org/10.1007/978-3-319-10575-8 11

2018 doi
[19]

Journal of Automated Reasoning 51, 57–77 (2013) https://doi.org/10

Brown, C.E.: Reducing higher-order theorem proving to a sequence of SAT prob- lems. Journal of Automated Reasoning 51, 57–77 (2013) https://doi.org/10. 1007/s10817-013-9283-8

2013
[20]

In: Emerson, E.A., Sistla, A.P

Shtrichman, O.: Tuning SAT checkers for bounded model checking. In: Emerson, E.A., Sistla, A.P. (eds.) Computer Aided Verification, pp. 480–494. Springer, Berlin, Heidelberg (2000). https://doi.org/10.1007/10722167 36

2000 doi
[21]

In: Proceedings Design, Automation and Test in Europe

Goldberg, E.I., Prasad, M.R., Brayton, R.K.: Using SAT for combinational equivalence checking. In: Proceedings Design, Automation and Test in Europe. Conference and Exhibition 2001, pp. 114–121. IEEE, Munich, Germany (2001). https://doi.org/10.1109/DATE.2001.915010 37

2001
[22]

Journal of Systems Architecture 51(8), 488–511 (2005) https: //doi.org/10.1016/j.sysarc.2004.10.006

Zeng, Z., Talupuru, K.R., Ciesielski, M.: Functional test generation based on word-level SAT. Journal of Systems Architecture 51(8), 488–511 (2005) https: //doi.org/10.1016/j.sysarc.2004.10.006

2005 doi
[23]

IEEE Journal of Oceanic Engineering 13(2), 14–42 (1988) https://doi.org/10

Simmons, A.B., Chappell, S.G.: Artificial intelligence-definition and practice. IEEE Journal of Oceanic Engineering 13(2), 14–42 (1988) https://doi.org/10. 1109/48.551

1988
[24]

McGraw-Hill Professional, New York, NY, USA (1997)

Mitchell, T.M.: Machine Learning. McGraw-Hill Professional, New York, NY, USA (1997). https://www.cs.cmu.edu/ ∼tom/mlbook.html

1997
[25]

Spartan Books, Washington, DC (1962)

Rosenblatt, F.: Principles of Neurodynamics: Perceptrons and the Theory of Brain Mechanisms. Spartan Books, Washington, DC (1962)

1962
[26]

MIT Press, Cambridge, MA (2016)

Goodfellow, I., Bengio, Y., Courville, A.: Deep Learning. MIT Press, Cambridge, MA (2016). http://www.deeplearningbook.org

2016
[27]

In: Proceedings of 2010 IEEE International Symposium on Circuits and Systems, pp

LeCun, Y., Kavukcuoglu, K., Farabet, C.: Convolutional networks and appli- cations in vision. In: Proceedings of 2010 IEEE International Symposium on Circuits and Systems, pp. 253–256. IEEE, Paris, France (2010). https://doi.org/ 10.1109/ISCAS.2010.5537907

2010
[28]

In: Don- ahoe, J.W., Dorsel, V.P

Jordan, M.I.: Serial order: A parallel distributed processing approach. In: Don- ahoe, J.W., Dorsel, V.P. (eds.) Neural-Network Models of Cognition. Advances in Psychology, vol. 121, pp. 471–495. North-Holland, Amsterdam (1997). https: //doi.org/10.1016/S0166-4115(97)80111-2

1997 doi
[29]

In: Guyon, I., Luxburg, U.V., Bengio, S., Wallach, H., Fergus, R., Vishwanathan, S., Garnett, R

Vaswani, A., Shazeer, N., Parmar, N., Uszkoreit, J., Jones, L., Gomez, A.N., Kaiser, L.u., Polosukhin, I.: Attention is all you need. In: Guyon, I., Luxburg, U.V., Bengio, S., Wallach, H., Fergus, R., Vishwanathan, S., Garnett, R. (eds.) Advances in Neural Information Processi...

2017
[30]

AI Open 1, 57–81 (2020) https://doi.org/10.1016/j.aiopen.2021.01.001

Zhou, J., Cui, G., Hu, S., Zhang, Z., Yang, C., Liu, Z., Wang, L., Li, C., Sun, M.: Graph neural networks: A review of methods and applications. AI Open 1, 57–81 (2020) https://doi.org/10.1016/j.aiopen.2021.01.001

2020 doi
[31]

SN Computer Science 2 (2021) https://doi

Sarker, I.H.: Deep learning: A comprehensive overview on techniques, taxonomy, applications and research directions. SN Computer Science 2 (2021) https://doi. org/10.1007/s42979-021-00815-1

2021 doi
[32]

Journal of artificial intelligence research 4, 237–285 (1996) https://doi.org/10

Kaelbling, L.P., Littman, M.L., Moore, A.W.: Reinforcement learning: A survey. Journal of artificial intelligence research 4, 237–285 (1996) https://doi.org/10. 1613/jair.301 38

1996
[33]

MIT Press, Cambridge, MA (2018)

Sutton, R.S., Barto, A.G.: Reinforcement Learning: An Introduction, 2nd edn. MIT Press, Cambridge, MA (2018). http://incompleteideas.net/book/ the-book-2nd.html

2018
[34]

Fundamentals of Artificial Intelligence, pp

Chowdhary, K.R.: Natural Language Processing. Fundamentals of Artificial Intelligence, pp. 603–649. Springer, New Delhi (2020). https://doi.org/10.1007/ 978-81-322-3972-7 19

2020
[35]

Multimedia Tools and Applications 82, 3713–3744 (2023) https://doi.org/10.1007/s11042-022-13428-4

Khurana, D., Koli, A., Khatter, K., Singh, S.: Natural language processing: state of the art, current trends and challenges. Multimedia Tools and Applications 82, 3713–3744 (2023) https://doi.org/10.1007/s11042-022-13428-4

2023 doi
[36]

ACM Transactions on Intelligent Systems and Technology 15(3), 1–45 (2024) https://doi.org/10.1145/3641289

Chang, Y., Wang, X., Wang, J., Wu, Y., Yang, L., Zhu, K., Chen, H., Yi, X., Wang, C., Wang, Y., Ye, W., Zhang, Y., Chang, Y., Yu, P.S., Yang, Q., Xie, X.: A survey on evaluation of large language models. ACM Transactions on Intelligent Systems and Technology 15(3), 1–45 (2024)...

2024 doi
[37]

IEEE/CAA Journal of Automatica Sinica 10(5), 1122–1136 (2023) https://doi.org/10.1109/JAS.2023.123618

Wu, T., He, S., Liu, J., Sun, S., Liu, K., Han, Q.-L., Tang, Y.: A brief overview of ChatGPT: The history, status quo and potential future devel- opment. IEEE/CAA Journal of Automatica Sinica 10(5), 1122–1136 (2023) https://doi.org/10.1109/JAS.2023.123618

2023
[38]

MIT press, Cam- bridge, MA (1998)

Mitchell, M.: An Introduction to Genetic Algorithms. MIT press, Cam- bridge, MA (1998). https://direct.mit.edu/books/monograph/4675/ An-Introduction-to-Genetic-Algorithms

1998
[39]

In: Wang, L

Kecman, V.: Support Vector Machines – An Introduction. In: Wang, L. (ed.) Support Vector Machines: Theory and Applications, pp. 1–47. Springer, Berlin, Heidelberg (2005). https://doi.org/10.1007/10984697 1

2005 doi
[40]

Wiley series in probability and statistics

Montgomery, D.C., Peck, E.A., Vining, G.G.: Introduction to Linear Regression Analysis, 6th edn. Wiley series in probability and statistics. John Wiley & Sons, New Jersey (2021). https://www.wiley-vch.de/en/ areas-interest/mathematics-statistics/statistics-16st/regression-anal...

2021
[41]

IEEE Transactions on Information Theory 13(1), 21–27 (1967) https://doi.org/10.1109/TIT.1967

Cover, T., Hart, P.: Nearest neighbor pattern classification. IEEE Transactions on Information Theory 13(1), 21–27 (1967) https://doi.org/10.1109/TIT.1967. 1053964

1967 doi
[42]

Taylor & Francis, New York, NY (1984)

Breiman, L., Friedman, J., Stone, C.J., Olshen, R.A.: Classification and Regres- sion Trees. Taylor & Francis, New York, NY (1984). https://doi.org/10.1201/ 9781315139470

1984
[43]

Machine learning 45(1), 5–32 (2001) https://doi

Breiman, L.: Random forests. Machine learning 45(1), 5–32 (2001) https://doi. org/10.1023/a:1010933404324 39

2001 doi
[44]

In: Bousquet, O., Luxburg, U., R¨ atsch, G

Tipping, M.E.: Bayesian Inference: An Introduction to Principles and Practice in Machine Learning. In: Bousquet, O., Luxburg, U., R¨ atsch, G. (eds.) Advanced Lectures on Machine Learning, pp. 41–62. Springer, Berlin, Heidelberg (2004). https://doi.org/10.1007/978-3-540-28650-9 3

2004 doi
[45]

In: Proceedings of the 18th International Conference on Evaluation and Assessment in Software Engineering

Wohlin, C.: Guidelines for snowballing in systematic literature studies and a replication in software engineering. In: Proceedings of the 18th International Conference on Evaluation and Assessment in Software Engineering. EASE ’14. Association for Computing Machinery, London, ...

2014
[46]

Electronic Notes in Theoretical Computer Science 86, 147–152 (2003) https://doi.org/10.1016/S1571-0661(04) 80659-5

Urban, J.: MPTP 0.1 - system description. Electronic Notes in Theoretical Computer Science 86, 147–152 (2003) https://doi.org/10.1016/S1571-0661(04) 80659-5

2003 doi
[47]

MIT press, Cambridge, MA (2018)

Sejnowski, T.J.: The Deep Learning Revolution. MIT press, Cambridge, MA (2018). https://mitpress.mit.edu/9780262038034/ the-deep-learning-revolution/

2018
[48]

Science 359(6377), 725–726 (2018) https://doi.org/10.1126/science.359.6377.725

Hutson, M.: Artificial intelligence faces reproducibility crisis. Science 359(6377), 725–726 (2018) https://doi.org/10.1126/science.359.6377.725

2018 doi
[49]

Brockman, G., Cheung, V., Pettersson, L., Schneider, J., Schulman, J., Tang, J., Zaremba, W.: OpenAI Gym (2016) arXiv:1606.01540 [cs.LG]

2016 arXiv
[50]

In: First International Symposium on Empir- ical Software Engineering and Measurement (ESEM 2007), pp

Dyba, T., Dingsoyr, T., Hanssen, G.K.: Applying systematic reviews to diverse study types: An experience report. In: First International Symposium on Empir- ical Software Engineering and Measurement (ESEM 2007), pp. 225–234. IEEE, Madrid, Spain (2007). https://doi.org/10.1109/...

2007 doi
[51]

Amrani, M., L´ ucio, L., Bibal, A.: ML + FV=♡? a survey on the application of machine learning to formal verification (2018) arXiv:1806.03600 [cs.SE]

2018 arXiv
[52]

IEEE Access 8, 108561– 108578 (2020) https://doi.org/10.1109/ACCESS.2020.3000907

Wang, F., Cao, Z., Tan, L., Zong, H.: Survey on learning-based formal methods: Taxonomy, applications and possible future directions. IEEE Access 8, 108561– 108578 (2020) https://doi.org/10.1109/ACCESS.2020.3000907

2020
[53]

Formal Methods in System Design 60, 1–26 (2023) https: //doi.org/10.1007/s10703-023-00430-1

Ganesh, V., Seshia, S.A., Jha, S.: Machine learning and logic: a new frontier in artificial intelligence. Formal Methods in System Design 60, 1–26 (2023) https: //doi.org/10.1007/s10703-023-00430-1

2023 doi
[54]

International Journal of Advanced Intelligence Paradigms 5(3), 233–256 (2013) https://doi.org/10.1504/IJAIP

Kilani, Y., Bsoul, M., Alsarhan, A., Al-Khasawneh, A.: A survey of the satisfiability-problems solving algorithms. International Journal of Advanced Intelligence Paradigms 5(3), 233–256 (2013) https://doi.org/10.1504/IJAIP. 2013.056447

2013
[55]

Foundations and Trends ® in Machine Learning 14(6), 807–989 (2021) https://doi.org/10.1561/2200000081

Holden, S.B.: Machine learning for automated theorem proving: Learning to 40 solve SAT and QSAT. Foundations and Trends ® in Machine Learning 14(6), 807–989 (2021) https://doi.org/10.1561/2200000081

2021 doi
[56]

Machine Intelligence Research 20, 640–655 (2023) https://doi.org/10.1007/s11633-022-1396-2

Guo, W., Zhen, H.-L., Li, X., Luo, W., Yuan, M., Jin, Y., Yan, J.: Machine learn- ing methods in solving the boolean satisfiability problem. Machine Intelligence Research 20, 640–655 (2023) https://doi.org/10.1007/s11633-022-1396-2

2023 doi
[57]

In: Zhang, Y

Granmo, O.-C., Bouhmala, N.: Using learning automata to enhance local-search based SAT solvers with learning capability. In: Zhang, Y. (ed.) Application of Machine Learning. IntechOpen, London, UK (2010). https://doi.org/10.5772/ 8610

2010
[58]

In: Biere, A., Heule, M., Maaren, H., Walsh, T

Hoos, H.H., Hutter, F., Leyton-Brown, K.: Automated configuration and selec- tion of SAT solvers. In: Biere, A., Heule, M., Maaren, H., Walsh, T. (eds.) Handbook of Satisfiability, pp. 481–507. IOS Press, Amsterdam, NL (2021)

2021
[59]

In: Sankaranarayanan, S., Sharygina, N

Fuchs, T., Bach, J., Iser, M.: Active learning for SAT solver benchmarking. In: Sankaranarayanan, S., Sharygina, N. (eds.) Tools and Algorithms for the Construction and Analysis of Systems. Lecture Notes in Computer Science, vol. 13993, pp. 407–425. Springer, Paris, France (20...

2023
[60]

In: Gomes, C., Sellmann, M

Amadini, R., Gabbrielli, M., Mauro, J.: An empirical evaluation of portfolios approaches for solving CSPs. In: Gomes, C., Sellmann, M. (eds.) Integration of AI and OR Techniques in Constraint Programming for Combinatorial Opti- mization Problems, pp. 316–324. Springer, Yorktow...

2013 doi
[61]

Journal of Intelligent Information Systems 58, 91–118 (2022) https://doi.org/10.1007/s10844-021-00666-5

Popescu, A., Polat-Erdeniz, S., Felfernig, A., Uta, M., Atas, M., Le, V.-M., Pilsl, K., Enzelsberger, M., Tran, T.N.T.: An overview of machine learning techniques in constraint solving. Journal of Intelligent Information Systems 58, 91–118 (2022) https://doi.org/10.1007/s10844...

2022 doi
[62]

In: Bonacina, M.P., Stickel, M.E

Urban, J., Vyskoˇ cil, J.: Theorem Proving in Large Formal Mathematics as an Emerging AI Field. In: Bonacina, M.P., Stickel, M.E. (eds.) Automated Reasoning and Mathematics. Lecture Notes in Computer Science, vol. 7788, pp. 240–257. Springer, Berlin, Heidelberg (2013). https:/...

2013
[63]

In: Stefan Geschke, P.S

Blanchette, J.C., K¨ uhlwein, D., Geschke, S., Loewe, B., Schlicht, P.: A sur- vey of axiom selection as a machine learning problem. In: Stefan Geschke, P.S. Benedikt Loewe (ed.) Infinity, Computability, and Metamathematics: Festschrift Celebrating the 60th Birthdays of Peter ...

2014
[64]

Journal of Automated Reasoning 41 57, 219–244 (2016) https://doi.org/10.1007/s10817-016-9362-8

Blanchette, J.C., Greenaway, D., Kaliszyk, C., K¨ uhlwein, D., Urban, J.: A learning-based fact selector for Isabelle/HOL. Journal of Automated Reasoning 41 57, 219–244 (2016) https://doi.org/10.1007/s10817-016-9362-8

2016 doi
[65]

In: Davenport, J.H., Kauers, M., Labahn, G., Urban, J

England, M.: Machine learning for mathematical software. In: Davenport, J.H., Kauers, M., Labahn, G., Urban, J. (eds.) Mathematical Software – ICMS 2018. Lecture Notes in Computer Science, vol. 10931, pp. 165–174. Springer, South Bend, IN, USA (2018). https://doi.org/10.1007/9...

2018 doi
[66]

(eds.) Proceedings of TextGraphs-16: Graph-based Methods for Natural Language Processing, pp

Tran, T.H.H., Martinc, M., Doucet, A., Pollak, S.: IJS at TextGraphs-16 natu- ral language premise selection task: Will contextual information improve natural language premise selection? In: Ustalov, D., Gao, Y., Panchenko, A., Valentino, M., Thayaparan, M., Nguyen, T.H., Penn...

2022
[67]

Artificial Intelligence 206, 79–111 (2014) https://doi

Hutter, F., Xu, L., Hoos, H.H., Leyton-Brown, K.: Algorithm runtime prediction: Methods & evaluation. Artificial Intelligence 206, 79–111 (2014) https://doi. org/10.1016/j.artint.2013.10.003

2014 doi
[68]

In: Tan, Y

Kumazawa, T., Takimoto, M., Kambayashi, Y.: A survey on the applications of swarm intelligence to software verification. In: Tan, Y. (ed.) Handbook of Research on Fireworks Algorithms and Swarm Intelligence, pp. 376–398. IGI Global, Hershey, PA (2020). https://doi.org/10.4018/...

2020 doi
[69]

(eds.) Machine Learning for Software Analysis: Models, Methods, and Applications

Bennaceur, A., Meinke, K.: In: Bennaceur, A., H¨ ahnle, R., Meinke, K. (eds.) Machine Learning for Software Analysis: Models, Methods, and Applications. Lecture Notes in Computer Science, vol. 11026, pp. 3–49. Springer, Dagstuhl Castle, Germany (2018). https://doi.org/10.1007/...

2018 doi
[70]

In: Gamper, J., Pinchinat, S., Sciavicco, G

Brunello, A., Montanari, A., Reynolds, M.: Synthesis of LTL Formulas from Natural Language Texts: State of the Art and Research Directions. In: Gamper, J., Pinchinat, S., Sciavicco, G. (eds.) 26th International Symposium on Temporal Representation and Reasoning (TIME 2019). Le...

2019 doi
[71]

In: 2019 IEEE 17th International Conference on Industrial Infor- matics (INDIN), pp

Buzhinsky, I.: Formalization of natural language requirements into temporal logics: a survey. In: 2019 IEEE 17th International Conference on Industrial Infor- matics (INDIN), pp. 400–406. IEEE, Helsinki, Finland (2019). https://doi.org/ 10.1109/INDIN41052.2019.8972130

2019
[72]

In: AAAI- 23 Special Programs, IAAI-23, EAAI-23, Student Papers and Demonstrations, vol

Fuggitti, F., Chakraborti, T.: NL2LTL–a python package for converting natural language (NL) instructions to linear temporal logic (LTL) formulas. In: AAAI- 23 Special Programs, IAAI-23, EAAI-23, Student Papers and Demonstrations, vol. 37. AAAI Press, Washington, DC, USA (2023)...

2023
[74]

Software and Systems Modeling 21(3), 1135–1157 (2022) https://doi.org/10.1007/s10270-022-00983-5

Barriga, A., Rutle, A., Heldal, R.: AI-powered model repair: an experience report—lessons learned, challenges, and opportunities. Software and Systems Modeling 21(3), 1135–1157 (2022) https://doi.org/10.1007/s10270-022-00983-5

2022 doi
[75]

In: 2022 IEEE Conference on Software Testing, Verification and Validation (ICST), pp

Haltermann, J., Wehrheim, H.: Machine learning based invariant generation: A framework and reproducibility study. In: 2022 IEEE Conference on Software Testing, Verification and Validation (ICST), pp. 12–23. IEEE, Valencia, Spain (2022). https://doi.org/10.1109/ICST53961.2022.00012

2022
[76]

IEEE Access 10, 49508–49527 (2022) https://doi.org/10

Pan, Z., Mishra, P.: A survey on hardware vulnerability analysis using machine learning. IEEE Access 10, 49508–49527 (2022) https://doi.org/10. 1109/ACCESS.2022.3173287

2022
[77]

In: 2022 International Symposium on iNnovative Informatics of Biskra (ISNIB), pp

Besbas, A., Belaiche, L., Slatnia, S., Kahloul, L., Khalgui, M.: Machine learning solutions to model checking: A brief literature review. In: 2022 International Symposium on iNnovative Informatics of Biskra (ISNIB), pp. 1–4. IEEE, Biskra, Algeria (2022). https://doi.org/10.110...

2022
[78]

In: International Conference on Learn- ing Representations

Amizadeh, S., Matusevych, S., Weimer, M.: Learning to solve Circuit-SAT: An unsupervised differentiable approach. In: International Conference on Learn- ing Representations. OpenReview.net, New Orleans, LA, USA (2019). https: //openreview.net/forum?id=BJxgz2R9t7

2019
[79]

In: Jain, L.C., Tsihrintzis, G.A., Balas, V.E., Sharma, D.K

Atkari, A., Dhargalkar, N., Angne, H.: Employing machine learning models to solve uniform random 3-SAT. In: Jain, L.C., Tsihrintzis, G.A., Balas, V.E., Sharma, D.K. (eds.) Data Communication and Networks. Advances in Intelligent Systems and Computing, vol. 1049, pp. 255–264. S...

2020 doi
[80]

In: 2022 IEEE 34th Interna- tional Conference on Tools with Artificial Intelligence (ICTAI), pp

Fournier, T., Lallouet, A., Cropsal, T., Glorian, G., Papadopoulos, A., Petitet, A., Perez, G., Sekar, S., Suijlen, W.: A deep reinforcement learning heuristic for SAT based on antagonist graph neural networks. In: 2022 IEEE 34th Interna- tional Conference on Tools with Artifi...

2022
[81]

In: Koyejo, S., Mohamed, S., Agarwal, A., Belgrave, D., Cho, K., Oh, A

Li, Z., Si, X.: NSNet: A general neural probabilistic framework for satisfi- ability problems. In: Koyejo, S., Mohamed, S., Agarwal, A., Belgrave, D., Cho, K., Oh, A. (eds.) Advances in Neural Information Processing Systems 35 (NeurIPS 2022), vol. 35, pp. 25573–25585. Curran A...

2022
[82]

In: Simonis, H

Nejati, S., Le Frioux, L., Ganesh, V.: A machine learning based splitting heuristic for divide-and-conquer solvers. In: Simonis, H. (ed.) Principles and Practice of Constraint Programming. Lecture Notes in Computer Science, vol. 12333, pp. 899–916. Springer, Louvain-la-Neuve, ...

2020
[83]

In: International Conference on Learning Representations

Selsam, D., Lamm, M., B¨ unz, B., Liang, P., Moura, L., Dill, D.L.: Learn- ing a SAT solver from single-bit supervision. In: International Conference on Learning Representations. OpenReview.net, New Orleans, LA, USA (2019). https://openreview.net/forum?id=HJMC iA5tm

2019
[84]

In: Arai, K

Xu, R., Lieberherr, K.: Towards tackling QSAT problems with deep learning and monte carlo tree search. In: Arai, K. (ed.) Intelligent Computing. Lecture Notes in Networks and Systems, vol. 507, pp. 45–58. Springer, London, UK (2022). https://doi.org/10.1007/978-3-031-10464-0 4

2022 doi
[85]

In: Wallach, H., Larochelle, H., Beygelzimer, A., Alch´ e-Buc, F., Fox, E., Garnett, R

Yolcu, E., Poczos, B.: Learning local search heuristics for boolean satisfiability. In: Wallach, H., Larochelle, H., Beygelzimer, A., Alch´ e-Buc, F., Fox, E., Garnett, R. (eds.) Advances in Neural Information Processing Systems, vol. 32. Cur- ran Associates, Inc., Vancouver, ...

2019
[86]

In: Gama, J., Li, T., Yu, Y., Chen, E., Zheng, Y., Teng, F

Zhang, C., Zhang, Y., Mao, J., Chen, W., Yue, L., Bai, G., Xu, M.: Towards better generalization for neural network-based SAT solvers. In: Gama, J., Li, T., Yu, Y., Chen, E., Zheng, Y., Teng, F. (eds.) Advances in Knowl- edge Discovery and Data Mining. Lecture Notes in Artific...

2022
[87]

In: Dolev, S., Kolesnikov, V., Lodha, S., Weiss, G

Sun, L., Gerault, D., Benamira, A., Peyrin, T.: NeuroGIFT: Using a machine learning based SAT solver for cryptanalysis. In: Dolev, S., Kolesnikov, V., Lodha, S., Weiss, G. (eds.) International Symposium on Cyber Security Cryp- tography and Machine Learning. Lecture Notes in Co...

2020
[88]

In: Proceedings of the AAAI Conference on Artificial Intelligence, vol

Cameron, C., Chen, R., Hartford, J., Leyton-Brown, K.: Predicting propositional satisfiability via end-to-end learning. In: Proceedings of the AAAI Conference on Artificial Intelligence, vol. 34, pp. 3324–3331. AAAI Press, New York, NY, USA (2020). https://doi.org/10.1609/aaai...

2020 doi
[89]

International Journal of Computational Intelligence Systems 15(1), 84 (2022) https://doi.org/10.1007/s44196-022-00139-9

Chang, W., Zhang, H., Luo, J.: Predicting propositional satisfiability based on graph attention networks. International Journal of Computational Intelligence Systems 15(1), 84 (2022) https://doi.org/10.1007/s44196-022-00139-9

2022 doi
[90]

In: Janota, M., Lynce, I

Selsam, D., Bjørner, N.: Guiding high-performance SAT solvers with Unsat- Core predictions. In: Janota, M., Lynce, I. (eds.) Theory and Applications of 44 Satisfiability Testing – SAT 2019. Lecture Notes in Computer Science, vol. 11628, pp. 336–353. Springer, Lisbon, Portugal ...

2019
[91]

In: Proceedings of the AAAI Conference on Artificial Intelligence, vol

Xu, L., Hoos, H.H.H., Leyton-Brown, K.: Predicting satisfiability at the phase transition. In: Proceedings of the AAAI Conference on Artificial Intelligence, vol. 26, pp. 584–590. AAAI Press, Toronto, Canada (2021). https://doi.org/10. 1609/aaai.v26i1.8142

2021
[92]

In: Bessiere, C

Zhang, W., Sun, Z., Zhu, Q., Li, G., Cai, S., Xiong, Y., Zhang, L.: NLo- calSAT: boosting local search with solution prediction. In: Bessiere, C. (ed.) Proceedings of the Twenty-Ninth International Joint Conference on Artificial Intelligence, pp. 1177–1183. International Joint...

2020 doi
[93]

In: 28th Inter- national Conference on Principles and Practice of Constraint Programming

Berden, S., Kumar, M., Kolb, S., Guns, T.: Learning MAX-SAT models from examples using genetic algorithms and knowledge compilation. In: 28th Inter- national Conference on Principles and Practice of Constraint Programming. Leibniz International Proceedings in Informatics, LIPI...

2022 doi
[94]

In: Larochelle, H., Ranzato, M., Hadsell, R., Balcan, M.F., Lin, H

Chang, O., Flokas, L., Lipson, H., Spranger, M.: Assessing SATNet’s abil- ity to solve the symbol grounding problem. In: Larochelle, H., Ranzato, M., Hadsell, R., Balcan, M.F., Lin, H. (eds.) Advances in Neural Information Processing Systems, vol. 33, pp. 1428–1439. Curran Ass...

2020
[95]

In: Marreiros, G., Martins, B., Paiva, A., Ribeiro, B., Sardinha, A

Framil, M., Cabalar, P., Santos, J.: A MaxSAT solver based on differential evo- lution (preliminary report). In: Marreiros, G., Martins, B., Paiva, A., Ribeiro, B., Sardinha, A. (eds.) Progress in Artificial Intelligence. Lecture Notes in Computer Science, vol. 13566, pp. 676–...

2022 doi
[96]

Artificial Intelligence 314, 103794 (2023) https://doi.org/10.1016/j.artint.2022.103794

Kumar, M., Kolb, S., Teso, S., De Raedt, L.: Learning MAX-SAT from contex- tual examples for combinatorial optimisation. Artificial Intelligence 314, 103794 (2023) https://doi.org/10.1016/j.artint.2022.103794

2023
[97]

Intelligent Decision Technologies 13(2), 193–210 (2019) https://doi.org/10.3233/idt-180036

Lassouaoui, M., Boughaci, D., Benhamou, B.: A multilevel synergy Thompson sampling hyper-heuristic for solving Max-SAT. Intelligent Decision Technologies 13(2), 193–210 (2019) https://doi.org/10.3233/idt-180036

2019 doi
[98]

Machine Learning: Science and Technology 2(3), 035032 (2021) https: //doi.org/10.1088/2632-2153/ac0496 45

Marino, R.: Learning from survey propagation: a neural network for MAX-E- 3-SAT. Machine Learning: Science and Technology 2(3), 035032 (2021) https: //doi.org/10.1088/2632-2153/ac0496 45

2021 doi
[99]

International Journal of Computational Intelligence Systems15(1) (2022) https://doi.org/10.1007/s44196-022-00120-6

Nurcahyadi, T., Blum, C., Many` a, F.: Negative learning ant colony optimization for MaxSAT. International Journal of Computational Intelligence Systems15(1) (2022) https://doi.org/10.1007/s44196-022-00120-6

2022 doi
[100]

In: Chikhi, S., Amine, A., Chaoui, A., Saidouni, D.E., Kholladi, M.K

Sadeg, S., Hamdad, L., Kada, O., Benatchba, K., Habbas, Z.: Meta-learning to select the best metaheuristic for the MaxSAT problem. In: Chikhi, S., Amine, A., Chaoui, A., Saidouni, D.E., Kholladi, M.K. (eds.) International Symposium on Modelling and Implementation of Complex Sy...

2021 doi
[101]

In: Raedt, L.D

Zheng, J., He, K., Zhou, J., Jin, Y., Li, C.-M., Many` a, F.: BandMaxSAT: A local search MaxSAT solver with multi-armed bandit. In: Raedt, L.D. (ed.) Thirty-First International Joint Conference on Artificial Intelligence (IJCAI- 22), pp. 1901–1907. International Joint Conferen...

2022 doi
[102]

In: Rocha, A., Steels, L., VandenHerik, J

Beskyd, F., Surynek, P.: Parameter setting in SAT solver using machine learning techniques. In: Rocha, A., Steels, L., VandenHerik, J. (eds.) Proceedings of the 14th International Conference on Agentes and Artifical Inteligence. ICAART, vol. 2, pp. 586–597. SciTePress, Virtual...

2022
[103]

(eds.) Advances in Neural Information Processing Systems, vol

Kurin, V., Godil, S., Whiteson, S., Catanzaro, B.: Can Q-learning with graph networks learn a generalizable branching heuristic for a SAT solver? In: Larochelle, H., Ranzato, M., Hadsell, R., Balcan, M.F., Lin, H. (eds.) Advances in Neural Information Processing Systems, vol. ...

2020
[104]

In: Moreno- D ´ ıaz, R., Pichler, F., Quesada-Arencibia, A

Lorenz, J.-H., Nickerl, J.: The potential of restarts for ProbSAT. In: Moreno- D ´ ıaz, R., Pichler, F., Quesada-Arencibia, A. (eds.) Computer Aided Systems Theory – EUROCAST 2019. Lecture Notes in Computer Science, vol. 12013, pp. 352–360. Springer, Las Palmas de Gran Canaria...

2020 doi
[105]

In: International Conference on Learning Representations

Lederman, G., Rabe, M., Seshia, S., Lee, E.A.: Learning heuristics for quantified Boolean formulas through reinforcement learning. In: International Conference on Learning Representations. OpenReview.net, Addis Ababa, Ethiopia (2020). https://openreview.net/forum?id=BJluxREKDB

2020
[106]

Automated Software Engineering 27(1), 153–186 (2020) https://doi.org/10.1007/s10515-020-00270-x

Richter, C., H¨ ullermeier, E., Jakobs, M.-C., Wehrheim, H.: Algorithm selection for software validation based on graph kernels. Automated Software Engineering 27(1), 153–186 (2020) https://doi.org/10.1007/s10515-020-00270-x

2020 doi
[107]

In: 2022 IEEE International Conference on Systems, Man, and Cybernetics 46 (SMC), pp

Sadreddin, A., Mouhoub, M., Sadaoui, S.: Portfolio selection for SAT instances. In: 2022 IEEE International Conference on Systems, Man, and Cybernetics 46 (SMC), pp. 2962–2967. IEEE, Prague, Czech Republic (2022). https://doi.org/ 10.1109/SMC53654.2022.9945151

2022
[108]

In: 2019 12th IEEE Conference on Software Testing, Validation and Verification (ICST), pp

Wang, W., Wang, K., Zhang, M., Khurshid, S.: Learning to optimize the Alloy Analyzer. In: 2019 12th IEEE Conference on Software Testing, Validation and Verification (ICST), pp. 228–239. IEEE, Xi’an, China (2019). https://doi.org/ 10.1109/ICST.2019.00031

2019
[110]

In: Kov´ asznai, G., Istv´ an, F., T´ om´ acs, T

Danisovszky, M., Yang, Z.G., Kusper, G.: Classification of SAT problem instances by machine learning methods. In: Kov´ asznai, G., Istv´ an, F., T´ om´ acs, T. (eds.) Proceedings of the 11th International Conference on Applied Informat- ics. CEUR Workshop Proceedings, vol. 265...

2020
[111]

In: International Conference on Life Sciences, Engineering and Technology

Farooque, M., Keni, A.: A brief analogy of NNs and literal selection procedures within SAT solvers. In: International Conference on Life Sciences, Engineering and Technology. International Society for Technology, Education, and Science (ISTES), Denver, CO, USA (2023). https://...

2023
[112]

In: 5th Conference on Artificial Intelligence and Theorem Proving

Han, J.M.: Learning cubing heuristics for SAT from DRAT proofs. In: 5th Conference on Artificial Intelligence and Theorem Proving. AITP Confer- ence, Aussois, France (2020). https://aitp-conference.org/2020/abstract/paper 23.pdf

2020
[113]

Data Technologies and Applications53(1), 85–107 (2019) https: //doi.org/10.1108/dta-07-2018-0068

Hireche, C., Drias, H.: Multidimensional appropriate clustering and DBSCAN for SAT solving. Data Technologies and Applications53(1), 85–107 (2019) https: //doi.org/10.1108/dta-07-2018-0068

2019 doi
[114]

Applied Soft Computing Journal 88, 106069 (2020) https://doi.org/10.1016/j

Hireche, C., Drias, H., Moulai, H.: Grid based clustering for satisfiability solving. Applied Soft Computing Journal 88, 106069 (2020) https://doi.org/10.1016/j. asoc.2020.106069

2020
[115]

In: First International Workshop on Deep Learning-aided Verification

Yan, Z., Li, M., Shi, Z., Zhang, W., Chen, Y.-C., Zhang, H.: The elephant in the room: Variable dependency in GNN-based SAT solving. In: First International Workshop on Deep Learning-aided Verification. OpenReview.net, Paris, France (2023). https://openreview.net/forum?id=yOyxNRK5MOM

2023
[116]

Journal of Universal Computer Science 26(2), 220–243 (2020) https: //doi.org/10.3897/jucs.2020.013 47

Fu, H., Xu, Y., Chen, S., Liu, J.: Improving WalkSAT for random 3-SAT problems. Journal of Universal Computer Science 26(2), 220–243 (2020) https: //doi.org/10.3897/jucs.2020.013 47

2020 doi
[117]

In: 2022 IEEE International Test Conference (ITC), pp

Huang, J., Zhen, H.-L., Wang, N., Mao, H., Yuan, M., Huang, Y.: Neural fault analysis for SAT-based ATPG. In: 2022 IEEE International Test Conference (ITC), pp. 36–45. IEEE, Anaheim, CA, USA (2022). https://doi.org/10.1109/ ITC50671.2022.00010

2022
[118]

In: Arai, K., Bhatia, R., Kapoor, S

Leventi-Peetz, A.M., Peetz, J.-V., Rohde, M.: ML supported predictions for SAT solvers performance. In: Arai, K., Bhatia, R., Kapoor, S. (eds.) Proceedings of the Future Technologies Conference (FTC) 2019. Advances in Intelligent Sys- tems and Computing, vol. 1069, pp. 64–78. ...

2020 doi
[119]

In: 2022 International Joint Conference on Neu- ral Networks (IJCNN), pp

Ozolins, E., Freivalds, K., Draguns, A., Gaile, E., Zakovskis, R., Kozlovics, S.: Goal-aware neural SAT solver. In: 2022 International Joint Conference on Neu- ral Networks (IJCNN), pp. 1–8. IEEE, Padua, Italy (2022). https://doi.org/10. 1109/IJCNN55064.2022.9892733

2022
[120]

In: Meel, K.S., Strichman, O

Garz´ on, I., Mesejo, P., Gir´ aldez-Cru, J.: On the performance of deep generative models of realistic SAT instances. In: Meel, K.S., Strichman, O. (eds.) 25th Inter- national Conference on Theory and Applications of Satisfiability Testing (SAT 2022). Leibniz International Pr...

2022 doi
[121]

In: Wallach, H., Larochelle, H., Beygelzimer, A., Alch´ e-Buc, F., Fox, E., Garnett, R

You, J., Wu, H., Barrett, C., Ramanujan, R., Leskovec, J.: G2SAT: Learn- ing to generate SAT formulas. In: Wallach, H., Larochelle, H., Beygelzimer, A., Alch´ e-Buc, F., Fox, E., Garnett, R. (eds.) Advances in Neural Information Processing Systems 32 (NeurIPS 2019), vol. 32. C...

2019
[122]

In: Graham-Lengrand, S., Preiner, M

Jakub ˚ uv, J., Janota, M., Piotrowski, B., Piepenbrock, J., Reynolds, A.: Select- ing quantifiers for instantiation in SMT. In: Graham-Lengrand, S., Preiner, M. (eds.) Proceedings of the 21st International Workshop on Satisfiability Modulo Theories (SMT 2023). CEUR Workshop P...

2023
[123]

In: Meel, K.S., Strichman, O

Janota, M., Piepenbrock, J., Piotrowski, B.: Towards learning quantifier instanti- ation in SMT. In: Meel, K.S., Strichman, O. (eds.) 25th International Conference on Theory and Applications of Satisfiability Testing (SAT 2022). Leibniz International Proceedings in Informatics...

2022 doi
[124]

In: 4th Conference on Artificial Intelligence and Theorem Proving

Blanchette, J.C., El Ouraoui, D., Fontaine, P., Kaliszyk, C.: Machine learning for instance selection in SMT solving. In: 4th Conference on Artificial Intelligence and Theorem Proving. AITP Conference, Obergurgl, Austria (2019). https:// aitp-conference.org/2019/abstract/paper...

2019
[125]

In: Julia M

Dunkelau, J., Krings, S., Schmidt, J.: Automated backend selection for ProB using deep learning. In: Julia M. Badger, K.Y.R. (ed.) NASA For- mal Methods Symposium. Lecture Notes in Computer Science, vol. 11460, pp. 130–147. Springer, Houston, TX, USA (2019). https://doi.org/10...

2019
[126]

In: 2021 IEEE 33rd International Conference on Tools with Artificial Intelligence (ICTAI), pp

H ˚ ula, J., Mojˇ z ´ ıˇ sek, D., Janota, M.: Graph neural networks for scheduling of SMT solvers. In: 2021 IEEE 33rd International Conference on Tools with Artificial Intelligence (ICTAI), pp. 447–451. IEEE, Washington, DC, USA (2021). https: //doi.org/10.1109/ICTAI52525.2021.00072

2021
[127]

In: 2023 IEEE/ACM 45th International Conference on Soft- ware Engineering (ICSE), pp

Leeson, W., Dwyer, M.B., Filieri, A.: Sibyl: Improving software engineering tools with SMT selection. In: 2023 IEEE/ACM 45th International Conference on Soft- ware Engineering (ICSE), pp. 2185–2197. IEEE, Melbourne, Australia (2023). https://doi.org/10.1109/ICSE48619.2023.00184

2023
[128]

In: Chu-Min Li, F.M

Pimpalkhare, N., Mora, F., Polgreen, E., Seshia, S.A.: MedleySolver: Online SMT algorithm selection. In: Chu-Min Li, F.M. (ed.) Theory and Applications of Satisfiability Testing — SAT 2021. Lecture Notes in Computer Science, vol. 12831, pp. 453–470. Springer, Barcelona, Spain ...

2021
[129]

In: Proceedings of the 35th IEEE/ACM International Conference on Automated Software Engineering

Pimpalkhare, N.: Dynamic algorithm selection for SMT. In: Proceedings of the 35th IEEE/ACM International Conference on Automated Software Engineering. ASE ’20, pp. 1376–1378. Association for Computing Machinery, Virtual Event (2021). https://doi.org/10.1145/3324884.3418922

2021
[130]

In: Groote, J.F., Larsen, K.G

Scott, J., Niemetz, A., Preiner, M., Nejati, S., Ganesh, V.: MachSMT: A machine learning-based algorithm selector for SMT solvers. In: Groote, J.F., Larsen, K.G. (eds.) International Conference on Tools and Algorithms for the Construction and Analysis of Systems. Lecture Notes...

2021
[131]

International Journal on Software Tools for Technology Transfer 25, 219–239 (2023) https://doi.org/10.1007/s10009-023-00696-0

Scott, J., Niemetz, A., Preiner, M., Nejati, S., Ganesh, V.: Algorithm selection for SMT. International Journal on Software Tools for Technology Transfer 25, 219–239 (2023) https://doi.org/10.1007/s10009-023-00696-0

2023 doi
[132]

In: Alexander Raschke, F.H

Dunkelau, J., Schmidt, J., Leuschel, M.: Analysing ProB’s constraint solving backends. In: Alexander Raschke, F.H. Dominique M´ ery (ed.) Rigorous State- Based Methods: 7th International Conference, ABZ 2020. Lecture Notes in Computer Science, vol. 12071, pp. 107–123. Springer...

2020 doi
[133]

In: Huisman, M., P˘ as˘ areanu, C., Zhan, N

Scott, J., Sudula, T., Rehman, H., Mora, F., Ganesh, V.: BanditFuzz: Fuzzing SMT solvers with multi-agent reinforcement learning. In: Huisman, M., P˘ as˘ areanu, C., Zhan, N. (eds.) International Symposium on Formal Methods. 49 Lecture Notes in Computer Science, vol. 13047, pp...

2021 doi
[134]

In: Proceedings of the 30th ACM SIGSOFT International Symposium on Software Testing and Analysis

Yao, P., Huang, H., Tang, W., Shi, Q., Wu, R., Zhang, C.: Fuzzing SMT solvers via two-dimensional input space exploration. In: Proceedings of the 30th ACM SIGSOFT International Symposium on Software Testing and Analysis. ISSTA 2021, pp. 322–335. Association for Computing Machi...

2021
[135]

In: 4th Conference on Artificial Intelligence and Theorem Proving, Obergurgl, Austria (2019)

Holden, E.K., Korovin, K.: SMAC and XGBoost your theorem prover. In: 4th Conference on Artificial Intelligence and Theorem Proving, Obergurgl, Austria (2019). https://aitp-conference.org/2019/abstract/paper%2031.pdf

2019
[136]

In: L´ opez-Ib´ a˜ nez, M

Nagashima, Y.: Towards evolutionary theorem proving for isabelle/HOL. In: L´ opez-Ib´ a˜ nez, M. (ed.) Proceedings of the Genetic and Evolutionary Com- putation Conference Companion. GECCO ’19, pp. 419–420. Association for Computing Machinery, Prague, Czech Republic (2019). ht...

2019
[137]

In: Fontaine, P., Korovin, K., Kotsireas, I.S., R¨ ummer, P., Tourret, S

B´ artek, F., Suda, M.: Learning precedences from simple symbol features. In: Fontaine, P., Korovin, K., Kotsireas, I.S., R¨ ummer, P., Tourret, S. (eds.) PAAR+SC-Square 2020 Practical Aspects of Automated Reasoning and Satisfi- ability Checking and Symbolic Computation Worksh...

2020
[139]

In: Fontaine, P

Chvalovsk´ y, K., Jakub ˚ uv, J., Suda, M., Urban, J.: ENIGMA-NG: Efficient neural and gradient-boosted inference guidance for E. In: Fontaine, P. (ed.) International Conference on Automated Deduction. Lecture Notes in Com- puter Science, vol. 11716, pp. 197–215. Springer, Nat...

2019 doi
[140]

In: Anupam Das, S.N

Chvalovsk´ y, K., Jakub ˚ uv, J., Olˇ s´ ak, M., Urban, J.: Learning theorem proving components. In: Anupam Das, S.N. (ed.) Automated Reasoning with Ana- lytic Tableaux and Related Methods. Lecture Notes in Computer Science, vol. 12842, pp. 266–278. Springer, Birmingham, UK (2...

2021
[141]

In: Piskac, R., Voronkov, A

Chvalovsk` y, K., Korovin, K., Piepenbrock, J., Urban, J.: Guiding an instanti- ation prover with graph neural networks. In: Piskac, R., Voronkov, A. (eds.) Proceedings of 24th International Conference on Logic for Programming, Artifi- cial Intelligence, and Reasoning. EPiC Se...

2023 doi
[142]

In: Proceedings of the AAAI Conference on Artificial Intelligence, vol

Crouse, M., Abdelaziz, I., Makni, B., Whitehead, S., Cornelio, C., Kapanipathi, P., Srinivas, K., Thost, V., Witbrock, M., Fokoue, A.: A deep reinforcement learning approach to first-order logic theorem proving. In: Proceedings of the AAAI Conference on Artificial Intelligence...

2021 doi
[143]

In: Jurafsky, D., Chai, J., Schluter, N., Tetreault, J

Ferreira, D., Freitas, A.: Premise selection in natural language mathematical texts. In: Jurafsky, D., Chai, J., Schluter, N., Tetreault, J. (eds.) Proceedings of the 58th Annual Meeting of the Association for Computational Linguistics, pp. 7365–7374. Association for Computati...

2020 doi
[144]

In: 1st Mathematical Reasoning in General Artificial Intelligence Workshop, ICLR 2021

Firoiu, V., Aygun, E., Anand, A., Ahmed, Z., Glorot, X., Orseau, L., Zhang, L., Precup, D., Mourad, S.: Training a first-order theorem prover from syn- thetic data. In: 1st Mathematical Reasoning in General Artificial Intelligence Workshop, ICLR 2021. Math-AI Organizers, Virtu...

2021
[145]

In: Cerrito, S., Popescu, A

Goertzel, Z., Jakub ˚ uv, J., Urban, J.: ENIGMA Watch: ProofWatch meets ENIGMA. In: Cerrito, S., Popescu, A. (eds.) Automated Reasoning with Ana- lytic Tableaux and Related Methods. Lecture Notes in Computer Science, vol. 11714, pp. 374–388. Springer, London, UK (2019). https:...

2019
[146]

In: 4th Conference on Artificial Intelligence and Theorem Proving

Goertzel, Z., Urban, J.: Usefulness of lemmas via graph neural networks. In: 4th Conference on Artificial Intelligence and Theorem Proving. AITP Con- ference, Obergurgl, Austria (2019). https://aitp-conference.org/2019/abstract/ AITP 2019 paper 32.pdf

2019
[148]

In: Andronick, J., Moura, L

Goertzel, Z.A., Jakub ˚ uv, J., Kaliszyk, C., Olˇ s´ ak, M., Piepenbrock, J., Urban, J.: The Isabelle ENIGMA. In: Andronick, J., Moura, L. (eds.) 13th International Conference on Interactive Theorem Proving (ITP 2022). Leibniz International Proceedings in Informatics (LIPIcs),...

2022
[149]

In: 6th Conference on Artificial Intelligence and Theorem Proving

Han, J.M., Xu, T., Polu, S., Neelakantan, A., Radford, A.: Contrastive finetuning of generative language models for informal premise selection. In: 6th Conference on Artificial Intelligence and Theorem Proving. AITP Conference, Virtual Event 51 (2021). https://aitp-conference....

2021
[150]

In: International Conference on Learning Represen- tations

Huang, D., Dhariwal, P., Song, D., Sutskever, I.: GamePad: A learning environ- ment for theorem proving. In: International Conference on Learning Represen- tations. OpenReview.net, New Orleans, LA, USA (2019). https://openreview. net/forum?id=r1xwKoR9Y7

2019
[151]

In: Harrison, J., O’Leary, J., Tolmach, A

Jakubuv, J., Urban, J.: Hammering Mizar by learning clause guidance. In: Harrison, J., O’Leary, J., Tolmach, A. (eds.) 10th International Conference on Interactive Theorem Proving (ITP 2019). Leibniz International Proceedings in Informatics (LIPIcs), vol. 141, pp. 1–8. Schloss...

2019 doi
[153]

In: Koyejo, S., Mohamed, S., Agarwal, A., Belgrave, D., Cho, K., Oh, A

Jiang, A.Q., Li, W., Tworkowski, S., Czechowski, K., Odrzyg´ o´ zd´ z, T., Mi l o´ s, P., Wu, Y., Jamnik, M.: Thor: Wielding hammers to integrate language mod- els and automated theorem provers. In: Koyejo, S., Mohamed, S., Agarwal, A., Belgrave, D., Cho, K., Oh, A. (eds.) Adv...

2022
[154]

In: Boris Konev, A.S

Liu, Q., Wu, Z., Wang, Z., Sutcliffe, G.: Evaluation of axiom selection techniques. In: Boris Konev, A.S. Claudia Schon (ed.) PAAR+SC-Square 2020 Practi- cal Aspects of Automated Reasoning and Satisfiability Checking and Symbolic Computation Workshop 2020. CEUR Workshop Procee...

2020
[155]

International Journal of Machine Learning and Cybernetics 13, 1301–1315 (2022) https://doi.org/10.1007/s13042-021-01448-9

Liu, Q., Xu, Y., He, X.: Attention recurrent cross-graph neural network for selecting premises. International Journal of Machine Learning and Cybernetics 13, 1301–1315 (2022) https://doi.org/10.1007/s13042-021-01448-9

2022 doi
[156]

https://ceur-ws.org/Vol-2752/paper5

CEUR-WS.org, Virtual Event (2020). https://ceur-ws.org/Vol-2752/paper5. pdf

2020
[157]

In: Garcez, E.J.-R

Morris, M., Minervini, P., Blunsom, P.: Learning proof path selection policies in neural theorem proving. In: Garcez, E.J.-R. (ed.) Proceedings of the 16th 52 International Workshop on Neural-Symbolic Learning and Reasoning (NeSy). CEUR Workshop Proceedings, vol. 3212. CEUR-WS...

2022
[159]

In: De Giacomo, G., Catala, A., Dilkina, B., Milano, M., Barro, S., Bugar ´ ın, A., Lang, J

Ols´ ak, M., Kaliszyk, C., Urban, J.: Property invariant embedding for automated reasoning. In: De Giacomo, G., Catala, A., Dilkina, B., Milano, M., Barro, S., Bugar ´ ın, A., Lang, J. (eds.) 24th European Conference on Artificial Intelligence. Fronties in Artificial Intellige...

2020 doi
[160]

Applied Soft Computing 104, 107200 (2021) https://doi.org/10.1016/j

Nawaz, M.S., Nawaz, M.Z., Hasan, O., Fournier-Viger, P., Sun, M.: An evolutionary/heuristic-based proof searching framework for interactive theorem prover. Applied Soft Computing 104, 107200 (2021) https://doi.org/10.1016/j. asoc.2021.107200

2021
[161]

Journal of Open Source Software 7(71), 3849 (2022) https://doi.org/ 10.21105/joss.03849

Shminke, B.: gym-saturation: an OpenAI Gym environment for saturation provers. Journal of Open Source Software 7(71), 3849 (2022) https://doi.org/ 10.21105/joss.03849

2022 doi
[162]

In: Albert, E., Kovacs, L

Piotrowski, B., Urban, J.: Stateful premise selection by recurrent neural net- works. In: Albert, E., Kovacs, L. (eds.) 23rd International Conference on Logic for Programming, Artificial Intelligence and Reasoning (LPAR-23). EPiC Series in Computing, vol. 73, pp. 409–422. Easy...

2020 doi
[163]

In: 7th Conference on Artificial Intelligence and Theorem Proving

Tworkowski, S., Mikula, M., Odrzyg´ o´ zd´ z, T., Czechowski, K., Antoniak, S., Jiang, A.Q., Szegedy, C., Kuci´ nski, L., Mil´ os, P., Wu, Y.: Formal premise selection with language models. In: 7th Conference on Artificial Intelligence and Theorem Proving. AITP Conference, Aus...

2022
[164]

In: Platzer, A., Sutcliffe, G

Suda, M.: Improving ENIGMA-style clause selection while learning from history. In: Platzer, A., Sutcliffe, G. (eds.) Automated Deduction – CADE 28. Lecture Notes in Computer Science, vol. 12699, pp. 543–561. Springer, Virtual Event (2021). https://doi.org/10.1007/978-3-030-79876-5 31

2021 doi
[165]

In: Koyejo, S., Mohamed, S., Agarwal, A., Belgrave, D., Cho, K., Oh, A

Welleck, S., Liu, J., Lu, X., Hajishirzi, H., Choi, Y.: Natural- Prover: Grounded mathematical proof generation with language models. In: Koyejo, S., Mohamed, S., Agarwal, A., Belgrave, D., Cho, K., Oh, A. (eds.) Advances in Neural Information Processing Systems 35 (NeurIPS 20...

2022
[166]

In: 4th Inter- national Conference on Frontiers Technology of Information and Computer (ICFTIC)

Wei, Y.: Applying autoencoder to automated theorem proving. In: 4th Inter- national Conference on Frontiers Technology of Information and Computer (ICFTIC). IEEE, Qingdao, China (2022). https://doi.org/10.1109/icftic57696. 2022.10075262

2022
[167]

In: Das, A., Negri, S

Zombori, Z., Urban, J., Olˇ s´ ak, M.: The role of entropy in guiding a connec- tion prover. In: Das, A., Negri, S. (eds.) International Conference on Automated Reasoning with Analytic Tableaux and Related Methods. Lecture Notes in Computer Science, vol. 12842, pp. 218–235. Sp...

2021 doi
[168]

In: Sattler, U., Suda, M

Zhang, L., Blaauwbroek, L., Kaliszyk, C., Urban, J.: Learning proof transforma- tions and its applications in interactive theorem proving. In: Sattler, U., Suda, M. (eds.) Frontiers of Combining Systems: 14th International Symposium. Lecture Notes in Computer Science, vol. 142...

2023 doi
[169]

Journal of Universal Computer Science 27(11), 1193–1202 (2021) https://doi.org/10.3897/jucs.76563

Baghdasaryan, A., Bolibekyan, H.: On recurrent neural network based theorem prover for first order minimal logic. Journal of Universal Computer Science 27(11), 1193–1202 (2021) https://doi.org/10.3897/jucs.76563

2021 doi
[170]

IEEE Transactions on Pattern Anal- ysis and Machine Intelligence 45(1), 738–751 (2023) https://doi.org/10.1109/ TPAMI.2022.3140382

Abdelaziz, I., Crouse, M., Makni, B., Austel, V., Cornelio, C., Ikbal, S., Kapa- nipathi, P., Makondo, N., Srinivas, K., Witbrock, M., Fokoue, A.: Learning to guide a saturation-based theorem prover. IEEE Transactions on Pattern Anal- ysis and Machine Intelligence 45(1), 738–7...

2023
[171]

In: Albert, E., Kovacs, L

Blaauwbroek, L., Urban, J., Geuvers, H.: Tactic learning and proving for the Coq proof assistant. In: Albert, E., Kovacs, L. (eds.) 23rd International Conference on Logic for Programming, Artificial Intelligence and Reasoning. EPiC Series in Computing, vol. 73, pp. 138–150. Ea...

2020 doi
[172]

In: Chaudhuri, K., Salakhutdinov, R

Bansal, K., Loos, S., Rabe, M., Szegedy, C., Wilcox, S.: HOList: An environment for machine learning of higher order logic theorem proving. In: Chaudhuri, K., Salakhutdinov, R. (eds.) Proceedings of the 36th International Conference on Machine Learning. Proceedings of Machine ...
[173]

Journal of Automated Reasoning65(2), 257–286 (2020) https://doi.org/10.1007/s10817-020-09580-x 54

Gauthier, T., Kaliszyk, C., Urban, J., Kumar, R., Norrish, M.: TacticToe: Learn- ing to prove with tactics. Journal of Automated Reasoning65(2), 257–286 (2020) https://doi.org/10.1007/s10817-020-09580-x 54

2020 doi
[175]

Journal of Automated Reasoning 65(2), 287–320 (2020) https://doi

F¨ arber, M., Kaliszyk, C., Urban, J.: Machine learning guidance for connection tableaux. Journal of Automated Reasoning 65(2), 287–320 (2020) https://doi. org/10.1007/s10817-020-09576-7

2020 doi
[176]

In: Guerrero, J

Mo, G., Xiong, Y., Huang, W., Ma, L.: Automated theorem proving via inter- acting with proof assistants by dynamic strategies. In: Guerrero, J. (ed.) 2020 6th International Conference on Big Data Computing and Communications (BIGCOM), pp. 71–75. IEEE, Deqing, China (2020). htt...

2020
[177]

Applied Intelligence 51, 1580–1601 (2021) https://doi.org/10.1007/ s10489-020-01837-7

Nawaz, M.S., Nawaz, M.Z., Hasan, O., Fournier-Viger, P., Sun, M.: Proof search- ing and prediction in HOL4 with evolutionary/heuristic and deep learning techniques. Applied Intelligence 51, 1580–1601 (2021) https://doi.org/10.1007/ s10489-020-01837-7

2021
[178]

In: Koyejo, S., Mohamed, S., Agarwal, A., Belgrave, D., Cho, K., Oh, A

Lample, G., Lacroix, T., Lachaux, M.-A., Rodriguez, A., Hayat, A., Lavril, T., Ebner, G., Martinet, X.: HyperTree proof search for neural theorem prov- ing. In: Koyejo, S., Mohamed, S., Agarwal, A., Belgrave, D., Cho, K., Oh, A. (eds.) Advances in Neural Information Processing...

2022
[179]

In: 6th Conference on Artificial Intelligence and Theorem Proving

Piepenbrock, J., Heskes, T., Janota, M., Urban, J.: Learning equational theorem proving. In: 6th Conference on Artificial Intelligence and Theorem Proving. AITP Conference, Aussois, France (2021). https://doi.org/10.48550/ARXIV. 2102.05547 . https://aitp-conference.org/2021/ab...

2021 doi arXiv
[180]

In: Blanchette, J., Kov´ acs, L., Pattin- son, D

Piepenbrock, J., Heskes, T., Janota, M., Urban, J.: Guiding an automated theorem prover with neural rewriting. In: Blanchette, J., Kov´ acs, L., Pattin- son, D. (eds.) International Joint Conference on Automated Reasoning. Lecture Notes in Computer Science, vol. 13385, pp. 597...

2022 doi
[181]

In: Proceedings of the AAAI Con- ference on Artificial Intelligence, vol

Paliwal, A., Loos, S., Rabe, M., Bansal, K., Szegedy, C.: Graph representations for higher-order logic and theorem proving. In: Proceedings of the AAAI Con- ference on Artificial Intelligence, vol. 34, pp. 2967–2974. AAAI Press, New York, NY, USA (2020). https://doi.org/10.160...

2020 doi
[182]

In: Herzig, 55 A., Popescu, A

Rawson, M., Reger, G.: A neurally-guided, parallel theorem prover. In: Herzig, 55 A., Popescu, A. (eds.) Frontiers of Combining Systems: 12th International Sym- posium, FroCoS 2019. Lecture Notes in Computer Science, vol. 11715, pp. 40–56. Springer, London, UK (2019). https://...

2019 doi
[183]

In: Sen, K., Naik, M

Sanchez-Stern, A., Alhessi, Y., Saul, L., Lerner, S.: Generating correctness proofs with neural networks. In: Sen, K., Naik, M. (eds.) Proceedings of the 4th ACM SIGPLAN International Workshop on Machine Learning and Programming Lan- guages. MAPL ’20. Association for Computing...

2020
[185]

In: Proceedings of the 61st Annual Meeting of the Association for Computational Linguistics, vol

Wang, H., Yuan, Y., Liu, Z., Shen, J., Yin, Y., Xiong, J., Xie, E., Shi, H., Li, Y., Li, L., Yin, J., Li, Z., Liang, X.: DT-solver: Automated theorem proving with dynamic-tree sampling guided by proof-level value function. In: Proceedings of the 61st Annual Meeting of the Asso...

2023 doi
[186]

In: Ranzato, M., Beygelzimer, A., Dauphin, Y., Liang, P.S., Vaughan, J.W

Wu, M., Norrish, M., Walder, C., Dezfouli, A.: TacticZero: Learning to prove theorems from scratch with deep reinforcement learning. In: Ranzato, M., Beygelzimer, A., Dauphin, Y., Liang, P.S., Vaughan, J.W. (eds.) Advances in Neural Information Processing Systems, vol. 34, pp....

2021
[189]

In: Das, A., Negri, S

Zombori, Z., Csisz´ arik, A., Michalewski, H., Kaliszyk, C., Urban, J.: Towards finding longer proofs. In: Das, A., Negri, S. (eds.) Automated Reasoning with Analytic Tableaux and Related Methods. Lecture Notes in Computer Science, vol. 12842, pp. 167–186. Springer, Birmingham...

2021
[190]

In: 4th Conference on Artificial Intelligence and Theorem Proving

Zombori, Z., Csisz´ arik, A., Michalewski, H., Kaliszyk, C., Urban, J.: Curricu- lum learning and theorem proving. In: 4th Conference on Artificial Intelligence and Theorem Proving. AITP Conference, Obergurgl, Austria (2019). https: //aitp-conference.org/2019/abstract/paper%2013.pdf

2019
[191]

IEEE Access 8, 119806–119818 (2020) https://doi.org/10.1109/ ACCESS.2020.3004199

Nawaz, M.S., Fournier-Viger, P., Zhang, J.: Proof learning in PVS with utility pattern mining. IEEE Access 8, 119806–119818 (2020) https://doi.org/10.1109/ ACCESS.2020.3004199

2020
[192]

In: Chaudhuri, K., Jegelka, S., Song, L., Szepesvari, C., Niu, G., Sabato, S

Ayg¨ un, E., Anand, A., Orseau, L., Glorot, X., Mcaleer, S.M., Firoiu, V., Zhang, L.M., Precup, D., Mourad, S.: Proving theorems using incremental learning and hindsight experience replay. In: Chaudhuri, K., Jegelka, S., Song, L., Szepesvari, C., Niu, G., Sabato, S. (eds.) Pro...

2022
[193]

In: 6th Conference on Artificial Intelligence and Theorem Proving

Jiang, A.Q., Li, W., Han, J.M., Wu, Y.: LISA: Language models of ISAbelle proofs. In: 6th Conference on Artificial Intelligence and Theorem Proving. 56 AITP Conference, Assouis and online, France (2021). https://aitp-conference. org/2021/abstract/paper 17.pdf

2021
[195]

In: Albert, E., Kovacs, L

Gauthier, T.: Deep reinforcement learning for synthesizing functions in higher- order logic. In: Albert, E., Kovacs, L. (eds.) 3rd International Conference on Logic for Programming, Artificial Intelligence and Reasoning. EPiC Series in Computing, vol. 73, pp. 230–248. EasyChai...

2020 doi
[196]

Pro- ceedings of the ACM on Programming Languages 4(OOPSLA), 1–31 (2020) https://doi.org/10.1145/3428299

First, E., Brun, Y., Guha, A.: TacTok: Semantics-aware proof synthesis. Pro- ceedings of the ACM on Programming Languages 4(OOPSLA), 1–31 (2020) https://doi.org/10.1145/3428299

2020 doi
[197]

In: International Conference on Learning Representations

Han, J.M., Rute, J., Wu, Y., Ayers, E., Polu, S.: Proof artifact co-training for theorem proving with language models. In: International Conference on Learning Representations. OpenReview.net, Virtual Event (2022). https://openreview. net/forum?id=rpxJc9j04U

2022
[198]

IEEE Trans- actions on Software Engineering 49(7), 3771–3792 (2023) https://doi.org/10

Kommrusch, S., Monperrus, M., Pouchet, L.-N.: Self-supervised learning to prove equivalence between straight-line programs via rewrite rules. IEEE Trans- actions on Software Engineering 49(7), 3771–3792 (2023) https://doi.org/10. 1109/TSE.2023.3271065

2023
[199]

In: Workshop on Graph Representation Learning at 33rd Neural Information Processing Systems

Glorot, X., Anand, A., Aygun, E., Mourad, S., Kohli, P., Precup, D.: Learning representations of logical formulae using graph neural networks. In: Workshop on Graph Representation Learning at 33rd Neural Information Processing Systems. Graph Representation Learning Committee, ...

2019
[200]

In: 7th Conference on Artificial Intelli- gence and Theorem Proving

Palermo, J., Ye, J., Han, J.M.: Synthetic proof term data augmentation for theorem proving with language models. In: 7th Conference on Artificial Intelli- gence and Theorem Proving. AITP Conference, Aussois, France (2022). https: //aitp-conference.org/2022/abstract/AITP 2022 p...

2022
[201]

Philosophical Transactions of the Royal Society A: Mathematical, Physical and Engineering Sciences 381(2251), 20220044 (2023) https://doi.org/10.1098/rsta

Poesia, G., Goodman, N.D.: Peano: learning formal mathematical reasoning. Philosophical Transactions of the Royal Society A: Mathematical, Physical and Engineering Sciences 381(2251), 20220044 (2023) https://doi.org/10.1098/rsta. 2022.0044

2023
[202]

In: Koyejo, S., Mohamed, S., Agarwal, A., Belgrave, D., Cho, K., Oh, A

Laurent, J., Platzer, A.: Learning to find proofs and theorems by learning to 57 refine search strategies: The case of loop invariant synthesis. In: Koyejo, S., Mohamed, S., Agarwal, A., Belgrave, D., Cho, K., Oh, A. (eds.) Advances in Neu- ral Information Processing Systems, ...

2022
[203]

In: Das, A., Negri, S

Rawson, M., Reger, G.: lazyCoP: Lazy paramodulation meets neurally guided search. In: Das, A., Negri, S. (eds.) Automated Reasoning with Analytic Tableaux and Related Methods. Lecture Notes in Computer Science, vol. 12842, pp. 187–199. Springer, Birmingham, UK (2021). https://...

2021
[204]

ACM Trans- actions on Programming Languages and Systems 45(2) (2023) https://doi.org/ 10.1145/3593374

Sanchez-Stern, A., First, E., Zhou, T., Kaufman, Z., Brun, Y., Ringer, T.: Passport: Improving automated formal verification using identifiers. ACM Trans- actions on Programming Languages and Systems 45(2) (2023) https://doi.org/ 10.1145/3593374

2023 doi
[205]

In: Sun, X., Zhang, X., Xia, Z., Bertino, E

Qian, H.: Research on automation strategy of Coq. In: Sun, X., Zhang, X., Xia, Z., Bertino, E. (eds.) Advances in Artificial Intelligence and Security. Communi- cations in Computer and Information Science, vol. 1423, pp. 656–665. Springer, Dublin, Ireland (2021). https://doi.o...

2021 doi
[206]

In: 5th Conference on Artificial Intelligence and Theorem Proving

Wu, Y., Jiang, A., Grosse, R., Ba, J.: Neural theorem proving on inequality problems. In: 5th Conference on Artificial Intelligence and Theorem Proving. AITP Conference, Obergurgl, Austria (2020). https://aitp-conference.org/2020/ abstract/paper 18.pdf

2020
[207]

In: Koyejo, S., Mohamed, S., Agarwal, A., Belgrave, D., Cho, K., Oh, A

Wu, Y., Jiang, A.Q., Li, W., Rabe, M., Staats, C., Jamnik, M., Szegedy, C.: Autoformalization with large language models. In: Koyejo, S., Mohamed, S., Agarwal, A., Belgrave, D., Cho, K., Oh, A. (eds.) Advances in Neural Information Processing Systems 35 (NeurIPS 2022), 58 vol....

2022
[208]

In: Larochelle, H., Ranzato, M., Hadsell, R., Balcan, M.F., Lin, H

Wang, M., Deng, J.: Learning to prove theorems by learning to generate theo- rems. In: Larochelle, H., Ranzato, M., Hadsell, R., Balcan, M.F., Lin, H. (eds.) Advances in Neural Information Processing Systems, vol. 33, pp. 18146–18157. Curran Associates, Inc., Virtual Event (20...

2020
[209]

In: Chaudhuri, K., Salakhutdinov, R

Yang, K., Deng, J.: Learning to prove theorems via interacting with proof assistants. In: Chaudhuri, K., Salakhutdinov, R. (eds.) Proceedings of the 36th International Conference on Machine Learning. Proceedings of Machine Learn- ing Research, vol. 97, pp. 6984–6994. PMLR, Lon...

2019
[210]

In: Ranzato, M., Beygelzimer, A., Dauphin, Y., Liang, P.S., Vaughan, J.W

Poesia, G., Dong, W., Goodman, N.: Contrastive reinforcement learning of symbolic reasoning domains. In: Ranzato, M., Beygelzimer, A., Dauphin, Y., Liang, P.S., Vaughan, J.W. (eds.) Advances in Neural Information Pro- cessing Systems, vol. 34, pp. 15946–15956. Curran Associate...

2021
[211]

In: 7th Conference on Artificial Intelligence and Theorem Proving

Wu, Y., Jiang, A., Li, W., Rabe, M.N., Staats, C., Jamnik, M., Szegedy, C.: Autoformalization for neural theorem proving. In: 7th Conference on Artificial Intelligence and Theorem Proving. AITP Conference, Aussois, France (2022). https://aitp-conference.org/2022/abstract/AITP ...

2022
[212]

Journal of Logic and Computation 31(8), 2057–2083 (2021) https://doi.org/10.1093/logcom/exab006

Purga L, S., Parsert, J., Kaliszyk, C.: A study of continuous vector representa- tions for theorem proving. Journal of Logic and Computation 31(8), 2057–2083 (2021) https://doi.org/10.1093/logcom/exab006

2021 doi
[213]

In: Konev, G

Suda, M.: Vampire with a brain is a good ITP hammer. In: Konev, G. Borisand Reger (ed.) Frontiers of Combining Systems. Lecture Notes in Com- puter Science, vol. 12941, pp. 192–209. Springer, Birmingham, UK (2021). https://doi.org/10.1007/978-3-030-86205-3 11

2021 doi
[214]

In: 5th Conference on Artificial Intelligence and Theorem Proving

Brown, C.E., Gauthier, T.: Self-learned formula synthesis in set theory. In: 5th Conference on Artificial Intelligence and Theorem Proving. AITP Conference, Aussois, France (2020). https://aitp-conference.org/2020/abstract/paper 1.pdf

2020
[215]

In: 5th Conference on Artificial Intelli- gence and Theorem Proving

Wu, M., Norrish, M., Walder, C., Dezfouli, A.: Reinforcement learning for interactive theorem proving in HOL4. In: 5th Conference on Artificial Intelli- gence and Theorem Proving. AITP Conference, Aussois, France (2020). https: //aitp-conference.org/2020/abstract/paper 7.pdf

2020
[216]

In: 2019 Interna- tional Symposium on Theoretical Aspects of Software Engineering (TASE), pp

Zhang, X., Li, Y., Hong, W., Sun, M.: Using recurrent neural network to predict 59 tactics for proving component connector properties in Coq. In: 2019 Interna- tional Symposium on Theoretical Aspects of Software Engineering (TASE), pp. 107–112. IEEE, Guilin, China (2019). http...

2019 doi
[217]

In: Hojjat, H., Massink, M

Nawaz, M.S., Sun, M., Fournier-Viger, P.: Proof guidance in PVS with sequen- tial pattern mining. In: Hojjat, H., Massink, M. (eds.) International Conference on Fundamentals of Software Engineering. Lecture Notes in Computer Science, vol. 11761, pp. 45–60. Springer, Tehran, Ir...

2019
[218]

In: Peltier, N., Sofronie-Stokkermans, V

Nie, P., Palmskog, K., Li, J.J., Gligoric, M.: Deep generation of Coq lemma names using elaborated terms. In: Peltier, N., Sofronie-Stokkermans, V. (eds.) International Joint Conference on Automated Reasoning. Lecture Notes in Com- puter Science, vol. 12167, pp. 97–118. Spring...

2020 doi
[219]

Annals of Mathematics and Artifi- cial Intelligence 85, 119–146 (2019) https://doi.org/10.1007/s10472-018-9598-6

Nikoli´ c, M., Marinkovi´ c, V., Kov´ acs, Z., Janiˇ ci´ c, P.: Portfolio theorem proving and prover runtime prediction for geometry. Annals of Mathematics and Artifi- cial Intelligence 85, 119–146 (2019) https://doi.org/10.1007/s10472-018-9598-6

2019 doi
[220]

In: Kamareddine, F., Sacerdoti Coen, C

Zhang, L., Blaauwbroek, L., Piotrowski, B., ˇCern` y, P., Kaliszyk, C., Urban, J.: Online machine learning techniques for Coq: A comparison. In: Kamareddine, F., Sacerdoti Coen, C. (eds.) Intelligent Computer Mathematics. Lecture Notes in Computer Science, vol. 12833, pp. 67–8...

2021 doi
[221]

In: Monica, D.D., Pozzato, G.L., Scala, E

Dunkelau, J., Baldus, L.: Ranking model checking backends for automated selec- tion via classification and regression learning. In: Monica, D.D., Pozzato, G.L., Scala, E. (eds.) OVERLAY’21: Workshop on Artificial Intelligence and fOrmal VERification, Logic, Automata, and sYnth...

2021
[222]

In: Dong, W., Talpin, J.-P

Gross, D., Jansen, N., Junges, S., P´ erez, G.A.: COOL-MC: A comprehensive tool for reinforcement learning and model checking. In: Dong, W., Talpin, J.-P. (eds.) International Symposium on Dependable Software Engineering: Theories, Tools, and Applications. Lecture Notes in Com...

2022 doi
[223]

In: Memmi, G., Yang, B., Kong, L., Zhang, T., Qiu, M

Cao, W., Wu, Y., Wang, Q., Zhang, J., Zhang, X., Qiu, M.: A novel R VFL- based algorithm selection approach for software model checking. In: Memmi, G., Yang, B., Kong, L., Zhang, T., Qiu, M. (eds.) Knowledge Science, Engineering and Management. Lecture Notes in Computer Scienc...

2022 doi
[224]

In: Deshmukh, J., Niˇ ckovi´ c, D

Jaeger, M., Larsen, K.G., Tibo, A.: From statistical model checking to run-time monitoring using a bayesian network approach. In: Deshmukh, J., Niˇ ckovi´ c, D. 60 (eds.) Runtime Verification. Lecture Notes in Computer Science, vol. 12399, pp. 517–535. Springer, Los Angeles, C...

2020
[225]

Swarm and Evolutionary Computation 44, 511–521 (2019) https://doi

Kumazawa, T., Takada, K., Takimoto, M., Kambayashi, Y.: Ant colony opti- mization based model checking extended by smell-like pheromone with hop counts. Swarm and Evolutionary Computation 44, 511–521 (2019) https://doi. org/10.1016/j.swevo.2018.06.002

2019 doi
[226]

In: 2023 ACM/IEEE 5th Work- shop on Machine Learning for CAD (MLCAD)

Hu, G., Zhang, W., Zhang, H.: NeuroPDR: Integrating neural networks in the PDR algorithm for hardware model checking. In: 2023 ACM/IEEE 5th Work- shop on Machine Learning for CAD (MLCAD). MLCAD, pp. 1–6. IEEE, Snow- bird, UT, USA (2023). https://doi.org/10.1109/MLCAD58807.2023...

2023
[227]

In: Mathieu, P., Dignum, F., Novais, P., Prieta, F

Kumazawa, T., Takimoto, M., Kodama, Y., Kambayashi, Y.: Enhancing safety checking coverage with multi-swarm particle swarm optimization. In: Mathieu, P., Dignum, F., Novais, P., Prieta, F. (eds.) Advances in Practical Applications of Agents, Multi-Agent Systems, and Cognitive ...

2023 doi
[228]

In: Proceedings of the 37th IEEE/ACM International Conference on Automated Software Engineering

Luo, W., Wan, H., Zhang, D., Du, J., Su, H.: Checking LTL satisfiability via end-to-end learning. In: Proceedings of the 37th IEEE/ACM International Conference on Automated Software Engineering. ASE ’22. Association for Computing Machinery, Rochester, MI, USA (2023). https://d...

2023
[229]

In: Nguyen, N.T., Iliadis, L., Maglogiannis, I., Trawi´ nski, B

Kumazawa, T., Takimoto, M., Kambayashi, Y.: Exploration strategies for model checking with ant colony OptimizationQD. In: Nguyen, N.T., Iliadis, L., Maglogiannis, I., Trawi´ nski, B. (eds.) Computational Collective Intelli- gence, pp. 264–276. Springer, Rhodes, Greece (2021). ...

2021
[230]

Software Quality Journal 30(1), 37–64 (2022) https://doi.org/10.1007/s11219-020-09542-x

Pira, E.: Using knowledge discovery to propose a two-phase model checking for safety analysis of graph transformations. Software Quality Journal 30(1), 37–64 (2022) https://doi.org/10.1007/s11219-020-09542-x

2022 doi
[231]

Soft Computing 23, 4531–4556 (2019) https://doi.org/10.1007/ s00500-018-3444-y

Rafe, V., Darghayedi, M., Pira, E.: MS-ACO: a multi-stage ant colony opti- mization to refute complex software systems specified through graph trans- formation. Soft Computing 23, 4531–4556 (2019) https://doi.org/10.1007/ s00500-018-3444-y

2019
[232]

In: Song, Y., Acharya, S., Nguyen, N

Ma, Y., Cao, Z., Liu, Y.: Genetic algorithm-based assume-guarantee reason- ing for stochastic model checking. In: Song, Y., Acharya, S., Nguyen, N. (eds.) IEEE/ACIS 17th International Conference on Software Engineering Research, Mangement and Applications (SERA). SERA, pp. 124...

2019
[233]

In: 2020 59th IEEE Conference on Decision and Control (CDC), pp

Wang, Y., Roohi, N., West, M., Viswanathan, M., Dullerud, G.E.: Statistically model checking PCTL specifications on markov decision processes via rein- forcement learning. In: 2020 59th IEEE Conference on Decision and Control (CDC), pp. 1392–1397. IEEE, Jeju, South Korea (2020...

2020
[234]

In: Cao, J., Vong, C.M., Miche, Y., Lendasse, A

Wang, Q., Cao, W., Jiang, J., Zhao, Y., Ming, Z.: NNR W-based algorithm selection for software model checking. In: Cao, J., Vong, C.M., Miche, Y., Lendasse, A. (eds.) Proceedings of ELM2019. Proceedings in Adaptation, Learn- ing and Optimization, vol. 14, pp. 11–21. Springer, ...

2021 doi
[235]

Journal of Information and Telecommunication 6(3), 341–359 (2022) https://doi.org/10.1080/24751839.2022.2047470 61

Tsutomu Kumazawa, M.T., Kambayashi, Y.: Exploration strategies for bal- ancing efficiency and comprehensibility in model checking with ant colony optimization. Journal of Information and Telecommunication 6(3), 341–359 (2022) https://doi.org/10.1080/24751839.2022.2047470 61

2022
[236]

In: 2022 Interna- tional Conference on Artificial Intelligence and Computer Information Technol- ogy (AICIT)

Zhu, W.: Approximate model checking based on deep forest. In: 2022 Interna- tional Conference on Artificial Intelligence and Computer Information Technol- ogy (AICIT). AICIT, pp. 1–4. IEEE, Yichang, China (2022). https://doi.org/ 10.1109/AICIT55386.2022.9930208

2022
[237]

International Arab Journal of Information Technology 19(2), 249–260 (2022) https://doi.org/10.34028/iajit/19/2/12

Zhu, W., Wu, H.: CTL model checking based on binary classification of machine learning. International Arab Journal of Information Technology 19(2), 249–260 (2022) https://doi.org/10.34028/iajit/19/2/12

2022 doi
[238]

IEEE Access 7, 135703–135719 (2019) https://doi.org/10

Zhu, W., Wu, H., Deng, M.: LTL model checking based on binary classification of machine learning. IEEE Access 7, 135703–135719 (2019) https://doi.org/10. 1109/ACCESS.2019.2942762

2019
[240]

In: Proceed- ings of the 37th IEEE/ACM International Conference on Automated Software Engineering

Wang, J., Wang, C.: Learning to synthesize relational invariants. In: Proceed- ings of the 37th IEEE/ACM International Conference on Automated Software Engineering. ASE ’22. Association for Computing Machinery, Rochester, MI, USA (2023). https://doi.org/10.1145/3551349.3556942

2023
[241]

In: Dr˘ agoi, C., Mukherjee, S., Namjoshi, K

Kobayashi, N., Sekiyama, T., Sato, I., Unno, H.: Toward neural-network-guided program synthesis and verification. In: Dr˘ agoi, C., Mukherjee, S., Namjoshi, K. (eds.) Static Analysis. Lecture Notes in Computer Science, vol. 12931, pp. 236–260. Springer, Chicago, IL, USA (2021)...

2021
[242]

In: Proceedings of the 44th International Conference on Software Engineering

Xu, R., Chen, J., He, F.: Data-driven loop bound learning for termination analysis. In: Proceedings of the 44th International Conference on Software Engineering. ICSE ’22, pp. 499–510. Association for Computing Machinery, Pittsburgh, PA, USA (2022). https://doi.org/10.1145/351...

2022
[243]

In: Donaldson, A.F., Torlak, E

Yao, J., Ryan, G., Wong, J., Jana, S., Gu, R.: Learning nonlinear loop invari- ants with gated continuous logic networks. In: Donaldson, A.F., Torlak, E. (eds.) Proceedings of the 41st ACM SIGPLAN Conference on Programming Language Design and Implementation. PLDI 2020, pp. 106...

2020 doi
[244]

In: 6th Conference on Artificial Intelligence and Theorem Proving

Laurent, J., Platzer, A.: Designing a theorem prover for reinforcement learn- ing and neural guidance. In: 6th Conference on Artificial Intelligence and Theorem Proving. AITP Conference, Aussois and online, France (2021). https: //aitp-conference.org/2021/abstract/paper 8.pdf 62

2021
[245]

Automated Software Engineering 26(3), 653–704 (2019) https://doi.org/10.1007/s10515-019-00264-4

Cai, C.-H., Sun, J., Dobbie, G.: Automatic B-model repair using model checking and machine learning. Automated Software Engineering 26(3), 653–704 (2019) https://doi.org/10.1007/s10515-019-00264-4

2019 doi
[246]

In: 2019 26th Asia-Pacific Software Engineering Conference (APSEC), Putrajaya, Malaysia, pp

Cai, C.-H., Sun, J., Dobbie, G., Lee, S.U.-J.: Achieving abstract machine reach- ability with learning-based model fulfilment. In: 2019 26th Asia-Pacific Software Engineering Conference (APSEC), Putrajaya, Malaysia, pp. 260–267 (2019). https://doi.org/10.1109/APSEC48747.2019.00043

2019
[247]

In: Just, R., Fraser, G

Yu, S., Wang, T., Wang, J.: Loop invariant inference through SMT solving enhanced reinforcement learning. In: Just, R., Fraser, G. (eds.) Proceedings of the 32nd ACM SIGSOFT International Symposium on Software Testing and Analysis. ISSTA 2023, pp. 175–187. Association for Comp...

2023
[248]

In: Koyejo, S., Mohamed, S., Agarwal, A., Belgrave, D., Cho, K., Oh, A

Abate, A., Edwards, A., Giacobbe, M.: Neural abstractions. In: Koyejo, S., Mohamed, S., Agarwal, A., Belgrave, D., Cho, K., Oh, A. (eds.) Advances in Neural Information Processing Systems 35 (NeurIPS 2022), vol. 35, pp. 26432–26447. Curran Associates, Inc., New Orleans, LA, US...

2022
[249]

In: 7th Conference on Artificial Intelligence and Theorem Proving

Bordg, A., Stathopoulos, Y.A., Paulson, L.C.: A parallel corpus of natural language and isabelle artefacts. In: 7th Conference on Artificial Intelligence and Theorem Proving. AITP Conference, Aussois and online, France (2022). https://aitp-conference.org/2022/abstract/AITP 202...

2022
[250]

Science of Computer Programming 214, 102732 (2022) https://doi.org/10.1016/j.scico.2021.102732

Cai, C.-H., Sun, J., Dobbie, G.: B model quality assessments on automated reachability repair with ISO/IEC 25010. Science of Computer Programming 214, 102732 (2022) https://doi.org/10.1016/j.scico.2021.102732

2022
[251]

In: Proceedings of the 44th Interna- tional Conference on Software Engineering

He, J., Bartocci, E., Niˇ ckovi´ c, D., Isakovic, H., Grosu, R.: DeepSTL: From english requirements to signal temporal logic. In: Proceedings of the 44th Interna- tional Conference on Software Engineering. ICSE ’22, pp. 610–622. Association for Computing Machinery, Pittsburgh,...

2022
[252]

IEEE Transactions on Computers 75(5), 1431–1446 (2022) https://doi.org/10

Hu, M., Zhang, M., Mallet, F., Fu, X., Chen, M.: Accelerating reinforcement learning-based CCSL specification synthesis using curiosity-driven exploration. IEEE Transactions on Computers 75(5), 1431–1446 (2022) https://doi.org/10. 1109/TC.2022.3197956

2022
[253]

In: Gervasi, V., Vogelsang, A

Cherukuri, H., Ferrari, A., Spoletini, P.: Towards explainable formal methods: From LTL to natural language with neural machine translation. In: Gervasi, V., Vogelsang, A. (eds.) International Working Conference on Requirements Engi- neering: Foundation for Software Quality. L...

2022
[254]

In: Gervasi, A

Nayak, A., Timmapathini, H.P., Murali, V., Ponnalagu, K., Venkoparao, V.G., Post, A.: Req2Spec: Transforming software requirements into formal specifica- tions using natural language processing. In: Gervasi, A. Vincenzoand Vogelsang (ed.) Requirements Engineering: Foundation f...

2022 doi
[255]

In: IEEE Global Conference on Consumer Electronics (GCCE), pp

Shigyo, Y., Katayama, T.: Proposal of an approach to generate VDM++ spec- ifications from natural language specification by machine learning. In: IEEE Global Conference on Consumer Electronics (GCCE), pp. 292–296. IEEE, Kobe, Japan (2020). https://doi.org/10.1109/GCCE50665.202...

2020
[256]

In: Yue, T., Mirakhorli, M

Koscinski, V., Gambardella, C., Gerstner, E., Zappavigna, M., Cassetti, J., Mirakhorli, M.: A natural language processing technique for formalization of sys- tems requirement specifications. In: Yue, T., Mirakhorli, M. (eds.) 2021 IEEE 29th International Requirements Engineeri...

2021
[257]

In: Proceedings of the 35th IEEE/ACM International Conference on Automated Software Engineering

Richter, C., Wehrheim, H.: Attend and represent: a novel view on algorithm selection for software verification. In: Proceedings of the 35th IEEE/ACM International Conference on Automated Software Engineering. Association for Computing Machinery, Virtual Event (2020). https://d...

2020 doi
[258]

Wang, Q., Jiang, J., Zhao, Y., Cao, W., Wang, C., Li, S.: Algorithm selection for 64 software verification based on adversarial LSTM. In: 2021 7th IEEE Intl Confer- ence on Big Data Security on Cloud (BigDataSecurity), IEEE Intl Conference on High Performance and Smart Computi...

2021
[259]

In: Cok, D.R

Puccetti, A., De Chalendar, G., Gibello, P.-Y.: Combining formal and machine learning techniques for the generation of JML specifications. In: Cok, D.R. (ed.) FTfJP ’21: Proceedings of the 23rd ACM International Workshop on Formal Techniques for Java-like Programs. FTfJP, pp. ...

2021
[260]

(eds.) Graph Neural Net- works in Program Analysis, pp

Allamanis, M.: In: Wu, L., Cui, P., Pei, J., Zhao, L. (eds.) Graph Neural Net- works in Program Analysis, pp. 483–497. Springer, Singapore (2022). https: //doi.org/10.1007/978-981-16-6054-2 22

2022 doi
[261]

Proceedings of the ACM on Programming Languages 3(OOPSLA), 1–30 (2019) https://doi.org/10.1145/3360567

Chen, J., Wei, J., Feng, Y., Bastani, O., Dillig, I.: Relational verification using reinforcement learning. Proceedings of the ACM on Programming Languages 3(OOPSLA), 1–30 (2019) https://doi.org/10.1145/3360567

2019 doi
[262]

In: Roy- choudhury, A., Cadar, C., Kim, M

Giacobbe, M., Kroening, D., Parsert, J.: Neural termination analysis. In: Roy- choudhury, A., Cadar, C., Kim, M. (eds.) Proceedings of the 30th ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering. ESEC/FSE 2022, pp. 633–6...

2022 doi
[263]

In: Raedt, L.D

Luo, W., Wan, H., Du, J., Li, X., Fu, Y., Ye, R., Zhang, D.: Teaching LTLf satisfiability checking to neural networks. In: Raedt, L.D. (ed.) Proceedings of the Thirty-First International Joint Conference on Artificial Intelligence (IJCAI- 22), pp. 3292–3298. International Join...

2022 doi
[264]

Journal on Artificial Intelligence 2(4), 177–187 (2020) https://doi.org/10.32604/ jai.2020.014829

Cao, W., Xie, Z., Zhou, X., Xu, Z., Zhou, C., Theodoropoulos, G., Wang, Q.: A learning framework for intelligent selection of software verification algorithms. Journal on Artificial Intelligence 2(4), 177–187 (2020) https://doi.org/10.32604/ jai.2020.014829

2020
[265]

In: Fieldsend, J.E

Kumazawa, T., Takimoto, M., Kambayashi, Y.: A safety checking algorithm with multi-swarm particle swarm optimization. In: Fieldsend, J.E. (ed.) Pro- ceedings of the Genetic and Evolutionary Computation Conference Companion. GECCO ’22, pp. 786–789. Association for Computing Mac...

2022
[266]

In: Benzm¨ uller, C., Miller, B

Nagashima, Y.: Simple dataset for proof method recommendation in Isabelle/HOL. In: Benzm¨ uller, C., Miller, B. (eds.) Intelligent Computer Math- ematics. Lecture Notes in Computer Science, vol. 12236, pp. 297–302. Springer, 65 Bertinoro, Italy (2020). https://doi.org/10.1007/...

2020 doi
[267]

In: Naumowicz, A., Thiemann, R

Reichel, T., Henderson, R.W., Touchet, A., Gardner, A., Ringer, T.: Proof repair infrastructure for supervised models: Building a large proof repair dataset. In: Naumowicz, A., Thiemann, R. (eds.) 14th International Conference on Interactive Theorem Proving (ITP 2023). Leibniz...

2023 doi
[268]

In: Lahiri, S.K., Wang, C

Si, X., Naik, A., Dai, H., Naik, M., Song, L.: Code2Inv: A deep learning frame- work for program verification. In: Lahiri, S.K., Wang, C. (eds.) International Conference on Computer Aided Verification. Lecture Notes in Computer Sci- ence, vol. 12225, pp. 151–164. Springer, Los...

2020 doi
[336]

https://ebooks.iospress.nl/volume/ handbook-of-satisfiability-second-edition

IOS press, Amsterdam (2015). https://ebooks.iospress.nl/volume/ handbook-of-satisfiability-second-edition

2015
[463]

https://proceedings.mlr.press/v97/ bansal19a.html

PMLR, Long Beach, CA, USA (2019). https://proceedings.mlr.press/v97/ bansal19a.html

2019

Pith tools

Reviewed August 12, 2026 · model on record in the stance chip above.

[1] [1]

Journal of Management Analytics 6, 1–29 (2019) https://doi.org/ 10.1080/23270012.2019.1570365

Lu, Y.: Artificial intelligence: a survey on evolution, models, applications and future trends. Journal of Management Analytics 6, 1–29 (2019) https://doi.org/ 10.1080/23270012.2019.1570365

arXiv 2019

[2] [2]

Discover Artificial Intelligence 3 (2023) https://doi.org/10.1007/s44163-023-00089-x

Elahi, M., Afolaranmi, S.O., Martinez Lastra, J.L., Perez Garcia, J.A.: A comprehensive literature review of the applications of AI techniques through the lifecycle of industrial equipment. Discover Artificial Intelligence 3 (2023) https://doi.org/10.1007/s44163-023-00089-x

work page doi:10.1007/s44163-023-00089-x 2023

[3] [3]

Annals of Translational Medicine 11(5) (2023) https:// doi.org/10.21037/atm-22-3773

Jiang, X., Xie, M., Ma, L., Dong, L., Li, D.: International publication trends in the application of artificial intelligence in ophthalmology research: an updated bibliometric analysis. Annals of Translational Medicine 11(5) (2023) https:// doi.org/10.21037/atm-22-3773

work page doi:10.21037/atm-22-3773 2023

[4] [4]

Mathematics 11(11) (2023) https://doi.org/10.3390/ math11112420

Chang, K.-H.: Artificial intelligence and information processing: A system- atic literature review. Mathematics 11(11) (2023) https://doi.org/10.3390/ math11112420

2023

[5] [5]

AI Perspectives 2 (2020) https://doi.org/10.1186/ s42467-020-00005-4

Barenkamp, M., Rebstadt, J., Thomas, O.: Applications of AI in classi- cal software engineering. AI Perspectives 2 (2020) https://doi.org/10.1186/ s42467-020-00005-4

2020

[6] [6]

IEEE Access 9, 140896–140920 (2021) https://doi.org/10.1109/ACCESS.2021.3119746

Shafiq, S., Mashkoor, A., Mayr-Dorn, C., Egyed, A.: A literature review of using machine learning in software development life cycle stages. IEEE Access 9, 140896–140920 (2021) https://doi.org/10.1109/ACCESS.2021.3119746

arXiv 2021

[7] [7]

(eds.): Software Engi- neering Body of Knowledge vol

Abran, A., Moore, J.W., Bourque, P., Dupuis, R. (eds.): Software Engi- neering Body of Knowledge vol. 25. IEEE Computer Society, Los Alamitos, CA, USA (2004). https://www.computer.org/education/bodies-of-knowledge/ software-engineering

2004

[8] [8]

Information and Software Technology 64, 1–18 (2015) https://doi.org/10.1016/j.infsof.2015.03.007

Petersen, K., Vakkalanka, S., Kuzniarz, L.: Guidelines for conducting systematic mapping studies in software engineering: An update. Information and Software Technology 64, 1–18 (2015) https://doi.org/10.1016/j.infsof.2015.03.007

doi:10.1016/j.infsof.2015.03.007 2015