CrypFormBench: Benchmarking Formal Analysis Capability of Large Language Models for Cryptographic Schemes
本文介绍了 CrypFormBench，这是一个包含 677 种密码方案和 7 种形式化验证语言、共计 700 个实例的综合基准测试，旨在评估并揭示大语言模型在生成和修正形式化安全证明方面的当前局限性，同时提供提高其性能的实用策略。
原始论文采用 CC BY 4.0 许可（http://creativecommons.org/licenses/by/4.0/）。 这是对下方论文的AI生成解释。它不是由作者撰写或认可的。如需技术准确性，请参阅原始论文。 阅读完整免责声明
以下是关于论文 "CrypFormBench" 的解释，采用了通俗易懂的语言和富有创意的类比。
大局观： “翻译官”难题
想象一下，你是一位顶尖的建筑师，负责设计极其安全的保险库（加密方案）。你用直白的英语编写蓝图，以便任何人都能理解设计方案。然而，为了实际建造并测试这些保险库是否存在弱点，你需要将这些英语蓝图翻译成一种非常严格、古老且复杂的语言，只有特定的高科技安全机器人（如 Scyther 或 Tamarin 等形式化验证工具）才能理解。
这种翻译非常困难。它需要一位既精通保险库设计，又精通机器人严苛语言的人类专家。如果你漏掉了一个微小的逗号，或者用错了词，机器人就会拒绝执行蓝图，或者更糟——它造出的保险库看起来很安全，但实际上隐藏着后门。
问题在于： 大语言模型（LLM）——即我们今天使用的 AI 聊天机器人——能否胜任这些专家级翻译官的角色？它们能否将一段纯英文的安全性协议描述，瞬间转化为完美的、无误的机器人代码？
答案（根据本论文）： 目前还不行。它们在阅读和修复方面正在进步，但在从零开始编写代码方面仍然感到吃力。
解决方案：CrypFormBench（AI 的“健身房”）
为了准确了解这些 AI 翻译官到底有多强，研究人员构建了一个庞大的测试场，名为 CrypFormBench（简称 C.F.B.）。
你可以把它想象成一个拥有 700 个不同锻炼站点的健身房：
- 器材： 他们收集了 700 个真实的安全性协议（例如用于你的手机、银行或互联网中的协议）。
- 语言： 他们将这些协议翻译成了 7 种不同的“机器人语言”（形式化语言，如 SPDL、HLPSL、EasyCrypt 等）。
- 测试项目： 他们不仅仅要求 AI 编写代码，还测试了五项特定技能：
- 解读（Interpretation）： “这是机器人代码；请用英语向我解释它。”（阅读能力）
- 生成（Generation）： “这是英文描述；请编写对应的机器人代码。”（从零开始编写）
- 补全（Completion）： “这是带有空白处的机器人代码；请填补空缺。”（修复部分工作）
- 转换（Transformation）： “这是语言 A 中的代码；请将其重写为语言 B。”（在不同机器人之间进行翻译）
- 纠错（Correction）： “这段机器人代码有错误；请修复它。”（调试能力）
结果：AI 的成绩单
研究人员测试了 9 种最智能的可用 AI 模型（包括 GPT-4o、Claude-3.5 和 DeepSeek）。以下是他们的发现：
1. “擅长阅读”的技能（解读与补全）
- 类比： 想象一个学生非常擅长阅读教科书，并且能根据上下文填补句子中缺失的单词。
- 结果： AI 在这方面表现得相当出色。当给定一段带有少量缺失部分的完整代码，或者要求其解释一段代码的功能时，它们的表现非常好。它们理解这些安全语言的“语法”。
2. “不擅长写作”的技能（生成与转换）
- 类를比： 现在，想象要求同一个学生从头开始写一本全新的教科书，或者在没有字典的情况下将一本书从法语翻译成日语。他们会开始产生幻觉、编造规则或忘记严格的语法。
- 结果： 这正是 AI 失手的地方。
- 生成： 当被要求根据纯英文描述编写完整的安全性协议时，大多数 AI 生成的代码甚至无法被机器人运行。这就像是在写一个语法破碎的句子。
- 转换： 当被要求将代码从一种机器人语言转换为另一种时，AI 经常会感到困惑。它们会混淆两种语言的规则，创造出一种在两种语言中都无法运行的“科学怪人”式代码。
- 得分： 即便是最强的 AI（Claude-3.5），得分也仅为 48.7 分（满分 100 分）。这意味着它们生成的代码中，只有不到一半是真正可用的。
3. “修复”的技能（纠错）
- 类比： 如果你给学生一个明显的拼写错误（例如把 "receive" 写成 "recieve"），他们可以轻松修复。但如果句子语法正确但逻辑错误（例如：“保险库对所有人开放，但它是安全的”），他们就会感到棘手。
- 结果： AI 擅长修复简单的语法错误（拼写错误）。然而，面对“语义”错误——即修复安全性协议本身的逻辑问题时，它们表现挣扎。
为什么这如此困难？
论文解释说，这些“机器人语言”并不像 Python 或 Java 那样简单。它们极其严格。
- “一个错误”原则： 在常规编程中，如果你漏掉了一个分号，计算机可能只会报错。但在这些安全语言中，漏掉一个词就可能改变整个安全证明的含义，导致原本安全的保险库看起来不安全，反之亦然。
- “上下文”问题： 这些协议通常依赖于长链条事件（例如：“如果 Alice 在步骤 1 发送消息，Bob 必须在步骤 2 回复，但前提是他尚未收到来自步骤 0 的消息”）。AI 往往会丢失这些长链条的追踪。
我们该怎么办？（“辅助轮”）
论文指出，虽然我们目前还不能依靠 AI 单独完成这项工作，但如果给予正确的帮助，我们可以将它们作为助手使用：
- 少样本提示（Few-Shot Prompting）： 不要只说“写这个”，先给 AI 展示三个如何编写此类代码的示例。这就像是给它一份“小抄”。
- Pass@K： 让 AI 尝试编写 5 次代码，然后从中挑选最好的一个。这能增加获得可用版本的概率。
- 人类参与（Human-in-the-Loop）： 利用 AI 起草代码，但在让安全机器人运行之前，必须由人类专家进行检查。
总结
论文得出结论：大型语言模型目前是理解和修复安全代码的优秀研究助手，但它们还不是构建全新安全性协议的可靠建筑师。
它们可以帮你阅读手册并修复拼写错误，但在你移交钥匙之前，你仍然需要一位人类专家来确保保险库确实是安全的。该基准测试（CrypFormBench）现已开放，供其他研究人员针对这些严格标准测试新的 AI 模型。
您所在领域的论文太多了？
获取与您研究关键词匹配的最新论文每日摘要——附技术摘要，使用您的语言。