Online Machine Learning Techniques for Coq: A Comparison
We present a comparison of several online machine learning techniques for tactical learning and proving in the Coq proof assistant. This work builds on top of Tactician, a plugin for Coq that learns from proofs written by the user to synthesize new proofs. Learning happens in an online manner, meaning that Tactician's machine learning model is updated immediately every time the user performs a step in an interactive proof. This has important advantages compared to the more studied offline learning systems: (1) it provides the user with a seamless, interactive experience with Tactician and, (2) it takes advantage of locality of proof similarity, which means that proofs similar to the current proof are likely to be found close by. We implement two online methods, namely approximate k-nearest neighbors based on locality sensitive hashing forests and random decision forests. Additionally, we conduct experiments with gradient boosted trees in an offline setting using XGBoost. We compare the relative performance of Tactician using these three learning methods on Coq's standard library.
Code (0)
등록된 구현이 없습니다.
Tasks
BIG-bench Machine LearningSimilar Papers 제목 키워드 기반
Fake Reviews Detection through Ensemble Learning
Customers represent their satisfactions of consuming products by sharing their experiences through the utilization of online reviews. Several machine learning-based approaches can automatically detect deceptive and fake …
BIG-bench Machine LearningEnsemble LearningFact or Factitious? Contextualized Opinion Spam Detection
In this paper we perform an analytic comparison of a number of techniques used to detect fake and deceptive online reviews. We apply a number machine learning approaches found to be effective, and introduce our own appro…
BIG-bench Machine LearningSpam detectionA general anomaly detection framework for fleet-based condition monitoring of machines
Machine failures decrease up-time and can lead to extra repair costs or even to human casualties and environmental pollution. Recent condition monitoring techniques use artificial intelligence in an effort to avoid time-…
Anomaly DetectionA Comprehensive Performance Comparison of Traditional and Ensemble Machine Learning Models for Online Fraud Detection
In the era of the digitally driven economy, where there has been an exponential surge in digital payment systems and other online activities, various forms of fraudulent activities have accompanied the digital growth, ou…
Fraud DetectionPreventing Discriminatory Decision-making in Evolving Data Streams
Bias in machine learning has rightly received significant attention over the last decade. However, most fair machine learning (fair-ML) work to address bias in decision-making systems has focused solely on the offline se…
Decision MakingFairness