Laurel: Unblocking Automated Verification with Large Language Models
Created by
- Haebom
Category
Empty
저자
Eric Mugnier, Emmanuel Anaya Gonzalez, Ranjit Jhala, Nadia Polikarpova, Yuanyuan Zhou
개요
본 논문은 Dafny와 같은 프로그램 검증기가 SMT 솔버에 증명을 위탁하는 자동화 과정에서 발생하는 어려움을 해결하기 위해, 대규모 언어 모델(LLM)을 이용하여 자동으로 assertion을 생성하는 도구인 Laurel을 제안한다. Laurel은 검증기의 에러 메시지를 분석하여 assertion을 삽입할 위치를 지정하고, 새로운 증명 유사성 측정 기준을 기반으로 동일한 코드베이스의 예시 assertion을 제공하는 두 가지 도메인 특화 프롬프팅 기법을 사용한다. 실제 Dafny 코드베이스에서 추출한 복잡한 lemma로 구성된 새로운 벤치마크 DafnyGym을 사용하여 평가한 결과, Laurel은 몇 번의 시도만으로 필요한 assertion의 56.6% 이상을 생성할 수 있음을 보여주었다. 이는 LLM을 통해 인간의 개입 없이 프로그램 검증기를 효율적으로 지원할 수 있음을 시사한다.
시사점, 한계점
•
시사점:
◦
대규모 언어 모델을 활용하여 프로그램 검증 과정의 자동화 수준을 향상시킬 수 있음을 보여줌.
◦
LLM 기반 assertion 생성을 통해 프로그램 검증 엔지니어의 부담을 줄일 수 있음.
◦
제안된 도메인 특화 프롬프팅 기법이 LLM의 assertion 생성 성공률을 높이는 데 효과적임.
◦
DafnyGym과 같은 새로운 벤치마크 데이터셋은 향후 관련 연구에 기여할 수 있음.
•
한계점:
◦
현재 56.6%의 성공률은 모든 assertion을 자동 생성하기에는 부족함. 더 높은 성공률을 달성하기 위한 추가 연구가 필요함.
◦
DafnyGym 벤치마크의 일반성에 대한 검토가 필요함. 다른 프로그래밍 언어나 검증기에 대한 적용 가능성을 추가로 연구해야 함.
◦
LLM의 출력 결과에 대한 신뢰성 및 안전성에 대한 추가적인 분석이 필요함.
