24.4k citations · 66.7k across the 24 of their papers we have counts for
28 papers
Definition Grounding in Theory-Level Auto-formalization
Leyan Pan, Christian Szegedy, Frederick Rajasekaran +3
LLM-based auto-formalization systems can now generate formally verified Lean code at unprecedented rates. However, a formalization advances mathematical research only when further…
Don't Trust: Verify -- Grounding LLM Quantitative Reasoning with Autoformalization
Jin Peng Zhou, Charles Staats, Wenda Li +3
Large language models (LLM), such as Google's Minerva and OpenAI's GPT families, are becoming increasingly capable of solving mathematical quantitative reasoning problems. However,…
Magnushammer: A Transformer-Based Approach to Premise Selection
Maciej Mikuła, Szymon Tworkowski, Szymon Antoniak +7
This paper presents a novel approach to premise selection, a crucial reasoning task in automated theorem proving. Traditionally, symbolic methods that rely on extensive domain know…
Autoformalization with Large Language Models
Yuhuai Wu, Albert Q. Jiang, Wenda Li +4
Autoformalization is the process of automatically translating from natural language mathematics to formal specifications and proofs. A successful autoformalization system could adv…
Memorizing Transformers
Yuhuai Wu, Markus N. Rabe, DeLesley Hutchins +1
Language models typically need to be trained or finetuned in order to acquire new knowledge, which involves updating their weights. We instead envision language models that can sim…
Hierarchical Transformers Are More Efficient Language Models
Piotr Nawrot, Szymon Tworkowski, Michał Tyrolski +4
Transformer models yield impressive results on many NLP and sequence modeling tasks. Remarkably, Transformers can handle long sequences which allows them to produce long coherent o…
LIME: Learning Inductive Bias for Primitives of Mathematical Reasoning
Yuhuai Wu, Markus Rabe, Wenda Li +3
While designing inductive bias in neural architectures has been widely studied, we hypothesize that transformer networks are flexible enough to learn inductive bias from suitable g…
Mathematical Reasoning via Self-supervised Skip-tree Training
Markus N. Rabe, Dennis Lee, Kshitij Bansal +1
We examine whether self-supervised language modeling applied to mathematical formulas enables logical reasoning. We suggest several logical reasoning tasks that can be used to eval…
Mathematical Reasoning in Latent Space
Dennis Lee, Christian Szegedy, Markus N. Rabe +2
We design and conduct a simple experiment to study whether neural networks can perform several steps of approximate reasoning in a fixed dimensional latent space. The set of rewrit…
Learning to Reason in Large Theories without Imitation
Kshitij Bansal, Christian Szegedy, Markus N. Rabe +2
In this paper, we demonstrate how to do automated theorem proving in the presence of a large knowledge base of potential premises without learning from human proofs. We suggest an…
Graph Representations for Higher-Order Logic and Theorem Proving
Aditya Paliwal, Sarah Loos, Markus Rabe +2
This paper presents the first use of graph neural networks (GNNs) for higher-order proof search and demonstrates that GNNs can improve upon state-of-the-art results in this domain.…
HOList: An Environment for Machine Learning of Higher-Order Theorem Proving
Kshitij Bansal, Sarah M. Loos, Markus N. Rabe +2
We present an environment, benchmark, and deep learning driven automated theorem prover for higher-order logic. Higher-order interactive theorem provers enable the formalization of…
Text Embeddings for Retrieval From a Large Knowledge Base
Tolgahan Cakaloglu, Christian Szegedy, Xiaowei Xu
Text embedding representing natural language documents in a semantic vector space can be used for document retrieval using nearest neighbor lookup. In order to study the feasibilit…
HolStep: A Machine Learning Dataset for Higher-order Logic Theorem Proving
Cezary Kaliszyk, François Chollet, Christian Szegedy
Large computer-understandable proofs consist of millions of intermediate logical steps. The vast majority of such steps originate from manually selected and manually guided heurist…
Deep Network Guided Proof Search
Sarah Loos, Geoffrey Irving, Christian Szegedy +1
Deep learning techniques lie at the heart of several significant AI advances in recent years including object recognition and detection, image captioning, machine translation, spee…
DeepMath - Deep Sequence Models for Premise Selection
Alex A. Alemi, Francois Chollet, Niklas Een +3
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…
Inception-v4, Inception-ResNet and the Impact of Residual Connections on Learning
Christian Szegedy, Sergey Ioffe, Vincent Vanhoucke +1
Very deep convolutional networks have been central to the largest advances in image recognition performance in recent years. One example is the Inception architecture that has been…
Rethinking the Inception Architecture for Computer Vision
Christian Szegedy, Vincent Vanhoucke, Sergey Ioffe +2
Convolutional networks are at the core of most state-of-the-art computer vision solutions for a wide variety of tasks. Since 2014 very deep convolutional networks started to become…
Large Scale Business Discovery from Street Level Imagery
Qian Yu, Christian Szegedy, Martin C. Stumpe +4
Search with local intent is becoming increasingly useful due to the popularity of the mobile device. The creation and maintenance of accurate listings of local businesses worldwide…
SSD: Single Shot MultiBox Detector
Wei Liu, Dragomir Anguelov, Dumitru Erhan +4
We present a method for detecting objects in images using a single deep neural network. Our approach, named SSD, discretizes the output space of bounding boxes into a set of defaul…
Batch Normalization: Accelerating Deep Network Training by Reducing Internal Covariate Shift
Sergey Ioffe, Christian Szegedy
Training Deep Neural Networks is complicated by the fact that the distribution of each layer's inputs changes during training, as the parameters of the previous layers change. This…
Training Deep Neural Networks on Noisy Labels with Bootstrapping
Scott Reed, Honglak Lee, Dragomir Anguelov +3
Current state-of-the-art deep learning systems for visual object recognition and detection use purely supervised training with regularization such as dropout to avoid overfitting.…
Explaining and Harnessing Adversarial Examples
Ian J. Goodfellow, Jonathon Shlens, Christian Szegedy
Several machine learning models, including neural networks, consistently misclassify adversarial examples---inputs formed by applying small but intentionally worst-case perturbatio…
Scalable, High-Quality Object Detection
Christian Szegedy, Scott Reed, Dumitru Erhan +2
Current high-quality object detection approaches use the scheme of salience-based object proposal methods followed by post-classification using deep convolutional features. This sp…