🚀 Usage
from transformers import AutoModelForCausalLM, AutoTokenizer repo = "jgalego/ada-coder-qwen2.5-1.5b"tokenizer = AutoTokenizer.from_pretrained(repo)model = AutoModelForCausalLM.from_pretrained(repo, dtype="auto") messages = [ {"role": "system", "content": "You write Ada 2022 and SPARK code that compiles cleanly with GNAT."}, {"role": "user", "content": "Write a function that returns the greatest common divisor of two Positive numbers."},]inputs = tokenizer.apply_chat_template( messages, add_generation_prompt=True, return_tensors="pt", return_dict=True,)out = model.generate(**inputs, max_new_tokens=512, do_sample=False)print(tokenizer.decode(out[0, inputs["input_ids"].shape[1] :], skip_special_tokens=True))
It also completes raw Ada source with no chat template, which is how it is scored below.
🏋️ Training
Table | |
|---|
| Base | Qwen/Qwen2.5-Coder-1.5B-Instruct |
| Data | r7_dataset.jsonl from the-clanker-lover/steelman-sft-ada, 6,110 instruction/code pairs that compile with GNAT |
| Method | LoRA, r=16, alpha=32, all linear layers, merged |
| Steps | 756 (2.0 epochs), batch size 16, max length 2048 |
| Learning rate | 0.0002, cosine |
| Mean train loss | 0.2271 |
| Hardware | NVIDIA A10G, 94 min |
Then GRPO on the MBPP-Ada problems in MultiPL-E (mbpp-adb), which share none with HumanEval-Ada. Each step samples 8 completions per problem from the raw prompt at temperature 0.8; GNAT builds and runs each against the problem's tests. Reward: 1 if it passes, 0.25 if it only compiles, 0 otherwise. LoRA r=16 on top of the previous model, merged after each round.
Table with columns: Round, Steps, Problems per step, Learning rate, Mean reward, first → last step, Hardware| Round | Steps | Problems per step | Learning rate | Mean reward, first → last step | Hardware |
|---|
| 1 | 45 | 8 | 2e-05 | 0.293 → 0.418 | NVIDIA A10G, 39 min |
📊 Results
nuprl/MultiPL-E HumanEval-Ada (humaneval-adb, 157 problems). Greedy decoding from the raw prompt, then built and run with the GNAT flags from MultiPL-E's eval_adb.py. A program passes when every pragma Assert holds.
Table with columns: Model, n, pass@1, Compile rate, Runtime errors, Timeouts| Model | n | pass@1 | Compile rate | Runtime errors | Timeouts |
|---|
| jgalego/ada-coder-qwen2.5-1.5b | 157 | 0.223 | 0.682 | 71 | 1 |
| jgalego/ada-coder-qwen2.5-1.5b@sft | 157 | 0.204 | 0.592 | 61 | 0 |
| Qwen/Qwen2.5-Coder-1.5B-Instruct | 157 | 0.089 | 0.35 | 41 | 0 |
| jgalego/ada-coder-qwen2.5-1.5b@grpo-2 | 157 | 0.204 | 0.694 | 77 | 0 |
Reference scores reported by the Steelman authors (model card, report) on the same benchmark with their own harness, temperature 0:
Table with columns: Model, pass@1, Compile rate| Model | pass@1 | Compile rate |
|---|
| Steelman 14B v0.3 (Qwen2.5-Coder-14B + R7 data) | 0.459 | 0.854 |
| Steelman 14B v0.2 (Qwen2.5-Coder-14B-Instruct + R6 data) | 0.471 | 0.752 |
| Qwen2.5-Coder-14B, untuned | 0.344 | 0.510 |
⚠️ Limitations
- Scored on small HumanEval-style functions, not on full programs or packages.
- Contracts are at most checked at run time (
-gnata); nothing here runs GNATprove.
- Trained on a single dataset; style follows that data.