HyperTree Proof Search for Neural Theorem Proving

23 May 2022

Papers citing "HyperTree Proof Search for Neural Theorem Proving"

50 / 96 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 12 0 0 16 May 2025
APOLLO: Automated LLM and Lean Collaboration for Advanced Formal Reasoning Azim Ospanov Farzan Farnia Roozbeh Yousefzadeh LRM 29 0 0 09 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 52 0 0 07 May 2025
HyperTree Planning: Enhancing LLM Reasoning via Hierarchical Thinking Runquan Gui Zhilin Wang Jun Wang Chi Ma Huiling Zhen M. Yuan Jianye Hao Defu Lian Enhong Chen Feng Wu LRM 141 0 0 05 May 2025
Hierarchical Attention Generates Better Proofs Jianlong Chen Chao Li Yang Yuan Andrew Chi-Chih Yao AIMat LRM 33 0 0 27 Apr 2025
Neural Theorem Proving: Generating and Structuring Proofs for Formal Verification Balaji Rao William Eiers Carlo Lipizzi 37 0 0 23 Apr 2025
Kimina-Prover Preview: Towards Large Formal Reasoning Models with Reinforcement Learning Haiming Wang Mert Unsal Xiaohan Lin Mantas Baksys Jiaheng Liu ... Zhouliang Yu Zhilin Wang Zhilin Yang Zhengying Liu Jia-Nan Li AIMat ReLM AI4TS LRM 54 8 0 15 Apr 2025
A Short Survey on Small Reasoning Models: Training, Inference, Applications and Research Directions Chengyu Wang Taolin Zhang Richang Hong Jun Huang ReLM LRM 45 1 0 12 Apr 2025
Leanabell-Prover: Posttraining Scaling in Formal Reasoning Jingyuan Zhang Qi Wang Xingguang Ji Yong-Jin Liu Yang Yue Fuzheng Zhang Di Zhang Guorui Zhou Kun Gai LRM 41 4 0 08 Apr 2025
A Survey on Mathematical Reasoning and Optimization with Large Language Models Ali Forootani OffRL LRM AI4CE 45 0 0 22 Mar 2025
Local Look-Ahead Guidance via Verifier-in-the-Loop for Automated Theorem Proving Sara Rajaee Kumar Pratik Gabriele Cesa Arash Behboodi OffRL LRM 61 0 0 12 Mar 2025
From Hypothesis to Publication: A Comprehensive Survey of AI-Driven Research Support Systems Zekun Zhou Xiaocheng Feng L. Huang Xiachong Feng Ziyun Song ... Baoxin Wang Dayong Wu Guoping Hu Ting Liu Bing Qin AI4TS 74 1 0 03 Mar 2025
CuDIP: Enhancing Theorem Proving in LLMs via Curriculum Learning-based Direct Preference Optimization Shuming Shi Ruobing Zuo Gaolei He Jianlin Wang Chenyang Xu Zhengfeng Yang 60 0 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 129 0 0 20 Feb 2025
Generating Millions Of Lean Theorems With Proofs By Exploring State Transition Graphs David Yin Jing Gao 42 0 0 16 Feb 2025
Position: Multimodal Large Language Models Can Significantly Advance Scientific Reasoning Yibo Yan Shen Wang Jiahao Huo Jingheng Ye Zhendong Chu Xuming Hu Philip S. Yu Carla P. Gomes B. Selman Qingsong Wen LRM 127 9 0 05 Feb 2025
The Karp Dataset Mason DiCicco Eamon Worden Conner Olsen Nikhil Gangaram Daniel Reichman Neil T. Heffernan ReLM LRM 56 0 0 24 Jan 2025
Mathematical Language Models: A Survey Wei 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
Formal Mathematical Reasoning: A New Frontier in AI Kaiyu Yang Gabriel Poesia Jingxuan He Wenda Li Kristin Lauter Swarat Chaudhuri Dawn Song LRM AI4CE 82 21 0 20 Dec 2024
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
Proposing and solving olympiad geometry with guided tree search Chi Zhang Jiajun Song Siyu Li Yitao Liang Yuxi Ma Wei Wang Yixin Zhu Song-Chun Zhu AIMat LRM 76 3 0 14 Dec 2024
Formal Theorem Proving by Rewarding LLMs to Decompose Proofs Hierarchically Kefan Dong Arvind V. Mahankali Tengyu Ma ReLM LRM 30 6 0 04 Nov 2024
Next-Token Prediction Task Assumes Optimal Data Ordering for LLM Training in Proof Generation Chenyang An Shima Imani Feng Yao Chengyu Dong Ali Abbasi ... Samuel Buss Jingbo Shang Gayathri Mahalingam Pramod Sharma Maurice Diesendruck LRM 31 1 0 30 Oct 2024
Scaling LLM Inference with Optimized Sample Compute Allocation Kexun Zhang Shang Zhou Danqing Wang William Yang Wang Lei Li 50 9 0 29 Oct 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 40 4 0 21 Oct 2024
Alchemy: Amplifying Theorem-Proving Capability through Symbolic Mutation Shaonan Wu Shuai Lu Y. Gong Nan Duan Ping Wei AIMat 45 0 0 21 Oct 2024
Proof Flow: Preliminary Study on Generative Flow Network Language Model Tuning for Formal Reasoning Matthew Ho Vincent Zhu Xiaoyin Chen Moksh Jain Nikolay Malkin Edwin Zhang LRM 37 2 0 17 Oct 2024
3D-Prover: Diversity Driven Theorem Proving With Determinantal Point Processes Sean Lamont Christian J. Walder Amir Dezfouli Paul Montague Michael Norrish 26 0 0 14 Oct 2024
Global Lyapunov functions: a long-standing open problem in mathematics, with symbolic transformers Alberto Alfarano François Charton Amaury Hayat 23 12 0 10 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 72 8 0 08 Oct 2024
ImProver: Agent-Based Automated Proof Optimization Riyaz Ahuja Jeremy Avigad Prasad Tetali Sean Welleck LLMAG 34 2 0 07 Oct 2024
SubgoalXL: Subgoal-based Expert Learning for Theorem Proving Xueliang Zhao Lin Zheng Haige Bo Changran Hu Urmish Thakker Lingpeng Kong LRM 40 2 0 20 Aug 2024
QEDCartographer: Automating Formal Verification Using Reward-Free Reinforcement Learning Alex Sanchez-Stern Abhishek Varghese Zhanna Kaufman Dylan Zhang Talia Ringer Yuriy Brun 18 2 0 17 Aug 2024
DeepSeek-Prover-V1.5: Harnessing Proof Assistant Feedback for Reinforcement Learning and Monte-Carlo Tree Search Huajian Xin Z. Z. Ren Junxiao Song Zhihong Shao Wanjia Zhao ... Dejian Yang Zhibin Gou Z. F. Wu Fuli Luo Chong Ruan AIMat LRM 47 51 0 15 Aug 2024
Learning the Simplicity of Scattering Amplitudes Clifford Cheung Aurélien Dersy Matthew D. Schwartz 27 3 0 08 Aug 2024
miniCTX: Neural Theorem Proving with (Long-)Contexts Jiewen Hu Thomas Zhu Sean Welleck AIMat 71 6 0 05 Aug 2024
LEAN-GitHub: Compiling GitHub LEAN repositories for a versatile LEAN prover Zijian Wu Jiayu Wang Dahua Lin Kai-xiang Chen 27 13 0 24 Jul 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 47 19 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
Towards Automated Functional Equation Proving: A Benchmark Dataset and A Domain-Specific In-Context Agent Mahdi Buali R. Hoehndorf 24 0 0 05 Jul 2024
TheoremLlama: Transforming General-Purpose LLMs into Lean4 Experts Ruida Wang Jipeng Zhang Yizhen Jia Rui Pan Shizhe Diao Renjie Pi Tong Zhang LRM 35 16 0 03 Jul 2024
Learning Formal Mathematics From Intrinsic Motivation Gabriel Poesia David Broman Nick Haber Noah D. Goodman LRM 38 9 0 30 Jun 2024
Towards Large Language Model Aided Program Refinement YuFan Cai Zhe Hou Xiaokun Luan David Miguel Sanan Baena Yun Lin Jun Sun Jin Song Dong 40 4 0 26 Jun 2024
From Decoding to Meta-Generation: Inference-time Algorithms for Large Language Models Sean Welleck Amanda Bertsch Matthew Finlayson Hailey Schoelkopf Alex Xie Graham Neubig Ilia Kulikov Zaid Harchaoui 33 50 0 24 Jun 2024
Proving Olympiad Algebraic Inequalities without Human Demonstrations Chenrui Wei Mengzhou Sun Wei Wang LRM 42 6 0 20 Jun 2024
miniCodeProps: a Minimal Benchmark for Proving Code Properties Evan Lohn Sean Welleck 32 2 0 16 Jun 2024
DafnyBench: A Benchmark for Formal Software Verification Chloe Loughridge Qinyi Sun Seth Ahrenbach Federico Cassano Chuyue Sun Ying Sheng Anish Mudide Md Rakib Hossain Misu Nada Amin Max Tegmark ALM AI4CE 46 8 0 12 Jun 2024
Lean Workbook: A large-scale Lean problem set formalized from natural language math problems Huaiyuan Ying Zijian Wu Yihan Geng Jiayu Wang Dahua Lin Kai Chen 43 26 0 06 Jun 2024
Autoformalizing Euclidean Geometry Logan Murphy Kaiyu Yang Jialiang Sun Zhaoyu Li A. Anandkumar Xujie Si 37 3 0 27 May 2024
Limits of Deep Learning: Sequence Modeling through the Lens of Complexity Theory Nikola Zubić Federico Soldá Aurelio Sulser Davide Scaramuzza LRM BDL 52 5 0 26 May 2024