s2n-bignum-bench: Практический бенчмарк для оценки способности больших языковых моделей к анализу низкоуровневого кода
s2n-bignum-bench: A practical benchmark for evaluating low-level code reasoning of LLMs
March 15, 2026
Авторы: Balaji Rao, John Harrison, Soonho Kong, Juneyoung Lee, Carlo Lipizzi
cs.AI
Аннотация
Нейросимволические подходы, сочетающие большие языковые модели (LLM) с формальными методами, недавно продемонстрировали высокие результаты на ориентированных на математику бенчмарках доказательства теорем. Однако успех в соревновательной математике сам по себе не доказывает способность строить доказательства для реальных реализаций. Мы устраняем этот разрыв с помощью бенчмарка, основанного на промышленной криптографической библиотеке, ассемблерные процедуры которой уже верифицированы в HOL Light. 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{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}.