S2N-BIGNUM-BENCH: LLM의 저수준 코드 추론 평가를 위한 실용적 벤치마크

기존 LLM 수학 증명 벤치마크는 경진대회용 수학 문제에 치중되어 실제 소프트웨어 공학적 검증 능력을 평가하기 어렵다. 이 논문은 실제 산업 현장에서 사용되는 AWS의 암호화 어셈블리 코드를 대상으로 LLM이 기계가 확인 가능한 증명을 생성할 수 있는지 평가하는 최초의 벤치마크를 제시하여 AI의 실무적 추론 능력을 측정한다.

LLM의 논리 추론 능력은 주로 텍스트 패턴 매칭과 Attention Mechanism을 통한 다음 토큰 예측에 기반한다. 수학 문제 풀이에서 LLM은 단계별 풀이 과정을 흉내 낼 수 있지만, 그 과정이 엄격한 논리 체계 내에서 무결한지 스스로 검증하는 데 한계가 있다. 특히 하드웨어 레지스터와 메모리 상태를 다루는 저수준 코드 검증은 추상적인 수학보다 훨씬 더 정밀한 상태 추적이 요구된다.

이 논문은 LLM을 대화형 정리 증명기(ITP)인 HOL Light와 결합하여 이 문제를 해결한다. ITP는 아주 작은 신뢰할 수 있는 커널을 통해 모든 논리적 단계를 검증하는 시스템이다. LLM은 이 시스템 위에서 증명 전략인 '전술(Tactic)'을 생성하는 역할을 수행한다. 이는 LLM의 생성 능력과 ITP의 결정론적 검증 능력을 결합하여, 모델이 단순히 정답을 맞히는 것이 아니라 논리적으로 완벽한 증명 과정을 설계할 수 있는지 테스트하는 구조다.

결과적으로 LLM은 ARM이나 x86 어셈블리 명령어가 실행된 후의 메모리 상태가 수학적 명세와 일치함을 증명해야 한다. 이는 모델이 하드웨어 아키텍처의 동작 원리(ISA Semantics)를 이해하고 이를 논리적 증명 단계와 연결할 수 있어야 함을 의미하며, 이를 통해 LLM의 실무적 추론 한계를 명확히 측정할 수 있다.

s2n-bignum-bench는 AWS의 오픈소스 암호화 라이브러리에서 2,284개의 증명 과제를 추출하여 구성했다. 각 과제는 증명에 필요한 정의와 이전 결과가 포함된 컨텍스트(setup.ml)와 증명해야 할 목표(query.txt)로 나뉜다. [입력값: 어셈블리 코드의 사전/사후 조건 및 HOL Light 환경 → 연산: LLM이 목표를 달성하기 위한 전술(Tactic) 시퀀스 생성 → 출력 의미: 생성된 증명이 HOL Light 커널에 의해 최종적으로 수용되는지 여부]

추출된 문제는 네 가지 카테고리로 분류된다. 비트 연산 성질을 다루는 Bit-vector lemmas(311개), 프로그램 상태 변화를 다루는 Program-state lemmas(552개), 실제 어셈블리 루틴의 정확성을 증명하는 Functional correctness(859개), 그리고 기타 보조 정리를 포함하는 Generic(562개)이다. 각 문제는 고유한 식별자를 가지며 독립적인 실행 환경에서 평가된다.

평가 파이프라인은 3단계로 진행된다. 먼저 OCaml 파서를 통해 제출된 증명의 구문 오류를 체크한다. 이후 HOL Light 환경에서 실제 증명을 실행하며, 이때 CHEAT_TAC이나 new_axiom과 같은 부정행위 전술 사용 여부를 커널 수준에서 감시한다. 마지막으로 각 문제별로 프로파일링된 가변 타임아웃(최대 3시간) 내에 증명이 완료되는지 확인하여 최종 성공 여부를 판정한다.

GPT-5.3-Codex 모델을 베이스라인으로 평가한 결과, 전체 2,284개 문제 중 Medium Effort 모드에서 101개(4.4%), High Effort 모드에서 121개(5.3%)의 성공률을 기록했다. 이는 기존 수학 중심 벤치마크에 비해 현저히 낮은 수치로, 저수준 코드 추론이 LLM에게 매우 어려운 과제임을 입증한다.

카테고리별 분석 결과, 일반적인 논리 정리를 다루는 Generic(11.7%)과 Bit-vector(8.7%)에서는 일부 성과를 거두었으나, 실제 ARM 및 x86 어셈블리 코드의 기능적 정확성을 증명하는 fc_arm 및 fc_x86 카테고리에서는 단 하나의 문제도 해결하지 못했다(0.0%). 이는 현재의 범용 LLM이 복잡한 하드웨어 명령어의 의미론을 파악하고 이를 정밀한 증명 단계로 변환하는 능력이 부족함을 시사한다.

오류 분석에서는 제출된 답변 중 상당수가 구문 오류로 인해 실행 단계에 진입하지 못했음이 확인됐다. Medium Effort에서는 743개, High Effort에서는 766개만이 구문 체크를 통과했으며, 이는 LLM이 정리 증명기의 엄격한 문법과 타입 체계를 준수하는 데에도 큰 어려움을 겪고 있음을 보여준다.

s2n-bignum-bench는 LCF 스타일의 정리 증명기인 HOL Light를 기반으로 설계되었다. LCF 스타일의 핵심은 아주 작은 '신뢰할 수 있는 커널'만이 정리(Theorem) 객체를 생성할 수 있다는 점이며, 이를 통해 LLM이 생성한 증명 과정에 논리적 비약이 있을 경우 커널이 이를 즉시 거부하도록 보장한다.

벤치마크의 각 문제는 독립적인 OCaml 모듈로 격리되어 있으며, 이는 모델이 증명 과정에서 다른 파일의 힌트를 참조하는 것을 방지하는 동시에 병렬 평가를 용이하게 한다. 또한 ISA(Instruction Set Architecture) 모델을 HOL Light 내에 수학적으로 정의하여, 어셈블리 명령어 하나하나가 레지스터와 메모리에 미치는 영향을 기호 실행(Symbolic Execution) 방식으로 추적할 수 있게 구성되었다.

데이터 오염을 방지하기 위해 타입 어노테이션을 명시적으로 노출하거나 난독화하는 메커니즘을 포함한다. 이는 모델이 단순히 학습 데이터에 포함된 증명 스크립트를 암기하여 출력하는 것을 막고, 주어진 컨텍스트 내에서 실제적인 논리 추론을 수행하도록 강제하는 역할을 한다.

현재 벤치마크는 기능적 정확성(Functional Correctness) 증명에 집중되어 있으며, 암호화 알고리즘에서 중요한 보안 속성인 상수 시간 실행(Constant-time) 보장이나 최적화된 루틴 간의 등가성 증명과 같은 관계적 속성은 아직 포함되지 않았다.