|
|
|
|
|
by amccollum
325 days ago
|
|
If everyone is using LLMs to write new code, and LLMs are trained on existing code from the internet, that creates an enormous barrier to the adoption of new programming languages, because no new code will be written in them, therefore LLMs will never learn to write the code. It is a self-reinforcing cycle. I've experienced this to some degree already in using LLMs to write Zig code (ironically, for my own pet programming language). Because Zig is still evolving so quickly, often the code the LLM produces is wrong because it's based on examples targeting incompatible prior versions of the language. Alternatively, if you ask an LLM to try to write code for a more esoteric language (e.g., Faust), the results are generally pretty terrible. |
|
[1] There are a lot of models that achieve this. E.g. Goedel-Prover-V2-32B [2] is a model based off of Qwen3-32B and fine tuned on Lean proofs. It works extremely well. I personally tried further fine tuning this model on Agda and although my dataset was pretty sloppy and small, it was pretty successful. If you actually sit down and generate a large dataset with variety it's pretty reachable to fine tune it for any similar prog lang.
[2] https://huggingface.co/Goedel-LM/Goedel-Prover-V2-32B