# Towards Neural Theorem Proving at Scale

arXiv: https://arxiv.org/abs/1807.08204 · HTML: https://mlsanity.com/paper/1807.08204/

## Key facts

- Cited by 11 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 21 Jul 2018.

## Built on by (most cited first, 11 of 11)

- [Relational Concept Bottleneck Models](https://mlsanity.com/paper/2308.11991/) (2023)
- [Neuro-Symbolic Temporal Point Processes](https://mlsanity.com/paper/2406.03914/) (2024)
- [Evaluating Step-by-Step Reasoning through Symbolic Verification](https://mlsanity.com/paper/2212.08686/) (2022)
- [Relational Reasoning Networks](https://mlsanity.com/paper/2106.00393/) (2021)
- [Principled and Efficient Motif Finding for Structure Learning of Lifted Graphical Models](https://mlsanity.com/paper/2302.04599/) (2023)
- [Neural Theorem Proving for Verification Conditions: A Real-World Benchmark](https://mlsanity.com/paper/2601.18944/) (2026)
- [Structured Q-learning For Antibody Design](https://mlsanity.com/paper/2209.04698/) (2022)
- [Parallel Neurosymbolic Integration with Concordia](https://mlsanity.com/paper/2306.00480/) (2023)
- [Semantic Reasoning with Differentiable Graph Transformations](https://mlsanity.com/paper/2107.09579/) (2021)
- [AGEL-Comp: A Neuro-Symbolic Framework for Compositional Generalization in Interactive Agents](https://mlsanity.com/paper/2604.26522/) (2026)
- [Generating Graph-Like Logical Rules for Knowledge Graph Reasoning via Diffusion Models](https://mlsanity.com/paper/2605.30747/) (2026)

## Abstract (arXiv)

Neural models combining representation learning and reasoning in an end-to-end trainable manner are receiving increasing interest. However, their use is severely limited by their computational complexity, which renders them unusable on real world datasets. We focus on the Neural Theorem Prover (NTP) model proposed by Rockt"aschel and Riedel (2017), a continuous relaxation of the Prolog backward chaining algorithm where unification between terms is replaced by the similarity between their embedding representations. For answering a given query, this model needs to consider all possible proof paths, and then aggregate results - this quickly becomes infeasible even for small Knowledge Bases (KBs). We observe that we can accurately approximate the inference process in this model by considering only proof paths associated with the highest proof scores. This enables inference and learning on previously impracticable KBs.