namin/llm-verified-with-monte-carlo-tree-search
View on GitHub ↗ ★ 297 Jupyter Notebook
LLM verified with Monte Carlo Tree Search
4 mentions on Hacker News by 3 people: 1 story, 3 comments · first 2023-11-11 · latest 2025-12-13
20082026
-
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 (…
comment by juliangamble · 2025-12-13 · in 50 years of proof assistants -
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.…
comment by namin · 2023-11-12 · in Show HN: LLM Verified with Monte Carlo Tree Search -
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:…
comment by wokwokwok · 2023-11-12 · in Show HN: LLM Verified with Monte Carlo Tree Search