Charlie Murphy
ABSTRACT
Frank Rosenblatt invented the perceptron algorithm in 1957 as part of an early attempt to build ``brain models'', artificial neural networks. In this paper, we apply tools from symbolic logic such as dependent type theory as implemented in Coq to build, and prove convergence of, one-layer perceptrons (specifically, we show that our Coq implementation converges to a binary classifier when trained on linearly separable datasets).
Our perceptron and proof are extensible, which we demonstrate by adapting our convergence proof to the averaged perceptron, a common variant of the basic perceptron algorithm. We perform experiments to evaluate the performance of our Coq perceptron vs. an arbitrary-precision C++ implementation and against a hybrid implementation in which separators learned in C++ are certified in Coq. We find that by carefully optimizing the extraction of our Coq perceptron, we can meet -- and occasionally exceed -- the performance of the arbitrary-precision C++ implementation. Our hybrid Coq certifier demonstrates an architecture for building high-assurance machine-learning systems that reuse existing codebases.
- Andreas Abel. Termination Checking with Types. ITA, 2004.Google Scholar
Cross Ref
- Edgar Anderson. The Irises of the Gaspé Peninsula. Bulletin of the American Iris Society, 59:2–5, 1935.Google Scholar
- Yves Bertot. Fixed precision patterns for the formal verification of mathematical constant approximations. In Proceedings of the 2015 Conference on Certified Programs and Proofs, pages 147–155. ACM, 2015. Google ScholarDigital Library
- Sooraj Bhat. Syntactic foundations for machine learning. PhD thesis, Georgia Institute of Technology, 2013.Google Scholar
- Hans-Dieter Block. The Perceptron: A Model for Brain Functioning. I. Reviews of Modern Physics, 34(1):123, 1962.Google ScholarCross Ref
- Sylvie Boldo and Guillaume Melquiond. Flocq: A unified library for proving floating-point algorithms in Coq. In Computer Arithmetic (ARITH), 2011 20th IEEE Symposium on, pages 243–252. IEEE, 2011. Google ScholarDigital Library
- Christophe Brun, Jean-François Dufourd, and Nicolas Magaud. Formal Proof in Coq and Derivation of an Imperative Program to Compute Convex Hulls. In Aut. Deduction in Geom. 2012.Google Scholar
- T-S Chang and Khaled AS Abdel-Ghaffar. A universal neural net with guaranteed convergence to zero system error. IEEE Transactions on signal processing, 40(12):3022–3031, 1992. Google ScholarDigital Library
- Byron Cook, Andreas Podelski, and Andrey Rybalchenko. Termination Proofs for Systems Code. In PLDI, 2006. Google ScholarDigital Library
- Koby Crammer and Yoram Singer. Ultraconservative online algorithms for multiclass problems. Journal of Machine Learning Research, 3(Jan): 951–991, 2003. Google ScholarDigital Library
- Hal Daumé, III. A course in machine learning. http://ciml.info/, 2017. Accessed: 2017-03-22. Ronald A Fisher. The Use of Multiple Measurements in Taxonomic Problems. Annals of Eugenics, 7(2):179–188, 1936.Google Scholar
- Benjamin Grégoire and Laurent Théry. A purely functional library for modular arithmetic and its application to certifying large prime numbers. In International Joint Conference on Automated Reasoning, pages 423– 437. Springer, 2006. Google ScholarDigital Library
- Suyog Gupta, Ankur Agrawal, Kailash Gopalakrishnan, and Pritish Narayanan. Deep learning with limited numerical precision. CoRR, abs/1502.02551, 392, 2015.Google Scholar
- Jónathan Heras, Ekaterina Komendantskaya, Moa Johansson, and Ewen Maclean. Proof-pattern Recognition and Lemma Discovery in ACL2. In LPAR, 2013.Google ScholarCross Ref
- Ekaterina Komendantskaya, Jónathan Heras, and Gudmund Grov. Machine Learning in Proof General: Interfacing Interfaces. arXiv preprint arXiv:1212.3618, 2012.Google Scholar
- M. Lichman. UCI Machine Learning Repository, 2013.Google Scholar
- Ulf Norell. Towards a Practical Programming Language Based on Dependent Type Theory, 2007.Google Scholar
- Seymour Papert. Some mathematical models of learning. In Proceedings of the Fourth London Symposium on Information Theory, 1961.Google Scholar
- David Pichardie and Yves Bertot. Formalizing convex hull algorithms. In International Conference on Theorem Proving in Higher Order Logics, pages 346–361. Springer, 2001. Google ScholarDigital Library
- Tahina Ramananandro, Paul Mountcastle, Benoît Meister, and Richard Lethin. A unified coq framework for verifying c programs with floatingpoint computations. In Proceedings of the 5th ACM SIGPLAN Conference on Certified Programs and Proofs, pages 15–26. ACM, 2016. Google ScholarDigital Library
- Frank Rosenblatt. The Perceptron – A Perceiving and Recognizing Automaton. Technical Report 85-460-1, Cornell Aeronautical Laboratory, 1957.Google Scholar
- Frank Rosenblatt. Principles of Neurodynamics; Perceptrons and the Theory of Brain Mechanisms. Spartan Books, 1962.Google Scholar
- The Coq Development Team. The Coq Proof Assistant. https://coq. inria.fr/, 2016. {Online; accessed 2-19-2016}. Dimitrios Vytiniotis, Thierry Coquand, and David Wahlstedt. Stop When You Are Almost-Full. In ITP. 2012.Google Scholar
Index Terms
- Verified perceptron convergence theorem
Recommendations
Global Convergence and Limit Cycle Behavior of Weights of Perceptron
In this paper, it is found that the weights of a perceptron are bounded for all initial weights if there exists a nonempty set of initial weights that the weights of the perceptron are bounded. Hence, the boundedness condition of the weights of the ...
Verified heap theorem prover by paramodulation
ICFP '12We present VeriStar, a verified theorem prover for a decidable subset of separation logic. Together with VeriSmall [3], a proved-sound Smallfoot-style program analysis for C minor, VeriStar demonstrates that fully machine-checked static analyses ...
Boundedness and Convergence of Split-Complex Back-Propagation Algorithm with Momentum and Penalty
This paper investigates the split-complex back-propagation algorithm with momentum and penalty for training complex-valued neural networks. Here the momentum are used to accelerate the convergence of the algorithm and the penalty are used to control the ...
Comments