Towards Neural Synthesis for SMT-Assisted Proof-Oriented Programming

This conference talk explores the potential of AI in automating proof-oriented programming, presenting a substantial dataset of F* programs and proofs to advance research in this area. Learn about the curation of 600K lines of open-source F* code from production systems like Windows and Linux, containing approximately 32K top-level definitions that represent type-directed program and proof synthesis problems. Discover how the researchers developed a program-fragment checker to verify candidate solutions and expanded their dataset to 940K lines with 54K definitions, creating what may be the largest corpus of SMT-assisted program proofs with reproducible checking. The presentation reveals promising findings about fine-tuned smaller language models (Phi-2, StarCoder) performing comparably to larger models like GPT-4 at lower computational costs, and demonstrates how type-based retrieval augmentation techniques significantly improve performance. Through detailed error analysis and case studies, gain insights into the strengths and weaknesses of various models and techniques for synthesizing programs with proofs in F*.