certigrad - Bug-free machine learning on stochastic computation graphs

  •        5

Specifically, Certigrad is a system for optimizing over stochastic computation graphs, that we debugged systematically in the Lean Theorem Prover, and ultimately proved correct in terms of the underlying mathematics. Stochastic computation graphs extend the computation graphs that underlie systems like TensorFlow and Theano by allowing nodes to represent random variables and by defining the loss function to be the expected value of the sum of the leaf nodes over all the random choices in the graph. Certigrad allows users to construct arbitrary stochastic computation graphs out of the primitives that we provide. The main purpose of the system is to take a program describing a stochastic computation graph and to run a randomized algorithm (stochastic backpropagation) that, in expectation, samples the gradients of the loss function with respect to the parameters.

https://github.com/dselsam/certigrad

Tags
Implementation
License
Platform

   




Related Projects

lean - Lean Theorem Prover

  •    C++

Stable and nightly binary releases of Lean are available on the homepage. For building Lean from source, see the build instructions.

deepmath - Experiments towards neural network theorem proving

  •    C++

The Deepmath project seeks to improve automated theorem proving using deep learning and other machine learning techniques. Deepmath is a collaboration between Google Research and several universities. The source code in this repository is not an official Google product, but is a research collaboration with external research teams.

cakeml - CakeML: A Verified Implementation of ML

  •    Standard

CakeML is a verified implementation of a significant subset of Standard ML. The source and proofs for CakeML are developed in the HOL4 theorem prover. We use the latest development version of HOL4, which we build on PolyML 5.7. Example build instructions can be found in build-instructions.sh.

FStar - Verification system for effectful programs

  •    OCaml

The F* tutorial provides a first taste of verified programming in F*, explaining things by example. The F* wiki contains additional, usually more in-depth, technical documentation on F*.

HOL - Canonical sources for HOL4 theorem-proving system

  •    Standard

This is the distribution directory for the Kananaskis release of HOL4. See http://hol-theorem-prover.org for online resources. The following is a brief listing of what's available in the distribution.


simple_bayes - A Naive Bayes machine learning implementation in Elixir.

  •    Elixir

A Naive Bayes machine learning implementation in Elixir. In machine learning, naive Bayes classifiers are a family of simple probabilistic classifiers based on applying Bayes' theorem with strong (naive) independence assumptions between the features.

juice - The Hacker's Machine Learning Engine (formerly known as leaf)

  •    Rust

Juice is a open Machine Learning Framework for hackers to build classical, deep or hybrid machine learning applications. It was inspired by the brilliant people behind TensorFlow, Torch, Caffe, Rust and numerous research papers and brings modularity, performance and portability to deep learning. Juice has one of the simplest APIs, is lean and tries to introduce minimal technical debt to your stack.

coq - Coq is a formal proof management system

  •    OCaml

Coq is a formal proof management system. It provides a formal language to write mathematical definitions, executable algorithms and theorems together with an environment for semi-interactive development of machine-checked proofs. Download the pre-built packages of the latest release for Windows and MacOS; read the help page on how to install Coq with OPAM; or refer to the INSTALL file for the procedure to install from source.

leaf - Open Machine Intelligence Framework for Hackers. (GPU/CPU)

  •    Rust

Leaf is a open Machine Learning Framework for hackers to build classical, deep or hybrid machine learning applications. It was inspired by the brilliant people behind TensorFlow, Torch, Caffe, Rust and numerous research papers and brings modularity, performance and portability to deep learning. Leaf has one of the simplest APIs, is lean and tries to introduce minimal technical debt to your stack.

Swift-Brain - Artificial intelligence/machine learning data structures and Swift algorithms for future iOS development

  •    Swift

The first neural network / machine learning library written in Swift. This is a project for AI algorithms in Swift for iOS and OS X development. This project includes algorithms focused on Bayes theorem, neural networks, SVMs, Matrices, etc.. Feel free to contribute.

