LLM이 쓴 언어 명세, 인터프리터와 일치함을 Lean으로 증명하다

Ship Your Interpreter

Basis의 연구진은 LLM에게 작은 프로그래밍 언어 WHILE의 형식적 의미론을 작성하게 한 뒤, 실제 C 인터프리터를 RISC-V로 컴파일하고 Lean으로 두 동작이 모든 프로그램에서 일치함을 증명했다. 테스트만으로는 59자 함수 이름에서 드러난 버퍼 제한 같은 미묘한 불일치를 잡아낼 수 없었다. 명세 자체를 검증하는 이 접근은 검증된 소프트웨어 확산의 병목을 푸는 열쇠로 제시된다.