RISC JKU

Machine Learning Literature

With focus on the relationship of machine learning to symbolic computation, computer algebra, automated reasoning, automatic programming, etc.

Tree Search, Game Playing, Reinforcement Learning, Pattern Analysis

  1. Browne, Cameron et al. (2012): A Survey of Monte Carlo Tree Search Methods
  2. Kishimoto, Akihiro et al. (2019): Depth-First Proof-Number Search with Heuristic Edge Cost and Application to Chemical Synthesis Planning
  3. Kipf, Thomas N. et al. (2017): Semi-Supervised Classification with Graph Convolutional Networks
  4. Mnih, Volodymyr et al. (2013): Playing Atari with Deep Reinforcement Learning
  5. Scarselli, Franco et al. (2009): The Graph Neural Network Model
  6. Schadd, Maarten P.D. et al. (2011): Single-Player Monte-Carlo Tree Search for SameGame
  7. Shawe-Taylor, John et al. (2016): Kernel Methods for Pattern Analysis
  8. Silver, David et al. (2016): Mastering the game of Go with deep neural networks and tree search
  9. Silver, David et al. (2017): Mastering the game of Go without human knowledge
  10. Sutton, Richard S. (2018): Reinforcement Learning - An Introduction
  11. Tai, Kai Sheng et al. (2015): Improved Semantic Representations From Tree-Structured Long Short-Term Memory Networks
  12. Wang, Minjie et al. (2019): Deep Graph Library: A Graph-Centric, Highly-Performant Package for Graph Neural Networks

Symbolic Computation and Machine Learning, Neuro-Symbolic AI

  1. Buchberger, Bruno (2023): Automated programming, symbolic computation, machine learning: my personal view
  2. Marra, Guiseppe et al. (2024): From statistical relational to neurosymbolic artificial intelligence: A survey
  3. Saker, Md Kamruzzaman et al. (2018): Neuro-Symbolic Artificial Intelligence - Current Trends
  4. Segler, Marwin H. S. et al. (2018): Planning chemical syntheses with deep neural networks and symbolic AI
  5. Wolfram, Stephen (2023): Wolfram|Alpha as the Way to Bring Computational Knowledge Superpowers to ChatGPT

Symbolic Object Representations

  1. Allamanis, Miltiadis et al. (2017): Learning Continuous Semantic Representations of Symbolic Expressions
  2. Chvalovský, Karel (2019): Top-Down Neural Model For Formulae
  3. Crouse, Maxwell et al. (2019): Improving Graph Neural Network Representations of Logical Formulae with Subgraph Pooling
  4. Dumancic, Sebastijan et al. (2019): Learning Relational Representations with Auto-encoding Logic Programs
  5. Goller, Christoph et al. (1996): Learning Task-Dependent Distributed Representations by Backpropagation Through Structure
  6. Kaliszyk, Cezary et al. (2015): Efficient Semantic Features for Automated Reasoning over Large Theories
  7. Mikolov, Tomas et al. (2013): Distributed Representations of Words and Phrases and their Compositionality
  8. Müller, Dennis et al. (2021): Disambiguating Symbolic Expressions in Informal Documents
  9. Olšák, Miroslav et al. (2019): Property Invariant Embedding for Automated Reasoning
  10. Paliwal, Marc et al. (2020): Graph Representations for Higher-Order Logic and Theorem Proving
  11. Parsert, Julian et al. (2020): Property Preserving Encoding of First-order Logic
  12. Purgal, Stanislaw et al. (2021): A Study of Continuous Vector Representations for Theorem Proving
  13. Rocktäschel, Tim et al. (2017): End-to-End Differentiable Proving
  14. Wang, Mingzhe et al. (2017): Premise Selection for Theorem Proving by Deep Graph Embedding
  15. Wang, Qingxian et al. (2021): JEFL: Joint Embedding of Formal Proof Libraries

Computer Mathematics/Algebra/Geometry

  1. Barket, Rashid et al. (2023): Generating Elementary Integrable Expressions
  2. Barket, Rashid et al. (2024): Symbolic Integration Algorithm Selection with Machine Learning: LSTMs vs Tree LSTMs
  3. Huang, Zongyan et al. (2024): Applying Machine Learning to the Problem of Choosing a Heuristic to Select the Variable Ordering for Cylindrical Algebraic Decomposition
  4. Jia, Fuqi et al. (2024): Suggesting Variable Order for Cylindrical Algebraic Decomposition via Reinforcement Learning
  5. Lample, Guillame et al. (2019): Deep Learning for Symbolic Mathematics
  6. Lenat, Doublas B. (1976): AM: An Artificial Intelligence Approach to Discovery in Mathematics as Heuristic Search
  7. Pickering, L. et al. (2024): Explainable AI Insights for Symbolic Computation: A case study on selecting the variable ordering for cylindrical algebraic decomposition
  8. Simpson, M.C. et al. (2016): Automatic Algorithm Selection in Computational Software Using Machine Learning
  9. Trinh, Trieu et al. (2024): Solving olympiad geometry without human demonstrations

