From daf76667b7212664ce83c8fd5aa5d48cb823e866 Mon Sep 17 00:00:00 2001 From: joheras Date: Fri, 31 May 2013 12:10:57 +0000 Subject: Moving ML4PG from coq directory to contrib directory. --- contrib/ML4PG/doc/src/images/algorithm1.png | Bin 0 -> 249326 bytes contrib/ML4PG/doc/src/images/algorithm2.png | Bin 0 -> 253897 bytes contrib/ML4PG/doc/src/images/clusters1.png | Bin 0 -> 117359 bytes contrib/ML4PG/doc/src/images/clusters1pg.png | Bin 0 -> 138300 bytes contrib/ML4PG/doc/src/images/clusters2.png | Bin 0 -> 93270 bytes contrib/ML4PG/doc/src/images/clusters2pg.png | Bin 0 -> 69517 bytes contrib/ML4PG/doc/src/images/export.png | Bin 0 -> 65552 bytes contrib/ML4PG/doc/src/images/fig1.png | Bin 0 -> 32650 bytes contrib/ML4PG/doc/src/images/fig1pg.png | Bin 0 -> 102528 bytes contrib/ML4PG/doc/src/images/fig2.png | Bin 0 -> 83087 bytes contrib/ML4PG/doc/src/images/fig3.png | Bin 0 -> 89061 bytes contrib/ML4PG/doc/src/images/fig4.png | Bin 0 -> 129581 bytes contrib/ML4PG/doc/src/images/fig5.png | Bin 0 -> 106362 bytes contrib/ML4PG/doc/src/images/frequencies.png | Bin 0 -> 125515 bytes contrib/ML4PG/doc/src/images/granularity.png | Bin 0 -> 122487 bytes contrib/ML4PG/doc/src/images/levels.png | Bin 0 -> 261362 bytes contrib/ML4PG/doc/src/images/ml_system1.png | Bin 0 -> 249326 bytes contrib/ML4PG/doc/src/images/ml_system2.png | Bin 0 -> 179177 bytes contrib/ML4PG/doc/src/ml4pg_manual.bib | 12 ++ contrib/ML4PG/doc/src/ml4pg_manual.pdf | Bin 0 -> 1100379 bytes contrib/ML4PG/doc/src/ml4pg_manual.tex | 209 +++++++++++++++++++++++++++ 21 files changed, 221 insertions(+) create mode 100644 contrib/ML4PG/doc/src/images/algorithm1.png create mode 100644 contrib/ML4PG/doc/src/images/algorithm2.png create mode 100644 contrib/ML4PG/doc/src/images/clusters1.png create mode 100644 contrib/ML4PG/doc/src/images/clusters1pg.png create mode 100644 contrib/ML4PG/doc/src/images/clusters2.png create mode 100644 contrib/ML4PG/doc/src/images/clusters2pg.png create mode 100644 contrib/ML4PG/doc/src/images/export.png create mode 100644 contrib/ML4PG/doc/src/images/fig1.png create mode 100644 contrib/ML4PG/doc/src/images/fig1pg.png create mode 100644 contrib/ML4PG/doc/src/images/fig2.png create mode 100644 contrib/ML4PG/doc/src/images/fig3.png create mode 100644 contrib/ML4PG/doc/src/images/fig4.png create mode 100644 contrib/ML4PG/doc/src/images/fig5.png create mode 100644 contrib/ML4PG/doc/src/images/frequencies.png create mode 100644 contrib/ML4PG/doc/src/images/granularity.png create mode 100644 contrib/ML4PG/doc/src/images/levels.png create mode 100644 contrib/ML4PG/doc/src/images/ml_system1.png create mode 100644 contrib/ML4PG/doc/src/images/ml_system2.png create mode 100644 contrib/ML4PG/doc/src/ml4pg_manual.bib create mode 100644 contrib/ML4PG/doc/src/ml4pg_manual.pdf create mode 100644 contrib/ML4PG/doc/src/ml4pg_manual.tex (limited to 'contrib/ML4PG/doc/src') diff --git a/contrib/ML4PG/doc/src/images/algorithm1.png b/contrib/ML4PG/doc/src/images/algorithm1.png new file mode 100644 index 00000000..8c8f47b5 Binary files /dev/null and b/contrib/ML4PG/doc/src/images/algorithm1.png differ diff --git a/contrib/ML4PG/doc/src/images/algorithm2.png b/contrib/ML4PG/doc/src/images/algorithm2.png new file mode 100644 index 00000000..6b5e0835 Binary files /dev/null and b/contrib/ML4PG/doc/src/images/algorithm2.png differ diff --git a/contrib/ML4PG/doc/src/images/clusters1.png b/contrib/ML4PG/doc/src/images/clusters1.png new file mode 100644 index 00000000..ca4ef219 Binary files /dev/null and b/contrib/ML4PG/doc/src/images/clusters1.png differ diff --git a/contrib/ML4PG/doc/src/images/clusters1pg.png b/contrib/ML4PG/doc/src/images/clusters1pg.png new file mode 100644 index 00000000..b39d409f Binary files /dev/null and b/contrib/ML4PG/doc/src/images/clusters1pg.png differ diff --git a/contrib/ML4PG/doc/src/images/clusters2.png b/contrib/ML4PG/doc/src/images/clusters2.png new file mode 100644 index 00000000..f091abbe Binary files /dev/null and b/contrib/ML4PG/doc/src/images/clusters2.png differ diff --git a/contrib/ML4PG/doc/src/images/clusters2pg.png b/contrib/ML4PG/doc/src/images/clusters2pg.png new file mode 100644 index 00000000..6ba6dcb4 Binary files /dev/null and b/contrib/ML4PG/doc/src/images/clusters2pg.png differ diff --git a/contrib/ML4PG/doc/src/images/export.png b/contrib/ML4PG/doc/src/images/export.png new file mode 100644 index 00000000..de048b47 Binary files /dev/null and b/contrib/ML4PG/doc/src/images/export.png differ diff --git a/contrib/ML4PG/doc/src/images/fig1.png b/contrib/ML4PG/doc/src/images/fig1.png new file mode 100644 index 00000000..955fd048 Binary files /dev/null and b/contrib/ML4PG/doc/src/images/fig1.png differ diff --git a/contrib/ML4PG/doc/src/images/fig1pg.png b/contrib/ML4PG/doc/src/images/fig1pg.png new file mode 100644 index 00000000..d4a0df9f Binary files /dev/null and b/contrib/ML4PG/doc/src/images/fig1pg.png differ diff --git a/contrib/ML4PG/doc/src/images/fig2.png b/contrib/ML4PG/doc/src/images/fig2.png new file mode 100644 index 00000000..ed8c399e Binary files /dev/null and b/contrib/ML4PG/doc/src/images/fig2.png differ diff --git a/contrib/ML4PG/doc/src/images/fig3.png b/contrib/ML4PG/doc/src/images/fig3.png new file mode 100644 index 00000000..f3741a0e Binary files /dev/null and b/contrib/ML4PG/doc/src/images/fig3.png differ diff --git a/contrib/ML4PG/doc/src/images/fig4.png b/contrib/ML4PG/doc/src/images/fig4.png new file mode 100644 index 00000000..9df097bd Binary files /dev/null and b/contrib/ML4PG/doc/src/images/fig4.png differ diff --git a/contrib/ML4PG/doc/src/images/fig5.png b/contrib/ML4PG/doc/src/images/fig5.png new file mode 100644 index 00000000..733a3d22 Binary files /dev/null and b/contrib/ML4PG/doc/src/images/fig5.png differ diff --git a/contrib/ML4PG/doc/src/images/frequencies.png b/contrib/ML4PG/doc/src/images/frequencies.png new file mode 100644 index 00000000..4f90b5fc Binary files /dev/null and b/contrib/ML4PG/doc/src/images/frequencies.png differ diff --git a/contrib/ML4PG/doc/src/images/granularity.png b/contrib/ML4PG/doc/src/images/granularity.png new file mode 100644 index 00000000..385b3972 Binary files /dev/null and b/contrib/ML4PG/doc/src/images/granularity.png differ diff --git a/contrib/ML4PG/doc/src/images/levels.png b/contrib/ML4PG/doc/src/images/levels.png new file mode 100644 index 00000000..48e02db7 Binary files /dev/null and b/contrib/ML4PG/doc/src/images/levels.png differ diff --git a/contrib/ML4PG/doc/src/images/ml_system1.png b/contrib/ML4PG/doc/src/images/ml_system1.png new file mode 100644 index 00000000..f11cebf1 Binary files /dev/null and b/contrib/ML4PG/doc/src/images/ml_system1.png differ diff --git a/contrib/ML4PG/doc/src/images/ml_system2.png b/contrib/ML4PG/doc/src/images/ml_system2.png new file mode 100644 index 00000000..792c423d Binary files /dev/null and b/contrib/ML4PG/doc/src/images/ml_system2.png differ diff --git a/contrib/ML4PG/doc/src/ml4pg_manual.bib b/contrib/ML4PG/doc/src/ml4pg_manual.bib new file mode 100644 index 00000000..07dcb4ba --- /dev/null +++ b/contrib/ML4PG/doc/src/ml4pg_manual.bib @@ -0,0 +1,12 @@ +@Article{KHG12, + author = {E. Komendantskaya and J. Heras and G. Grov}, + title = {Machine Learning in Proof General: interfacing interfaces}, + year = {2012}, +} + + +@Article{HK13, + author = {J. Heras and E. Komendantskaya}, + title = {ML4PG Case studies}, + year = {2013}, +} \ No newline at end of file diff --git a/contrib/ML4PG/doc/src/ml4pg_manual.pdf b/contrib/ML4PG/doc/src/ml4pg_manual.pdf new file mode 100644 index 00000000..c13f6801 Binary files /dev/null and b/contrib/ML4PG/doc/src/ml4pg_manual.pdf differ diff --git a/contrib/ML4PG/doc/src/ml4pg_manual.tex b/contrib/ML4PG/doc/src/ml4pg_manual.tex new file mode 100644 index 00000000..2eb92b7e --- /dev/null +++ b/contrib/ML4PG/doc/src/ml4pg_manual.tex @@ -0,0 +1,209 @@ +\documentclass[10pt]{article} + + +\usepackage[utf8]{inputenc} + +\usepackage{hyperref} +\usepackage{graphicx} +\usepackage{amssymb} +\usepackage{color} +\usepackage{listings} +\usepackage{tikz} +\usepackage{verbatim} +\usepackage{theorem} + + + +\begin{document} + +\title{ML4PG: Machine learning for Proof General} +\author{J\'onathan Heras and Ekaterina Komendantskaya\\ +\{jonathanheras,katya\}@computing.dundee.ac.uk} + \maketitle + + + +\tableofcontents + + +\section{Using ML4PG} + + +To illustrate the use of ML4PG, we will use the file \verb"ml4pg.v" which can be find in the same folder of this manual. +This file contains various lemmas about natural numbers and lists. + +\subsection{Getting started} + +Open the file \verb"ml4pg.v" using emacs. The Proof General interface is the usual one, but it includes a new option in the Coq menu +called ML4PG. + +\begin{figure} + \centering + \includegraphics[scale=0.4]{images/fig1pg.png} + \caption{Proof General with the ML4PG option.}\label{fig1} +\end{figure} + +If you select this option, the interface asks you if you are developing your proofs using the plain Coq style or the SSReflect style, in this case we select the Coq mode (c). +Subsequently, the interface asks you if you want to extract the information associated with the lemmas which have been previously developed in this library. In this case, +we select no (c). Once that this is done, the Proof General interface is extended with a new menu called \emph{Statistics} and two buttons, see Figure~\ref{fig3}. + +\begin{figure} + \centering + \includegraphics[scale=0.4]{images/fig3.png} + \caption{ML4PG interface with all the options active.}\label{fig3} +\end{figure} + + +\subsection{Extracting feature vectors} + +Feature vectors can be extracted in two different ways: + +\begin{itemize} + \item During the development of the proofs. To this aim, you have to use the shortcut Ctrl-C Ctrl-M to process the next proof command. + \item Several proofs at the same time. If you want to extract the feature vectors of several proofs, go to the last proof and use the shortcut Ctrl-C Space. + You can also use the \emph{Extract info up to point} option of the statistics menu. +\end{itemize} + +Go to the end of \verb"emacs ml4pg.v" file; there, you can see two unfinished proofs: \verb"M3_3b" and \verb"aux7_bis". Put the cursor at the end of +the proof of Lemma \verb"andb_false_r" and use the shortcut Ctrl-C Space or the \emph{Extract info up to point} option of the statistics menu. In this +way the information associated with each proof will be extracted and you will be able to use it to obtain proof clusters (groups of similar proofs). + +Now, let us explain the functionality of the options included in the Statistics menu. + +\subsection{Configuration menu} + +The different options to configure the Machine-learning environments were detailed in~\cite{KHG12}. All those options can be accessed from the Configuration +submenu of the Statistics menu, see Figure~\ref{fig3}. + + + +\paragraph{Algorithms:} + +The user can select different algorithms to obtain proof similarities (all of them behave similar, see~\cite{HK13}). +ML4PG offers different algorithms, see Figure~\ref{algorithms}. + +In the case of MATLAB; there are three algorithms available: K-means and Gaussian. In the case of Weka, the algorithms +which are available are: K-means, EM and FarthestFirst. + +\begin{figure} + \centering + \includegraphics[scale=0.4]{images/algorithm2.png} + \caption{The ML algorithms menu.}\label{algorithms} +\end{figure} + +\paragraph{Granularity:} + +In the machine learning literature, there exists a number of heuristics to determine this optimal number of clusters. +We used them as an inspiration to formulate our own algorithm for ML4PG, tailored +to the interactive proofs. It takes into consideration the size of the proof library and an auxiliary parameter + -- called granularity. This parameter is used to calculate the optimal number of +proof clusters, the process to calculate this optimal number was described in~\cite{KHG12}. The user decides the +granularity in ML4PG menu (see Figure~\ref{granularity}), by selecting a value between 1 and 5, where 1 stands for a +low granularity (producing big and general clusters) and 5 stands for a high granularity (producing small +and precise clusters). + + +\begin{figure} + \centering + \includegraphics[scale=0.4]{images/granularity.png} + \caption{ML4PG granularity menu.}\label{granularity} +\end{figure} + + + +\paragraph{Frequencies:} + +Clustering techniques divide data into n groups of similar objects (called clusters), where the value of +n is a ``learning'' parameter provided by the user together with other inputs to the clustering algorithms. +Increasing the value of n means that the algorithm will try to separate objects into more classes, and, as a +consequence, each cluster will contain examples with higher correlation. The frequencies of clusters can +serve for analysis of their reliability. Results of one run of a clustering algorithm may differ from another, +even on the same data set. This is due to the fact that clustering algorithms randomly choose examples +to start from, and then, form clusters relative to those examples. However, it may happen that certain +clusters are found repeatedly – and frequently – in different runs; then, we can use these frequencies to +determine the reliable clusters. The frequencies can be determined using the threshold presented in Figure~\ref{frequencies}, +a detailed description of this parameter was given in~\cite{KHG12}. + + +\begin{figure} + \centering + \includegraphics[scale=0.4]{images/frequencies.png} + \caption{ML4PG frequencies menu.}\label{frequencies} +\end{figure} + + +\subsection{Show clusters} + +The option \emph{Show Clusters} of the Statistics menu shows clusters when a library is clustered +irrespective of the current proof goal. An example using the \verb"ml4pg.v" library with the options: + +\begin{itemize} + \item Algorithm: K-means, + \item Granularity: 3, + \item Frequencies: 1. +\end{itemize} + +\noindent is shown in Figure~\ref{clusters1}. + +\begin{figure} + \centering + \includegraphics[scale=0.23]{images/clusters1pg.png} + \caption{Clusters for the ml4pg library. The Proof General window has been split into two windows positioned side by +side: the left one keeps the current proof script, and the right one shows the clusters. If the user clicks +on the name of a theorem showed in the right screen, such a window is split horizontally and a brief description of the selected +theorem is shown.}\label{clusters1} +\end{figure} + +This functionality can also invoked using the second right most button of the Proof General toolbar. + +\subsection{Show similar theorems} + +The example above shows one mode of working with ML4PG: that is, when a library is clustered +irrespective of the current proof goal. However, it may be useful to use this technology to aid the interactive +proof development. In which case, we can cluster libraries relative to a few initial proof steps for the +current proof goal. An example using the \verb"ml4pg.v" library with the options: + +\begin{itemize} + \item Algorithm: FarthestFirst, + \item Granularity: 2, + \item Frequencies: 2. +\end{itemize} + +\noindent and with the few steps included about the proof of \verb"M3_3b" is shown in Figure~\ref{clusters2}. + + +\begin{figure} + \centering + \includegraphics[scale=0.23]{images/clusters2pg.png} + \caption{On the right side, several suggestions provided by ML4PG. If the user clicks on the name of one of the +suggested lemmas, a brief description about it is shown.}\label{clusters2} +\end{figure} + +This functionality can also invoked using the right most button of the Proof General toolbar. + +\subsection{Export Library} + +Using the Export library option, the user can export the library for further use (see Figure~\ref{export}) with the +Available libraries for clustering option. + + +\begin{figure} + \centering + \includegraphics[scale=0.4]{images/export.png} + \caption{ML4PG export menu.}\label{export} +\end{figure} + + + + + + + + + + +\bibliographystyle{plain} +\bibliography{ml4pg_manual} + + +\end{document} -- cgit v1.2.3