草图、初稿与证明：利用非正式证明引导形式化定理证明器

现有数学证明的机械化形式化过程一向极为困难。尽管数十年来在自动化与证明助手方面已有大量研究，撰写形式化证明依然费时费力，仅少数专家能够胜任。以往的研究在自动化形式化方面主要聚焦于强大的搜索算法，却未充分利用已有的非形式化证明资源。在本工作中，我们提出一种名为“草稿、构图、证明”（Draft, Sketch, and Prove，简称DSP）的方法，该方法将非形式化证明映射为形式化证明的草图，并利用这些草图引导自动化定理证明器，通过聚焦于更易处理的子问题来优化其搜索过程。我们考察了两种相关场景：非形式化证明由人类编写，或由语言模型生成。实验与消融研究结果表明，大型语言模型能够生成结构良好、与非形式化证明保持一致推理路径的形式化草图。借助这些草图引导自动化证明器，其在数学竞赛题集上的表现从20.9%提升至39.3%。