SWE-bench Verified is a human-filtered subset of 500 instances from SWE-bench created in collaboration with OpenAI to provide a reliable evaluation set for coding agents and language models. Human annotators reviewed each instance to ensure problem descriptions are clear, test patches are correct, and tasks are solvable with available information. The Verified leaderboard shows results from a wide variety of AI coding systems, and a Bash Only view isolates language model performance using mini-SWE-agent in a minimal bash environment.
- Human validation ensures clarity, correctness of test patches, and solvability
- Bash-only comparison uses mini-SWE-agent with ReAct loop, no tools or scaffold
- Leaderboard distinguishes mini-SWE-agent LM results from full agent systems via Agent dropdown
- Release 2.x uses tool calling vs 1.x parses actions from output strings, making releases not directly comparable
- Human validation ensures clarity, correctness of test patches, and solvability
- Bash-only comparison uses mini-SWE-agent with ReAct loop, no tools or scaffold
- Leaderboard distinguishes mini-SWE-agent LM results from full agent systems via Agent dropdown
- Release 2.x uses tool calling vs 1.x parses actions from output strings, making releases not directly comparable
- Demonstrates how to improve two pretrained models' proficiency in the Dafny verified programming language.
- Uses 178 programming problems from the MBPP dataset for prompting GPT-4 and PaLM-2 to generate methods in Dafny.
- Three types of prompts were used: a direct contextless prompt, one that includes a signature of the method and test cases, and a third one that decomposes the problem into steps and includes dynamically chosen similar examples.
- GPT-4 was able to generate verified (and human-evaluated) Dafny methods in 58% of the cases with the third prompt.
- Contributes a collection of 153 MBPP problems implemented and formally verified in Dafny, 50 written by authors and 103 synthesized by GPT-4.
- Uses 178 programming problems from the MBPP dataset for prompting GPT-4 and PaLM-2 to generate methods in Dafny.
- Three types of prompts were used: a direct contextless prompt, one that includes a signature of the method and test cases, and a third one that decomposes the problem into steps and includes dynamically chosen similar examples.
- GPT-4 was able to generate verified (and human-evaluated) Dafny methods in 58% of the cases with the third prompt.
- Contributes a collection of 153 MBPP problems implemented and formally verified in Dafny, 50 written by authors and 103 synthesized by GPT-4.
