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

1. Problem Statement

While Large Language Models (LLMs) have demonstrated success in solving competition-style mathematical problems (e.g., Olympiad or Putnam competitions) using formal theorem provers, there is a significant gap in their ability to reason about real-world, low-level software implementations.

• The Gap: Existing benchmarks focus on abstract mathematics. Success in these domains does not guarantee an LLM can construct machine-checkable proofs for industrial cryptographic code, which involves complex architectural states, memory aliasing, endianness, and specific Instruction Set Architecture (ISA) semantics.
• The Challenge: Verifying low-level cryptographic assembly requires a distinct form of reasoning: starting from preconditions on registers/memory, symbolically executing decoded ARM or x86 instructions, and proving the final state satisfies a mathematical postcondition. This is qualitatively different from abstract theorem proving.

2. Methodology: S2N-BIGNUM-BENCH

The authors introduce s2n-bignum-bench, a new benchmark derived from the s2n-bignum library, an industrial-grade cryptographic library used at AWS. The library contains hand-tuned big-integer assembly routines (for x86 and ARM) that have already been formally verified using HOL Light (a minimalist interactive theorem prover).

Benchmark Construction

• Source Material: The benchmark is extracted from the open-source s2n-bignum repository (pinned to a specific commit).
• Task Format: Each of the 2,284 problems is a "context-query" task.
  • Context: A self-contained OCaml/HOL Light setup (setup.ml) that loads necessary definitions, constants, and previously proved theorems. The original proof bodies are replaced with a placeholder (CHEAT TAC).
  • Query: The specific theorem goal (query.txt) that the LLM must prove.
• Categorization: Problems are partitioned into four categories based on heuristics:
  1. Bit-vector lemmas (311)
  2. Program-state lemmas (552)
  3. Functional correctness (859): Split into ARM (437) and x86 (422) assembly verification.
  4. Generic (562): Auxiliary facts.
• Isolation: Each problem has a unique identifier (arch.filename.thm.N) to ensure standalone evaluation.

Evaluation Pipeline

• Submission: LLMs submit a proof script (a tactic expression) intended to replace the CHEAT TAC placeholder.
• Integrity Checks:
  • Syntax/Type Checking: Compiles the submission in the benchmark context to catch parser errors.
  • Axiom Detection: Checks if the submission introduces forbidden axioms (e.g., new_axiom) or uses CHEAT TAC.
  • Contamination Mitigation: Uses type-annotation obfuscation (printing types in verbose mode) to prevent models from memorizing specific theorem statements, though this is limited by HOL Light's parser consistency.
• Timeout Management: To handle the wide variance in proof execution times (milliseconds to hours), the benchmark uses a per-problem timeout map derived from profiling ground-truth human proofs. This prevents resource exhaustion while avoiding false negatives for legitimate but expensive proofs.

3. Key Contributions

1. First Industrial Assembly Benchmark: It is the first public benchmark focused on machine-checkable proof synthesis for industrial low-level cryptographic assembly in HOL Light.
2. End-to-End Pipeline: Provides a complete, offline evaluation harness, including artifact extraction, problem retrieval, and integrity checking mechanisms.
3. Security-Focused Integrity: Implements robust defenses against cheating (forbidden tactics) and data contamination (obfuscation), ensuring the validity of the evaluation.
4. Real-World Relevance: Shifts the focus from abstract math to ISA-aware, bit-precise reasoning, measuring capabilities closer to actual verification workflows used in security-critical systems.

4. Results (Baseline Experiments)

The authors evaluated GPT-5.3-Codex (accessed via codex-cli) as a preliminary baseline using a zero-shot prompting strategy.

• Performance:
  • Medium-effort mode: Solved 4.4% (101/2,284) of the problems.
  • High-effort mode: Solved 5.3% (121/2,284) of the problems.
• Category Breakdown:
  • The model performed best on Generic (11.7%) and Bit-vector (8.7%) lemmas.
  • Performance dropped significantly on Program-state (5.1%) and was 0.0% on Functional correctness for both ARM and x86 assembly in the high-effort mode (though 42 and 6 attempts were made, none succeeded).
• Observations: The low success rate on functional correctness highlights the current difficulty LLMs face in synthesizing complex, multi-step proofs for real assembly code, even with strong reasoning models.

5. Significance and Future Impact

• Paradigm Shift: This benchmark moves the field of Neural Theorem Proving (NTP) beyond "competition math" toward systems verification. It tests whether models can handle the nuances of hardware semantics, which is crucial for verifying cryptographic libraries.
• Reproducibility: By releasing isolated artifacts and an offline evaluation harness, the authors enable the research community to rigorously test and compare different NTP approaches without relying on cloud-based, non-deterministic setups.
• Future Directions: The authors note that while the current release focuses on functional correctness, the underlying s2n-bignum corpus also supports relational properties (e.g., constant-time discipline). This suggests a natural path for future benchmark extensions to evaluate security properties beyond extensional correctness.

In summary, s2n-bignum-bench establishes a rigorous, high-stakes testbed for evaluating the ability of LLMs to perform formal verification on real-world, security-critical code, revealing that while current models show promise in abstract reasoning, they struggle significantly with the complexities of low-level assembly verification.