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

arXiv:2603.14628v2 Announce Type: replace-cross Abstract: 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 alread