Fetching the paper…
Reading the bibliography…
Noisy data, non-convex objectives, model misspecification, and numerical instability can all cause undesired behaviors in machine learning systems.
Edinburgh lcf: a mechanised logic of computation
Gordon, Michael JC · 1979
Earlier work this paper cites.
The calculus of constructions
Coquand, Thierry and Huet, Gérard · 1988
Earlier work this paper cites.
Pvs: A prototype verification system
Owre, Sam, Rushby, John M, and Shankar, Natarajan · 1992
Earlier work this paper cites.
An overview of the mizar project
Rudnicki, Piotr · 1992
Earlier work this paper cites.
Introduction to hol a theorem proving environment for higher order logic
Gordon, Michael JC and Melham, Tom F · 1993
Earlier work this paper cites.
Hol light: A tutorial introduction
Harrison, John · 1996
Earlier work this paper cites.
Accuracy and stability of numerical algorithms
Higham, Nicholas J · 2002
Earlier work this paper cites.
Isabelle/HOL: a proof assistant for higher-order logic , volume 2283
Nipkow, Tobias, Paulson, Lawrence C, and Wenzel, Markus · 2002
Earlier work this paper cites.
Floating-point verification using theorem proving
Harrison, John · 2006
Earlier work this paper cites.
Formal proof–the four-color theorem
Gonthier, Georges · 2008
Cited alongside, same era.
sel4: Formal verification of an os kernel
Klein, Gerwin, Elphinstone, Kevin, Heiser, Gernot, Andronick, June, Cock, David, Derrin, Philip, Elkaduwe, Dhammika, Engelhardt, Kai, Kolanski, Rafal, Norrish, Michael, et al · 2009
Cited alongside, same era.
Formal verification of a realistic compiler
Leroy, Xavier · 2009
Cited alongside, same era.
Theano: a CPU and GPU math expression compiler
Bergstra, J., Breuleux, O., Bastien, F., Lamblin, P., Pascanu, R., Desjardins, G., Turian, J., Warde-Farley, D., and Bengio, Y · 2010
Cited alongside, same era.
Eigen v3
Guennebaud, Gaël, Jacob, Benoît, et al · 2010
Cited alongside, same era.
The bedrock structured programming system: Combining generative metaprogramming and hoare logic in an extensible program verifier
Chlipala, Adam · 2013
Cited alongside, same era.
TensorFlow: Large-scale machine learning on heterogeneous systems, 2015
Abadi, Martín, Agarwal, Ashish, Barham, Paul, Brevdo, Eugene, Chen, Zhifeng, Citro, Craig, Corrado, Greg S., Davis, Andy, Dean, Jeffrey, Devin, Matthieu, Ghemawat, Sanjay, Goodfellow, Ian, Harp, Andrew, Irving, Geoffrey, Isard, Michael, Jia, Yangqing, Jozefowicz, Rafal, Kaiser, Lukasz, Kudlur, Manjunath, Levenberg, Josh, Mané, Dan, Monga, Rajat, Moore, Sherry, Murray, Derek, Olah, Chris, Schuster, Mike, Shlens, Jonathon, Steiner, Benoit, Sutskever, Ilya, Talwar, Kunal, Tucker, Paul, Vanhoucke, Vincent, Vasudevan, Vijay, Viégas, Fernanda, Vinyals, Oriol, Warden, Pete, Wattenberg, Martin, Wicke, Martin, Yu, Yuan, and Zheng, Xiaoqiang · 2015
Later among the works it cites.
Verified compilation of floating-point computations
Boldo, Sylvie, Jourdan, Jacques-Henri, Leroy, Xavier, and Melquiond, Guillaume · 2015
Later among the works it cites.
Using crash hoare logic for certifying the fscq file system
Chen, Haogang, Ziegler, Daniel, Chajed, Tej, Chlipala, Adam, Kaashoek, M Frans, and Zeldovich, Nickolai · 2015
Later among the works it cites.
The Lean theorem prover (system description)
de Moura, Leonardo, Kong, Soonho, Avigad, Jeremy, Van Doorn, Floris, and von Raumer, Jakob · 2015
Later among the works it cites.
alphaXiv searches the wider corpus for related work and actual follow-ups.
alphaXiv is searching for related work…
A machine-checked proof of the odd order theorem
Gonthier, Georges, Asperti, Andrea, Avigad, Jeremy, Bertot, Yves, Cohen, Cyril, Garillot, François, Le Roux, Stéphane, Mahboubi, Assia, O’Connor, Russell, Biha, Sidi Ould, et al · 2013
Cited alongside, same era.
Auto-encoding variational Bayes
Kingma, D. P. and Welling, M · 2014
Cited alongside, same era.
Adam: A method for stochastic optimization
Kingma, Diederik and Ba, Jimmy · 2014
Cited alongside, same era.
Hales, Thomas, Adams, Mark, Bauer, Gertrud, Dang, Dat Tat, Harrison, John, Hoang, Truong Le, Kaliszyk, Cezary, Magron, Victor, McLaughlin, Sean, Nguyen, Thang Tat, et al · 2015
Later among the works it cites.
Gradient estimation using stochastic computation graphs
Schulman, John, Heess, Nicolas, Weber, Theophane, and Abbeel, Pieter · 2015
Later among the works it cites.
The Coq proof assistant reference manual: Version 8.5
Coq Development Team · 2016
Later among the works it cites.
A unified coq framework for verifying c programs with floating-point computations
Ramananandro, Tahina, Mountcastle, Paul, Meister, Benoît, and Lethin, Richard · 2016
Later among the works it cites.