"AI 해킹 막으려면 수학적 증명뿐"… LLM으로 코드 인터프리터 동작 완벽 검증한 연구 등장

요약 인공지능 연구소 Basis의 연구진이 대형 언어 모델(LLM)과 수학적 증명 검증 도구인 Lean을 결합해 프로그래밍 언어의 인터프리터 동작을 기계어 수준까지 완벽하게 검증하는 새로운 기법을 발표했습니다. 최근 LLM이 소프트웨어의 보안 취약점을 찾아내 악용하는 능력이 비약적으로 발전함에 따라, 시스템을 근본적으로 안전하게 만들기 위한 '검증된 소프트웨어(Verified Software)'의 중요성이 커지고 있습니다. 소프트웨어가 버그 없이 의도대로 작동함을 수학적으로 증명하려면 먼저 해당 프로그래밍 언어의 모든 문법과 동작을 수학적으로 서술한 '정형 시맨틱(Formal Semantics)'이 필요한데, 이는 통상 전문가들이 수년에 걸쳐 작성해야 하는 거대한 병목이었습니다. 연구진은 LLM이 이 정형 시맨틱을 직접 작성하게 하되, 인터프리터를 이미 정형화된 RISC-V 저수준 기계어로 컴파일한 뒤 LLM이 작성한 시맨틱 규칙과 실제 컴파일된 인터프리터의 실행 결과가 모든 프로그램에 대해 100% 일치함을 Lean에서 수학적으로 증명하도록 유도했습니다. 실험에는 교재용 소형 언어인 WHILE을 확장한 언어(1,855줄의 C언어 인터프리터)가 사용되었으며, LLM이 시맨틱 규칙과 증명을 동시에 발전시키도록 하여 규칙에 오류가 있으면 증명 과정에서 막히도록 설계했습니다. 연구진은 정형 시맨틱과 증명 전체 코드를 깃허브에 공개하며, 향후 모든 소프트웨어로 확장 가능한 안전한 검증 체계를 목표로 하고 있다고 밝혔습니다.