4 papers
Learning the Error Patterns of Language Models
Jinwoo Kim, Taylor Berg-KirkPatrick, Loris D'Antoni
When generating outputs for domains with specific validity constraints (e.g., a program should compile), LLMs often fail in a small number of focused ways: for example, by using Py…
Continuous Diffusion Models Can Obey Formal Syntax
Jinwoo Kim, Taylor Berg-Kirkpatrick, Loris D'Antoni
Diffusion language models offer a promising alternative to autoregressive models due to their global, non-causal generation process, but their continuous latent dynamics make discr…
What are the Right Symmetries for Formal Theorem Proving?
Krzysztof Olejniczak, Radoslav Dimitrov, Xingyue Huang +3
Formal theorem provers based on large language models (LLMs) are highly sensitive to superficial variations in problem representation: semantically equivalent statements can exhibi…
Semantics of Sets of Programs
Jinwoo Kim, Shaan Nagy, Thomas Reps +1
Applications like program synthesis sometimes require proving that a property holds for all of the infinitely many programs described by a grammar - i.e., an inductively defined se…