mlsanityData to 7 Oct 2026

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

arXiv 2402.08147 ↗First posted 13 Feb 2024cs.SE cs.AI cs.LGcited by 13

On the map: LLM reasoning → Reasoning for agents, planning and code

Abstract (arXiv)

Large Language Models (LLMs) can generate useful code, but often the code they generate cannot be trusted to be sound. In this paper, we present VerMCTS, an approach to begin to resolve this issue by generating verified programs in Dafny and Coq. VerMCTS uses a logical verifier in concert with an LLM to guide a modified Monte Carlo Tree Search (MCTS). This approach leverages the verifier to gain intermediate feedback inside the search algorithm by checking partial programs at each step to estimate an upper bound on the value function. To measure the performance of VerMCTS, we develop a new suite of multi-step verified programming problems in Dafny and Coq. In terms of pass@T, a new metric which computes the pass rate given a budget of T tokens sampled from the LLM, VerMCTS leads to more than a 30% absolute increase in average pass@5000 across the suite over repeated sampling from the base language model. Our code and benchmarks are available at https://github.com/namin/llm-verified-with-monte-carlo-tree-search .

Key facts. Cited by 13 papers in the map (data through 7 Oct 2026). Placed in Reasoning for agents, planning and code, one of 17 directions in LLM reasoning. Builds on 20 of its 36 references that are in the map. First posted on arXiv 13 Feb 2024.

Builds on

20 of 36 references.

Closest ancestors · 1

Same direction, newest first

  1. 2023LEVER: Learning to Verify Language-to-Code Generation with Execution16 Feb

Other references · 19

  1. 2021Evaluating Large Language Models Trained on Codecited by 8,053
  2. 2023Reflexion: Language Agents with Verbal Reinforcement Learningcited by 4,064
  3. 2021Program Synthesis with Large Language Modelscited by 3,509
  4. 2019The Curious Case of Neural Text Degenerationcited by 2,881
  5. 2023Code Llama: Open Foundation Models for Codecited by 2,105
  6. 2023LeanDojo: Theorem Proving with Retrieval-Augmented Language Modelscited by 414
  7. 2022Draft, Sketch, and Prove: Guiding Formal Theorem Provers with Informal Proofscited by 278
  8. 2022HyperTree Proof Search for Neural Theorem Provingcited by 192
  9. 2023Planning with Large Language Models for Code Generationcited by 179
  10. 2021Proof Artifact Co-training for Theorem Proving with Language Modelscited by 130
  11. 2023Baldur: Whole-Proof Generation and Repair with Large Language Modelscited by 118
  12. 2022Re2G: Retrieve, Rerank, Generatecited by 102
7 more
  1. 2022Coder Reviewer Reranking for Code Generationcited by 83
  2. 2023Can ChatGPT replace StackOverflow? A Study on Robustness and Reliability of Large Language Model Code Generationcited by 72
  3. 2022Top-Down Synthesis for Library Learningcited by 57
  4. 2015Program Synthesis using Natural Languagecited by 41
  5. 2023Refactoring Programs Using Large Language Models with Few-Shot Examplescited by 27
  6. 2020Optimal Neural Program Synthesis from Multimodal Specificationscited by 15
  7. 2023Type Prediction With Program Decomposition and Fill-in-the-Type Trainingcited by 6

Built on by

Cited by year (2026 to 7 Oct)

Citing papers per year: 2024: 2; 2025: 9; 2026: 2.

13 papers.

Sort:

By area:

  1. 2025Towards Reasoning Era: A Survey of Long Chain-of-Thought for Reasoning Large Language Modelscited by 381
  2. 2025Monte Carlo Tree Diffusion for System 2 Planningcited by 33
  3. 2024Laurel: Unblocking Automated Verification with Large Language Modelscited by 10
  4. 2025From Token to Line: Enhancing Code Generation with a Long-Term Perspectivecited by 4
  5. 2025SIGMA: Refining Large Language Model Reasoning via Sibling-Guided Monte Carlo Augmentationcited by 3
  6. 2025Inferring multiple helper Dafny assertions with LLMscited by 3
  7. 2025Streaming Looking Ahead with Token-level Self-rewardcited by 2
  8. 2025EduFlow: Advancing MLLMs' Problem-Solving Proficiency through Multi-Stage, Multi-Perspective Critiquecited by 2
  9. 2025Do AI models help produce verified bug fixes?cited by 2
  10. 2024Enhancing Formal Theorem Proving: A Comprehensive Dataset for Training AI Models on Coq Codecited by 1
  11. 2025Foundation of Intelligence: Review of Math Word Problems from Human Cognition Perspectivecited by 1
  12. 2026Verifier-Guided Code Translation via Meta-Step Decodingcited by 1
1 more
  1. 2026Djinnlang: Higher-Level Programming by Unambiguous Specification with an LLM in the Compilercited by 0

Similar, not cited

Close in wording, no citation either way

  1. 2025VeriEquivBench: An Equivalence Score for Ground-Truth-Free Evaluation of Formally Verifiable Code
  2. 2026Narrowing the Complexity Gap in the Evaluation of Large Language Models ↗
  3. 2026Automating Formal Verification with Reinforcement Learning and Recursive Inference
  4. 2025HardTests: Synthesizing High-Quality Test Cases for LLM Coding
  5. 2023Turbulence: Systematically and Automatically Testing Instruction-Tuned Large Language Models for Code
  6. 2024Planning-Driven Programming: A Large Language Model Programming Workflow
  7. 2026CangjieBench: Benchmarking LLMs on a Low-Resource General-Purpose Programming Language
  8. 2024AlphaVerus: Bootstrapping Formally Verified Code Generation through Self-Improving Translation and Treefinement