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

Balaji Rao, John Harrison, Soonho Kong +2

Neurosymbolic approaches leveraging Large Language Models (LLMs) with formal methods have recently achieved strong results on mathematics-oriented theorem-proving benchmarks. Howev…