Machine Learning in Proof General: Interfacing Interfaces
Machine Learning in Proof General: Interfacing Interfaces
复制标题
DOI：
10.4204/eptcs.118.2
复制
发表时间：
2012-12
影响因子：
3.4
通讯作者：
Ekaterina Komendantskaya;Jónathan Heras;G. Grov
中科院分区：
文献类型：
--
作者：
Ekaterina Komendantskaya;Jónathan Heras;G. Grov
我们提出ML4PG-用于证明一般的机器学习扩展。它允许用户收集与目标，应用策略序列的形状，互动式高级证明库中的证明树结构相关的证明统计信息。收集的数据使用MATLAB和WEKA中的最新机器学习算法聚类。 ML4PG提供了Proof General和MATLAB/WEKA之间的自动接口。 ML4PG使用聚类的结果在交互式证明开发过程中提供了证明提示。
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.