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}.

翻译：近年来，利用大语言模型与形式化方法的神经符号方法在面向数学的定理证明基准测试中取得了显著成果。然而，竞赛类数学的成功本身并不能证明其构建关于实际实现证明的能力。为此，我们提出一个源自工业密码学库的基准测试，该库的汇编程序已在HOL Light中得到验证。s2n-bignum是AWS用于提供加密快速汇编程序的库，其正确性通过形式化验证确立。对该库进行形式化验证是自动推理小组的一项重要成果，涉及两项任务：（1）将程序的正确行为精确地规约为数学命题，（2）证明该命题的正确性。在s2n-bignum案例中，这两项任务均由人类专家完成。在\textit{s2n-bignum-bench}中，我们提供形式化规约，要求大语言模型在固定证明检查超时内生成能被HOL Light接受的证明脚本。据我们所知，\textit{s2n-bignum-bench}是首个聚焦于HOL Light中工业级底层密码汇编程序可机器检查证明合成的公开基准。该基准为评估超越竞赛数学的大语言模型定理证明能力，提供了一个具有挑战性且实际相关的测试平台。基准搭建和使用代码见：\href{https://github.com/kings-crown/s2n-bignum-bench}{s2n-bignum-bench}。