Draft, Sketch, and Prove: Guiding Formal Theorem Provers with Informal Proofs

21 October 2022

Albert Q. Jiang

Papers citing "Draft, Sketch, and Prove: Guiding Formal Theorem Provers with Informal Proofs"

31 / 31 papers shown

Title
MPS-Prover: Advancing Stepwise Theorem Proving by Multi-Perspective Search and Data Curation Zhenwen Liang Linfeng Song Yang Li Tao Yang Feng Zhang Haitao Mi Dong Yu LRM 7 0 0 16 May 2025
Beyond Theorem Proving: Formulation, Framework and Benchmark for Formal Problem-Solving Qi Liu Xinhao Zheng Renqiu Xia Xingzhi Qi Qinxiang Cao Junchi Yan AIMat 50 0 0 07 May 2025
CombiBench: Benchmarking LLM Capability for Combinatorial Mathematics J. Liu Xiaohan Lin Jonas Bayer Yael Dillies Weijie Jiang ... Zhengfeng Yang J. Zhang Lihong Zhi J. Li Zhengying Liu 104 0 0 06 May 2025
Towards Automated Scoping of AI for Social Good Projects Jacob Emmerson Rayid Ghani Zheyuan Ryan Shi 139 0 0 28 Apr 2025
APE-Bench I: Towards File-level Automated Proof Engineering of Formal Math Libraries Huajian Xin Luming Li Xiaoran Jin Jacques Fleuriot Wenda Li AIMat 52 0 0 27 Apr 2025
Hierarchical Attention Generates Better Proofs Jianlong Chen Chao Li Yang Yuan Andrew Chi-Chih Yao AIMat LRM 33 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 154 0 0 03 Apr 2025
LeanProgress: Guiding Search for Neural Theorem Proving via Proof Progress Prediction Suozhi Huang Peiyang Song Robert Joseph George Anima Anandkumar AI4TS LRM 44 2 0 25 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 124 0 0 20 Feb 2025
Formalizing Complex Mathematical Statements with LLMs: A Study on Mathematical Definitions Lan Zhang Marco Valentino André Freitas 44 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
Alchemy: Amplifying Theorem-Proving Capability through Symbolic Mutation Shaonan Wu Shuai Lu Y. Gong Nan Duan Ping Wei AIMat 40 0 0 21 Oct 2024
Herald: A Natural Language Annotated Lean 4 Dataset Guoxiong Gao Yutong Wang Jiedong Jiang Qi Gao Zihan Qin Tianyi Xu Bin Dong 83 3 0 09 Oct 2024
miniCTX: Neural Theorem Proving with (Long-)Contexts Jiewen Hu Thomas Zhu Sean Welleck AIMat 68 6 0 05 Aug 2024
PutnamBench: Evaluating Neural Theorem-Provers on the Putnam Mathematical Competition George Tsoukalas Jasper Lee John Jennings Jimmy Xin Michelle Ding Michael Jennings Amitayush Thakur Swarat Chaudhuri LRM AIMat 41 18 0 15 Jul 2024
Lean-STaR: Learning to Interleave Thinking and Proving Haohan Lin Zhiqing Sun Yiming Yang Sean Welleck ReLM LRM 72 23 0 14 Jul 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 33 11 0 23 May 2024
ChartX & ChartVLM: A Versatile Benchmark and Foundation Model for Complicated Chart Reasoning Renqiu Xia Bo-Wen Zhang Hancheng Ye Xiangchao Yan Qi Liu ... Min Dou Botian Shi Junchi Yan Junchi Yan Yu Qiao LRM 57 52 0 19 Feb 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 18 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
Neural Algorithmic Reasoning Without Intermediate Supervision Gleb Rodionov Liudmila Prokhorenkova OffRL LRM OOD 26 10 0 23 Jun 2023
Faith and Fate: Limits of Transformers on Compositionality Nouha Dziri Ximing Lu Melanie Sclar Xiang Lorraine Li Liwei Jian ... Sean Welleck Xiang Ren Allyson Ettinger Zaïd Harchaoui Yejin Choi ReLM LRM 30 328 0 29 May 2023
Logic-LM: Empowering Large Language Models with Symbolic Solvers for Faithful Logical Reasoning Liangming Pan Alon Albalak Xinyi Wang William Yang Wang ReLM LRM AI4CE 49 232 0 20 May 2023
A Survey of Safety and Trustworthiness of Large Language Models through the Lens of Verification and Validation Xiaowei Huang Wenjie Ruan Wei Huang Gao Jin Yizhen Dong ... Sihao Wu Peipei Xu Dengyu Wu André Freitas Mustafa A. Mustafa ALM 36 82 0 19 May 2023
Is deep learning a useful tool for the pure mathematician? G. Williamson FedML 21 13 0 25 Apr 2023
ReCEval: Evaluating Reasoning Chains via Correctness and Informativeness Archiki Prasad Swarnadeep Saha Xiang Zhou Mohit Bansal LRM 24 44 0 21 Apr 2023
Progressive-Hint Prompting Improves Reasoning in Large Language Models Chuanyang Zheng Zhengying Liu Enze Xie Zhenguo Li Yu Li LLMAG ReLM LRM 32 102 0 19 Apr 2023
Autoformalization with Large Language Models Yuhuai Wu Albert Q. Jiang Wenda Li M. Rabe Charles Staats M. Jamnik Christian Szegedy AI4CE 110 156 0 25 May 2022
Formal Mathematics Statement Curriculum Learning Stanislas Polu Jesse Michael Han Kunhao Zheng Mantas Baksys Igor Babuschkin Ilya Sutskever AIMat 81 116 0 03 Feb 2022