Using LLMs for program synthesis is very promising, but also comes with safety and reliability issues. One way to approach this problem is to add a verification step to the code generation process. For example, we can ask an LLM to prove the correctness of its code, and then feed program and proof into a proof assistant.

Done naively, this leads to reattempting the same problem many times (until all proofs are fully correct), resulting in high costs and potentially no success at all. Prior work uses a Monte-Carlo Tree Search to incrementally find the correct code. At each step of the search, an LLM generates completes a piece of code, and a verifier ensures it is correct so far.

In this work, I extend the approach in two ways. First, I show that it can be adapted and used when generating Python programs. Instead of a proof assistant, I use extensive unit- and property-based testing. Second, I also explore alternative search algorithms such as variants of interleaving search.