README.md

CoqPerceptron

Verified Coq Implementation of the Rational-Valued Perceptron Algorithm and Rational-Valued Averaged-Perceptron Algorithm.

Key Files

Coq

• QvecArith.v: vector arithmetic
• PerceptronDef.v: Coq Perceptron
• PerceptronSound.v: soundness
• TerminationRefinement.v: termination refinement proofs
• MCEBounds.v: the "AC bounds" lemmas
• PerceptronConvergence.v: convergence proof
• extraction.v: fueled Perceptron and extraction

Benchmarks/

• cpp/: C++ implementation of Perceptron; also, program to generate random data sets
• hs/:Extracted CoqPerceptron to Haskell
• hsopt/: Soundly Optimized Extraction of CoqPercepton to Haskell
• data/: Real-world and randomly-generated data sets
• output/:Output and timing results from running the CPP, HS, and HSOpt verions of the Perceptron.
• scripts/: Scripts for generated random data sets and running benchmarks

Building the Coq Development

Simply type

make

Prerequisites

For building CoqPerceptron and C++ Perceptron Implementations

• Coq 8.5pl2
• GHC 7.6.3
• G++ 4.8.4
• Boost 1.54

For creating the plotting files

• Python 2.7.6
• matplotlib 1.3.1
• gnuplot 4.6.4

Our development may compile with other versions, but this hasn't been tested.

Building CoqPerceptron (Benchmarks/hs/)

  cd Benchmarks/hs
  make

Building Optimized CoqPerceptron (Benchmarks/hsopt)

  cd Benchmarks/hsopt
  make

Building C++ Perceptron Implementation (Benchmarks/cpp)

  cd Benchmarks/cpp
  make

Running Benchmarks

Generating new DataSets

Note: This will overwrite the data in data/

  cd Benchmarks
  scripts/gen_data.sh

Run each Perceptron implementation on the generated data

  scripts/runbenchmarks.sh cpp/perceptron data/ output/cpp output/fuels hs/RunValidator output/cpp_valid.dat > output/cpptimes 2> output/cpp_validtimes
  scripts/runbenchmarks.sh hs/RunPerceptron data/ output/hs > output/hstimes
  scripts/runbenchmarks.sh hsopt/RunPerceptron data/ output/hsopt > output/hsopttimes

Note: You may wish to put this in a script and run that as each command may take a considerable amount of time to run

Creating Plot Files

  cpp/makeplotfiles
  cd plots
  python makeplots.py
  gnuplot epochs.gplot