어려운 작업이 더 이상 어렵지 않을 때

LLM을 활용해 Move 언어의 새로운 타입 시스템을 위한 형식적 건전성 증명(formal soundness proofs)을 단 4주 만에 완료했다. 이는 기존 프로그래밍 언어(PL) 연구에서 전체 노력의 80~90%를 차지하던 메타 이론의 기계화 과정을 획기적으로 단축한 사례다.

이러한 변화는 PL 연구의 출판 문화를 근본적으로 바꾸고 있다. 과거에는 연구의 가치를 인정받기 위해 막대한 인간의 노력(대규모 구현, 벤치마킹, 수작업 증명)이 필수적이었으나, 이제는 숙련된 연구자가 LLM을 통해 한 달 내에 수준 높은 논문을 작성할 수 있게 되었다.

실제로 POPL 논문 제출 건수가 약 350건에서 600건으로 두 배 가까이 급증하는 등 변화가 나타나고 있다. 이는 단순한 AI 생성물의 증가가 아니라, 증명과 구현 같은 번거로운 과정을 자동화하여 연구 속도를 10배 높인 결과다.

앞으로 PL 연구자들은 더 높은 기준을 설정해야 한다. 단순한 계산 모델 정의를 넘어, LLM과 같은 현대적 도구를 활용해 과거에는 상상할 수 없었던 더 야심 찬 도전 과제에 집중해야 할 것이다.