LLM이 생성한 Lean 프로그램의 형식적 명세를 검증하는 데 있어 property-based testing(PBT)​이 상징적 증명에 비해 비용 효율적인 대안임이 밝혀졌습니다.

명세는 프로그램과 기계 간의 수학적 계약으로, 명세가 부정확하면 검증 결과가 무의미해집니다.

기존의 상징적 명세 검증 방식은 SMT 솔버의 자동화 한계로 인해 Lean에서는 느리고 비용이 많이 듭니다.

이에 저자들은 명세의 적합성(admissibility)​, 건전성(soundness)​, 고유성(uniqueness) 세 가지 속성을 분리해 PBT로 빠르게 반례를 찾아내는 방식을 제안했습니다.

Lean 4의 PBT 라이브러리인 Plausible을 활용해 LLM이 작성한 명세의 약점을 효과적으로 탐지했으며, 실제로 VERINA와 CLEVER 벤치마크에서 약 10%의 명세 오류를 발견했습니다.

특히, 범위 제약 누락, 산술 연산의 암묵적 동작, 그리고 구현 버그까지 PBT가 드러내는 사례가 소개되었습니다.

PBT는 완전한 증명을 대체하지는 못하지만, 명세 자체의 신뢰성 검증에 있어 비용 대비 효율적인 방법임을 입증했습니다.

향후 연구로는 명세의 다중 허용 출력 문제 해결과 명세 언어 제한을 통한 명세의 명확성 향상이 제안됩니다.

요약하면, PBT와 상징적 증명을 결합해 형식 검증 비용을 줄이고 신뢰성을 높이는 새로운 검증 패러다임이 가능해졌습니다.