草拟、勾勒与证明：以非形式化证明引导形式化定理证明器
人工智能
2023-02-21 v3 机器学习
摘要
将已有数学证明形式化是一个众所周知的困难过程。尽管在自动化与证明助手方面已有数十年的研究，撰写形式化证明仍然繁琐且仅有少数专家能够掌握。先前关于自动化形式化的研究聚焦于强大的搜索算法，而未尝试利用可用的非形式化证明。在本工作中，我们引入草拟、勾勒与证明（Draft, Sketch, and Prove, DSP）方法，该方法将非形式化证明映射为形式化证明草图，并利用这些草图通过引导自动证明器搜索更简单的子问题来指导其证明。我们研究了两种相关设定：非形式化证明由人类撰写或由语言模型生成。我们的实验与消融研究表明，大语言模型能够生成结构良好、遵循与非形式化证明相同推理步骤的形式化草图。用这些草图引导自动证明器，使其在一组数学竞赛问题上的性能从 20.9% 提升至 39.3%。
引用
@article{arxiv.2210.12283,
title = {Draft, Sketch, and Prove: Guiding Formal Theorem Provers with Informal Proofs},
author = {Albert Q. Jiang and Sean Welleck and Jin Peng Zhou and Wenda Li and Jiacheng Liu and Mateja Jamnik and Timothée Lacroix and Yuhuai Wu and Guillaume Lample},
journal= {arXiv preprint arXiv:2210.12283},
year = {2023}
}