Inferring multiple helper Dafny assertions with LLMs
Created by
- Haebom
Category
Empty
저자
Alvaro Silva, Alexandra Mendes, Ruben Martins
개요
Dafny 검증기는 강력한 정확성 보장을 제공하지만, 많은 수동 보조 어설션을 필요로 하여 채택에 큰 어려움을 야기합니다. 본 연구는 대규모 언어 모델(LLM)을 사용하여 Dafny 프로그램에서 누락된 보조 어설션을 자동으로 추론하는 방법을 연구합니다. 특히 여러 개의 누락된 어설션이 있는 경우에 중점을 둡니다. 이를 위해, DafnyBench 벤치마크를 어설션이 하나, 둘 또는 모두 제거된 큐레이션된 데이터 세트로 확장하고, 추론 난이도를 분석하기 위한 어설션 유형 분류법을 도입했습니다. LLM 예측과 오류 메시지 휴리스틱을 결합한 하이브리드 방법을 통해 오류 위치를 개선했습니다. DAISY (Dafny Assertion Inference SYstem)라는 새로운 도구로 이 접근 방식을 구현했습니다. DAISY는 단일 누락 어설션의 경우 프로그램의 63.4%, 다중 누락 어설션의 경우 31.7%를 검증합니다. 또한, 여러 유효한 복구 전략이 존재하고 모든 원래 어설션을 복구할 필요가 없음을 강조합니다.
시사점, 한계점
•
LLM을 활용하여 Dafny 프로그램의 누락된 보조 어설션을 자동 추론하여, 증명 엔지니어링 노력을 크게 줄임.
•
다중 누락 어설션 경우에도 유의미한 검증 성공률을 보임.
•
증명에 여러 유효한 복구 전략이 존재함을 보여줌.
•
DafnyBench 벤치마크를 확장하고 어설션 유형 분류법을 도입하여 분석 기반 마련.
•
단일 어설션의 경우 63.4%, 다중 어설션의 경우 31.7%의 검증 성공률은 개선의 여지가 있음.
•
모든 원래 어설션을 복구하는 것이 항상 필요한 것은 아님.
•
도구의 정확도 및 적용 범위는 추가적인 연구를 통해 개선될 수 있음.
