arXiv💻 cs.LO

Proof Strategy Extraction from LLMs for Enhancing Symbolic Provers

本文提出了 Strat2Rocq 框架，通过离线提取大语言模型的证明策略并将其形式化为 Rocq 引理，在在线阶段增强 CoqHammer 等符号证明器的自动化能力，从而在开源软件验证项目中显著提升了证明成功率。

Jian Fang, Yican Sun, Yingfei Xiong

发布于 2026-03-05
📖 1 分钟阅读☕ 轻松阅读
查看于 arXiv ↗PDF ↗

Each language version is independently generated for its own context, not a direct translation.

这篇论文讲述了一个非常有趣的故事：如何让“笨”但安全的数学证明机器，学会“聪明”但昂贵的 AI 大模型的解题技巧。

我们可以把这篇论文的核心思想想象成**“把天才的解题直觉，变成普通人的工具书”**。

1. 背景：两个性格迥异的“证明者”

想象一下，在软件验证（确保代码不出错）的世界里，有两个主要的“证明者”：

  • 符号证明器（Symbolic Provers，比如 CoqHammer）：
    • 性格： 像是一个严谨、死板但极其可靠的会计。它完全按照规则办事，不需要休息，不会撒谎，而且可以在你自家的电脑上运行（安全、便宜）。
    • 缺点： 它太死板了。遇到稍微复杂一点的数学题，它不知道“走捷径”，必须一步一步按死规则推导，经常卡在半路走不出来。
  • 大语言模型（LLMs）：
    • 性格： 像是一个才华横溢但有点“神神叨叨”的天才数学家。它一眼就能看出题目的规律，能直接跳到答案，甚至能发现人类都没注意到的捷径。
    • 缺点： 它太“贵”了（需要超级计算机），而且如果把它请进公司，可能会把公司的机密代码泄露出去（不安全）。

过去的问题： 人们试图把这两个结合起来，让天才数学家（LLM）在线指导会计（符号证明器）。但这既花钱又有安全风险。

2. 核心创意：提取“解题秘籍”

这篇论文提出了一个大胆的想法：既然不能总请天才数学家来现场指导，那能不能在他解题的时候，偷偷把他脑子里的“解题套路”记下来，整理成一本“秘籍”，然后交给那个死板的会计去用呢？

这就是论文提出的 Strat2Rocq 框架。

3. 工作流程：三步走战略

这个过程分为两个阶段，就像**“离线备课”和“在线考试”**：

第一阶段：离线备课（把直觉变成规则）

  • 场景： 作者找了一大堆数学题（训练集）。
  • 动作： 他们让那个“天才数学家”（LLM）来做这些题，并让它用大白话把解题思路写出来。
    • 比如： 天才说：“哎呀，这个式子 a+b+ca+b+c 直接等于 c+b+ac+b+a，不用一步步算！”
  • 转化： 系统把这些“大白话”的直觉，自动翻译成严谨的数学公式（称为引理 Lemmas）。
    • 比如： 把“直接等于”翻译成一条正式的数学定理：Lemma power_1: ...
  • 结果： 得到了一大堆新的“解题秘籍”（引理库）。这些秘籍是 LLM 从海量数据中学到的“直觉”，现在变成了严谨的规则。

第二阶段：在线考试（死板会计用秘籍）

  • 场景： 现在遇到一个新的、很难证明的数学题。
  • 动作： 我们不再请天才数学家，而是把刚才整理好的“解题秘籍”（引理库）直接塞给那个“死板会计”（CoqHammer）。
  • 效果： 会计本来只会死算，但现在它手里有了“秘籍”。当它看到题目时，它可以直接引用秘籍里的捷径，瞬间就证明了以前证明不了的题目！

4. 一个生动的比喻：导航仪 vs. 老司机

  • 符号证明器就像是一个只有基础地图的导航仪。它知道路怎么走，但遇到复杂的路况（复杂的数学证明），它只能一条路一条路地试，很慢且容易迷路。
  • 大语言模型就像是一位经验丰富的老司机。他不用看地图，凭直觉就知道哪条小路能抄近道。
  • Strat2Rocq 的做法：
    1. 先让老司机（LLM）开一次车，把他脑子里的“抄近道经验”（比如“遇到红灯右转能避开拥堵”）记录下来。
    2. 把这些经验整理成新的交通规则（引理）。
    3. 把这些新规则更新到导航仪（符号证明器）的数据库里。
    4. 以后，导航仪虽然还是那个导航仪，但它现在知道了那些“抄近道”的规则，也能像老司机一样快速到达目的地了！

5. 实验结果：效果惊人

作者用真实的开源软件项目（像 CompCert 编译器这种大项目）做了测试：

  • 成功率提升： 给符号证明器加上这些“秘籍”后，它成功证明题目的比例提高了 13.41%。这意味着以前很多证明不了的安全漏洞，现在能自动证明了。
  • 意外惊喜： 这些“秘籍”不仅帮了死板的会计，反过来给“天才数学家”（LLM 代理）看，也能让它解题更准（提升 4%），而且用的“脑子”（Token 消耗）更少了。
  • 通用性： 不管用的是哪个品牌的“天才数学家”（不同的 LLM），这套提取方法都管用。

6. 总结：为什么这很重要？

这篇论文最大的贡献在于**“去魅”与“落地”**：

  1. 安全与省钱： 我们不需要在每次证明代码时都去调用昂贵且危险的 AI 服务。我们只需要在离线阶段（比如晚上）把 AI 的智慧提取出来，变成静态的规则库。
  2. 永久传承： 一旦提取成功，这些“策略”就变成了代码的一部分。哪怕以后 AI 模型更新了，这些提炼出来的核心智慧依然保留在符号证明器里，随时可用。
  3. 理解 AI： 这也让我们明白，AI 并不是真的在“思考”，它其实是在模仿人类积累的数学直觉。如果我们能把这些直觉变成规则，我们就能用更简单、更安全的方式解决复杂问题。

一句话总结：
这就好比把爱因斯坦的解题直觉，写成了小学生都能看懂的公式，让最普通的计算器也能算出爱因斯坦的难题，而且不用付爱因斯坦的出场费，也不用担心他泄露机密。

类似论文