llm-verified-with-monte-carlo-tree-search

I'd like to call out the work from Nada Amin in this area: Dafny and verification-aware programming, including proof by induction to verify properties of programs (for example, that an optimizer preserves semantics). Dafny Sketcher (https://github.com/namin/dafny-sketcher) Multi-stage programming, a principled approach to writing programs that write programs, and its incarnation in multi-stage relational programming for faster synthesis of programs with holes—with the theoretical insight that a staged interpreter is a compiler, and a staged relational interpreter for a functional language can turn functions into relations running backwards for synthesis. multi-stage miniKanren (https://github.com/namin/staged-miniKanren) Monte Carlo Tree Search, specifically the VerMCTS variant, and when this exploration-exploitation sweet spot is a good

Thanks for taking a look! This is not the main loop. This just generates one completion that succeeds (or gives up) deferring to the Dafny checker to decide. The main loop is the simulate function of the MCTS library. https://github.com/namin/llm-verified-with-monte-carlo-tree-... The main advantage of MCTS is that it takes care of the exploitation/exploration trade off based on the scores propagated by the child finder. I hope this helps. Let me know if this addresses your question.

Anyone who's game able to explain what this actually does? The main loop looks simple: def generate_complete(text, montecarlo): text = llm.generate(text, 1)[0] score = score_func(text) if score is not None: if score < 0: return None else: if can_be_solution(text, min_lines, check_fun): montecarlo.solution = text return text else: return generate_complete(text, montecarlo) ...but, the heart of it (1) just basically checks if the dafny syntax is valid by posting to https://dafny.livecode.ch/check How is 'syntax is valid' a valid scoring mechanism here? If you look at the output examples (2), all I can see if generating functions and lemmas; this is equivalent to generating a function a bunch of tests fo

This is a weekend hack that I'd like to further develop as it's working surprisingly well. Using MCTS, we can explore a space of possible verified programs with an LLM. We check the partial programs at each step, and so steer towards programs that pass the verifier. https://github.com/namin/llm-verified-with-monte-carlo-tree-...