type
status
date
slug
summary
tags
category
icon
password
Property
Mar 4, 2024 03:40 PM
Problem Statement
- Formalizing mathematical proofs typically relies on human experts to transcribe intricate mathematical concepts into structured formal languages verifiable by interactive theorem prover like Lean or Isabelle. This process, while robust, is often labor-intensive and demands a high level of expertise.
- LM的出现，two predominant paradigms have been extensively explored：1）step-by-step proof generation；2）construct entire proofs in a single decoding process
文章1：Draft, Sketch, and Prove: Guiding Formal Theorem Provers with Informal Proofs
BackGround
Formal Proof Automation 最近几年遇到的较为挑战性任务。
- formal data的缺乏（需要大量专家经验的标注）→ 所以就有大量方法来进行合成数据，如自监督，RL等
- 尽管informal mathematical data在网上大量充斥着，然而产生的错误的reasoning step很难检测到
Method
他们借助informal mathematical proofs来作为连接手段。
先prompt LM生成informal proof，再生成formal sketch；最后由外部tool补全detailed proofs。
Results
文章2：LEGO-Prover: Neural Theorem Proving with Growing Libraries
数学的发展并不仅仅是简单的重复尝试解题，还包括从实例中「抽象」出普遍的数学结构和定理、从特殊的定理推广到一般的定理和根据已有的定理演绎地「推出」新的结论。为此提出了grown library。
LEGO-Prover 采取了一系列的流程来实现对定理证明的规划、实施和可复用定理库的收集：
- 给定一个以自然语言描述的数学定理及其人类编写的形式化描述，使用 GPT-3.5（informal solver）直接生成的自然语言证明。
- 使用分解器（decomposer）将这一自然语言证明分解为具体的证明步骤，并以引理的形式对这些证明步骤中的子目标进行对应的形式语言描述（作为检索的 request）。
- 利用这些以形式语言描述的子目标尝试从定理库（也即 skill library）中检索相关的已证明定理，将其与上述内容一同输入 GPT-3.5（formalizer），在这些提示的基础上进行目标定理的形式化证明，并使用形式化验证器检验证明的正确性。
- 从通过验证的形式化证明中，提取出除目标定理外的其他通过验证的定理（或引理）和在分解过程后得到的子目标形式语言描述，对它们进行 embedding 后加入到维护的定理库中。
此外，LEGO-Prover 还对定理库进行了专门的整理和维护流程，对分解过程中收集到的子目标进行单独的证明尝试，通过多种类别的 prompt 引导 GPT-3.5 对证明过程中收集到的成功证明的定理进行演化，从具体的证明实例抽象出一般的数学命题，以增进定理库中命题的多样性、概括性和可复用性：
some disadvantages：
- 不太符合continual learning的setting，在一个固定的problem library里反复进行迭代更新theorem library
- problem scalability依然不大，当新的lemma变多时，如何进行处理？
- 模块的复用性、泛化性
一些想法：
- 设置成真正continual learning 的 setting
- decompose这一步能不能condition on grown library去找更近的shortcut？
- retrieve-based？？