Machine Learning in Proof General: Interfacing Interfaces
We present ML4PG - a machine learning extension for Proof General. It allows users to gather proof statistics related to shapes of goals, sequences of applied tactics, and proof tree structures from the libraries of interactive higher-order proofs written in Coq and SSReflect. The gathered data is clustered using the state-of-the-art machine learning algorithms available in MATLAB and Weka. ML4PG provides automated interfacing between Proof General and MATLAB/Weka. The results of clustering are used by ML4PG to provide proof hints in the process of interactive proof development.
Code (0)
등록된 구현이 없습니다.
Tasks
BIG-bench Machine LearningClusteringSimilar Papers 제목 키워드 기반
Peripheral brain interfacing: Reading high-frequency brain signals from the output of the nervous system
Accurate and robust recording and decoding from the central nervous system (CNS) is essential for advances in human-machine interfacing. However, technologies used to directly measure CNS activity are limited by their re…
An approach to interfacing the brain with quantum computers: practical steps and caveats
We report on the first proof-of-concept system demonstrating how one can control a qubit with mental activity. We developed a method to encode neural correlates of mental activity as instructions for a quantum computer. …
Beyond Sight: Probing Alignment Between Image Models and Blind V1
Neural activity in the visual cortex of blind humans persists in the absence of visual stimuli. However, little is known about the preservation of visual representation capacity in these cortical regions, which could hav…
A Technique Based on Chaos for Brain Computer Interfacing
A user of Brain Computer Interface (BCI) system must be able to control external computer devices with brain activity. Although the proof-of-concept was given decades ago, the reliable translation of user intent into dev…
Brain Computer InterfaceClassificationClusteringEEG+3Model-Agnostic Meta-Learning for EEG Motor Imagery Decoding in Brain-Computer-Interfacing
We introduce here the idea of Meta-Learning for training EEG BCI decoders. Meta-Learning is a way of training machine learning systems so they learn to learn. We apply here meta-learning to a simple Deep Learning BCI arc…
DecoderEEGElectroencephalogram (EEG)Meta-Learning+2