이 논문은 Why3를 위한 단계별 LLM 기반 파이프라인인 Diversify2Verify를 소개합니다. 이는 재귀적 및 명령형 배열/리스트 구현을 다양하게 생성하여 자동 검증 가능성을 높입니다. 이 접근 방식은 표현 특화 계약을 추론하고 검증 실패를 처리하기 위해 유계 검증자 안내 주석 복구를 사용합니다.

  • 저자들은 정수, 배열, 리스트에 대한 73개 작업의 벤치마크를 구성하여 292개의 구현 변형을 생성했습니다.
  • Diversify2Verify는 초기에 96개의 아티팩트를 검증했으며, 두 번의 복구 단계를 거쳐 154개로 증가했습니다.
  • 아티팩트 수준의 검증률이 32.9%에서 52.7%로 향상되었습니다.
  • 작업 수준에서는 73개 작업 중 49개 작업에서 최소 하나의 변형이 검증되어 67.1%의 성공률을 달성했습니다.

이 결과는 구현 다양성이 작업 등가 프로그램 중에서 검증에 유리한 아티팩트를 찾는 데 도움이 됨을 보여줍니다.