s2n-bignum-bench：评估大语言模型低层代码推理能力的实用基准 s2n-bignum-bench: A practical benchmark for evaluating low-level code reasoning of LLMs
基于AWS密码学库的形式化证明基准，评估LLM在工业级汇编代码上的推理能力
前置知识
交互式定理证明器
交互式定理证明器是用于验证数学定理和程序正确性的软件系统，用户通过编写证明脚本来引导证明过程。HOL Light采用LCF方法，所有推导最终由一个极小的可信内核检查，内核只产生类型为thm（定理类型）的值。HOL Light是OCaml实现的极简证明系统，其证明脚本本身就是OCaml程序，通过策略（tactics）来消解目标。
本文基准完全基于HOL Light，理解其工作机制对理解任务本质至关重要，包括证明脚本的语法、策略的使用方式以及内核检查机制。
低级代码形式化验证
低级代码形式化验证是指对汇编或机器码级别的程序进行数学化证明，确保其满足给定的功能规范。这个过程需要精确建模处理器指令集架构（ISA）的语义，包括寄存器状态、内存、字节序等。验证通常通过符号执行实现：从预条件出发，逐步执行每条指令，将程序状态转换为数学表达式，最终验证后条件是否成立。
s2n-bignum-bench的核心就是要求模型证明真实汇编代码的正确性，这与抽象数学证明有本质区别，涉及架构状态、别名分析和字节序等低层概念。
神经定理证明
神经定理证明结合大语言模型与交互式定理证明器，模型提出证明步骤，ITP作为验证器检查每一步的正确性。这与仅输出答案的基准（如GSM8K）不同，要求结构化、可验证的推理链。NTP系统的关键挑战包括理解数学规范、选择合适策略、处理长上下文以及避免无效推理。
本文工作属于NTP领域，但将评估从竞赛数学扩展到真实的代码验证场景，这对理解LLM推理能力的边界和局限性具有重要意义。
策略和证明脚本
策略是HOL Light中用于转换证明目标的函数，如REWRITE_TAC（应用重写规则）、GEN_TAC（引入全称量词）、REFL_TAC（反射性）等。证明脚本是策略的组合，通常用THEN操作符串联。例如证明x*(y+z)=x*z+x*y可以用REWRITE_TAC[LEFT_ADD_DISTRIB] THEN GEN_REWRITE_TAC LAND_CONV [ADD_SYM] THEN REFL_TAC。
基准要求LLM输出合法的HOL Light策略表达式，理解策略的语义和组合方式是评估模型能力的核心。
研究动机
现有的神经定理证明基准主要关注竞赛风格的数学问题，如MiniF2F的488个奥数级别问题和PutnamBench的672个竞赛数学定理。虽然在这些基准上的成功证明了LLM的结构化推理能力，但抽象数学竞赛题的成功并不能直接转化为处理实际工程系统的能力。密码学库和系统代码的正确性具有直接的安全和可靠性后果，但这种低级实现推理能力在现有基准中严重不足。竞赛数学证明不涉及架构状态、内存别名分析或字节序问题，而这些都是验证真实汇编代码必不可少的要素。即使模型在抽象数学上表现出色，也不代表具备处理低级代码推理的能力。
本文的目标是本文的目标是构建s2n-bignum-bench，一个基于真实工业级密码学库的机器可检查证明合成基准，专注于HOL Light中验证的低级代码。该基准源自AWS使用的s2n-bignum密码学库，其汇编例程已经在HOL Light中完成形式化验证。基准要求模型为给定的形式化规范生成可被HOL Light内核接受的证明脚本，在固定的证明检查超时内完成。通过这个基准，作者希望能够评估NTP系统构建真实汇编代码满足规范证明的能力，填补竞赛数学与真实工程验证之间的空白。
与已有工作不同的是，本文的独特切入点在于专注于HOL Light中工业级低级密码学汇编代码的机器可检查证明合成，这是现有基准中未充分代表的生态系统。与NTP4VC（验证条件证明）、VeriBench-FTP（代码验证证明）和miniCTX（上下文依赖证明）等工作不同，s2n-bignum-bench提供了完整的目标代码制品和可信的ISA语义，要求模型进行ISA感知、位精确的推理。每份证明都必须展示从寄存器和内存预条件出发，特定解码的ARM或x86指令序列如何产生满足数学后条件的最终状态，这涉及在特定程序计数器偏移处分解程序、通过ISA特定解码和执行语义符号执行每个段、以及在每步简化结果符号状态术语。这种推理方式在质的上与抽象数学和高级验证条件证明都不同。
核心方法
s2n-bignum-bench的构建方法是：从开源的s2n-bignum仓库中提取2,284个HOL Light上下文-查询任务，内联相关的OCaml模块，定位形式为let THM = prove(goal, proof)的顶层定理绑定，将goal提取为查询。伴随的上下文是一个自包含的OCaml/HOL Light设置，加载复现原始证明环境所需的定义、常量和先前证明的结果，但将每个原始证明体替换为占位符CHEAT_TAC。这样就将任务隔离为在相同接口和导入下合成新的机器可检查证明。为了区分不同问题，引入了问题标识符概念，格式为arch.filename.thm.N，例如arm.bignum_montsqr_p256.lemma1.0，其中N表示引理的出现索引。基准还提供了将选定问题提取到包含setup.ml和query.txt的目录中的制品，允许每个问题的可重现、独立尝试。
核心创新点在于将工业级密码学库的完整形式化验证任务转换为可重复的机器可检查证明合成基准。与现有基准使用人工构造的数学问题不同，s2n-bignum-bench使用生产环境中真实验证的汇编代码及其HOL Light证明，这意味着每个问题都有确定的正确答案和明确的成功标准。基准还实现了多项完整性机制来检测不健全或无效的提交，包括检查新引入的公理、禁止的占位符（如CHEAT_TAC）、提交证明表达式的解析器级别验证，以及基于类型注解混淆的污染缓解机制。这些机制确保基准的公平性和结果的可靠性，防止模型通过作弊或记忆训练数据来获得虚高的分数。
方法步骤详情
基准构建和使用的完整流程包括四个步骤。第一步是基准构建，从pinned的HOL Light和s2n-bignum源中提取定理元数据，产生包含2,284个问题的语料库。每个问题包括存储在query.txt中的HOL Light布尔术语，和包含建立证明上下文所需HOL Light会话前导码的对应setup.ml文件。第二步是问题检索，问题可以以两种等价格式检索：作为平面CSV使用retrieve-problem.py --csv-only，或作为problems目录下/query.txt文件的目录树。第三步是提示和推理流水线，使用zero-shot提示模板，包含一个工作示例，指导模型仅输出策略表达式而不包含其他自然语言解释。第四步是评估流水线，包括三个阶段：语法检查和组装（编译为有效的OCaml/HOL Light策略表达式）、证明执行（在HOL Light中使用每个问题的超时、前后公理计数比较和标准编译运行日志执行）、裁决收集（每个问题获得OK、FAIL、CHEATING、TIMEOUT或ERROR五个裁决之一）。
技术新颖性
s2n-bignum-bench的技术新颖性体现在多个方面。首先，这是第一个专注于HOL Light中工业级低级密码学汇编例程的机器可检查证明合成公开基准。其次，基准提供了基于目标代码制品和可信ISA语义的端到端离线评估流水线，包括构建基准、检索问题和运行评估的完整工具链。第三，基准实现了多项完整性检查机制，包括检测禁止占位符（如CHEAT_TAC）、检测新引入的公理（通过比较axioms()函数的输出）、解析器级别的语法验证以及基于类型注解混淆的污染缓解。第四，基准基于部署的密码学代码库，测量ISA感知、位精确的推理，这种推理比竞赛数学更接近真实验证工作流。最后，基准提供了每个问题的超时映射，通过分析原始人工证明的运行时间，为不同类型的问题分配适当的超时值，避免单一全局超时带来的不公平性。
实验结果
初步基线实验使用GPT-5.3-Codex在中等努力模式下达到4.4%的二进制证明完成率，在高努力模式下达到5.3%，净增20个证明。改进主要集中在程序状态类别（+12个问题）和通用类别（+7个问题）。从完整基准的2,284个问题中，中等努力运行产生了743个通过语法检查并到达证明执行的答案，高努力运行产生了766个，其余答案因未编译为有效的OCaml/HOL Light策略表达式而被排除在语法检查阶段。在问题类别上表现差异显著：通用类别在中等努力模式下解决59/562个问题（10.5%），高努力模式下解决66/562个（11.7%）；位向量类别中等努力模式解决26/311个（8.4%），高努力模式解决27/311个（8.7%）；程序状态类别中等努力模式解决16/552个（2.9%），高努力模式解决28/552个（5.1%）；然而，功能正确性类别在两种模式下解决率均为0%，包括437个ARM问题和422个x86问题。中等努力运行产生44个超时和3个错误，高努力运行产生47个超时和4个错误。这些结果表明当前模型在简单的引理上表现尚可，但在处理复杂的低级代码验证任务上仍然非常困难。
查看结构化数据
| 任务 | 指标 | 本文 | 基线 | 提升 |
|---|---|---|---|---|
| HOL Light证明合成（全部2284问题） | 二进制证明完成率 | 4.4% (中等努力) / 5.3% (高努力) | 无（首次基准） | 基线建立 |
| 通用类别证明合成 | 二进制证明完成率 | 10.5% (中等努力) / 11.7% (高努力) | 无 | +1.2% |
| 位向量类别证明合成 | 二进制证明完成率 | 8.4% (中等努力) / 8.7% (高努力) | 无 | +0.3% |
| 程序状态类别证明合成 | 二进制证明完成率 | 2.9% (中等努力) / 5.1% (高努力) | 无 | +2.2% |
| 功能正确性证明合成 | 二进制证明完成率 | 0.0% (ARM和x86均为0) | 无 | 无进展 |
| 语法检查通过率 | 通过语法检查的答案比例 | 32.5% (中等努力) / 33.5% (高努力) | 无 | +1.0% |
局限与改进
作者承认的局限性包括：类型注解混淆机制仅对约70%的问题集有效，因为HOL Light的打印机和解析器不是完全Pollack一致的，对于这些查询选择使用原始表示而不混淆；当前基准专注于外延正确性，但最近的HOL Light开发也形式化了关系属性（如常时间纪律和优化例程与验证友好例程之间的等价性），这为未来扩展提供了自然路径。从我的观察来看，基准还存在以下局限：零shot提示模板可能不是最优的，更复杂的提示技术或few-shot学习可能提高性能；仅评估了单个模型（GPT-5.3-Codex），缺乏对其他模型的比较；语法检查通过率较低（约33%），表明模型在生成有效的HOL Light策略表达式语法上存在困难；功能正确性问题解决率为0%，表明模型在处理需要理解整个汇编例程语义的长链推理上仍然完全失败；实验仅报告了pass@1指标，没有探索pass@k或其他多样性指标。
独立分析的弱点
独立分析的弱点包括：首先，零shot提示可能不足以引导模型理解HOL Light证明的复杂结构，可以探索few-shot提示、思维链或多步骤推理等更复杂的提示策略。其次，当前评估仅使用pass@1指标，这在需要精确匹配证明脚本的场景下过于严格，可以引入pass@k指标或允许等价但不完全相同的证明。第三，语法检查通过率仅为33%左右，表明模型在生成合法的OCaml/HOL Light语法上存在系统性困难，这可能需要在预训练或微调阶段增加更多HOL Light代码数据。第四，功能正确性问题解决率为0%，这可能是因为这些证明需要理解整个汇编例程的全局语义，当前模型可能需要更好的上下文理解和长链推理能力。第五，基准没有评估模型在不同证明策略选择上的表现，如重写vs位操作vs符号执行，这种细粒度的分析可以更好地理解模型的推理偏好。
未来方向
作者提出的未来工作方向包括将基准扩展到外延正确性之外，纳入关系属性如常时间纪律和例程等价性。基于当前成果的可延伸方向包括：探索更复杂的提示技术如few-shot学习、思维链或交互式证明生成；在HOL Light代码上对模型进行微调，提高语法检查通过率和证明合成质量；开发更好的超时分配策略，基于问题特征而非仅仅是历史运行时间；引入更多的完整性检查机制，如检测循环推理或不必要的公理；扩展基准到其他架构（如RISC-V）或其他形式化系统（如Lean4、Isabelle）；研究模型在不同问题类别上的性能差异，特别是为什么功能正确性问题如此困难；开发用于分析模型证明策略选择偏好的工具；探索自动化证明辅助工具与LLM的结合，如策略推荐或中间目标生成。随着HOL Light在s2n-bignum上的持续发展，基准可以自然扩展到包括更多关系属性和更复杂的验证场景。
复现评估
s2n-bignum-bench的复现性非常好。基准代码公开可用，提供了完整的端到端流水线来构建基准、检索问题和运行离线评估。所有制品（setup.ml、query.txt、超时映射等）都随基准发布，可以完全离线运行而无需互联网连接。基准使用pinned的HOL Light和s2n-bignum源，确保了实验的可重现性。评估脚本包括语法检查、证明执行和裁决收集的完整流程，输出CSV文件方便结果分析。实验使用GPT-5.3-Codex通过codex-cli访问，虽然模型本身是闭源的，但提示模板和评估脚本在官方仓库中公开。超时配置基于原始人工证明的三次运行分析，提供了详细的统计信息。算力需求取决于模型选择和问题数量，单个问题可能从几毫秒到几小时不等，基准提供了per-problem超时映射来合理分配资源。总体而言，研究者可以相对容易地复现实验或在基准上评估自己的模型，这是该基准的一个重要优势。
论文图表
表格展示了中等努力和高努力模式下各个问题类别的详细实验结果。对于通用类别（562个问题），中等努力模式评估330个，解决59个，失败239个，超时/错误32个，成功率10.5%；高努力模式评估349个，解决66个，失败246个，超时/错误37个，成功率11.7%。位向量类别（311个）中等模式解决26个（8.4%），高努力模式解决27个（8.7%）。程序状态类别（552个）中等模式解决16个（2.9%），高努力模式解决28个（5.1%）。功能正确性ARM（437个）和x86（422个）在两种模式下解决率均为0%。总计2284个问题，中等努力模式评估743个，解决101个，成功率4.4%；高努力模式评估766个，解决121个，成功率5.3%。
这个表格对理解论文至关重要，因为它提供了基线实验的完整定量结果。读者可以清楚地看到模型在不同类型问题上的性能差异：通用和位向量类别表现相对较好，程序状态类别表现较差，而功能正确性类别完全失败。这个表格还展示了语法检查的低通过率（约33%），以及超时和错误的相对频率。这些数据为理解LLM在低级代码推理上的当前能力和局限性提供了直接的证据。