인간이 20년 걸리던 코드 검증, AI한테 시켰더니 수조 번 테스트도 못 잡은 버그까지 털어버림
핵심 요약
앤트로픽이 Theorem과 협력해 클로드로 123개 오픈소스 라이브러리의 정식 소프트웨어 검증을 어셈블리 레벨에서 성공시켰습니다.
수조 번의 테스트에서도 잡히지 않던 오랜 버그를 찾아내는 등 막대한 인력과 시간이 들던 정식 검증의 대중화 가능성을 입증했습니다.
연구진은 검증 결과 일부를 공개하고 다른 오픈소스 프로젝트에도 해당 파이프라인을 지원할 예정입니다.
요약 AI 연구 기업 앤트로픽(Anthropic)이 Theorem과의 협업을 통해 대규모 언어 모델(LLM)인 클로드(Claude)를 활용해 대규모 정식 소프트웨어 검증(Formal Software Verification)을 수행한 연구 결과를 발표했습니다.
정식 검증은 프로그램을 수학적 모델로 변환해 보안 규칙을 엄격하게 증명하는 기법이지만, 기존에는 항공우주 소프트웨어나 극도로 중요한 커널처럼 수십 년 단위의 전문 인력이 투입되는 특수 분야에서만 제한적으로 쓰였습니다. 일례로 seL4 커널의 경우 구현에는 2인년이 들었으나 정식 검증에는 20인년이 소요될 정도였습니다.
연구진은 클로드를 투입해 123개 오픈소스 라이브러리의 RISC-V 어셈블리 코드 레벨에서 보안 속성을 증명하는 실험을 진행했습니다. 그 결과 싱글스레드 바이너리 및 64MB 이하 입력 등의 특정 전제 조건 하에서 메모리 안전성 오류나 단언 실패(assertion failure) 없이 정상 종료됨을 증명해 냈습니다. 이 과정에서 수조 번의 기존 테스트를 거치며 수년간 발견되지 않았던 잠재적 버그들까지 클로드가 새롭게 찾아내는 성과도 거두었습니다. 앤트로픽은 검증 파이프라인의 일부 증명 데이터와 관련 시맨틱을 공개하며 오픈소스 생태계 전반으로 정식 검증 적용을 확대할 계획을 밝혔습니다.