BriefGPT.xyz
Oct, 2022
Draft, Sketch, and Prove: 用非正式证明指导形式化定理证明器
Draft, Sketch, and Prove: Guiding Formal Theorem Provers with Informal Proofs
HTML
PDF
Albert Q. Jiang, Sean Welleck, Jin Peng Zhou, Wenda Li, Jiacheng Liu...
TL;DR
本文介绍了一种名为DSP的方法,可以将非正式证明映射到正式证明草图并指导自动证明器,使其搜索更容易的子问题。实验证明语言模型能够产生结构良好的正式草图,并将其指导自动证明器,从而提高性能达到39.3%。
Abstract
The
formalization
of existing mathematical proofs is a notoriously difficult process. Despite decades of research on automation and
proof assistants
, writing formal proofs remains arduous and only accessible to a
→