Upload README.md with huggingface_hub

README.md

@@ -0,0 +1,49 @@
+---
+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 — Per-Line Fault Localizer for Verus
+
+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."*
+
+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 (run #10, this checkpoint)
+
+| Measurement | 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**: its per-line top-1 recall jumps from 4% to 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; pre-fix checkpoints (run #7) are marker-RELIANT (signal collapses without markers).
+
+## License
+
+MIT (see [GitHub repo](https://github.com/ozlabsai/VericodingEBM)).