Portrait de Xavier Glorot n'est pas disponible

Xavier Glorot

Alumni

Publications

Proving Theorems using Incremental Learning and Hindsight Experience Replay
Maxwell Crouse
Eser Aygün
Laurent Orseau
Bassem Makni
Vernon Ralph Austel
Cristina Cornelio
Shajith Ikbal
Stephen McAleer
Vlad Firoiu
Pavan Kapanipathi
Lei Zhang
Ndivhuwo Makondo
Shibl Mourad
Traditional automated theorem provers for first-order logic depend on speed-optimized search and many handcrafted heuristics that are design… (voir plus)ed to work best over a wide range of domains. Machine learning approaches in literature either depend on these traditional provers to bootstrap themselves or fall short on reaching comparable performance. In this paper, we propose a general incremental learning algorithm for training domain specific provers for first-order logic without equality, based only on a basic given-clause algorithm, but using a learned clause-scoring function. Clauses are represented as graphs and presented to transformer networks with spectral features. To address the sparsity and the initial lack of training data as well as the lack of a natural curriculum, we adapt hindsight experience replay to theorem proving, so as to be able to learn even when no proof can be found. We show that provers trained this way can match and sometimes surpass state-of-the-art traditional provers on the TPTP dataset in terms of both quantity and quality of the proofs.
Training a First-Order Theorem Prover from Synthetic Data
Vlad Firoiu
Eser Aygün
Laurent Orseau
Lei Zhang
Shibl Mourad
SPE: Symmetrical Prompt Enhancement for Factual Knowledge Retrieval
James M. Crawford
Matthew L. Ginsberg
Jacob Devlin
Ming-Wei Chang
Kenton Lee
Alex Graves
Abdel rahman Mohamed
Adi Haviv
Jonathan Berant
Amir Globerson
Chloe Kiddon
Pedro M. Domingos
Brian Lester
Rami Al-rfou'
Noah Constant. 2021
Weizhe Yuan … (voir 6 de plus)
Jinlan Fu
Zhengbao Jiang
Xiao Liu
Yanan Zheng
Zhengxiao Du
Ming Ding
Pretrained language models (PLMs) have 001 been shown to accumulate factual knowledge 002 from their unsupervised pretraining proce-003 dure… (voir plus)s (Petroni et al., 2019). Prompting is an 004 effective way to query such knowledge from 005 PLMs. Recently, continuous prompt methods 006 have been shown to have a larger potential 007 than discrete prompt methods in generating ef-008 fective queries (Liu et al., 2021a). However, 009 these methods do not consider symmetry of 010 the task. In this work, we propose Symmet-011 rical Prompt Enhancement (SPE), a continu-012 ous prompt-based method for fact retrieval that 013 leverages the symmetry of the task. Our results 014 on LAMA, a popular fact retrieval dataset, 015 show significant improvement of SPE over pre-016 vious prompt methods
Learning to Prove from Synthetic Theorems
Eser Aygün
Vlad Firoiu
Laurent Orseau
Shibl Mourad
A major challenge in applying machine learning to automated theorem proving is the scarcity of training data, which is a key ingredient in t… (voir plus)raining successful deep learning models. To tackle this problem, we propose an approach that relies on training with synthetic theorems, generated from a set of axioms. We show that such theorems can be used to train an automated prover and that the learned prover transfers successfully to human-generated theorems. We demonstrate that a prover trained exclusively on synthetic theorems can solve a substantial fraction of problems in TPTP, a benchmark dataset that is used to compare state-of-the-art heuristic provers. Our approach outperforms a model trained on human-generated problems in most axiom sets, thereby showing the promise of using synthetic data for this task.
Learning representations of Logical Formulae using Graph Neural Networks
Eser Aygün
Shibl Mourad
Pushmeet Kohli
We explore the use of Graph Neural Networks(GNNs) for learning representations of propositional and first-order logical formulae. Tradition… (voir plus)al non-graphical based approaches like CNNs and LSTMs do not exploit invariant properties like variable renaming and order invariance predominantly present in logical formulae. In this work, we explicitly try to encode these logical invariances using GNNs. We use the task of entailment proposed in Evans et al. [2018] for propositional logic. We also explore our approach for the task of proof length prediction in first-order logic. We use the Mizar-40 dataset to evaluate several representation learning approaches for proof length prediction task. We observe that GNNs significantly outperform the other traditional approaches on both these tasks.
Theano: A Python framework for fast computation of mathematical expressions
Rami Al-Rfou
Amjad Almahairi
Christof Angermueller
Frédéric Bastien
Justin Bayer
Anatoly Belikov
Alexander Belopolsky
Josh Bleecher Snyder
Pierre-Luc Carrier
Paul Christiano
Myriam Côté
Yann N. Dauphin
Julien Demouth
Sander Dieleman
Ziye Fan
Mathieu Germain
Matt Graham
Balázs Hidasi
Arjun Jain
Kai Jia
Mikhail Korobov
Vivek Kulkarni
Pascal Lamblin
Eric Larsen
Sean Lee
Simon Lefrancois
Jesse A. Livezey
Cory Lorenz
Jeremiah Lowin
Qianli Ma
Robert T. McGibbon
Mehdi Mirza
Alberto Orlandi
Christopher Pal
Colin Raffel
Daniel Renshaw
Matthew Rocklin
Adriana Romero
Markus Roth
Peter Sadowski
John Salvatier
Jan Schlüter
John Schulman
Gabriel Schwartz
Iulian Vlad Serban
Samira Shabanian
Sigurd Spieckermann
S. Ramana Subramanyam
Gijs van Tulder
Sebastian Urban
Dustin J. Webb
Matthew Willson
Lijun Xue
Theano is a Python library that allows to define, optimize, and evaluate mathematical expressions involving multi-dimensional arrays efficie… (voir plus)ntly. Since its introduction, it has been one of the most used CPU and GPU mathematical compilers - especially in the machine learning community - and has shown steady performance improvements. Theano is being actively and continuously developed since 2008, multiple frameworks have been built on top of it and it has been used to produce many state-of-the-art machine learning models. The present article is structured as follows. Section I provides an overview of the Theano software and its community. Section II presents the principal features of Theano and how to use them, and compares them with other similar projects. Section III focuses on recently-introduced functionalities and improvements. Section IV compares the performance of Theano against Torch7 and TensorFlow on several machine learning models. Section V discusses current limitations of Theano and potential ways of improving it.