VerMCTS: Synthesizing Multi-Step Programs using a Verifier, a Large Language Model, and Tree Search

This conference talk presents VerMCTS, an innovative approach to synthesizing verified programs in Dafny and Coq by combining Large Language Models (LLMs) with logical verifiers and Monte Carlo Tree Search (MCTS). Learn how this method achieves more than 30% absolute increase in pass rates by using verifiers to provide intermediate feedback during the search process. The researchers developed a new suite of multi-step verified programming problems and introduced the pass@$T$ metric to evaluate performance based on tokens sampled from the LLM. Presented at the Dafny 2025 workshop on January 19, 2025, this 21-minute video features work by researchers from Harvard, Technical University of Munich, Northeastern University, University of Alabama at Birmingham, and University of Oxford.