node-facenet - Solve face verification, recognition and clustering problems: A TensorFlow backed FaceNet implementation for Node

  •    TypeScript

A TensorFlow backed FaceNet implementation for Node.js, which can solve face verification, recognition and clustering problems. FaceNet is a deep convolutional network designed by Google, trained to solve face verification, recognition and clustering problem with efficiently at scale.

HOL theorem-proving system

  •    

HOL is a system for proving theorems in Higher Order Logic. It comes with a large variety of existing theories formalising various parts of mathematics and theoretical computer science.

keras-contrib - Keras community contributions

  •    Python

This library is the official extension repository for the python deep learning library Keras. It contains additional layers, activations, loss functions, optimizers, etc. which are not yet available within Keras itself. All of these additional modules can be used in conjunction with core Keras models and modules. As the community contributions in Keras-Contrib are tested, used, validated, and their utility proven, they may be integrated into the Keras core repository. In the interest of keeping Keras succinct, clean, and powerfully simple, only the most useful contributions make it into Keras. This contribution repository is both the proving ground for new functionality, and the archive for functionality that (while useful) may not fit well into the Keras paradigm.

practical-machine-learning-with-python - Master the essential skills needed to recognize and solve complex real-world problems with Machine Learning and Deep Learning by leveraging the highly popular Python Machine Learning Eco-system

  •    Jupyter

"Data is the new oil" is a saying which you must have heard by now along with the huge interest building up around Big Data and Machine Learning in the recent past along with Artificial Intelligence and Deep Learning. Besides this, data scientists have been termed as having "The sexiest job in the 21st Century" which makes it all the more worthwhile to build up some valuable expertise in these areas. Getting started with machine learning in the real world can be overwhelming with the vast amount of resources out there on the web. "Practical Machine Learning with Python" follows a structured and comprehensive three-tiered approach packed with concepts, methodologies, hands-on examples, and code. This book is packed with over 500 pages of useful information which helps its readers master the essential skills needed to recognize and solve complex problems with Machine Learning and Deep Learning by following a data-driven mindset. By using real-world case studies that leverage the popular Python Machine Learning ecosystem, this book is your perfect companion for learning the art and science of Machine Learning to become a successful practitioner. The concepts, techniques, tools, frameworks, and methodologies used in this book will teach you how to think, design, build, and execute Machine Learning systems and projects successfully.

Math-of-Machine-Learning-Course-by-Siraj - Implements common data science methods and machine learning algorithms from scratch in python

  •    Jupyter

This repository was initially created to submit machine learning assignments for Siraj Raval's online machine learning course. The purpose of the course was to learn how to implement the most common machine learning algorithms from scratch (without using machine learning libraries such as tensorflow, PyTorch, scikit-learn, etc). Although that course has ended now, I am continuing to learn data science and machine learning from other sources such as Coursera, online blogs, and attending machine learning lectures at University of Toronto. Sticking to the theme of implementing machine learning algortihms from scratch, I will continue to post detailed notebooks in python here as I learn more.

Cosette - Cosette is an automated SQL solver powered by Coq/Lean and Rosette.

  •    Lean

Cosette is a language, and an automated solver for reasoning SQL equivalences.

mlpack - mlpack: a scalable C++ machine learning library --

  •    C++

mlpack is an intuitive, fast, and flexible C++ machine learning library with bindings to other languages. It is meant to be a machine learning analog to LAPACK, and aims to implement a wide array of machine learning methods and functions as a "swiss army knife" for machine learning researchers. In addition to its powerful C++ interface, mlpack also provides command-line programs and Python bindings. Citations are beneficial for the growth and improvement of mlpack.

schnitzelpress - A lean, mean blogging machine for hackers and fools.

  •    Ruby

A lean, mean blogging machine for hackers and fools.

vim-config - Lean mean (Neo)Vim machine, carefully crafted with :heart: Use with Neovim v0

  •    Vim

Lean mean Neo/vim machine, 30-45ms startup time. Best with Neovim or Vim 8 with +python3 extensions enabled.