Improving stateful premise selection with transformers

DOI10.1007/978-3-030-81097-9_6zbMath1485.68286OpenAlexW3185544449MaRDI QIDQ2128800

Jürgen Schmidhuber, Michael Wand, Krsto Proroković

Publication date: 22 April 2022

Full work available at URL: https://doi.org/10.1007/978-3-030-81097-9_6

zbMATH Keywords

neural networksmachine learningpremise selection

Mathematics Subject Classification ID

Learning and adaptive systems in artificial intelligence (68T05) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Uses Software

• MPTP 0.2
• TPTP
• Mizar
• Flyspeck
• Metamath
• PyTorch
• XGBoost
• OpenNMT
• DeepMath
• ATPboost

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• MizAR 40 for Mizar 40
• Logic for programming, artificial intelligence, and reasoning. 17th international conference, LPAR-17, Yogyakarta, Indonesia, October 10--15, 2010. Proceedings
• MPTP 0.2: Design, implementation, and initial experiments
• Lightweight relevance filtering for machine-generated resolution problems
• ATPboost: learning premise selection in binary setting with ATP feedback
• A survey of languages for formalizing mathematics
• Learning-assisted automated reasoning with \(\mathsf{Flyspeck}\)
• The TPTP World – Infrastructure for Automated Reasoning
• Deep Network Guided Proof Search
• Sine Qua Non for Large Theory Reasoning

This page was built for publication: Improving stateful premise selection with transformers