DeepMath encodes conjectures and candidate premises with recurrent and convolutional neural architectures and learns whether a premise is useful for a target theorem.
Alexander A. Alemi, François Chollet, Niklas Eén, Geoffrey Irving, Christian Szegedy and Josef Urban trained neural sequence models to rank candidate premises for Mizar conjectures. The paper reported competitive large-scale premise-selection results using a two-stage architecture that avoided the hand-engineered features used by earlier state-of-the-art systems.
DeepMath encodes conjectures and candidate premises with recurrent and convolutional neural architectures and learns whether a premise is useful for a target theorem. The release turned large formal proof corpora into training data for neural relevance models, making representation learning a central component of automated theorem-proving pipelines.
Premise selection is a major bottleneck when automated provers operate over large mathematical libraries. DeepMath showed that neural models could learn useful relevance signals at this scale, supplying a methodological bridge from earlier feature-based learning to later neural proof-search guidance, graph representations and learned retrieval systems for formal mathematics.
Significance rationale: DeepMath was an important early large-scale application of deep neural sequence models to premise selection over formal mathematics. By learning directly from Mizar theorem and proof corpora without relying on the hand-engineered feature pipelines that dominated earlier systems, it helped establish deep learning as a practical representation-and-ranking approach for large-theory theorem proving and directly preceded neural guidance inside prover search.
—
—
The arXiv and NeurIPS research records establish the DeepMath premise-selection approach and the reported Mizar evaluation. This records the public research claim and does not imply independent reproduction of the reported metrics.
The public TensorFlow Deepmath repository retains the `deepmath/premises` implementation with neural premise-selection models. E3 denotes inspectable research code rather than independent reproduction of the published benchmark results.
No corrections recorded.
