HyperTree Proof Search for Neural Theorem Proving

23 May 2022

Papers citing "HyperTree Proof Search for Neural Theorem Proving"

47 / 97 papers shown

Title
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
Proving Theorems Recursively Haiming Wang Huajian Xin Zhengying Liu Wenda Li Yinya Huang ... Zhicheng YANG Jing Tang Jian Yin Zhenguo Li Xiaodan Liang LRM 41 12 0 23 May 2024
DeepSeek-Prover: Advancing Theorem Proving in LLMs through Large-Scale Synthetic Data Huajian Xin Daya Guo Zhihong Shao Z. Z. Ren Qihao Zhu Bo Liu Chong Ruan Wenda Li Xiaodan Liang SyDa 45 64 0 23 May 2024
ATG: Benchmarking Automated Theorem Generation for Generative Language Models Xiaohan Lin Qingxing Cao Yinya Huang Zhicheng YANG Zhengying Liu Zhenguo Li Xiaodan Liang 26 4 0 05 May 2024
Towards Neural Synthesis for SMT-Assisted Proof-Oriented Programming Saikat Chakraborty Gabriel Ebner Siddharth Bhat Sarah Fakhoury Sakina Fatima Shuvendu K. Lahiri Nikhil Swamy 48 15 0 03 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 41 1 0 29 Apr 2024
Lean Copilot: Large Language Models as Copilots for Theorem Proving in Lean Peiyang Song Kaiyu Yang A. Anandkumar 42 25 0 18 Apr 2024
A Survey on Deep Learning for Theorem Proving Zhaoyu Li Jialiang Sun Logan Murphy Qidong Su Zenan Li Xian Zhang Kaiyu Yang Xujie Si LRM 56 21 0 15 Apr 2024
Learn from Failure: Fine-Tuning LLMs with Trial-and-Error Data for Intuitionistic Propositional Logic Proving Chenyang An Zhibo Chen Qihao Ye Emily First Letian Peng Jiayun Zhang Zihan Wang Sorin Lerner Jingbo Shang LRM 42 7 0 10 Apr 2024
LeanReasoner: Boosting Complex Logical Reasoning with Lean Dongwei Jiang Marcio Fonseca Shay B. Cohen LRM 28 14 0 20 Mar 2024
Learning Guided Automated Reasoning: A Brief Survey Lasse Blaauwbroek David M. Cerna Thibault Gauthier Jan Jakubruv C. Kaliszyk Martin Suda Josef Urban LRM 35 4 0 06 Mar 2024
VerMCTS: Synthesizing Multi-Step Programs using a Verifier, a Large Language Model, and Tree Search David Brandfonbrener Simon Henniger Sibi Raja Tarun Prasad Chloe Loughridge ... Sabrina Ruixin Hu Jianang Yang William E. Byrd Robert Zinkov Nada Amin LRM 59 5 0 13 Feb 2024
EvoGPT-f: An Evolutionary GPT Framework for Benchmarking Formal Math Languages Johnathan Mercer 39 0 0 12 Feb 2024
InternLM-Math: Open Math Large Language Models Toward Verifiable Reasoning Huaiyuan Ying Shuo Zhang Linyang Li Zhejian Zhou Yunfan Shao ... Hang Yan Xipeng Qiu Jiayu Wang Kai-xiang Chen Dahua Lin ReLM LRM 34 70 0 09 Feb 2024
Graph2Tac: Online Representation Learning of Formal Math Concepts Lasse Blaauwbroek Miroslav Olšák Jason Rute F. I. S. Massolo Jelle Piepenbrock Vasily Pestun 17 10 0 05 Jan 2024
Enhancing Neural Theorem Proving through Data Augmentation and Dynamic Sampling Method Rahul Vishwakarma Subhankar Mishra AIMat 19 1 0 20 Dec 2023
Modeling Complex Mathematical Reasoning via Large Language Model based MathAgent Haoran Liao Qinyi Du Shaohua Hu Hao He Yanyan Xu Jidong Tian Yaohui Jin LRM AI4CE 32 1 0 14 Dec 2023
Game Solving with Online Fine-Tuning Ti-Rong Wu Hung Guei Ting Han Wei Chung-Chin Shih Jui-Te Chin I-Chen Wu OnRL 19 1 0 13 Nov 2023
Finding Increasingly Large Extremal Graphs with AlphaZero and Tabu Search Abbas Mehrabian Ankit Anand Hyunjik Kim Nicolas Sonnerat Matej Balog ... Laurent Orseau Joonkyung Lee Anurag Murty Naredla Doina Precup Adam Zsolt Wagner 21 7 0 06 Nov 2023
FormalGeo: An Extensible Formalized Framework for Olympiad Geometric Problem Solving Xiaokai Zhang Na Zhu Yiming He Jia Zou Qike Huang ... Cheng Qin Zhen Zeng Shaorong Xie Xiangfeng Luo Tuo Leng AIMat AI4CE 27 4 0 27 Oct 2023
Llemma: An Open Language Model For Mathematics Zhangir Azerbayev Hailey Schoelkopf Keiran Paster Marco Dos Santos Stephen Marcus McAleer Albert Q. Jiang Jia Deng Stella Biderman Sean Welleck CLL 34 273 0 16 Oct 2023
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 24 15 0 16 Oct 2023
The Search-and-Mix Paradigm in Approximate Nash Equilibrium Algorithms Xiaotie Deng Dongchen Li Hanyu Li 11 0 0 12 Oct 2023
An In-Context Learning Agent for Formal Theorem-Proving Amitayush Thakur George Tsoukalas Yeming Wen Jimmy Xin Swarat Chaudhuri LLMAG 25 24 0 06 Oct 2023
Notes on a Path to AI Assistance in Mathematical Reasoning Alex Kontorovich 17 0 0 04 Oct 2023
SNIP: Bridging Mathematical Symbolic and Numeric Realms with Unified Pre-training Kazem Meidani Parshin Shojaee Chandan K. Reddy A. Farimani 23 18 0 03 Oct 2023
LEGO-Prover: Neural Theorem Proving with Growing Libraries Haiming Wang Huajian Xin Chuanyang Zheng Lin Li Zhengying Liu ... Enze Xie Jian Yin Zhenguo Li Heng Liao Xiaodan Liang LRM 39 63 0 01 Oct 2023
The Mathematical Game Marc Pierre Quentin Cohen-Solal Tristan Cazenave 11 1 0 22 Sep 2023
Provably safe systems: the only path to controllable AGI Max Tegmark Steve Omohundro 16 21 0 05 Sep 2023
Monte-Carlo Tree Search for Multi-Agent Pathfinding: Preliminary Results Yelisey Pitanov Alexey Skrynnik Anton Andreychuk Konstantin Yakovlev Aleksandr I. Panov 29 2 0 25 Jul 2023
LeanDojo: Theorem Proving with Retrieval-Augmented Language Models Kaiyu Yang Aidan M. Swope Alex Gu Rahul Chalamala Peiyang Song Shixing Yu Saad Godil R. Prenger Anima Anandkumar RALM 19 213 0 27 Jun 2023
Decomposing the Enigma: Subgoal-based Demonstration Learning for Formal Theorem Proving Xueliang Zhao Wenda Li Lingpeng Kong 38 28 0 25 May 2023
Progressive-Hint Prompting Improves Reasoning in Large Language Models Chuanyang Zheng Zhengying Liu Enze Xie Zhenguo Li Yu Li LLMAG ReLM LRM 41 103 0 19 Apr 2023
Tool Learning with Foundation Models Yujia Qin Shengding Hu Yankai Lin Weize Chen Ning Ding ... Cheng Yang Tongshuang Wu Heng Ji Zhiyuan Liu Maosong Sun 42 200 0 17 Apr 2023
Baldur: Whole-Proof Generation and Repair with Large Language Models E. First M. Rabe Talia Ringer Yuriy Brun 67 94 0 08 Mar 2023
Magnushammer: A Transformer-Based Approach to Premise Selection Maciej Mikuła Szymon Tworkowski Szymon Antoniak Bartosz Piotrowski Albert Qiaochu Jiang Jinyi Zhou Christian Szegedy Lukasz Kuciñski Piotr Milo's Yuhuai Wu 47 42 0 08 Mar 2023
CoProver: A Recommender System for Proof Construction Eric Yeh Briland Hitaj S. Owre Maena Quemener N. Shankar 28 4 0 01 Mar 2023
ProofNet: Autoformalizing and Formally Proving Undergraduate-Level Mathematics Zhangir Azerbayev Bartosz Piotrowski Hailey Schoelkopf Edward W. Ayers Dragomir R. Radev J. Avigad AIMat 16 70 0 24 Feb 2023
Deep Generative Symbolic Regression with Monte-Carlo-Tree-Search Pierre-Alexandre Kamienny Guillaume Lample Sylvain Lamprier M. Virgolin 34 25 0 22 Feb 2023
Augmented Language Models: a Survey Grégoire Mialon Roberto Dessì Maria Lomeli Christoforos Nalmpantis Ramakanth Pasunuru ... Jane Dwivedi-Yu Asli Celikyilmaz Edouard Grave Yann LeCun Thomas Scialom LRM KELM 47 368 0 15 Feb 2023
A Survey of Deep Learning for Mathematical Reasoning Pan Lu Liang Qiu Wenhao Yu Sean Welleck Kai-Wei Chang ReLM LRM 46 139 0 20 Dec 2022
LEMMA: Bootstrapping High-Level Mathematical Reasoning with Learned Symbolic Abstractions Zhening Li Gabriel Poesia Omar Costilla-Reyes Noah D. Goodman Armando Solar-Lezama 21 7 0 16 Nov 2022
Towards a Mathematics Formalisation Assistant using Large Language Models Ayush Agrawal Siddhartha Gadgil Navin Goyal Ashvni Narayanan Anand Tadipatri 27 15 0 14 Nov 2022
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 73 158 0 21 Oct 2022
The Alignment Problem from a Deep Learning Perspective Richard Ngo Lawrence Chan Sören Mindermann 68 183 0 30 Aug 2022
Formal Mathematics Statement Curriculum Learning Stanislas Polu Jesse Michael Han Kunhao Zheng Mantas Baksys Igor Babuschkin Ilya Sutskever AIMat 91 118 0 03 Feb 2022
Self-Supervised Learning to Prove Equivalence Between Straight-Line Programs via Rewrite Rules Steve Kommrusch Monperrus Martin L. Pouchet 19 9 0 22 Sep 2021