Thor: Wielding Hammers to Integrate Language Models and Automated Theorem Provers

22 May 2022

Albert Q. Jiang

Papers citing "Thor: Wielding Hammers to Integrate Language Models and Automated Theorem Provers"

22 / 22 papers shown

Title
APOLLO: Automated LLM and Lean Collaboration for Advanced Formal Reasoning Azim Ospanov Farzan Farnia Roozbeh Yousefzadeh LRM 26 0 0 09 May 2025
Towards Automated Scoping of AI for Social Good Projects Jacob Emmerson Rayid Ghani Zheyuan Ryan Shi 103 0 0 28 Apr 2025
Hierarchical Attention Generates Better Proofs Jianlong Chen Chao Li Yang Yuan Andrew Chi-Chih Yao AIMat LRM 31 0 0 27 Apr 2025
Generative Evaluation of Complex Reasoning in Large Language Models Haowei Lin X. Wang Ruilin Yan Baizhou Huang Haotian Ye Jianhua Zhu Zihao Wang James Y. Zou Jianzhu Ma Yitao Liang ReLM ELM LRM 130 0 0 03 Apr 2025
Activation Steering in Neural Theorem Provers Shashank Kirtania LLMSV 126 0 0 21 Feb 2025
Simplifying Formal Proof-Generating Models with ChatGPT and Basic Searching Techniques Sangjun Han Taeil Hur Youngmi Hur Kathy Sangkyung Lee Myungyoon Lee Hyojae Lim 107 0 0 20 Feb 2025
Building A Proof-Oriented Programmer That Is 64% Better Than GPT-4o Under Data Scarcity Dylan Zhang Justin Wang Tianran Sun 36 0 0 17 Feb 2025
Mathematical Language Models: A Survey W. Liu Hanglei Hu Jie Zhou Yuyang Ding Junsong Li ... Mengliang He Qin Chen Bo Jiang Aimin Zhou Liang He LRM 79 12 0 03 Jan 2025
Rango: Adaptive Retrieval-Augmented Proving for Automated Software Verification Kyle Thompson Nuno Saavedra Pedro Carrott Kevin Fisher Alex Sanchez-Stern Yuriy Brun J. Ferreira Sorin Lerner E. First LRM 100 1 0 18 Dec 2024
Pantograph: A Machine-to-Machine Interaction Interface for Advanced Theorem Proving, High Level Reasoning, and Data Extraction in Lean 4 Leni Aniva Chuyue Sun Brando Miranda Clark W. Barrett Sanmi Koyejo 38 4 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 70 8 0 08 Oct 2024
AutoVerus: Automated Proof Generation for Rust Code Chenyuan Yang Xuheng Li Md Rakib Hossain Misu Jianan Yao Weidong Cui ... Jacob R. Lorch Shuai Lu Fan Yang Ziqiao Zhou Shan Lu 27 7 0 19 Sep 2024
miniCTX: Neural Theorem Proving with (Long-)Contexts Jiewen Hu Thomas Zhu Sean Welleck AIMat 58 6 0 05 Aug 2024
Proving Theorems Recursively Haiming Wang Huajian Xin Zhengying Liu Wenda Li Yinya Huang ... Zhicheng YANG Jing Tang Jian Yin Zhenguo Li Xiaodan Liang LRM 28 10 0 23 May 2024
Exploring the Limits of Fine-grained LLM-based Physics Inference via Premise Removal Interventions Jordan Meadows Tamsin James André Freitas ReLM LRM AI4CE 31 1 0 29 Apr 2024
TRIGO: Benchmarking Formal Mathematical Proof Reduction for Generative Language Models Jing Xiong Jianhao Shen Ye Yuan Haiming Wang Yichun Yin ... Yinya Huang Chuanyang Zheng Xiaodan Liang Ming Zhang Qun Liu AIMat LRM 16 15 0 16 Oct 2023
FIMO: A Challenge Formal Dataset for Automated Theorem Proving Chengwu Liu Jianhao Shen Huajian Xin Zhengying Liu Ye Yuan ... Chuanyang Zheng Yichun Yin Lin Li Ming Zhang Qun Liu AIMat AI4CE 27 31 0 08 Sep 2023
Progressive-Hint Prompting Improves Reasoning in Large Language Models Chuanyang Zheng Zhengying Liu Enze Xie Zhenguo Li Yu Li LLMAG ReLM LRM 19 100 0 19 Apr 2023
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 63 157 0 21 Oct 2022
Solving Quantitative Reasoning Problems with Language Models Aitor Lewkowycz Anders Andreassen David Dohan Ethan Dyer Henryk Michalewski ... Theo Gutman-Solo Yuhuai Wu Behnam Neyshabur Guy Gur-Ari Vedant Misra ReLM ELM LRM 51 739 0 29 Jun 2022
Formal Mathematics Statement Curriculum Learning Stanislas Polu Jesse Michael Han Kunhao Zheng Mantas Baksys Igor Babuschkin Ilya Sutskever AIMat 73 115 0 03 Feb 2022
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 248 1,986 0 31 Dec 2020