RISC JKU

Literature on Machine Learning & Symbolic Computation

With focus on the relationship between machine learning and symbolic computation, computer algebra, automated reasoning, automatic programming, etc.
  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. Hinkelmann, Knut et al. (2025): Hybride KI mit Machine Learning und Knowledge Graphs - Innovative Lösungen aus der Praxis
  3. Marra, Guiseppe et al. (2024): From statistical relational to neurosymbolic artificial intelligence: A survey
  4. Saker, Md Kamruzzaman et al. (2018): Neuro-Symbolic Artificial Intelligence - Current Trends
  5. Segler, Marwin H. S. et al. (2018): Planning chemical syntheses with deep neural networks and symbolic AI
  6. 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. Barket, Rashid et al. (2024): Transformers to Predict the Applicability of Symbolic Integration Routines
  4. Huang, Zongyan et al. (2024): Applying Machine Learning to the Problem of Choosing a Heuristic to Select the Variable Ordering for Cylindrical Algebraic Decomposition
  5. Jia, Fuqi et al. (2024): Suggesting Variable Order for Cylindrical Algebraic Decomposition via Reinforcement Learning
  6. Lample, Guillame et al. (2019): Deep Learning for Symbolic Mathematics
  7. Lenat, Doublas B. (1976): AM: An Artificial Intelligence Approach to Discovery in Mathematics as Heuristic Search
  8. Pickering, L. et al. (2024): Explainable AI Insights for Symbolic Computation: A case study on selecting the variable ordering for cylindrical algebraic decomposition
  9. Simpson, M.C. et al. (2016): Automatic Algorithm Selection in Computational Software Using Machine Learning
  10. 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

