AI 형식 검증

LLM이 증명 스크립트와 형식 명세를 대신 써서, 코드가 모든 입력에서 원하는 성질을 지킨다는 것을 수학적으로 증명하는 방법이다. 테스트만으로는 부족한 보안·안전 코드에서 증명 검사기와 LLM을 반복해서 돌리는 방식으로 쓴다.

형식 검증은 원래 안전이 아주 중요한 코드에만 전문가가 손으로 증명을 써서 적용하던 방법이다. LLM이 증명 스크립트까지 쓰게 되면서 일반 소프트웨어에도 적용할 수 있는 수준으로 비용이 내려가고 있다. LLM으로 검증된 코드를 만드는 일을 바이브 코딩에 빗대 '베리코딩(vericoding)'이라 부르기도 한다.

환각이 문제 되지 않는 드문 작업

LLM이 엉터리 증명을 써도 괜찮다. 증명 검사기가 잘못된 증명을 거부하고 에이전트에게 다시 시도하게 만들기 때문이다. 검사기는 작고 그 자체가 검증된 코드라서 틀린 증명이 몰래 통과하기 어렵다. 그래서 증명 작성은 LLM에 특히 잘 맞는 일로 꼽힌다.

검증기와 LLM이 결과를 주고받는다

실제 흐름은 검증 도구와 LLM 사이의 반복이다. 버그 수정이라면 검증기가 문제를 찾아 결과를 내고, 그 내용으로 프롬프트를 만들어 LLM에 수정을 맡긴 뒤, 고친 코드를 다시 검증기에 넣어 통과 여부를 확인한다.

비용과 사람 몫은 아직 크다

가장 큰 한계는 비용이다. 증명 하나에 수억 토큰이 들 수 있어서 널리 쓰려면 효율이 관건이고, 새 모델일수록 토큰을 덜 쓰는 흐름은 있다. 지금은 전문 지식을 가진 사람이 과정을 이끌어야 한다는 점도 남아 있다.

검증 대상 시스템은 수학처럼 수많은 교재에 나오는 구조가 아니라서 학습 데이터 밖에서 LLM 추론이 막힐 수 있다는 지적도 있다. 증명이 통과해도 명세가 틀리면 의미가 없으니 명세는 반드시 사람이 확인한다.

사람들은 주로 이렇게 쓴다