s2n-bignum-bench: Un benchmark práctico para evaluar el razonamiento de código de bajo nivel en LLMs
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
Resumen
Los enfoques neurosimbólicos que aprovechan los Modelos de Lenguaje a Gran Escala (LLMs) con métodos formales han logrado recientemente resultados sólidos en benchmarks de demostración de teoremas orientados a las matemáticas. Sin embargo, el éxito en matemáticas de estilo competitivo no demuestra por sí mismo la capacidad de construir pruebas sobre implementaciones del mundo real. Abordamos esta brecha con un benchmark derivado de una biblioteca criptográfica industrial cuyas rutinas en lenguaje ensamblador ya están verificadas en HOL Light. s2n-bignum es una biblioteca utilizada en AWS para proporcionar rutinas rápidas en ensamblador para criptografía, y su corrección está establecida mediante verificación formal. La tarea de verificar formalmente esta biblioteca ha sido un logro significativo para el Grupo de Razonamiento Automatizado. Implicó dos tareas: (1) especificar con precisión el comportamiento correcto de un programa como una proposición matemática, y (2) demostrar que la proposición es correcta. En el caso de s2n-bignum, ambas tareas fueron realizadas por expertos humanos. En s2n-bignum-bench, proporcionamos la especificación formal y pedimos al LLM que genere un script de prueba que sea aceptado por HOL Light dentro de un tiempo límite fijo para la comprobación de pruebas. Hasta donde sabemos, s2n-bignum-bench es el primer benchmark público centrado en la síntesis de pruebas comprobables por máquina para rutinas criptográficas industriales de bajo nivel en lenguaje ensamblador en HOL Light. Este benchmark proporciona un campo de pruebas desafiante y prácticamente relevante para evaluar la demostración de teoremas basada en LLMs más allá de las matemáticas competitivas. El código para configurar y utilizar el benchmark está disponible aquí: 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}.