Skip to content

Commit

Permalink
Merge branch 'master' into HEAD
Browse files Browse the repository at this point in the history
  • Loading branch information
quinn-dougherty committed Sep 13, 2024
2 parents 965dcdb + b56eaaf commit ee305ad
Show file tree
Hide file tree
Showing 4 changed files with 382 additions and 26 deletions.
7 changes: 7 additions & 0 deletions README.md
Original file line number Diff line number Diff line change
Expand Up @@ -31,6 +31,13 @@ challenging LLMs to write dependently typed _and_ formally verified code
- [ ] trawl aoc of the ones we have lean4 solutions for some nontriviality:
- meaning a way to beat the dumb way on O()

## Conceptually 3
- ask llm to generate property tests for apps problems
- subject corresponding apps solutions to those property tests
- ask llm to generate sorry'd out lean theorems from property tests
- output task: original task plus sorry'd out lean theorems.

## TODO
- [ ] read dafny benchmark paper
- [ ] read the APPS easies.
- [ ] remember that we should show baselines from openai, anthropic, and deepseek, and llama
Loading

0 comments on commit ee305ad

Please sign in to comment.