Differences

This shows you the differences between two versions of the page.

--- ml:automatic_theorem_proving [2024/06/02 05:08] – [Neural Theorem Proving] jmflanig
+++ ml:automatic_theorem_proving [2025/10/07 14:31] (current) – [Autoformalization] jmflanig
@@ Line 4: / Line 4: @@
   * [[https://arxiv.org/pdf/2205.15231.pdf|Jordan Meadows & André Freitas 2022 - A Survey in Mathematical Language Processing]]
   * **[[https://arxiv.org/pdf/2212.10535.pdf|Lu et al 2022 - A Survey of Deep Learning for Mathematical Reasoning]]**
-  * [[https://arxiv.org/pdf/2404.09939|Li et al 2024 - Survey on Deep Learning for Theorem Proving]]
+  * **[[https://arxiv.org/pdf/2404.09939|Li et al 2024 - Survey on Deep Learning for Theorem Proving]]**
   * Formalizing mathematics
     * [[http://cl-informatik.uibk.ac.at/users/cek/docs/20/ckfr-cicm20.pdf|Kaliszyk & Rabe 2020 - A Survey of Languages for Formalizing Mathematics]]
+  * Autoformalization
+    * [[https://arxiv.org/pdf/2505.23486|Weng et al 2025 - Autoformalization in the Era of Large Language Models: A Survey]]
 ===== Papers =====
@@ Line 18: / Line 20: @@
 ==== Neural Theorem Proving ====
+  * **Overviews**
+    * [[https://arxiv.org/pdf/2404.09939|Li et al 2024 - A Survey on Deep Learning for Theorem Proving]]
+  * **Bibliographies**
+    * [[https://github.com/zhaoyu-li/DL4TP|Deep Learning for Theorem Proving (DL4TP)]]
   * **Step-by-step Proof Generation**
-    * [[https://arxiv.org/pdf/2009.03393|Polu & Sutskever 2020 - Generative Language Modeling for Automated Theorem Proving]] Maintains a proof tree with a queue of open goals, and tries to expand the goal with the highest LLM logprob to reach it. Metamath formalization language. Introduces WebMath pre-training.
+    * GPT-f: [[https://arxiv.org/pdf/2009.03393|Polu & Sutskever 2020 - Generative Language Modeling for Automated Theorem Proving]] Maintains a proof tree with a queue of open goals, and tries to expand the goal with the highest LLM logprob to reach it. Metamath formalization language. Introduces WebMath pre-training.
-    * [[https://arxiv.org/pdf/2102.06203|Han et al 2021 - Proof Artifact Co-training for Theorem Proving with Language Models]] Uses a best-first search algorithm: maintains a priority queue of search nodes, of tactic state (partial proof) and metadata, sorted by heuristic score.  For Lean.  Introduces the LeanStep dataset to to predict the next tactic give a goal state, built from mathlib.
+    * [[https://arxiv.org/pdf/2102.06203|Han et al 2021 - Proof Artifact Co-training for Theorem Proving with Language Models]] Generates the next tactic using an LLM. Uses a best-first search algorithm: maintains a priority queue of search nodes, of tactic state (partial proof) and metadata, sorted by LLM heuristic score.  For Lean.  Introduces the LeanStep dataset to to predict the next tactic give a goal state, built from mathlib.  Uses an interesting PACT pretraining dataset (sec 3.2).
     * [[https://aitp-conference.org/2021/abstract/paper_17.pdf|Jiang et al 2021 - LISA: Language models of ISAbelle proofs]]
     * [[https://arxiv.org/pdf/2202.01344.pdf|Polu et al 2022 - Formal Mathematics Statement Curriculum Learning]]
-    * [[https://arxiv.org/pdf/2205.10893|Jiang et al 2022 - Thor: Wielding Hammers to Integrate Language Models and Automated Theorem Provers]]
+    * [[https://arxiv.org/pdf/2205.10893|Jiang et al 2022 - Thor: Wielding Hammers to Integrate Language Models and Automated Theorem Provers]] Uses automated theorem prover premise selection (hammers) to retrieve the relevant premises, and then uses LLMs as in GPT-f ([[https://arxiv.org/pdf/2009.03393|Polu & Sutskever 2020]]).  Increases success rate on PISA from 39.0% to 57.0%.
     * [[https://arxiv.org/pdf/2205.11491|Lample et al 2022 - HyperTree Proof Search for Neural Theorem Proving]]
     * [[https://arxiv.org/pdf/2306.15626|Yang et al 2023 - LeanDojo: Theorem Proving with Retrieval-Augmented Language Models]]
     * [[https://aclanthology.org/2023.acl-long.706.pdf|Wang et al 2023 - DT-Solver: Automated Theorem Proving with Dynamic-Tree Sampling Guided by Proof-level Value Function]]
     * [[https://arxiv.org/pdf/2310.00656|Wang et al 2023 - LEGO-Prover: Neural Theorem Proving with Growing Libraries]]
+    * [[https://mathai2023.github.io/papers/29.pdf|Thakur et al 2023 - A Language-Agent Approach to Formal Theorem-Proving]]
+    * [[https://arxiv.org/pdf/2405.14414|Wang et al 2024 - Proving Theorems Recursively]]
   * **Construction All-In-One Go**
     * [[https://arxiv.org/pdf/2210.12283|Jiang et al 2022 - Draft, Sketch, and Prove: Guiding Formal Theorem Provers with Informal Proofs]]
     * [[https://arxiv.org/pdf/2305.16366|Zhao et al 2023 - Decomposing the Enigma: Subgoal-based Demonstration Learning for Formal Theorem Proving]]
     * [[https://arxiv.org/pdf/2303.04910|First et al 2023 - Baldur: Whole-Proof Generation and Repair with Large Language Models]]
+  * [[https://arxiv.org/pdf/2310.18457|Welleck & Saha 2023 - LLMSTEP: LLM proofstep suggestions in Lean]]
+  * [[https://arxiv.org/pdf/2412.20735|Li et al 2024 - HunyuanProver: A Scalable Data Synthesis Framework and Guided Tree Search for Automated Theorem Proving]]
+  * [[https://arxiv.org/pdf/2502.00212|Dong & Ma 2025 - STP: Self-play LLM Theorem Provers with Iterative Conjecturing and Proving]]
+  * [[https://arxiv.org/pdf/2505.20613|Shen et al 2025 - REAL-Prover: Retrieval Augmented Lean Prover for Mathematical Reasoning]]
@@ Line 57: / Line 69: @@
       * Paper: [[http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.100.2087&rep=rep1&type=pdf|Urban et al 2007 - Combining Mizar and TPTP Semantic Presentation Tools]] {{papers:combining_mizar_and_tptp_semantic_presentation_and_verification_tools.pdf|pdf}}
       * Dataset: [[https://www.tptp.org/MizarTPTP/|website]]
+  * [[https://arxiv.org/pdf/2407.11214|Tsoukalas et al 2024 - PUTNAMBENCH: Evaluating Neural Theorem-Provers on the Putnam Mathematical Competition]]
 ===== Formalizing Mathematics =====
@@ Line 67: / Line 80: @@
     * **[[https://drops.dagstuhl.de/opus/volltexte/2021/13906/pdf/LIPIcs-ITP-2021-11.pdf|Byliński et al 2021 - Syntactic-Semantic Form of Mizar Articles]]** Gives an overview and a good historical introduction in the intro.
     * [[https://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.368.286&rep=rep1&type=pdf|Grzegorz Bancerek 2006 - Automatic Translation in Formalized Mathematics]]
+===== Autoformalization =====
+  * Overviews
+    * [[https://leanprover.zulipchat.com/user_uploads/3121/lWKHE1MCcJ1ZwiF2poPoJckC/Autoformalization.pdf|Szegedy 2019 - A Promising Path Towards Autoformalization and General Artificial Intelligence]] Great
+    * [[https://arxiv.org/pdf/2311.00007|Avigad et al 2023 - Mathematics and the Formal Turn]] Great overview of the reasons to autoformalize mathematics
+    * [[https://arxiv.org/pdf/2505.23486|Weng et al 2025 - Autoformalization in the Era of Large Language Models: A Survey]]
 === Informal Math to Formal Math Parsing ===
@@ Line 119: / Line 138: @@
 ===== People =====
+  * [[https://www.andrew.cmu.edu/user/avigad/papers.html|Jeremy Avigad]]
   * [[https://scholar.google.com/citations?user=bp68Q1kAAAAJ&hl=en|Cezary Kaliszyk]] [[http://cl-informatik.uibk.ac.at/users/cek/|homepage]]
   * [[https://scholar.google.com/citations?user=3QeF7mAAAAAJ&hl=en|Christian Szegedy]] (at Google)