mlsanityData to 7 Oct 2026

Learning to Find Proofs and Theorems by Learning to Refine Search Strategies: The Case of Loop Invariant Synthesis

arXiv 2205.14229 ↗First posted 27 May 2022cs.AIcited by 5

Not on the map. Why?

Abstract (arXiv)

We propose a new approach to automated theorem proving where an AlphaZero-style agent is self-training to refine a generic high-level expert strategy expressed as a nondeterministic program. An analogous teacher agent is self-training to generate tasks of suitable relevance and difficulty for the learner. This allows leveraging minimal amounts of domain knowledge to tackle problems for which training data is unavailable or hard to synthesize. As a specific illustration, we consider loop invariant synthesis for imperative programs and use neural networks to refine both the teacher and solver strategies.

Key facts. Cited by 5 papers in the map (data through 7 Oct 2026). Builds on 22 of its 53 references that are in the map. First posted on arXiv 27 May 2022.

Builds on

22 of 53 references.

References · 22

  1. 2017Attention Is All You Needcited by 59,932
  2. 2019PyTorch: An Imperative Style, High-Performance Deep Learning Librarycited by 20,160
  3. 2019Fast Graph Representation Learning with PyTorch Geometriccited by 2,414
  4. 2017Ray: A Distributed Framework for Emerging AI Applicationscited by 516
  5. 2020Generative Language Modeling for Automated Theorem Provingcited by 379
  6. 2019Deep Learning for Symbolic Mathematicscited by 266
  7. 2021Proof Artifact Co-training for Theorem Proving with Language Modelscited by 130
  8. 2019Learning to Prove Theorems via Interacting with Proof Assistantscited by 107
  9. 2018Leveraging Grammar and Reinforcement Learning for Neural Program Synthesiscited by 83
  10. 2018Reinforcement Learning of Theorem Provingcited by 69
  11. 2019Accelerating Self-Play Learning in Gocited by 60
  12. 2020Teaching Temporal Logics to Neural Networkscited by 51
10 more
  1. 2018GamePad: A Learning Environment for Theorem Provingcited by 48
  2. 2020INT: An Inequality Benchmark for Evaluating Generalization in Theorem Provingcited by 44
  3. 2020Learning to Prove Theorems by Learning to Generate Theoremscited by 43
  4. 2021TacticZero: Learning to Prove Theorems from Scratch with Deep Reinforcement Learningcited by 37
  5. 2019Learning to Reason in Large Theories without Imitationcited by 27
  6. 2019CLN2INV: Learning Loop Invariants with Continuous Logic Networkscited by 20
  7. 2020Learning to Prove from Synthetic Theoremscited by 13
  8. 2019Ilinva: Using Abduction to Generate Loop Invariantscited by 3
  9. 2020Universal Policies for Software-Defined MDPscited by 2
  10. 2014Monad Transformers for Backtracking Searchcited by 1

Built on by

Cited by year (2026 to 7 Oct)

Citing papers per year: 2023: 2; 2024: 2; 2025: 0; 2026: 1.

5 papers.

  1. 2023Lyra: Orchestrating Dual Correction in Automated Theorem Provingcited by 24
  2. 2023Reinforcement Learning and Data-Generation for Syntax-Guided Synthesiscited by 3
  3. 2024Intersymbolic AI: Interlinking Symbolic AI and Subsymbolic AIcited by 3
  4. 2024Application of AI to formal methods - an analysis of current trendscited by 2
  5. 2026Self-Supervised Theorem Discovery in a Formal Axiomatic Systemcited by 0