能解决奥林匹克级别定理的大语言模型，依然无法可靠地验证汇编例程。神经符号系统在竞赛风格数学基准上表现亮眼，但这类基准测试的是抽象证明构建，而非对真实代码在机器层面行为的推理。
s2n-bignum-bench 通过直接取材于已在 AWS 生产部署的工业级密码学库来填补这一空白。该库 s2n-bignum 提供了密码学操作的汇编例程，其正确性已在 HOL Light（一种用于机器验证数学的证明助手）中经过形式化验证。该基准要求模型解决两个不同的子问题：为汇编例程编写精确的行为规约，以及构建证明这些规约成立的形式化证明。二者在真实工业验证工作流中都不可或缺，却均未出现在标准定理证明基准中。库中的汇编例程层级低、经过性能优化，其行为与数学竞赛数据集中占主导地位的结构化代数推理存在显著差异。
这一局限既是实践层面的，也是概念层面的。擅长 AIME 或 Lean 形式化数学的模型，并未学会阅读汇编代码、推理寄存器状态，或将 C 风格内存语义转化为形式逻辑——而这些恰恰是本任务的前提条件，并非通用推理能力的附带产物。对于正在构建或评估代码推理系统的团队，在声称能泛化到生产软件之前，有必要先运行这一基准。那些主要在数学语料库上训练或评估证明生成能力的系统，在此类任务上应预期出现显著的性能差距。
核心要点：
- 竞赛数学基准测试抽象证明构建；s2n-bignum-bench 测试真实汇编例程的规约编写与证明构建，暴露了现有基准所掩盖的能力缺口
- 在数学基准上的强定理证明表现，无法预测工业代码验证的表现，因为两类任务所需的底层推理原语截然不同
- 评估大语言模型用于形式验证或代码正确性工具的团队，应在将数学领域结果推广至生产软件之前，先针对此基准进行测试
来源：s2n-bignum-bench: A Practical Benchmark for Evaluating Low-Level Code Reasoning of LLMs
编辑备注：所提供的摘要在句中截断，在任何性能数字报告之前已中断。以上条目呈现了结构性论点与基准设计，但缺少具体模型结果、通过率或对比数据。建议在发布前获取完整论文以补充量化证据。
来源：s2n-bignum-bench: A practical benchmark for evaluating low-level code reasoning