Language-Model Probabilistic Programming for Improving Autoformalization via Cycle(…)
summary
Proposes a GenLM-based decoder that steers a 70B LLM with two real-valued potentials: incremental type-checking via Lean by affixing dummy conclusions at safe checkpoints, and cycle-consistency by backtranslating formalizations and scoring similarity to the original informal statement. Uses sequential Monte Carlo to sample from the unnormalized posterior, rescoring candidates rather than harshly masking tokens. Reports improved accuracy on miniF2F and LeanEuclid with fewer tokens and lower runtime.
AI-written summary · about
chapters (16)
- 0:00Autoformalization research intro
- 0:21Autoformalization and challenges
- 1:27Autoformalization pipeline
- 2:09First LLM prompt attempt
- 2:53Prompting limits for Lean
- 3:13Constrained decoding attempt
- 3:56Constrained decoding distortion
- 4:17GenLM probabilistic programming
- 5:42Sequential Monte Carlo sampling
- 6:23Well-typed Lean via cycles
- 7:28Cycle consistency enforcement
- 8:13Pipeline summary and output
- 8:35Results and takeaways
- 9:17Q&A: Well-typed terms
- 10:45Q&A: Lean meta variables
- 11:48Q&A: Model choice and performance
related talks
11mEffective Sequential Monte Carlo for Language Model Probabilistic Programs
52mGeneralization in the representations and computations of frontier language models.
19mLLMs reasoning and agentic capabilities over time
01h 00mHuman and machine inductive biases for compositional linguistic generalization
55mLessons Learned From Implementing Generative AI Solutions
01h 22mBeyond Decoding: Meta-Generation Algorithms for Large Language Models
28mExplaining Machine Learning Models with LLMs
27mExploring the Mechanisms of LLM Reasoning Capabilities