Large Language Models

  1. Austin, Jacob et al. (2021): Program Synthesis with Large Language Models
  2. Boix-Adserà, Enrich al. (2024): When can transformers reason with abstract symbols?
  3. Cobbe, Karl et al. (2021): Training Verifiers to Solve Math Word Problems
  4. Delétan, Grégoir et al. (2023): Neural Networks and the Chomsky Hierarchy
  5. Dziri, Nouha et al. (2023): Faith and Fate: Limits of Transformers on Compositionality
  6. Jiang, Bowen et al. (2024): A Peek into Token Bias: Large Language Models Are Not Yet Genuine Reasoners
  7. Johansson, Moa et al. (2023): Exploring Mathematical Conjecturing with Large Language Models
  8. Kambhampati, Subbarao (2024): Can Large Language Models Reason and Plan?
  9. Koppmann, Michael et al. (2024): KI-Assistenten und LLMs - was taugt der Code?
  10. Li, Quintong et al. (2024): GSM-Plus: A Comprehensive Benchmark for Evaluating the Robustness of LLMs as Mathematical Problem Solvers
  11. Li, Zhiyuan et al. (2024): Chain of Thought Empowers Transformers to Solve Inherently Serial Problems
  12. Li, Zihao et al. (2024): One-Layer Transformer Provably Learns One-Nearest Neighbor In Context
  13. Marcus, Gary (2024): LLMs don’t do formal reasoning - and that is a HUGE problem
  14. Mirzadeh, Iman et al. (2024): GSM-Symbolic: Understanding the Limitations of Mathematical Reasoning in Large Language Models
  15. OpenAI (2024): Learning to Reason with LLMs
  16. Peng, Binghui (2024): On Limitations of the Transformer Architecture
  17. Raihan, Nishat et al. (2025): Large Language Models in Computer Science Education: A Systematic Literature Review
  18. Razeghi, Yasaman (2022): Impact of Pretraining Term Frequencies on Few-Shot Reasoning
  19. Reiser, Marco et al. (2024): Wozu das Programmieren auf Prompt-Ebene führt
  20. Schaeffer, Rylan al. (2023): Are Emergent Abilities of Large Language Models a Mirage?
  21. Schatten, Alexander et al. (2024): Was soll schon schiefgehen - LLMs in der Softwareentwicklung
  22. Schürmann, Tim (2024): Die kleine Codefabrik: KI-Tools für Entwickler
  23. Shi, Freda, et al. (2023): Large Language Models Can Be Easily Distracted by Irrelevant Context
  24. Valmeekam, Karthik et al. (2022): PlanBench: An Extensible Benchmark for Evaluating Large Language Models on Planning and Reasoning about Change
  25. Valmeekam, Karthik et al. (2024): LLMs Still Can't Plan; Can LRMs? A Preliminary Evaluation of OpenAI's o1 on PlanBench
  26. Wei, Jason et al. (2022): Chain-of-Thought Prompting Elicits Reasoning in Large Language Models
  27. Weiss, Gail et al. (2021): Thinking Like Transformers
  28. Ye, Tian et al. (2024): Physics of Language Models: Part 2.1, Grade-School Math and the Hidden Reasoning Process
  29. Zhang, Hugh et al. (2024): A Careful Examination of Large Language Model Performance on Grade School Arithmetic
  30. Zhou, Hattie et al. (2024): What Algorithms can Transformers Learn? A Study in Length Generalization

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. Kaliszyk, Cezary et al. (2013): Stronger Automation for Flyspeck by Feature Weighting and Strategy Evolution
  42. Kaliszyk, Cezary et al. (2014): Learning-Assisted Automated Reasoning with Flyspeck
  43. Kaliszyk, Cezary et al. (2014): Machine Learner for Automated Reasoning 0.4 and 0.5
  44. Kaliszyk, Cezary et al. (2015): Learning-assisted theorem proving with millions of lemmas
  45. Kaliszyk, Cezary et al. (2015): FEMaLeCoP: Fairly Efficient Machine Learning Connection Prover
  46. Kaliszyk, Cezary et al. (2015): System description: E.T. 0.1
  47. Kaliszyk, Cezary et al. (2017): HolStep: A Machine Learning Dataset for Higher-order Logic Theorem Proving
  48. Kaliszyk, Cezary et al. (2018): Reinforcement Learning of Theorem Proving
  49. Komendantskay, Ekaterina et al. (2012): Machine learning in Proof General: Interfacing Interfaces
  50. Kühlwein, Daniel et al. (2012): Overview and Evaluation of Premise Selection Techniques for Large Theory Mathematics
  51. Kühlwein, Daniel et al. (2013): MaSh: Machine Learning for Sledgehammer
  52. Kühlwein, Daniel et al. (2015): MaLeS: A Framework for Automatic Tuning of Automated Theorem Provers
  53. Lample, Guillame et al. (2022): HyperTree Proof Search for Neural Theorem Proving
  54. Loos, Sarah et al. (2017): Deep Network Guided Proof Search
  55. Nagashima, Yutaka et al. (2018): PaMpeR: Proof Method Recommendation System for Isabelle/HOL
  56. Pierre, Marc et al. (2023): The Mathematical Game
  57. Pioetrowski, Bartosz et al. (2018): ATPboost: Learning Premise Selection in Binary Setting with ATP Feedback
  58. Pioetrowski, Bartosz et al. (2020): Stateful Premise Selection by Recurrent Neural Networks
  59. Pioetrowski, Bartosz et al. (2023): Machine-Learned Premise Selection for Lean
  60. Purgal, Stanislaw J. al (2022): Adversarial Learning to Reason in an Arbitrary Logic
  61. Rabe, Markus N. et al. (2020): Mathematical Reasoning via Self-supervised Skip-tree Training
  62. Rawson, Michael et al. (2019): A Neurally-Guided Parallel Theorem Prover
  63. Rawson, Michael et al. (2020): Directed Graph Networks for Logical Reasoning (Extended Abstract)
  64. Rawson, Michael et al. (2020): Directed Graph Networks for Logical Entailment
  65. Rawson, Michael et al. (2021): lazyCoP: Lazy Paramodulation Meets Neurally Guided Search
  66. Rute, Jason et al. (2023): Graph2Tac: Learning hierarchical representations of math concepts in theorem proving
  67. Rute, Jason et al. (2024): Graph2Tac: Online Representation Learning of Formal Math Concepts
  68. Sanchez-Stern, Alex et al. (2022): Passport: Improving Automated Formal Verification Using Identifiers
  69. Sanchez-Stern, Alex et al. (2024): Generating Correctness Proofs with Neural Networks
  70. Schäfer, Simon (2015): Breeding Theorem Proving Heuristics with Genetic Algorithms
  71. Schulz, Stephan (2000): Learning Search Control Knowledge for Equational Deduction
  72. Shankar, Natarajan (2013): Automated Reasoning, Fast and Slow
  73. Sharma, Rahul et al. (2011): Interpolants as Classifiers
  74. Steen, Alexander et al. (2016): Agent-Based HOL Reasoning
  75. Suda, Martin (2021): Improving ENIGMA-style Clause Selection while Learning From History
  76. Suda, Martin (2021): Vampire with a Brain Is a Good ITP Hammer
  77. Urban, Josef (1998): Experimenting with Machine Learning in Automatic Theorem Proving
  78. Urban, Josef et al. (2007): MaLARea: a Metasystem for Automated Reasoning in Large Theories
  79. Urban, Josef et al. (2008): MaLARea SG1 - Machine Learner for Automated Reasoning with Semantic Guidance
  80. Urban, Josef et al. (2011): MaLeCoP: Machine Learning Connection Prover
  81. Urban, Josef (2014): BliStr: The Blind Strategymaker
  82. Urban, Josef et al. (2020): First Neural Conjecturing Datasets and Experiments
  83. Wang, Mingzhe et al. (2020): Learning to Prove Theorems by Learning to Generate Theorems
  84. Whalen, Daniel (2016): Holophrasm: a neural Automated Theorem Prover for higher-order logic
  85. Yang, Kaiyu et al. (2019): Learning to Prove Theorems via Interacting with Proof Assistants
  86. Yang, Kaiyu et al. (2023): LeanDojo: Theorem Proving with Retrieval-Augmented Language Models
  87. Zhang, Liao et al. (2021): Online Machine Learning Techniques for Coq: A Comparison.
  88. Zhang, Liao et al. (2023): Learning Proof Transformations and Its Applications in Interactive Theorem Proving
  89. 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
  90. Zombori, Zsolt et al. (2019): Towards Finding Longer Proofs
  91. Zombori, Zsolt et al. (2021): The Role of Entropy in Guiding a Connection Prover

Wolfgang Schreiner
Last modified: October 14, 2024