VerMCTS: Synthesizing Multi-Step Programs using a Verifier, a Large Language Model,(…)
summary
VerMCTS combines a logical verifier, an LLM (FinCode Llama v2), and a modified Monte Carlo Tree Search to synthesize Dafny and Coq programs and proofs; it checkpoints partial programs with the verifier, backtracks on verified failures, and scores prefixes to guide search. A new 15-problem suite shows VerMCTS achieves >30% absolute increase in pass@5000 over repeated LM sampling, builds multi-step programs (some ~100 lines) and proofs, and reports verifier-in-the-loop MCTS gains.
AI-written summary · about
chapters (14)
- 0:00VerMCTS introduction
- 1:06LLM creativity meets verifier
- 2:32Problem setup challenges
- 4:19Algorithm overview
- 7:12Verifier integration details
- 7:55Experimental setup
- 9:41Results: Dafny vs Coq
- 11:08Summary and future work
- 12:10Benchmarking discussion
- 13:36Computational budget
- 14:39Correctness evaluation
- 16:24Benchmark complexity
- 18:10Unsolved problems analysis
- 20:14Conclusion
related talks
53mSemantics-based program manipulation in the age of LLMs
16mLemur: Integrating Large Language Models in Automated Program Verification
21mA Case Study on the Effectiveness of LLMs in Verification with Proof Assistants
15mLaurel: Unblocking Automated Verification with Large Language Models
22mTowards Verified Code Reasoning by LLMs
19mAutomated Program Refinement: Guide and Verify Code Large Language Model with(…)
18mToward Repository-Level Program Verification with Large Language Models
16mDafnyPro: LLM-Assisted Automated Verification for Dafny Programs