Towards Neural Synthesis for SMT-Assisted Proof-Oriented Programming
summary
Curated a reproducible dataset of about 600K lines and 32K top-level F definitions (extended to 940K lines and 54K defs) plus a program‑fragment checker that calls F to accept only verifiable candidates, and measure success as pass@10; models get 31% on a held‑out project with full context and retrieval, dropping to 21% without file context. Retrieval uses embeddings of type+name and nearby file content, and fine‑tuned small models such as StarCoder-level models match GPT‑4 quality at much lower cost, with fine‑tuning eliminating most syntax errors.
AI-written summary · about
chapters (12)
- 0:00F* and talk intro
- 1:10F* overview and syntax
- 2:33F* code dataset
- 4:00F* definition challenges
- 6:53Dataset construction
- 8:21Dataset split for eval
- 9:47Prompt setup for eval
- 11:58Model performance
- 13:24Fine-tuning smaller models
- 14:49Retrieval augmentation
- 15:51Future work
- 17:20Q&A
related talks
41m"Do What I Mean": The History of AI and Program Synthesis
54mA World Without Programmers?
19mAutomated Program Refinement: Guide and Verify Code Large Language Model with(…)
01h 04mInvited Talk: Finding Good Programs by Avoiding Bad Ones
01h 03mImproved Assistance for Interactive Proof
15mKeynote: Pre-training and Fine-tuning of Code Generation Models
01h 09mCodex presentation & demo
37mGPT-3-Powered Type Error Debugging: Investigating the Use of Large Language Models...