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