Draft, Sketch, and Prove 用 LLM 生成形式证明骨架，把 informal proof 变成 formal prover 的搜索指南

Jiang、Welleck 等提出 Draft, Sketch, and Prove（DSP）：先从人类或语言模型生成的 informal proof 提取 formal proof sketch，再把复杂目标拆成更容易由 automated theorem prover 解决的子问题。论文表明 LLM 能生成与 informal proof 推理步骤一致的结构化 formal sketches；在数学竞赛题集合上，这种 sketch-guided proving 将成功率从 20.9% 提升到 39.3%。