Francois Chollet
Deep learning researcher. Author of Keras.
Research Areas
Authored Publications
Google Publications
Other Publications
Sort By
Preview abstract
Large computer-understandable proofs consist of millions of intermediate logical
steps. The vast majority of such steps originate from manually selected and manually
guided heuristics applied to intermediate goals. So far, machine learning has
generally not been used to filter or generate these steps. In this paper, we introduce
a new dataset based on Higher-Order Logic (HOL) proofs, for the purpose of developing
new machine learning-based theorem-proving strategies. We make this
dataset publicly available under the BSD license. We propose various machine
learning tasks that can be performed on this dataset, and discuss their significance
for theorem proving. We also benchmark a set of baseline deep learning models
suited for the tasks (including convolutional neural networks and recurrent neural
networks). The results of our baseline models shows the promise of applying deep
learning to HOL theorem proving.
View details
Preview abstract
Depthwise separable convolutions reduce the number of parameters and computation used in convolutional operations while increasing representational efficiency. They have been shown to be successful in image classification models, both in obtaining better models than previously possible for a given parameter count (the Xception architecture) and considerably reducing the number of parameters required to perform at a given level (the MobileNets family of architectures). Recently, convolutional sequence-to-sequence networks have been applied to machine translation tasks with good results. In this work, we study how depthwise separable convolutions can be applied to neural machine translation. We introduce a new architecture inspired by Xception and ByteNet, called SliceNet, which enables a significant reduction of the parameter count and amount of computation needed to obtain results like ByteNet, and, with a similar parameter count, achieves new state-of-the-art results. In addition to showing that depthwise separable convolutions perform well for machine translation, we investigate the architectural changes that they enable: we observe that thanks to depthwise separability, we can increase the length of convolution windows, removing the need for filter dilation. We also introduce a new "super-separable" convolution operation that further reduces the number of parameters and computational cost for obtaining state-of-the-art results.
View details
Preview abstract
We study the effectiveness of neural sequence models for premise selection in automated theorem proving, one of the main bottlenecks in the formalization of mathematics. We propose a two stage approach for this task that yields good results for the premise selection task on the Mizar corpus while avoiding the hand-engineered features of existing state-of-the-art models. To our knowledge, this is the first time deep learning has been applied to theorem proving.
View details
No Results Found