Learning Rules Explaining Interactive Theorem Proving Tactic Prediction

• URL: http://arxiv.org/abs/2411.01188v1
• Date: Sat, 02 Nov 2024 09:18:33 GMT
• Title: Learning Rules Explaining Interactive Theorem Proving Tactic Prediction
• Authors: Liao Zhang, David M. Cerna, Cezary Kaliszyk,
• Abstract summary: We represent the problem as an Inductive Logic Programming (ILP) task. Using the ILP representation we enriched the feature space by encoding additional, computationally expensive properties. We use this enriched feature space to learn rules explaining when a tactic is applicable to a given proof state.
• Score: 5.229806149125529
• License:
• Abstract: Formally verifying the correctness of mathematical proofs is more accessible than ever, however, the learning curve remains steep for many of the state-of-the-art interactive theorem provers (ITP). Deriving the most appropriate subsequent proof step, and reasoning about it, given the multitude of possibilities, remains a daunting task for novice users. To improve the situation, several investigations have developed machine learning based guidance for tactic selection. Such approaches struggle to learn non-trivial relationships between the chosen tactic and the structure of the proof state and represent them as symbolic expressions. To address these issues we (i) We represent the problem as an Inductive Logic Programming (ILP) task, (ii) Using the ILP representation we enriched the feature space by encoding additional, computationally expensive properties as background knowledge predicates, (iii) We use this enriched feature space to learn rules explaining when a tactic is applicable to a given proof state, (iv) we use the learned rules to filter the output of an existing tactic selection approach and empirically show improvement over the non-filtering approaches.

Related papers

• Interpretable Anomaly Detection via Discrete Optimization [1.7150329136228712]
  We propose a framework for learning inherently interpretable anomaly detectors from sequential data. We show that this problem is computationally hard and develop two learning algorithms based on constraint optimization. Using a prototype implementation, we demonstrate that our approach shows promising results in terms of accuracy and F1 score.
  arXiv  Detail & Related papers  (2023-03-24T16:19:15Z)
• Lexicographic Multi-Objective Reinforcement Learning [65.90380946224869]
  We present a family of both action-value and policy gradient algorithms that can be used to solve such problems. We show how our algorithms can be used to impose safety constraints on the behaviour of an agent, and compare their performance in this context with that of other constrained reinforcement learning algorithms.
  arXiv  Detail & Related papers  (2022-12-28T10:22:36Z)
• Reinforcement Learning in Presence of Discrete Markovian Context Evolution [7.467644044726776]
  We consider a context-dependent Reinforcement Learning setting, which is characterized by: a) an unknown finite number of not directly observable contexts; b) abrupt (discontinuous) context changes occurring during an episode; and c) Markovian context evolution. We adapt a sticky Hierarchical Dirichlet Process (HDP) prior for model learning, which is arguably best-suited for Markov process modeling. We argue that the combination of these two components allows to infer the number of contexts from data thus dealing with the context cardinality assumption.
  arXiv  Detail & Related papers  (2022-02-14T08:52:36Z)
• Efficient Performance Bounds for Primal-Dual Reinforcement Learning from Demonstrations [1.0609815608017066]
  We consider large-scale Markov decision processes with an unknown cost function and address the problem of learning a policy from a finite set of expert demonstrations. Existing inverse reinforcement learning methods come with strong theoretical guarantees, but are computationally expensive. We introduce a novel bilinear saddle-point framework using Lagrangian duality to bridge the gap between theory and practice.
  arXiv  Detail & Related papers  (2021-12-28T05:47:24Z)
• Probing as Quantifying the Inductive Bias of Pre-trained Representations [99.93552997506438]
  We present a novel framework for probing where the goal is to evaluate the inductive bias of representations for a particular task. We apply our framework to a series of token-, arc-, and sentence-level tasks.
  arXiv  Detail & Related papers  (2021-10-15T22:01:16Z)
• MCDAL: Maximum Classifier Discrepancy for Active Learning [74.73133545019877]
  Recent state-of-the-art active learning methods have mostly leveraged Generative Adversarial Networks (GAN) for sample acquisition. We propose in this paper a novel active learning framework that we call Maximum Discrepancy for Active Learning (MCDAL) In particular, we utilize two auxiliary classification layers that learn tighter decision boundaries by maximizing the discrepancies among them.
  arXiv  Detail & Related papers  (2021-07-23T06:57:08Z)
• TacticZero: Learning to Prove Theorems from Scratch with Deep Reinforcement Learning [6.764610878007278]
  We propose a novel approach to interactive theorem-proving (ITP) using deep reinforcement learning. We formulate the process of ITP as a Markov decision process (MDP) in which each state represents a set of potential derivation paths. We show that the framework provides comparable performance to that of the approaches that use human experts.
  arXiv  Detail & Related papers  (2021-02-19T06:08:39Z)
• Multi-Agent Reinforcement Learning with Temporal Logic Specifications [65.79056365594654]
  We study the problem of learning to satisfy temporal logic specifications with a group of agents in an unknown environment. We develop the first multi-agent reinforcement learning technique for temporal logic specifications. We provide correctness and convergence guarantees for our main algorithm.
  arXiv  Detail & Related papers  (2021-02-01T01:13:03Z)
• Learning Implicitly with Noisy Data in Linear Arithmetic [94.66549436482306]
  We extend implicit learning in PAC-Semantics to handle intervals and threshold uncertainty in the language of linear arithmetic. We show that our implicit approach to learning optimal linear programming objective constraints significantly outperforms an explicit approach in practice.
  arXiv  Detail & Related papers  (2020-10-23T19:08:46Z)
• Can We Learn Heuristics For Graphical Model Inference Using Reinforcement Learning? [114.24881214319048]
  We show that we can learn programs, i.e., policies, for solving inference in higher order Conditional Random Fields (CRFs) using reinforcement learning. Our method solves inference tasks efficiently without imposing any constraints on the form of the potentials.
  arXiv  Detail & Related papers  (2020-04-27T19:24:04Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.