11 ms·
Type-constrained code generation with language models
- jiggawatts 1y agoThis was an obvious next step. Most current products can only restrict the token prediction to valid JSON or a specific JSON schema at best. There's no reason that this should be the only grammar available for constrained output mode. The real challenge will be to make this detect and switch languages automatically. For example, a snippet of code could include a LaTeX formula in a comment and SQL in a string literal. There are many more examples, such as regex inside a shell script, and so on. The obvious next step after that is back-tracking. It's possible to emit a token that is valid, but then allows no further completions that are valid. In other words, the model can paint itself into a corner. To my knowledge, no current online LLM service uses any kind of backtracking, they run in append ("forwards") mode only.
- helltone 1y agoBacktracking idea is interesting, could maybe diffusion help? At some point it turns into sat solving.
- grafmax 1y agoSat solving I guess because types encode proofs?
- deleted 1y ago[deleted]
- deleted 1y ago[deleted]
- deleted 1y ago[deleted]
- deleted 1y ago[deleted]
- foota 1y agoI believe Microsoft introduced a framework that did this sort of backtracking that you're suggesting. I'm not sure how much traction it got.
- tough 1y agoSRLCG: Self-Rectified Large-Scale Code Generation with Multidimensional Chain-of-Thought and Dynamic Backtracking https://arxiv.org/abs/2504.00532 https://arxiv.org/abs/2504.00532 IterGen: Iterative Semantic-aware Structured LLM Generation with Backtracking https://arxiv.org/abs/2410.07295 https://arxiv.org/abs/2410.07295 ROCODE: Integrating Backtracking Mechanism and Program Analysis in Large Language Models for Code Generation https://arxiv.org/abs/2411.07112v1 https://arxiv.org/abs/2411.07112v1
- pizza 1y agoAnother one: SequenceMatch: Imitation Learning for Autoregressive Sequence Modelling with Backtracking https://arxiv.org/abs/2306.05426 https://arxiv.org/abs/2306.05426 There was also an hn thread: https://news.ycombinator.com/item?id=36425375 https://news.ycombinator.com/item?id=36425375
- nielstron 1y agore detecting and switching language: you could run several constraint systems in parallel and switch as soon as one of them rejects the input and another accepts it re backtracking: a core part of this paper is ensuring a prefix property. that is there is always a legitimate completion and the model can not "corner" itself! research needs to be done for what kind of languages and language features this prefix property can be ensured
- ArcaneMoose 1y agoI think TypeScript is uniquely positioned to be the optimal language for LLMs. Tons of training data (benefiting from all the JS examples as well) plus the structure of types for LLMs to follow and tools to enforce.
- yoyohello13 1y agoGod help us…
- marviel 1y agowhat do you dislike about it?
- treyd 1y agoTypeScript is arguably one of the weaker statically typed languages, with how it allows `any` to quietly violate the type checked assumptions. It makes it harder to do a lot of the basic typing mistakes in JS, but it doesn't prevent them by any means, especially if you have to interface with (typeless) JS code. So for these reasons alone I would be against using TS as a lingua franca for LLM codegen (as is GP I assume). As another commenter mentioned, LLMs have a tendency to throw their hands^Hlogits up when presented with complex TS type errors and just resort to using `any` to get it to compile (and probably hiding bugs). And that doesn't even touch the issues with the JS/TS ecosystem and runtimes more broadly.
- agos 1y agotsc can be configured to avoid implicit use of any ("noImplicitAny": true) and ESLint can be set up to avoid explicit use of any. Typeless JS code is also a thing of the past. But the devil is in the details - some libraries are typed quite crappily, some have unnecessary complex types, and the code that the LLMs was trained on is probably not the best in the world
- tpm 1y ago
- homebrewer 1y agoHejlsberg mentioned the ability to quickly provide accurate type information to LLMs as one of the reasons for rewriting tsc into Go: https://youtu.be/10qowKUW82U?t=3186 https://youtu.be/10qowKUW82U?t=3186
- tough 1y agoBut isn't TypeScript already a typed language to begin with?
- habitue 1y agoThis is about the speed with which the compiler can advise an LLM that a particular thing checks or doesn't check. Typescript is much slower than Go
- tough 1y agookay so basically the faster compiling means a tigher feedback loop for the LLM to -know- if the code compiles or not etc? interesting is go faster than rust?
- yoyohello13 1y agoGo’s compiler is WAY faster than Rust’s. As far as speed of the actual program, Rust will generally be faster.
- notnullorvoid 1y agoGo or Rust compiler speeds won't have any effect here. The program in this context is the TypeScript compiler.
- koakuma-chan 1y agocargo check is WAY faster than go build
- notnullorvoid 1y agoThe general idea seems very promising, I had been hoping someone would do something like this since seeing JSON schema structured outputs for LLMs. Need to dig in a bit more on the implementation, but I was surprised that the paper didn't mention hooking into existing language service/server. There's more than types that an LLM could leverage from existing language tooling. Auto imports is a good example, it is handy for the human developer to keep a linear writing flow, something a LLM needs even more.
- nielstron 1y agothe problem with LSPs is that they don't guarantee generating a type annotation that we can use for constraints, i.e. we can not ensure the prefix property using LSPs. so we had to roll our own :) Pulling in more features to help the system is definitely worth looking into!
- tough 1y agoThe code can be found here: https://github.com/eth-sri/type-constrained-code-generation https://github.com/eth-sri/type-constrained-code-generation
- compacct27 1y agoHonestly it's already working great in Cursor. Even adapting one type structure to another is quickly handled.
- slt2021 1y agowe really need LLM trained on AST, instead of token, is there any research on this?
- tough 1y agoASTrust: Towards More Trustworthy and Interpretable LLMs for Code through Syntax-Grounded Explanations https://arxiv.org/abs/2407.08983 https://arxiv.org/abs/2407.08983 AST-T5: Structure-Aware Pretraining for Code Generation and Understanding https://arxiv.org/abs/2401.03003 https://arxiv.org/abs/2401.03003 CodeGRAG: Bridging the Gap between Natural Language and Programming Language via Graphical Retrieval Augmented Generation https://arxiv.org/abs/2405.02355 https://arxiv.org/abs/2405.02355
- nielstron 1y agoThe downside is that you need to properly preprocess code, have less non-code Training Data, and can not adapt easily to new programming languages
- koakuma-chan 1y agoThe vibe code society would benefit way more if libraries hosted their docs in a way that's easy to copy and paste into an LLM.
- tough 1y agomany docs now include llms.txt https://llmstxt.org/ https://llmstxt.org/
- koakuma-chan 1y agoI saw that but it doesn't work for me. I use Gemini 2.5 Pro Preview right now, and it cannot fetch content from links. What I am looking for is a large text file with public API class, function, etc. signatures, plain text documentation and code examples.
- tough 1y agohttps://ai-sdk.dev/llms.txt https://ai-sdk.dev/llms.txt
- koakuma-chan 1y agoDepends on the library I guess, I spent 12~ hours today vibe coding with LiveKit and their /llms.txt is https://docs.livekit.io/llms.txt https://docs.livekit.io/llms.txt
- muglug 1y agoReally cool results! That this research comes out of universities, and not large AI labs, makes me think those labs believe that larger models are still the way to go.
- bmc7505 1y agoThe correct way to do this is with finite model theory but we're not there yet.
- _jayhack_ 1y agoAlso worth checking out MultiLSPy, effectively a python wrapper around multiple LSPs: https://github.com/microsoft/multilspy https://github.com/microsoft/multilspy Used in multiple similar publications, including "Guiding Language Models of Code with Global Context using Monitors" (https://arxiv.org/abs/2306.10763 https://arxiv.org/abs/2306.10763), which uses static analysis beyond the type system to filter out e.g. invalid variable names, invalid control flow etc.
- nielstron 1y agoYes this work is super cool too! Note that LSPs can not guarantee resolving the necessary types that we use to ensure the prefix property, which we leverage to avoid backtracking and generation loops.
- nikolayasdf123 1y agonice. the speed of AI development is accelerating so fast
- cpfiffer 1y agoWe (.txt, the outlines people) had a brief thread about this paper on twitter if you're interested: https://x.com/dottxtai/status/1922322194379551128 https://x.com/dottxtai/status/1922322194379551128
- hongbo_zhang 1y agoWe published a similar paper for MoonBit: Explore the Design of an AI-Friendly Programming Language https://conf.researchr.org/details/icse-2024/llm4code-2024-papers/9/MoonBit-Explore-the-Design-of-an-AI-Friendly-Programming-Language https://conf.researchr.org/details/icse-2024/llm4code-2024-p...
- int19h 1y agoBeen using Devin for a few months now, for Typescript and Python. I've never seen it check-in uncompilable code, but watching the Devin console I can see it building and using the code to ensure commits are not complete garbage. When it has checked-in compilable and almost right but slightly wrong code, automatically running lint and tests (it doesn't always run them before checking in) from ci triggers it to push a fix on its own. Feedback loops are nice, but they can be expensive, and time consuming (oh look at me complain that it takes Devin a whopping 15 minutes to complete a task) so I can definitely see the value in type constraints.
- android521 1y agois Devin worth the money? Would it be a big jump in productivity migrating from cursor to Devin?
- int19h 1y agoit has been worth it for me, ymmv of course. also they have a pay-as-you-go tier now as well. I pay the full $500 though. This month I'm going to blow past the base allowance and tap into 'gift credits' speaking of which if anyone wants a referral code (gift creds for me, and for you) hmu
- informal007 1y agoWould it better if we move the feedback loops into RL-stage of LLM training? Are there some related works?
- nielstron 1y agowe were thinking about doing exactly this, the closest current work is probably the amazing "Learning Formal Mathematics from Intrinsic Motivation" by Poesia et al (they use constraints too increase the likelihood of generating correct theorems/proofs during RL) https://arxiv.org/abs/2407.00695 https://arxiv.org/abs/2407.00695
- informal007 1y agoYes, RL works well in fields where answer can be verified in different degree. That's why AlphaGo success, it also should work in code generation and math.
- imtringued 1y agoYour reward function can simply be the distance between the constrained output and the unconstrained output, that way you won't even need synthetic data, just a dataset of prompts to RL against.
- informal007 1y agoHow to get "unconstrained output" and evaluate the distance between them? Evaluation method which can decide distance between two sentences is hard to find, best option is closed-source LLM API even it's not the most ideal option. As a result, we also must use current LLM to improve our models.
- weiwenhao 1y agoDoes llm really understand the code at this stage?
- Corey_ 1y agoI completely agree that TypeScript is ideal for LLMs. The type system and the extensive training data make it the best choice. But as someone who's been working with TypeScript for a while, I still see LLMs struggling with complex generics or even simple types. It’s better than before, but still far from perfect. Also, TypeScript error messages can be a pain. When LLMs encounter something like "SomeType is not assignable," instead of handling it properly, they often just cast it to any. This happens way too often.
- energy123 1y agoThis is what I'd consider doing if I was a small AI lab. Don't try to build a frontier LLM that beats all benchmarks. Try to make the world's best LLM at one programming language. Create your RL pipeline that puts all your resources into making the LLM the best at that language. Even better if there's a dearth of human-created training data on Github, since all your competitors will be bad at it. Google somewhat did this with javascript in their latest Gemini-2.5 Pro release. But what about doing it for a smaller language? Google isn't going to do that, but there is still a lot of demand.
- Drakim 1y agoIt makes sense to specialize it on one programming language to dedicate all of the LLM's intellectual space to that one domain, but on the flip side I wonder how much the LLM's sharpness and reasoning capabilities is increased by having more data to train on even if it's the wrong programming language. As a developer I certainly think my programming skills in a specific language was improved by knowing other languages so I can contrast and compare.
- tough 1y agoYou could just have specialized fine-tunes for esxh programling la guage that are only called when writing code, a more general bigger model could pass the plan/pseudo code to it
- eigenspace 1y agoI'm not saying this is a bad idea, but it does sound like a rather risky prospect. You're basically proposing a bet against the ability of LLMs to generalize across programming languages, and to embed concepts at a deeper level than the syntax. Many people do think this, but I'm not sure many of them are running AI labs.
- tough 1y agoit feels to me most of the real usage of AI is in coding right now, so a small lab that decided to go all in into just code-gen would have at least the differentiator of a narrower field to beat the bigger incumbents doing it all? I dunno tho. Big AI labs also have their own agendas and would rather keep scaling and growing than serving a rather smaller real market ? Once you're into real usage territory, you can't no longer use make up numbers to justify future growth.
- kreetx 1y agoThey should extend this to Haskell and make use of the Curry-Howard isomorphism: define the program you want by a type signature and have the LLM find the implementation.
- chriswarbo 1y agoThe classic approach to this is Djinn https://hackage.haskell.org/package/djinn https://hackage.haskell.org/package/djinn It's not very good with concrete types (Text, Int, MyCustomThing, etc.) but is good for polymorphic functions whose parts only fit together in a few ways. More recent work is better at using concrete types, and choosing functions from Hackage, like Hoogle+ https://github.com/TyGuS/hoogle_plus https://github.com/TyGuS/hoogle_plus and Hectare https://dl.acm.org/doi/10.1145/3547622 https://dl.acm.org/doi/10.1145/3547622 There's also "inductive programming" (producing a function from input/output examples), with Haskell implementations like Magic Haskeller http://nautilus.cs.miyazaki-u.ac.jp/~skata/MagicHaskeller.html http://nautilus.cs.miyazaki-u.ac.jp/~skata/MagicHaskeller.ht...
- seeknotfind 1y agoThis is anticipated from work on constrained output from LLMs, and it's good to see it being developed. One nitpick though, this paper mentions the complexities of implementing type checking for program prefixes in languages that are not context free. It's true this is extremely difficult for languages which are context sensitive, especially because types may be defined after they are used. However, it does not mention that it is impossible to implement such a program for Turing complete languages such as C++. I would never miss such an opportunity to criticize C++ and highlight the need for better language design. I love you C++.
- nielstron 1y agonoted. we'll make sure to critizise turing complete type systems more thoroughly next time :))
- _alternator_ 1y agoUntil a couple weeks ago, I considered this a promising approach. What changed? Agents, and Claude code in particular. My prior experience was that LLMs were not much better than reading the docs, and certainly you wouldn’t get far vibe-coding in Rust. But Claude code behaves like I would, writing code that does t compile (typical LLM behavior), then reading the errors, correcting the code, and iterating until it compiles. Its first attempt at a graph based scheduler in Rust took about $3 and 10 minutes to work correctly. It was ~500 loc, so definitely faster than what I can write in rust. (To be fair I spent a decent amount of time drafting a description of what I wanted in a markdown file to get Claude started).
- gdiamos 1y agoIf you have two methods that both improve accuracy, why not stack them?
- _alternator_ 1y agoThis reasoning is at odds with recent history. A lot of effort was put into making machines that could only output grammatically correct sentences. Yet LLMs output grammatically correct sentences when needed, and a whole lot more as context demands, without ever hardcoding it. It would be foolish to restrict LLMs to only grammatical sentences at this point, but it might be a good tool to run on generated docs because sometimes words are misspelled or sentences are confusing. Similarly, we have a tool that makes sure the type and syntax are correct, namely, a compiler. Building an LLM that can only output syntactically correct code is one approach of stacking them, but in fact it will significantly worsen the ability of the LLM to reason and construct code. The winning choice seems to be to emulate the workflow of humans: code, compile, read errors, repeat.
- gitroom 1y ago[flagged]
- LostBenjamin 1y agoAs an author of this paper, I am very excited see the great discussion here! Several people mentioned the generation - compilation - fixing loop. Just want to remind you that our approach works for not only the generation step but also the fixing step. This is because fixing is essentially asking LLMs to generate a new version of the code. The paper actually has a "repair" experiment to demonstrate this and our approach achieves significant gain in this experiment, i.e., 37% relative improvement in functional correctness.
- tough 1y agoThank you for your research really impressive work!
- yewW0tm8 1y ago37% gain relative to what? What percent of generated functions were incorrect?
- LostBenjamin 1y agocompared to vanilla LLM decoding.
- thesz 1y ago> To address this challenge, we introduce a type-constrained decoding approach that leverages type systems to guide code generation. This should not work with type inference even at the level of C++ "auto x = " - "auto" does not constrain "x" at all and what is right of equal sign is not constrained either.. In Haskell, the gap is even wider. A long "where" clause may have dependencies constraining things in different direction. But, what important I see here is the continuation of reinvention of Cyc, from different starting point. ;) Definitely, "every big LLM has in support code an ad-hoc bug ridden inefficient implementation of half of Cyc." Cyc was written in Lisp, most of LLM support code is C/C++, thus, it is just a corrolary of Greenspun's Tenth Rule.
- drumnerd 1y agoThis was obviously coming, and it should be tuned to Haskell and Agda