Automatic Formalization

  1. Kaliszyk, Cezary et al. (2014): Developing Corpus-Based Translation Methods between Informal and Formal Mathematics: Project Description
  2. Kaliszyk, Cezary et al. (2017): Automating Formalization by Statistical and Semantic Parsing of Mathematics
  3. Wang, Qingxian et al. (2018): First Experiments with Neural Translation of Informal to Formal Mathematics
  4. Wang, Qingxian et al. (2020): Exploration of Neural Machine Translation in Autoformalization of Mathematics in Mizar
  5. Youssef, Abdou et al. (2018): Deep Learning for Math Knowledge Processing

Program Synthesis, Rule Learning, Logic Programming

  1. Evans, Richard et al. (2019): Learning Explanatory Rules from Noisy Data
  2. Fierens, Daan et al. (2013): Inference and Learning in Probabilistic Logic Programs using Weighted Boolean Formulas
  3. Gauthier, Thibault (2020): Deep Reinforcement Learning for Synthesizing Functions in Higher-Order Logic
  4. Gauthier, Thibault et al. (2023): Alien Coding
  5. Glanois, Claire et al. (2021): Neuro-Symbolic Hierarchical Rule Induction
  6. Landwehr, Niels et al. (2006): kFOIL: Learning Simple Relational Kernels
  7. Landwehr, Niels et al. (2007): Integrating Naıve Bayes and FOIL
  8. Langley, Patrick W. (1977): BACON: A Production System That Discovers Empirical Laws
  9. Manhaeve, Robin et al. (2018): DeepProbLog: Neural Probabilistic Logic Programming
  10. Manhaeve, Robin et al. (2019): Neural Probabilistic Logic Programming in DeepProbLog
  11. Manhaeve, Robin et al. (2021): Neuro-Symbolic AI = Neural + Logical + Probabilistic AI
  12. Purgal, Stanislaw J. et al. (2023): Learning Higher-Order Logic Programs From Failures
  13. Purgal, Stanislaw J. et al. (2023): Differentiable Inductive Logic Programming in High-Dimensional Space
  14. Quinlinian, J.R. (1990): Learning Logical Definitions from Relations

Knowledge Graphs

  1. Amayuelas, Alfonso et al. (2011): Neural Methods for Logical Reasoning over Knowledge Graphs
  2. Shi, Ming et al. (2024): Convolutional Neural Network Knowledge Graph Link Prediction Model Based on Relational Memory
  3. Trouillon, Théo et al. (2016): Complex Embeddings for Simple Link Prediction

SAT and SMT Solving

  1. Balunović, Mislav et al. (2018): Learning to Solve SMT Formulas
  2. Chang, Oscar (2023): Assessing SATNet’s Ability to Solve the Symbol Grounding Problem
  3. El Ouraoui, Daniel et al. (2019): Machine Learning for Instance Selection in SMT Solving
  4. Holden, Sean B. (2021): Machine Learning for Automated Theorem Proving: Learning to Solve SAT and QSAT
  5. Jakubuv, Jan et al. (2023): Selecting Quantifiers for Instantiation in SMT
  6. Piepenbrock, Jelle et al. (2022): Machine Learning Meets The Herbrand Universe
  7. Piepenbrock, Jelle et al. (2024): First Experiments with Neural cvc5
  8. Pimpalkhare, Nikhil et al. (2021): MedleySolver: Online SMT Algorithm Selection
  9. Scott, Joseph et al. (2021): MachSMT: A Machine Learning-based Algorithm Selector for SMT Solvers
  10. Selsam, Daniel et al. (2019): Learning a SAT Solver from Single-Bit Supervision
  11. Topan, Sever et al. (2021): Techniques for Symbol Grounding with SATNet
  12. Wang, Po-Wei et al. (2019): SATNet: Bridging deep learning and logical reasoning using a differentiable satisfiability solver

First-/Higher-Order Logic

