File size: 2,357 Bytes
3a72ccf 69eaac5 3a72ccf 69eaac5 3a72ccf 69eaac5 3a72ccf 69eaac5 3a72ccf 69eaac5 3a72ccf 69eaac5 3a72ccf | 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 | ---
license: mit
language:
- en
base_model: Qwen/Qwen2.5-Coder-1.5B-Instruct
tags:
- code
- verus
- formal-verification
- fault-localization
- energy-based-model
- lora
- peft
library_name: peft
---
# VericodingEBM — Hybrid-Averse checkpoint
A LoRA + per-line scalar head trained on top of [Qwen2.5-Coder-1.5B-Instruct](https://huggingface.co/Qwen/Qwen2.5-Coder-1.5B-Instruct) to score every line of a Verus implementation with an energy proxy for *"this line is the bug."*
This is the canonical **Hybrid-Averse** checkpoint reported in the paper — the post-fix model that learned to anti-correlate with the `// FAILS` debug marker rather than rely on it.
Submitted to the Apart × Atlas Computing **Secure Program Synthesis Hackathon, Track 3 (Vericoding)**.
📄 **Paper:** see [`paper/main.pdf`](https://github.com/ozlabsai/VericodingEBM/blob/main/paper/main.pdf)
💾 **Code + reproducibility:** https://github.com/ozlabsai/VericodingEBM
📊 **Training data:** [`OzLabs/VericodingEBM-data`](https://huggingface.co/datasets/OzLabs/VericodingEBM-data)
## Headline results (Hybrid-Averse)
| Measurement | Hybrid-Averse (this model) | Best frontier LLM |
|---|---|---|
| Per-line top-3 recall on Verus dev-test (n=609 FAILs) | **0.84** | 0.74 (Claude Opus 4.7) |
| Whole-impl discrimination AUROC | 0.78 | **0.91** (GPT-5.5) |
| Closed-loop CEGIS repair@1 (n=100) | 25% | **30%** (LLM self-judged) |
## What's in this repo
- `adapter/` — LoRA adapter (PEFT format, rank 16, alpha 32, embed_lora_rank 8) for Qwen2.5-Coder-1.5B-Instruct
- `head.pt` — per-line scoring head weights (small MLP over sentinel-token hidden states)
- `scalar_head.pt` — whole-impl attention-pool head weights
To run inference you need all three files plus the training code at https://github.com/ozlabsai/VericodingEBM.
## Marker-leak audit (paper §4.6)
This checkpoint is **marker-AVERSE**: per-line top-1 recall jumps from 4% → 56% when the `// FAILS` debug markers are stripped from the input (delta = −52pp). This is the result of the counterfactual-marker augmentation described in paper §B. The pre-audit **Sentinel-Reliant** checkpoint (not released here) shows the opposite regime — signal collapses without markers, exposing the leak that motivated this work.
## License
MIT (see [GitHub repo](https://github.com/ozlabsai/VericodingEBM)).
|