The Tactician (extended version): A Seamless, Interactive Tactic Learner and Prover for Coq

• URL: http://arxiv.org/abs/2008.00120v1
• Date: Fri, 31 Jul 2020 23:47:29 GMT
• Title: The Tactician (extended version): A Seamless, Interactive Tactic Learner and Prover for Coq
• Authors: Lasse Blaauwbroek, Josef Urban and Herman Geuvers
• Abstract summary: We present Tactician, a tactic learner and prover for the Coq Proof Assistant. Tactician helps users make tactical proof decisions while they retain control over the general proof strategy. We give an overview of Tactician from the user's point of view, regarding both day-to-day usage and issues of package dependency management.
• Score: 0.6445605125467572
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: We present Tactician, a tactic learner and prover for the Coq Proof Assistant. Tactician helps users make tactical proof decisions while they retain control over the general proof strategy. To this end, Tactician learns from previously written tactic scripts and gives users either suggestions about the next tactic to be executed or altogether takes over the burden of proof synthesis. Tactician's goal is to provide users with a seamless, interactive, and intuitive experience together with robust and adaptive proof automation. In this paper, we give an overview of Tactician from the user's point of view, regarding both day-to-day usage and issues of package dependency management while learning in the large. Finally, we give a peek into Tactician's implementation as a Coq plugin and machine learning platform.

Related papers

• Learning Rules Explaining Interactive Theorem Proving Tactic Prediction [5.229806149125529]
  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.
  arXiv  Detail & Related papers  (2024-11-02T09:18:33Z)
• RLIF: Interactive Imitation Learning as Reinforcement Learning [56.997263135104504]
  We show how off-policy reinforcement learning can enable improved performance under assumptions that are similar but potentially even more practical than those of interactive imitation learning. Our proposed method uses reinforcement learning with user intervention signals themselves as rewards. This relaxes the assumption that intervening experts in interactive imitation learning should be near-optimal and enables the algorithm to learn behaviors that improve over the potential suboptimal human expert.
  arXiv  Detail & Related papers  (2023-11-21T21:05:21Z)
• TacticAI: an AI assistant for football tactics [41.74699109772055]
  TacticAI is an AI football tactics assistant developed and evaluated in close collaboration with domain experts from Liverpool FC. We focus on analysing corner kicks, as they offer coaches the most direct opportunities for interventions and improvements. We show that TacticAI's model suggestions are not only indistinguishable from real tactics, but also favoured over existing tactics 90% of the time.
  arXiv  Detail & Related papers  (2023-10-16T16:25:15Z)
• Chain-of-Thought Predictive Control [32.30974063877643]
  We study generalizable policy learning from demonstrations for complex low-level control. We propose a novel hierarchical imitation learning method that utilizes sub-optimal demos.
  arXiv  Detail & Related papers  (2023-04-03T07:59:13Z)
• Transductive Learning for Unsupervised Text Style Transfer [60.65782243927698]
  Unsupervised style transfer models are mainly based on an inductive learning approach. We propose a novel transductive learning approach based on a retrieval-based context-aware style representation.
  arXiv  Detail & Related papers  (2021-09-16T08:57:20Z)
• Online Machine Learning Techniques for Coq: A Comparison [2.9412498294532856]
  We present a comparison of several online machine learning techniques for tactical learning and proving in the Coq proof assistant. This work builds on Tactician, a plugin for Coq that learns from proofs written by the user to synthesize new proofs.
  arXiv  Detail & Related papers  (2021-04-12T05:12:35Z)
• Can Semantic Labels Assist Self-Supervised Visual Representation Learning? [194.1681088693248]
  We present a new algorithm named Supervised Contrastive Adjustment in Neighborhood (SCAN) In a series of downstream tasks, SCAN achieves superior performance compared to previous fully-supervised and self-supervised methods. Our study reveals that semantic labels are useful in assisting self-supervised methods, opening a new direction for the community.
  arXiv  Detail & Related papers  (2020-11-17T13:25:00Z)
• Empowering Active Learning to Jointly Optimize System and User Demands [70.66168547821019]
  We propose a new active learning approach that jointly optimize the active learning system (training efficiently) and the user (receiving useful instances) We study our approach in an educational application, which particularly benefits from this technique as the system needs to rapidly learn to predict the appropriateness of an exercise to a particular user. We evaluate multiple learning strategies and user types with data from real users and find that our joint approach better satisfies both objectives when alternative methods lead to many unsuitable exercises for end users.
  arXiv  Detail & Related papers  (2020-05-09T16:02:52Z)
• Tactic Learning and Proving for the Coq Proof Assistant [0.5735035463793007]
  Our system predicts appropriate tactics and finds proofs in the form of tactic scripts. The performance of the system is evaluated on the Coq Standard Library. When combined with the CoqHammer system, the two systems together prove 56.7% of the library's lemmas.
  arXiv  Detail & Related papers  (2020-03-20T08:22:30Z)
• Reward-Conditioned Policies [100.64167842905069]
  imitation learning requires near-optimal expert data. Can we learn effective policies via supervised learning without demonstrations? We show how such an approach can be derived as a principled method for policy search.
  arXiv  Detail & Related papers  (2019-12-31T18:07:43Z)

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.