大模型写密码证明：三分天下与盲目自信
论文讲的是：系统评估大语言模型在密码协议符号验证中的能力，发现其能生成部分有用引理但存在严重局限。
1问题
想象你正在设计一套“秘密握手”协议：两个人要在公共场合确认对方身份且不泄露秘密。密码学家不靠直觉，而是靠严密的数学推导来证明这套握手是安全的。这个过程就像解一道极其复杂的几何题，每一步推理都需要一个“引理”作为台阶。如果第一步的台阶踩空了，整个安全证明就会崩塌。对于人类专家来说，写出这些精妙的台阶已经够累了；现在的问题是，能不能让 AI 替我们把这些难啃的台阶搭好？如果不能，我们在自动化安全验证这条路上还得走多久？这个困境的核心在于，我们无法确定 AI 到底是在认真解题，还是在胡编乱造看似正确的废话，因为错误的引理会导致后续所有证明无效。
2翻译
为了搞清楚 AI 的底细，研究人员没有只盯着最终结果看，而是发明了一把新尺子，叫“求解树覆盖率”。这把尺子的逻辑是这样的：把一份完美的密码证明看作一棵树，树干是主线，树枝是那些支撑主线的辅助推理（即引理）。AI 生成的证明也是一棵树。这尺子不直接问“对不对”，而是比较两棵树的相似度——AI 长出的树枝，有多少比例跟完美范本上的树枝重叠。这就好比说，你画了一棵松树，我告诉你你的针叶有 38% 长得和我理想中的一样。数据显示，目前最强的几个大模型平均覆盖率只有 38.82%。这意味着，哪怕是最聪明的模型，也只能在不到四成的地方找准辅助推理的方向。更有趣的是，有 14.4% 的 AI 输出，其覆盖率超过了 80%，说明在某些简单或标准场景下，它们确实能做出高质量的辅助证明。但这恰恰是一个反直觉的发现：大多数时候它很烂，偶尔又惊艳得像个天才，这种极端的方差让我们很难放心使用。而且，当你试图通过增加算力或输入信息来提升效果时，收益递减得非常快，甚至因为验证过程本身太沉重，导致整体效率还不如人肉检查几页纸来得实在。
3核心概念
首先登场的是主角的工具——“求解树覆盖率”。这不是普通的准确率，而是一种基于结构相似度的度量。它假设证明是由骨架和血肉组成的，AI 只需要先搭建出靠谱的骨架（引理），最后的血肉填充才有的放矢。其次，研究依赖于“符号验证”这一特定战场。这里不考虑真实的比特流传输错误，只关注逻辑步骤是否闭环。在这个世界里，攻击者被视为一个拥有无限算力的对手，只要逻辑链条上有漏洞，就能被攻破。最后，最关键的“设计选择”是把问题转化为“辅助生成”而非“端到端生成”。研究人员没有强求 AI 一次性写完整个证明，而是让它专注于生成中间的关键引理。这是一个务实的选择，因为完全自动化的数学证明目前仍是天方夜谭，而辅助人类完成最难的部分，才是当下技术最真实的落脚点。
4洞见
大模型在形式化验证中不是全能的数学家，而是一个虽然经常跑题、但偶尔能精准命中关键分支的“灵感助手”；它的价值不在于替代专家，而在于提供高覆盖率的候选引理供人类筛选。
5博导审稿
这篇论文的选题眼光非常独到，切中了当前 AI for Science 中最硬核的领域之一。作者没有随波逐流地刷榜，而是建立了严谨的评估体系，这是值得肯定的。但是，方法成熟度上有一个根本预设需要警惕：即“结构相似度高等同于逻辑正确性高”。这在很多时候可能是一种幻觉，AI 可能生成了看似合理的废话，撞上了标准答案的表面相似，但内核却是空洞的。实验诚意方面，数字展示得很清晰，但对于“复杂多阶段协议”的性能衰减描述略显单薄，读者可能会追问在极端恶劣场景下的具体表现。写作功力中规中矩，逻辑清晰。判决：weak accept。理由在于评估体系的创新性弥补了应用深度的不足，为后续研究提供了必要的基准线。
6启发
这意味着你可以把大模型当作你的“草稿纸合伙人”，而不是“签字官”。迁移视角：在你的代码静态分析工具中，不要指望 LLM 直接找出 bug，但可以让它生成可能的攻击路径假设，再由传统引擎去验证这些假设。混搭视角：将传统的定理证明器（如 Coq 或 Isabelle）与大模型结合，用传统工具锁死逻辑框架，用大模型填充框架内的缺失步骤，实现人机回环。反转视角：如果你一直认为 AI 在数学任务上是笨拙的，这篇论文提示你，在结构化极强的符号系统中，模糊匹配（覆盖率）比精确匹配更有早期筛选价值。