s2n-bignum-bench: A practical benchmark for evaluating low-level code reasoning of LLMs
이 논문은 경쟁 수학 문제를 넘어 실제 산업용 저수준 암호화 어셈블리 코드의 검증 능력을 평가하기 위해, AWS 의 s2n-bignum 라이브러리를 기반으로 HOL Light 에서 기계 검증 가능한 증명 생성을 수행하는 새로운 벤치마크인 's2n-bignum-bench'를 제안합니다.
원저자:Balaji Rao, John Harrison, Soonho Kong, Juneyoung Lee, Carlo Lipizzi
지금까지 AI 가 수학적 추론 능력을 테스트받던 방식은 마치 수학 올림피아드를 치르는 것과 비슷했습니다.
기존 방식 (MiniF2F 등): "이 복잡한 수학 공식이 맞는지 증명해봐"라고 물으면, AI 가 논리적으로 답을 내놓습니다. 이는 AI 가 논리적으로 생각할 수 있음을 보여줍니다.
하지만 문제점: 수학 문제를 잘 푼다고 해서, 실제 공장 기계나 암호화 소프트웨어처럼 복잡한 현실 세계의 문제를 해결할 수 있다는 보장은 없습니다. 마치 수학 경시대회에서 1 등 한 사람이 갑자기 비행기 엔진을 고칠 수 있다는 뜻은 아니죠.
이 논문은 **"실제 AWS(아마존 웹 서비스) 에서 사용하는 암호화 소프트웨어의 저수준 (Assembly) 코드"**를 검증할 수 있는 새로운 시험지를 만들었습니다.
🛠️ 2. 이 시험지가 왜 특별한가? (s2n-bignum-bench)
이 벤치마크는 **AWS 의 's2n-bignum'**이라는 라이브러리를 기반으로 합니다. 이 라이브러리는 암호를 빠르게 처리하기 위해 직접 쓴 **컴퓨터의 가장 기초적인 언어 (어셈블리)**로 만들어졌습니다.
비유: 기존 시험지가 "이론물리학 문제"였다면, 이 시험지는 **"실제 원자로의 제어판 회로도가 올바르게 작동하는지 확인하는 작업"**과 같습니다.
과제: AI 에게 "이 코드가 수학적으로 옳은지 증명해줘"라고 요청합니다. 이때 AI 는 단순히 답을 말하면 안 되고, HOL Light라는 특수한 '증명 도구'가 읽을 수 있는 엄격한 증명 스크립트를 직접 작성해야 합니다.
🎯 3. 이 연구의 핵심 기여 (4 가지 특징)
저자들은 이 시험지를 만들기 위해 다음과 같은 노력들을 했습니다:
2,284 개의 개별 문제: AWS 의 실제 코드에서 2,284 개의 작은 증명 과제를 잘라내어, 각각 독립적인 시험 문제로 만들었습니다.
완전한 오프라인 평가: 인터넷 없이도 AI 가 답을 내고, 그 답이 맞는지 자동으로 검사하는 시스템을 갖췄습니다.
사기 방지 시스템 (Integrity):
AI 가 "CHEAT TAC(속임수)" 같은 단어를 쓰거나, 증명에 필요한 가짜 규칙을 만들어내면 즉시 걸러냅니다.
마치 시험 감독관이 "이 답안은 복사한 거 아니야?"라고 의심하며 꼼꼼히 확인하는 것과 같습니다.
실제 환경 반영: 이 시험은 컴퓨터의 메모리, 비트 (bit) 단위 연산, 하드웨어의 특성까지 고려해야 하므로, 단순한 수학 문제보다 훨씬 어렵고 현실적입니다.
📊 4. 결과는 어땠나요? (AI 의 현재 실력)
저자들은 최신 AI 모델 (GPT-5.3-Codex) 을 이 시험에 도전시켰습니다. 결과는 다음과 같았습니다:
성공률: 전체 2,284 문제 중 **약 4.4% ~ 5.3%**만 성공했습니다.
의미: 이 수치는 낮아 보이지만, **"실제 산업용 암호화 코드를 검증하는 증명"**이라는 과제의 난이도가 매우 높기 때문입니다. 마치 초보자가 F1 레이싱 카를 몰고서 100m 를 주파하는 것과 비슷합니다.
결론: AI 가 수학 경시대회에서는 잘하지만, 현실 세계의 복잡한 코드를 검증하는 능력은 아직 초기 단계임을 보여주었습니다.
💡 5. 왜 이 연구가 중요한가?
이 연구는 AI 가 단순히 "지식"을 가지고 있는 것을 넘어, 안전하고 신뢰할 수 있는 소프트웨어를 직접 검증할 수 있는 능력을 갖추기 위한 첫걸음입니다.
비유: AI 가 이제까지 "수학책"만 읽었다면, 이 벤치마크는 AI 를 실제 병원 수술실로 데려가서 수술 도구 사용법을 검증하는 것과 같습니다.
미래: 이 벤치마크를 통해 AI 가 더 발전하면, 우리가 사용하는 은행 앱, 암호화 통신, 자율주행차 등의 소프트웨어가 해킹이나 오류 없이 안전하게 작동하도록 AI 가 직접 검증해줄 날이 올지도 모릅니다.
📝 요약
이 논문은 **"AI 가 진짜로 현실 세계의 복잡한 컴퓨터 코드를 검증할 수 있는가?"**를 테스트하기 위해, AWS 의 실제 암호화 코드를 바탕으로 한 새로운 시험지를 만들었다고 말합니다. 아직 AI 는 이 시험에서 많이 떨어졌지만, 이 시험지를 통해 AI 의 '실전 능력'을 키우고, 더 안전한 소프트웨어 세상을 만들 수 있는 길을 열었습니다.
1. 문제 정의 (Problem)
최근 대규모 언어 모델 (LLM) 과 형식 방법 (Formal Methods) 을 결합한 신경 형식 증명 (Neurosymbolic Theorem Proving) 은 수학 올림피아드 수준의 벤치마크 (예: MiniF2F, PutnamBench) 에서 우수한 성과를 거두고 있습니다. 그러나 이러한 성공이 실제 엔지니어링 시스템, 특히 저수준의 암호학 코드가 구현된 기계어 (Assembly) 에 대한 증명 능력을 보장하지는 않습니다.
기존 벤치마크들은 추상적인 수학 문제나 고수준의 검증 조건 (Verification Conditions) 에 집중되어 있어, 다음과 같은 핵심적인 격차가 존재합니다:
아키텍처 상태의 부재: 수학 증명과 달리 저수준 코드 증명은 레지스터, 메모리, 엔디안 (Endianness), 메모리 별칭 (Aliasing) 등 하드웨어 아키텍처 상태를 고려해야 합니다.
실제 구현의 검증 부재: 대회용 수학 문제와 달리, 실제 배포된 암호학 라이브러리의 기계어 코드가 명세와 일치함을 증명하는 작업은 LLM 평가에서 소외되어 왔습니다.
2. 방법론 (Methodology)
저자들은 AWS 에서 사용하는 암호학 라이브러리인 s2n-bignum을 기반으로 한 새로운 벤치마크인 s2n-bignum-bench를 제안했습니다.
데이터 소스: AWS 의 Automated Reasoning Group 이 이미 HOL Light(고차 논리 증명 시스템) 로 검증한 s2n-bignum 라이브러리의 증명 의무 (Proof Obligations) 를 활용합니다.
작업 구성:
총 2,284 개의 증명 과제를 독립적인 컨텍스트 - 쿼리 (Context-Query) 태스크로 패키징했습니다.
각 과제는 HOL Light 의 OCaml 모듈을 포함하며, 원래 증명 본문은 CHEAT TAC (Lean 의 sorry 와 유사한 플레이스홀더) 로 대체된 상태입니다.
LLM 에게는 목표 명세 (Goal) 와 필요한 정의/상수만 제공되며, **HOL Light 가 수용할 수 있는 유효한 증명 스크립트 (Proof Script)**를 생성하도록 요구합니다.
문제 분류:
Bit-vector lemmas (311 개): 비트 벡터 관련 보조 정리.
Program-state lemmas (552 개): 프로그램 상태 (레지스터/메모리) 관련 정리.
Functional correctness (859 개): ARM 및 x86 아키텍처의 기능적 정확성 증명.
Generic (562 개): 기타 보조 사실.
평가 프로토콜:
제출된 증명 스크립트는 HOL Light 커널에서 컴파일 및 실행되어 검증됩니다.
정합성 검사:new_axiom 사용 여부, CHEAT TAC 사용 여부, 파서 레벨의 구문 오류를 자동으로 감지하여 부정행위를 차단합니다.
오염 방지: 문제의 타입 주석을 모호하게 변형 (Obfuscation) 하여 LLM 이 훈련 데이터에서 암기된 문제를 해결하는 것을 방지합니다.
타임아웃 관리: 증명 복잡도에 따라 문제별 타임아웃을 동적으로 할당하여 계산 자원의 비효율적 소모를 방지합니다.
3. 주요 기여 (Key Contributions)
산업용 저수준 암호학 어셈블리 검증 벤치마크: HOL Light 에서 기계어 코드의 기능적 정확성을 검증하는 첫 번째 공개 벤치마크를 제공합니다.
완전한 오프라인 평가 파이프라인: 2,284 개의 독립적인 문제 아티팩트, 설정 스크립트, 평가 도구를 제공하여 재현 가능한 평가를 가능하게 합니다.
강력한 무결성 및 오염 방어 메커니즘: 금지된 명령어 사용 감지, 파서 검증, 타입 주석 변형을 통한 데이터 오염 방지를 구현했습니다.
실제 검증 워크플로우에 근접한 평가: 추상 수학이 아닌, ISA(명령어 세트 아키텍처) 를 인지하고 비트 단위로 정밀한 추론이 필요한 실제 검증 작업을 평가합니다.
4. 결과 (Results)
저자들은 GPT-5.3-Codex 를 기반으로 한 초기 베이스라인 실험을 수행했습니다.
성능: 전체 2,284 개 문제 중 Medium-effort 모드에서 4.4% (101 개), **High-effort 모드에서 5.3% (121 개)**의 성공률을 기록했습니다.
분포:
generic 및 bit-vector 카테고리에서 상대적으로 높은 성공률 (약 10% 이상) 을 보였습니다.
program-state 카테고리에서는 2.9%~5.1% 수준이었습니다.
실제 기능적 정확성 (Functional Correctness) 을 증명해야 하는 ARM 및 x86 어셈블리 문제 (fc arm, fc x86) 에서는 0% 의 성공률을 기록했습니다. 이는 현재 LLM 이 복잡한 저수준 기계어 증명을 수행하는 데 여전히 큰 한계가 있음을 시사합니다.
의미: 이러한 낮은 성공률은 해당 작업이 단순한 패턴 매칭을 넘어선 심층적인 추론과 형식적 검증 능력을 필요로 함을 보여줍니다.
5. 의의 (Significance)
실제 적용 가능성: 이 벤치마크는 LLM 이 실제 보안 및 신뢰성이 중요한 시스템 (암호학 라이브러리 등) 의 저수준 코드를 검증할 수 있는 능력을 평가하는 새로운 표준을 제시합니다.
연구 방향 전환: 대회용 수학 문제 중심의 평가에서 벗어나, 실제 소프트웨어 공학 및 시스템 검증에 필요한 ISA 인지형 (ISA-aware) 비트 정밀 추론 능력을 평가하는 패러다임 전환을 촉진합니다.
향후 확장 가능성: 현재는 기능적 정확성에 초점을 맞추고 있으나, 향후 상수 시간 (Constant-time) 준수성이나 최적화된 루틴과 검증 친화적 루틴 간의 동치성 증명 등 관계적 속성 (Relational Properties) 으로 벤치마크를 확장할 수 있는 토대를 마련했습니다.
결론적으로, s2n-bignum-bench는 LLM 이 이론적 수학 능력을 넘어 실제 산업 수준의 저수준 시스템 코드를 형식적으로 검증할 수 있는지를 측정하는 필수적인 도구로 자리매김할 것으로 기대됩니다.