测试大模型对真实加密代码的证明能力，挑战传统数学竞赛式评估局限。
s2n-bignum-bench: A practical benchmark for evaluating low-level code reasoning of LLMs
- 基于已形式验证的工业级汇编库s2n-bignum构建可机器检验的证明任务
- 要求LLM在限定时间内生成HOL Light可接受的证明脚本
- 适合研究大模型低层代码推理与形式化验证的学者使用
结合大语言模型与形式化方法的神经符号方法在数学定理证明基准上表现优异。然而，竞赛类数学题的成功并不足以证明其对真实软件实现的证明能力。为此，我们提出s2n-bignum-bench，该基准源自AWS工业级密码学库s2n-bignum的汇编实现，其正确性已在HOL Light中通过人工专家完成形式化验证。该任务包含两个步骤：(1) 将程序行为精确描述为数学命题；(2) 证明该命题成立。在本工作中，我们提供形式化规范，要求大模型生成能在固定证明检查超时内被HOL Light接受的证明脚本。据我们所知，s2n-bignum-bench是首个面向工业级低层密码学汇编代码、基于HOL Light的机器可检证明合成公开基准。该基准为超越竞赛数学的大模型定理证明能力评估提供了极具挑战性且贴近实际的应用场景。代码仓库地址：https://github.com/kings-crown/s2n-bignum-bench。
原文摘要 · Abstract (English)
Neurosymbolic approaches leveraging Large Language Models (LLMs) with formal methods have recently achieved strong results on mathematics-oriented theorem-proving benchmarks. However, success on competition-style mathematics does not by itself demonstrate the ability to construct proofs about real-world implementations. We address this gap with a benchmark derived from an industrial cryptographic library whose assembly routines are already verified in HOL Light. s2n-bignum is a library used at AWS for providing fast assembly routines for cryptography, and its correctness is established by formal verification. The task of formally verifying this library has been a significant achievement for the Automated Reasoning Group. It involved two tasks: (1) precisely specifying the correct behavior of a program as a mathematical proposition, and (2) proving that the proposition is correct. In the case of s2n-bignum, both tasks were carried out by human experts. In \textit{s2n-bignum-bench}, we provide the formal specification and ask the LLM to generate a proof script that is accepted by HOL Light within a fixed proof-check timeout. To our knowledge, \textit{s2n-bignum-bench} is the first public benchmark focused on machine-checkable proof synthesis for industrial low-level cryptographic assembly routines in HOL Light. This benchmark provides a challenging and practically relevant testbed for evaluating LLM-based theorem proving beyond competition mathematics. The code to set up and use the benchmark is available here: \href{https://github.com/kings-crown/s2n-bignum-bench}{s2n-bignum-bench}.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。