Decomposing the Enigma: Subgoal-based Demonstration Learning for Formal
Theorem Proving

Decomposing the Enigma: Subgoal-based Demonstration Learning for Formal Theorem Proving

25 May 2023

Lingpeng Kong

Papers citing "Decomposing the Enigma: Subgoal-based Demonstration Learning for Formal Theorem Proving"

13 / 13 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
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
Beyond Autoregression: Discrete Diffusion for Complex Reasoning and Planning Jiacheng Ye Jiahui Gao Shansan Gong Lin Zheng Xin Jiang Z. Li Lingpeng Kong DiffM LRM 37 15 0 18 Oct 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 29 18 0 15 Jul 2024
Lean-STaR: Learning to Interleave Thinking and Proving Haohan Lin Zhiqing Sun Yiming Yang Sean Welleck ReLM LRM 65 23 0 14 Jul 2024
Baldur: Whole-Proof Generation and Repair with Large Language Models E. First M. Rabe Talia Ringer Yuriy Brun 59 90 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 37 41 0 08 Mar 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 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 156 0 25 May 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
Fantastically Ordered Prompts and Where to Find Them: Overcoming Few-Shot Prompt Order Sensitivity Yao Lu Max Bartolo Alastair Moore Sebastian Riedel Pontus Stenetorp AILaw LRM 274 1,114 0 18 Apr 2021
What Makes Good In-Context Examples for GPT- $3$ ? Jiachang Liu Dinghan Shen Yizhe Zhang Bill Dolan Lawrence Carin Weizhu Chen AAML RALM 275 1,296 0 17 Jan 2021
Asymmetric self-play for automatic goal discovery in robotic manipulation OpenAI OpenAI Matthias Plappert Raul Sampedro Tao Xu Ilge Akkaya ... Hyeonwoo Noh Lilian Weng Qiming Yuan Casey Chu Wojciech Zaremba SSL 60 76 0 13 Jan 2021