Algorithm 862: MATLAB tensor classes for fast algorithm prototyping, ACM Trans. Math. Softw, vol.32, issue.4, pp.635-653, 2006. ,
Expressiveness of deep learning. Archive of Formal Proofs, 2016. ,
URL : https://hal.archives-ouvertes.fr/hal-01599172
An Isabelle formalization of the expressiveness of deep learning, 2016. ,
A formal proof of the expressiveness of deep learning, Interactive Theorem Proving (ITP 2017), vol.10499, pp.46-64, 2017. ,
URL : https://hal.archives-ouvertes.fr/hal-01599172
Formal proofs of transcendence for e and ? as an application of multivariate and symmetric polynomials, Certified Programs and Proofs (CPP 2016), pp.76-87, 2016. ,
URL : https://hal.archives-ouvertes.fr/hal-01240025
Canonical big operators, Theorem Proving in Higher Order Logics, vol.5170, pp.86-101, 2008. ,
URL : https://hal.archives-ouvertes.fr/inria-00331193
Syntactic foundations for machine learning, 2013. ,
Semi-intelligible Isar proofs from machine-generated proofs, J. Autom. Reasoning, vol.56, issue.2, pp.155-200, 2016. ,
URL : https://hal.archives-ouvertes.fr/hal-01211748
A learning-based fact selector for Isabelle/HOL, J. Autom. Reasoning, vol.57, issue.3, pp.219-244, 2016. ,
URL : https://hal.archives-ouvertes.fr/hal-01386986
Formalization of quantum protocols using Coq, Workshop on Quantum Physics and Logic (QPL 2015), vol.195, pp.71-83, 2015. ,
Fast LCF-style proof reconstruction for Z3, Interactive Theorem Proving (ITP 2010), vol.6172, pp.179-194, 2010. ,
The probability that a slightly perturbed numerical analysis problem is difficult, Math. Comput, vol.77, issue.263, pp.1559-1583, 2008. ,
The zero set of a polynomial, 2005. ,
A formulation of the simple theory of types, J. Symb. Log, vol.5, issue.2, pp.56-68, 1940. ,
Deep SimNets, Computer Vision and Pattern Recognition (CVPR 2016), pp.4782-4791, 2016. ,
On the expressive power of deep learning: A tensor analysis, Conference on Learning Theory (COLT 2016), JMLR Workshop and Conference Proceedings, vol.49, pp.698-728, 2016. ,
Convolutional rectifier networks as generalized tensor decompositions, International Conference on Machine Learning (ICML 2016, vol.48, pp.955-963, 2016. ,
Inductive bias of deep convolutional networks through pooling geometry, 2016. ,
Boosting dilated convolutional networks with mixed tensor decompositions, 2017. ,
, Edinburgh LCF: A Mechanised Logic of Computation, vol.78, 1979.
Towards abstract and executable multivariate polynomials in Isabelle, p.2014, 2014. ,
Train faster, generalize better: Stability of stochastic gradient descent, International Conference on Machine Learning (ICML 2016, vol.48, pp.1225-1234, 2016. ,
A HOL theory of Euclidean space, Theorem Proving in Higher Order Logics, vol.3603, pp.114-129, 2005. ,
Three chapters of measure theory in Isabelle/HOL, Interactive Theorem Proving (ITP 2011), vol.6898, pp.135-151, 2011. ,
, Gröbner bases theory. Archive of Formal Proofs, 2016.
Case studies in proof checking, 2007. ,
Deep learning without poor local minima, Advances in Neural Information Processing Systems (NIPS 2016), NIPS, vol.29, pp.586-594, 2016. ,
, Groups, rings and modules. Archive of Formal Proofs, 2004.
On the formal analysis of HMM using theorem proving, International Conference on Formal Engineering Methods (ICFEM 2014), vol.8829, pp.316-331, 2014. ,
On the volume of tubular neighborhoods of real algebraic varieties, Proc. Amer. Math. Soc, vol.143, issue.5, pp.1875-1889, 2015. ,
Z3: An efficient SMT solver, Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2008), vol.4963, pp.337-340, 2008. ,
Verified perceptron convergence theorem, Machine Learning and Programming Languages, pp.43-50, 2017. ,
, Concrete Semantics: With Isabelle/HOL, 2014.
, Isabelle/HOL: A Proof Assistant for Higher-Order Logic, vol.2283, 2002.
Three years of experience with Sledgehammer, a practical link between automatic and interactive theorem provers, International Workshop on the Implementation of Logics (IWIL-2010), vol.2, pp.1-11, 2012. ,
Source-level proof reconstruction for interactive theorem proving, Theorem Proving in Higher Order Logics, vol.4732, pp.232-245, 2007. ,
Sum-product networks: A new deep architecture, Uncertainty in Artificial Intelligence (UAI 2011), pp.337-346, 2011. ,
Tensor product of matrices. Archive of Formal Proofs, 2016. ,
Developing bug-free machine learning systems with formal mathematics, International Conference on Machine Learning, vol.70, pp.3047-3056, 2017. ,
Executable multivariate polynomials. Archive of Formal Proofs, 2010. ,
Matrices, Jordan normal forms, and spectral radius theory. Archive of Formal Proofs, 2015. ,
Deep learning and the information bottleneck principle, Information Theory Workshop (ITW 2015), pp.1-5, 2015. ,
Isar-A generic interpretative approach to readable formal proof documents, Theorem Proving in Higher Order Logics (TPHOLs '99), vol.1690, pp.167-184, 1999. ,