DafnyBench

DAFNYBENCH : 공식 소프트웨어 검증을위한 벤치 마크

논문의 데이터 세트 및 코드 dafnybench : 공식 소프트웨어 검증을위한 벤치 마크

데이터 세트도 다운로드 할 수 있습니까? 포옹 얼굴.

개요

Dafnybench는 750 개가 넘는 Dafny 프로그램을 통해 공식 소프트웨어 검증을위한 기계 학습 시스템을 교육하고 평가하는 데 가장 큰 벤치 마크입니다.

용법

• 데이터 세트 : DafnyBench의 데이터 세트 (782 프로그램 포함)는 ground_truth 세트 및 hints_removed 세트를 포함하는 DafnyBench 디렉토리에서 찾을 수 있습니다 (컴파일러 힌트, 즉 Annoataions, 제거).
• 평가 : 모델에 hints_removed 세트의 테스트 파일에서 누락 된 힌트를 채우도록 모델에 DAFNYBENCH의 LLMS를 평가하고 재구성 된 프로그램을 DAFNY에 의해 확인할 수 있는지 확인합니다. eval 디렉토리를 참조하십시오.

평가를 위해 설정 하시겠습니까?

1. 이 튜토리얼에 따라 컴퓨터에 dafny를 설치하십시오
2. 이 저장소에 클론 및 cd
3. 다음 줄을 실행하여 환경을 설정하십시오.

 python -m venv stats
source stats/bin/activate
pip install -r requirements.txt
cd eval

4. 루트 디렉토리의 환경 변수 설정 :

 export DAFNYBENCH_ROOT=

5. 컴퓨터에서 DAFNY 실행 파일로의 환경 변수 설정 (예 : /opt/homebrew/bin/Dafny ) :

 export DAFNY_PATH=

6. API 액세스를 통해 LLM을 평가하는 경우 API 키를 설정하십시오. 예를 들어:

 export OPENAI_API_KEY=

7. 단일 테스트 프로그램에서 LLM을 평가하도록 선택할 수 있습니다.

 python fill_hints.py --model "gpt-4o" --test_file "Clover_abs_no_hints.dfy" --feedback_turn 3 --dafny_path "$DAFNY_PATH"

또는 전체 데이터 세트를 평가하십시오.

 export model_to_eval='gpt-4o'
./run_eval.sh

내용물 ?

• DafnyBench
  • 782 Dafny 프로그램 모음. 각 프로그램에는 dafny & a hints_removed 버전으로 힌트 (즉, 주석)가 제거 된 ground_truth 버전이 있습니다.
• eval
  • dafnybench에서 LLM을 평가하기위한 스크립트가 포함되어 있습니다
• results
  • results_summary 모든 테스트 프로그램에서 LLMS의 성공을 요약하는 데이터 프레임
  • reconstructed_files 힌트가 채워진 LLM 출력
  • analysis - 결과 분석을위한 노트북이 포함되어 있습니다

인용?

 @article { loughridge2024dafnybench ,
         title = { DafnyBench: A Benchmark for Formal Software Verification } , 
         author = { Chloe Loughridge and Qinyi Sun and Seth Ahrenbach and Federico Cassano and Chuyue Sun and Ying Sheng and Anish Mudide and Md Rakib Hossain Misu and Nada Amin and Max Tegmark } ,
         year = { 2024 } ,
         journal = { arXiv preprint arXiv:2406.08467 }
}