Magnushammer: A Transformer-Based Approach to Premise Selection

Magnushammer: A Transformer-Based Approach to Premise Selection

8 March 2023

Szymon Tworkowski

Szymon Antoniak

Bartosz Piotrowski

Albert Qiaochu Jiang

Christian Szegedy

Lukasz Kuciñski

Papers citing "Magnushammer: A Transformer-Based Approach to Premise Selection"

11 / 11 papers shown

Title
Hierarchical Attention Generates Better Proofs Jianlong Chen Chao Li Yang Yuan Andrew Chi-Chih Yao AIMat LRM 26 0 0 27 Apr 2025
Alchemy: Amplifying Theorem-Proving Capability through Symbolic Mutation Shaonan Wu Shuai Lu Y. Gong Nan Duan Ping Wei AIMat 31 0 0 21 Oct 2024
LeanAgent: Lifelong Learning for Formal Theorem Proving Adarsh Kumarappan Mo Tiwari Peiyang Song Robert Joseph George Chaowei Xiao Anima Anandkumar CLL LLMAG LRM 50 8 0 08 Oct 2024
Can Transformers Do Enumerative Geometry? Baran Hashemi Roderic G. Corominas Alessandro Giacchetto 32 2 0 27 Aug 2024
Draft, Sketch, and Prove: Guiding Formal Theorem Provers with Informal Proofs Albert Q. Jiang Sean Welleck Jin Peng Zhou Wenda Li Jiacheng Liu M. Jamnik Timothée Lacroix Yuhuai Wu Guillaume Lample AIMat 58 154 0 21 Oct 2022
Autoformalization with Large Language Models Yuhuai Wu Albert Q. Jiang Wenda Li M. Rabe Charles Staats M. Jamnik Christian Szegedy AI4CE 108 107 0 25 May 2022
Formal Mathematics Statement Curriculum Learning Stanislas Polu Jesse Michael Han Kunhao Zheng Mantas Baksys Igor Babuschkin Ilya Sutskever AIMat 61 115 0 03 Feb 2022
BEIR: A Heterogenous Benchmark for Zero-shot Evaluation of Information Retrieval Models Nandan Thakur Nils Reimers Andreas Rucklé Abhishek Srivastava Iryna Gurevych VLM 229 720 0 17 Apr 2021
The Pile: An 800GB Dataset of Diverse Text for Language Modeling Leo Gao Stella Biderman Sid Black Laurence Golding Travis Hoppe ... Horace He Anish Thite Noa Nabeshima Shawn Presser Connor Leahy AIMat 236 1,508 0 31 Dec 2020
Scaling Laws for Neural Language Models Jared Kaplan Sam McCandlish T. Henighan Tom B. Brown B. Chess R. Child Scott Gray Alec Radford Jeff Wu Dario Amodei 220 3,054 0 23 Jan 2020
MizAR 40 for Mizar 40 C. Kaliszyk Josef Urban VLM AI4CE LRM AIMat 54 131 0 10 Oct 2013