s2n-bignum-bench: Um benchmark prático para avaliação do raciocínio de LLMs sobre código de baixo nível
s2n-bignum-bench: A practical benchmark for evaluating low-level code reasoning of LLMs
March 15, 2026
Autores: Balaji Rao, John Harrison, Soonho Kong, Juneyoung Lee, Carlo Lipizzi
cs.AI
Resumo
As abordagens nerossimbólicas que alavancam Modelos de Linguagem de Grande Porte (LLMs) com métodos formais têm obtido recentemente resultados sólidos em benchmarks de demonstração de teoremas com orientação matemática. No entanto, o sucesso em matemática de estilo competitivo não demonstra, por si só, a capacidade de construir provas sobre implementações do mundo real. Nós abordamos esta lacuna com um benchmark derivado de uma biblioteca criptográfica industrial cujas rotinas em assembly já são verificadas em HOL Light.
s2n-bignum é uma biblioteca usada na AWS para fornecer rotinas de assembly rápidas para criptografia, e sua correção é estabelecida por verificação formal. A tarefa de verificar formalmente esta biblioteca tem sido uma conquista significativa para o Grupo de Raciocínio Automatizado. Envolveu duas tarefas: (1) especificar com precisão o comportamento correto de um programa como uma proposição matemática, e (2) provar que a proposição está correta. No caso do s2n-bignum, ambas as tarefas foram realizadas por especialistas humanos.
Em s2n-bignum-bench, fornecemos a especificação formal e solicitamos que o LLM gere um script de prova que seja aceito pelo HOL Light dentro de um tempo limite fixo para verificação de provas. Até onde sabemos, o s2n-bignum-bench é o primeiro benchmark público focado na síntese de provas verificáveis por máquina para rotinas criptográficas industriais de baixo nível em assembly no HOL Light. Este benchmark fornece um ambiente de teste desafiador e praticamente relevante para avaliar a demonstração de teoremas baseada em LLM para além da matemática competitiva.
O código para configurar e usar o benchmark está disponível aqui: https://github.com/kings-crown/s2n-bignum-bench{s2n-bignum-bench}.
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 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, 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: https://github.com/kings-crown/s2n-bignum-bench{s2n-bignum-bench}.