| --- |
| 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)). |
|
|