Surveys:
  1. Abdelaziz, Ibrahim et al. (2021): Learning to Guide a Saturation-Based Theorem Prover
  2. Alama, Jesse et al. (2022): Premise Selection for Mathematics by Corpus Analysis and Kernel Methods
  3. Alemi, Alexander A. et al. (2016): DeepMath - Deep Sequence Models for Premise Selection
  4. Aygün, Eser et al. (2021): Proving Theorems using Incremental Learning and Hindsight Experience Replay
  5. Bansal, Kshitij et al. (2019): HOList: An Environment for Machine Learning of Higher-Order Theorem Proving
  6. Bártek, Filip et al. (2021): Neural Precedence Recommender
  7. Bártek, Filip et al. (2023): How Much Should This Symbol Weigh? A GNN-Advised Clause Selection
  8. Blanchette, Jasmin C. et al. (2015): Hammering towards QED
  9. Blanchette, Jasmin C. et al. (2016): A Learning-Based Fact Selector for Isabelle/HOL
  10. Blauuwbroek, Lasse et al. (2020): The Tactician - A Seamless, Interactive Tactic Learner and Prover for Coq
  11. Bridge, James P. (2010): Machine learning and automated theorem proving
  12. Chvalovský, Karel et al. (2019): ENIGMA-NG: Efficient Neural and Gradient-Boosted Inference Guidance for E
  13. Chvalovský, Karel et al. (2021): Learning Theorem Proving Components
  14. Chvalovský, Karel et al. (2023): Guiding an Instantiation Prover with Graph Neural Networks
  15. Crouse, Maxwell et al. (2021): A Deep Reinforcement Learning Approach to First-Order Logic Theorem Proving
  16. Evans, Richard et al. (2018): Can Neural Networks Understand Logical Entailment?
  17. Färber, Michael et al. (2011): Internal Guidance for Satallax
  18. Färber, Michael et al. (2015): Random Forests for Premise Selection
  19. Färber, Michael et al. (2019): Monte Carlo Tableau Proof Search
  20. Färber, Michael et al. (2021): Machine Learning Guidance for Connection Tableaux
  21. First, Emily et al. (2020): TacTok: Semantics-Aware Proof Synthesis
  22. First, Emily et al. (2022): Diversity-Driven Automated Formal Verification
  23. Fuchs, Matthias (1998): A Feature-based Learning Method for Theorem Proving
  24. Gauthier, Thibault et al. (2015): Premise Selection and External Provers for HOL4
  25. Gauthier, Thibault et al. (2016): Initial Experiments with Statistical Conjecturing over Large Formal Corpora
  26. Gauthier, Thibault et al. (2021): TacticToe: Learning to Prove with Tactics
  27. Goertzel; Zarathustra et al. (2019): ENIGMAWatch: ProofWatch Meets ENIGMA
  28. Goertzel; Zarathustra et al. (2021): Fast and Slow Enigmas and Parental Guidance
  29. Goller, Christoph et al. (1999): Learning Search-Control Heuristics for Automated Deduction Systems with Folding Architecture Networks
  30. Grandsen, Thomas et al. (2015): SEPIA: Search for Proofs Using Inferred Automata
  31. Holden, Edvard K. et al. (2021): Heterogeneous Heuristic Optimisation and Scheduling for First-Order Theorem Proving
  32. Holden, Edvard K. et al. (2023): Graph Sequence Learning for Premise Selection
  33. Huang, Daniel et al. (2018): GamePad: A Learning Environment for Theorem Proving
  34. Jakubuv, Jan et al. (2016): BliStrTune: Hierarchical Invention of Theorem Proving Strategies
  35. Jakubuv, Jan et al. (2017): ENIGMA: Efficient Learning-based Inference Guiding Machine
  36. Jakubuv, Jan et al. (2018): Enhancing ENIGMA Given Clause Guidance
  37. Jakubuv, Jan et al. (2019): ENIGMA Anonymous: Symbol-Independent Inference Guiding Machine (System Description)
  38. Jakubuv, Jan et al. (2019): Hammering Mizar by Learning Clause Guidance
  39. Jiang, Albert Q. et al. (2022): Thor: Wielding Hammers to Integrate Language Models and Automated Theorem Provers
  40. Jiang, Albert Q. et al. (2023): Draft, Sketch, and Prove: Guiding Formal Theorem Provers with Informal Proofs
  41. Johansson, Moa et al. (2023): Exploring Mathematical Conjecturing with Large Language Models
  42. Kaliszyk, Cezary et al. (2013): Stronger Automation for Flyspeck by Feature Weighting and Strategy Evolution
  43. Kaliszyk, Cezary et al. (2014): Learning-Assisted Automated Reasoning with Flyspeck
  44. Kaliszyk, Cezary et al. (2014): Machine Learner for Automated Reasoning 0.4 and 0.5
  45. Kaliszyk, Cezary et al. (2015): Learning-assisted theorem proving with millions of lemmas
  46. Kaliszyk, Cezary et al. (2015): FEMaLeCoP: Fairly Efficient Machine Learning Connection Prover
  47. Kaliszyk, Cezary et al. (2015): System description: E.T. 0.1
  48. Kaliszyk, Cezary et al. (2017): HolStep: A Machine Learning Dataset for Higher-order Logic Theorem Proving
  49. Kaliszyk, Cezary et al. (2018): Reinforcement Learning of Theorem Proving
  50. Komendantskay, Ekaterina et al. (2012): Machine learning in Proof General: Interfacing Interfaces
  51. Kühlwein, Daniel et al. (2012): Overview and Evaluation of Premise Selection Techniques for Large Theory Mathematics
  52. Kühlwein, Daniel et al. (2013): MaSh: Machine Learning for Sledgehammer
  53. Kühlwein, Daniel et al. (2015): MaLeS: A Framework for Automatic Tuning of Automated Theorem Provers
  54. Lample, Guillame et al. (2022): HyperTree Proof Search for Neural Theorem Proving
  55. Loos, Sarah et al. (2017): Deep Network Guided Proof Search
  56. Nagashima, Yutaka et al. (2018): PaMpeR: Proof Method Recommendation System for Isabelle/HOL
  57. Pierre, Marc et al. (2023): The Mathematical Game
  58. Pioetrowski, Bartosz et al. (2018): ATPboost: Learning Premise Selection in Binary Setting with ATP Feedback
  59. Pioetrowski, Bartosz et al. (2020): Stateful Premise Selection by Recurrent Neural Networks
  60. Pioetrowski, Bartosz et al. (2023): Machine-Learned Premise Selection for Lean
  61. Purgal, Stanislaw J. al (2022): Adversarial Learning to Reason in an Arbitrary Logic
  62. Rabe, Markus N. et al. (2020): Mathematical Reasoning via Self-supervised Skip-tree Training
  63. Rawson, Michael et al. (2019): A Neurally-Guided Parallel Theorem Prover
  64. Rawson, Michael et al. (2020): Directed Graph Networks for Logical Reasoning (Extended Abstract)
  65. Rawson, Michael et al. (2020): Directed Graph Networks for Logical Entailment
  66. Rawson, Michael et al. (2021): lazyCoP: Lazy Paramodulation Meets Neurally Guided Search
  67. Rute, Jason et al. (2023): Graph2Tac: Learning hierarchical representations of math concepts in theorem proving
  68. Rute, Jason et al. (2024): Graph2Tac: Online Representation Learning of Formal Math Concepts
  69. Sanchez-Stern, Alex et al. (2022): Passport: Improving Automated Formal Verification Using Identifiers
  70. Sanchez-Stern, Alex et al. (2024): Generating Correctness Proofs with Neural Networks
  71. Schäfer, Simon (2015): Breeding Theorem Proving Heuristics with Genetic Algorithms
  72. Schulz, Stephan (2000): Learning Search Control Knowledge for Equational Deduction
  73. Shankar, Natarajan (2013): Automated Reasoning, Fast and Slow
  74. Sharma, Rahul et al. (2011): Interpolants as Classifiers
  75. Steen, Alexander et al. (2016): Agent-Based HOL Reasoning
  76. Suda, Martin (2021): Improving ENIGMA-style Clause Selection while Learning From History
  77. Suda, Martin (2021): Vampire with a Brain Is a Good ITP Hammer
  78. Urban, Josef (1998): Experimenting with Machine Learning in Automatic Theorem Proving
  79. Urban, Josef et al. (2007): MaLARea: a Metasystem for Automated Reasoning in Large Theories
  80. Urban, Josef et al. (2008): MaLARea SG1 - Machine Learner for Automated Reasoning with Semantic Guidance
  81. Urban, Josef et al. (2011): MaLeCoP: Machine Learning Connection Prover
  82. Urban, Josef (2014): BliStr: The Blind Strategymaker
  83. Urban, Josef et al. (2020): First Neural Conjecturing Datasets and Experiments
  84. Wang, Mingzhe et al. (2020): Learning to Prove Theorems by Learning to Generate Theorems
  85. Whalen, Daniel (2016): Holophrasm: a neural Automated Theorem Prover for higher-order logic
  86. Yang, Kaiyu et al. (2019): Learning to Prove Theorems via Interacting with Proof Assistants
  87. Yang, Kaiyu et al. (2023): LeanDojo: Theorem Proving with Retrieval-Augmented Language Models
  88. Zhang, Liao et al. (2021): Online Machine Learning Techniques for Coq: A Comparison.
  89. Zhang, Liao et al. (2023): Learning Proof Transformations and Its Applications in Interactive Theorem Proving
  90. Ziener, Marco et al. (2017): Mixing automated theorem proving and machine learning - Bridging the gap between numerical and symbolic reasoning with a potpourri of computer science
  91. Zombori, Zsolt et al. (2019): Towards Finding Longer Proofs
  92. Zombori, Zsolt et al. (2021): The Role of Entropy in Guiding a Connection Prover