s2n-bignum-bench : Un benchmark pratique pour évaluer le raisonnement sur le code bas niveau des LLM
s2n-bignum-bench: A practical benchmark for evaluating low-level code reasoning of LLMs
March 15, 2026
Auteurs: Balaji Rao, John Harrison, Soonho Kong, Juneyoung Lee, Carlo Lipizzi
cs.AI
Résumé
Les approches neurosymboliques qui combinent les grands modèles de langage (LLM) avec des méthodes formelles ont récemment obtenu des résultats solides sur des benchmarks de démonstration de théorèmes orientés mathématiques. Cependant, la réussite sur des problèmes mathématiques de type concours ne démontre pas en soi la capacité à construire des preuves concernant des implémentations du monde réel. Nous comblons cette lacune avec un benchmark dérivé d'une bibliothèque cryptographique industrielle dont les routines assembleur sont déjà vérifiées dans HOL Light. s2n-bignum est une bibliothèque utilisée chez AWS pour fournir des routines assembleur rapides pour la cryptographie, et son exactitude est établie par vérification formelle. La tâche de vérification formelle de cette bibliothèque a été une réalisation significative pour le groupe de raisonnement automatique. Elle impliquait deux tâches : (1) spécifier précisément le comportement correct d'un programme comme une proposition mathématique, et (2) prouver que la proposition est correcte. Dans le cas de s2n-bignum, ces deux tâches ont été réalisées par des experts humains. Dans s2n-bignum-bench, nous fournissons la spécification formelle et demandons au LLM de générer un script de preuve qui est accepté par HOL Light dans un délai de vérification fixe. À notre connaissance, s2n-bignum-bench est le premier benchmark public axé sur la synthèse de preuves vérifiables par machine pour des routines assembleur cryptographiques industrielles de bas niveau dans HOL Light. Ce benchmark constitue un banc d'essai exigeant et pertinemment pratique pour évaluer la démonstration de théorèmes basée sur les LLM au-delà des mathématiques de compétition. Le code pour configurer et utiliser le benchmark est disponible ici : 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}.