Fine-tuning 8b AI model on Ada/SPARK

General
, ,
1

So for context I recently got my hands on a laptop with 8 GB VRAM running an NVIDIA graphics card.

I experimented a bit with local models that fit my hardware constraints, though it is safe to say that local models at this range are frankly quite terrible at Ada. I have tried qwen3:8b, gemma4:e4b and the like. They are ok at the common languages like Python but I suppose their training dataset is lacking on Ada.

I tried this on ollama + pi coding agent on WSL, which is probably one of the lighter harness set ups one can use.

Even with AdaCore’s provisioned skills the model is prone to hallucinations and not using Alire properly.

Thus I plan to start working on a finetune for qwen3:8b for it to better understand Ada projects. If you are interested, do drop your repository links if you wish for your repository to be used for training during the fine-tuning process. GitHub technically uses all public GitHub repositories for their AI model training but we are a bit more ethical than that.

Please check that your repository has generally permissive licensing or you explicitly make an exception for use in model training. I do not want AGPLv3 spilling over when the finetuned model should be as permissive as possible for the benefit for everyone (I am thinking Apache 2.0)

Once the finetune is done I plan to have it released on HuggingFace as open weights (not open source, as the underlying Qwen model like almost every other AI model is open weights). That being said, I am to be as transparent with fine-tuning dataset weights and all as possible.

I also do not just want to train it on Ada 2022, as Ada 2012/SPARK 2014 is still widely used out there. The end goal is to have a finetuned model suitable for working on Ada that runs on consumer hardware.

P.S. corrected model name to qwen3:8b instead of qwen3.8, I cannot run qwen3.8 (at least it’s 9b variant iirc) that well with enough context window size to be useful in 8 GB VRAM.

2

Hmm it seems there has been similar fine-tuning done earlier on, I will take inspiration and learn from it :smiley:

3

Hi !

This is an interesting project. Last year I experimented with DeepSeek and upgraded my laptop to 64 Gb / 2Tb for this (before memory got so expensive). Compared to what Opus, Fable and the like offer, it was disappointing. If you want some Ada 83 training do not hesitate to access my Ada 83 compiler sources if helpful.

If you have an established project environment tell where it is and if you need some help.

4

Thanks :smiley: , Ada 83 would be great to have in the training dataset. As for project environment wise I will start setting it up at a later time. Obtaining quality training data iirc is the most difficult and time consuming part of model fine-tuning/training. I could use synthetic data and other techniques later one but a decently sized corpus of quality source code by the community that is clear/specific to implementation and use case would help immensely.

My educated guess here is that if I can make an 8B model write Ada well larger parameter models will run even better, though we are still some time away from there.

From what I heard models like DeepSeek are pretty good but the local model scene is moving rather quickly even just within this year. I believe there are better models you can now run in 64 GB VRAM (if that is what you have).

5

Also hope the team at AdaCore are fine with me using docs to distil for model training, otherwise do lmk.

6

Life update: Repo is set up but I will have to polish up a fair bit before dropping the URL here. That being said it is on my GitHub already.

7

I published evrything under MIT license so LLM can be trained on that, have a look, feel free to use.

8

Thanks so much, the algorithms will be a great source to add to the training dataset.

Repo still needs more polish but I believe even for the initial naive implementation I am already starting to see some improvements in various metrics.

Progress thus far, if you are curious:

GitHub - bladeacer/q3as: Finetuning Qwen3:8b for Ada/SPARK. · GitHub

Unlike the Steelman project I will be adopting Ada eval’s methodology to evaluating LLMs, especially when it comes to contract and proof writing.

That being said I have not looked too much into it myself.

Looking forward to running model training with the improvements I have been working on.

9

Glad I could be of help. I have been busy with Gemini whose answers (and compiler output fed back into it. Mistral ate a month’s worth of allowance in 2 days. But when I found out GrokBot can do Ada and GNATPROVE without me needing to have to copypaste.
I decided to go all in for a month and create those much-needed Ada trainingsset.
I sure do hope we see all LLMs use Alire properly.

10

I’ve attempted fine tunes. I believe the main issue is in training cases for ada spark. My effort is on hugging face, its a tuned qwen 3.8 coder and I think takes at least 16 gig of graphics. Its called Rosie.

11

mhm training data is always the bottleneck regardless of finetuning task or use case.

will look up your repo on huggingface, thanks for the head’s up.

12

theres a 0.3 and a 0.5 version, but these are really for working with that crucible factory

13

Finally got the codebase to a state when I can run the first proper training run for proof of concept.

At 500 steps (which is quite low), there already seems to be some improvements in build pass and unit test success rates for the Ada side of things. Teaching it SPARK however is a fair bit more difficult.