s2n-bignum-bench: LLM의 저수준 코드 추론 능력을 평가하기 위한 실용적인 벤치마크

s2n-bignum-bench: A practical benchmark for evaluating low-level code reasoning of LLMs

최근, 형식적 방법론을 활용한 대규모 언어 모델(LLM) 기반 신경-기호 접근 방식이 수학 관련 정理 증명 벤치마크에서 뛰어난 성과를 거두었습니다. 그러나 경쟁적인 수학 문제 해결 능력은 실제 구현에 대한 증명을 구성하는 능력으로 이어지지 않습니다. 본 연구에서는 이러한 격차를 해소하기 위해, 이미 HOL Light에서 어셈블리 루틴이 검증된 산업용 암호화 라이브러리에서 파생된 벤치마크인 s2n-bignum-bench를 제시합니다. s2n-bignum은 AWS에서 암호화의 빠른 어셈블리 루틴을 제공하는 데 사용되는 라이브러리이며, 그 정확성은 형식적 검증을 통해 확립되었습니다. 이 라이브러리의 형식적 검증 작업은 자동 추론 그룹의 중요한 성과였습니다. 이 작업은 (1) 프로그램의 정확한 동작을 수학적 명제로 명확하게 정의하고, (2) 그 명제가 정확함을 증명하는 두 가지 과제로 구성되었습니다. s2n-bignum의 경우, 두 가지 작업 모두 인간 전문가에 의해 수행되었습니다. s2n-bignum-bench에서는 형식적 명세를 제공하고, LLM이 HOL Light에서 특정 시간 내에 통과되는 증명 스크립트를 생성하도록 요청합니다. 현재까지, s2n-bignum-bench는 HOL Light에서 산업용 저수준 암호화 어셈블리 루틴에 대한 기계 검증 가능한 증명 생성에 초점을 맞춘 최초의 공개 벤치마크입니다. 이 벤치마크는 경쟁적인 수학 문제 외에도 LLM 기반 정理 증명의 능력을 평가하기 위한 도전적이고 실용적인 테스트 환경을 제공합니다. 벤치마크를 설정하고 사용하는 데 필요한 코드는 다음 위치에서 확인할 수 있습니다: [https://github.com/kings-crown/s2n-bignum-bench](https://github.com/kings-crown/s2n-bignum-bench)

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