Reproduce “Building A Proof-Oriented Programmer That Is 64% Better Than GPT-4o Under Data Scarcity” on OpenResearch
Turn your favorite coding agents into research agents that review literature, develop hypotheses, and run experiments.
Universal app for Apple silicon and Intel. Requires macOS 11 or later.
About this paper
Dylan Zhang, Justin Wang, Tianran Sun
PoPilot trains models to generate and repair repository-level proofs in F*, a language whose compiler checks proofs against types expressing properties. It creates tasks and repair examples, using compiler checks and errors to filter solutions. On 1,000 held-out tasks, its 14B-parameter model scores 39.4% Gen+Rep versus GPT-4o’s 23.9%. This supports results on this F* benchmark, not other languages.
Summary by alphaXiv.
Tip: change arxiv.org to autoarxiv.org in any arXiv abstract link to open the paper here.