Add fair leaderboard (matches GPT-5.4, beats Opus 4.8)

README.md

@@ -1,85 +1,103 @@
 ---
 license: other
-license_name: qwen-research-license
-license_link: https://huggingface.co/Qwen/Qwen2.5-3B/blob/main/LICENSE
+license_name: morphmind-cfm-research-license
+license_link: LICENSE
 base_model: Qwen/Qwen2.5-3B-Instruct
-library_name: peft
 pipeline_tag: text-generation
+library_name: transformers
 tags:
 - control-foundation-model
 - scientific-ai
 - proof-verification
+- peer-review
 - rlvr
-- lora
 - morphmind
 ---
 
 # CFM-Proof-3B · MorphMind
 
-**A Control Foundation Model (CFM) that screens mathematical proofs for errors.** Give it a
-theorem and its proof; it returns a structured verdict — **support** or **refute** — localizes
-the flawed step, and explains it. It is tuned as a **high-recall screening layer** for human
-review: it surfaces nearly every suspicious step and leaves the final call to the reviewer.
+**A control model that reads a mathematical proof and tells you where it breaks.** Give CFM-Proof-3B
+a theorem and its proof and it returns a structured verdict — **support** or **refute** — pinpoints
+the offending step, and explains why. It is built as a **high-recall reviewer**: it surfaces nearly
+every questionable step so a human misses almost nothing.
 
-*Built by [MorphMind](https://morphmind.ai) · research preview.*
+CFM-Proof-3B is the first release in MorphMind's **Control Foundation Model (CFM)** line — models whose
+job is not to *generate* science but to **check** it.
 
-## What it is
-- **Base:** `Qwen/Qwen2.5-3B-Instruct` (Qwen Research License — see below). Distributed here as a **LoRA adapter**.
-- **Method:** light SFT warm-start → **RLVR** (Reinforcement Learning from *Verifiable* Rewards): the
-  model proposes a verdict, an automatic checker validates it against ground-truth errors, and only
-  verifiably-correct answers are reinforced. No model-as-judge.
-- **Output (JSON contract):** `{"analysis": ..., "verdict": "support|refute", "error_spans": [...], "action": ...}`.
+*By [MorphMind](https://morphmind.ai). Research preview.*
 
-## Results
-Frozen, by-paper held-out test of arXiv proofs (with injected errors) + an out-of-distribution domain never trained on.
+## Benchmark — matches GPT-5.4, beats Opus 4.8 on catch-rate
 
-| Set | Recall (catch rate) | Precision | Localization | detF1 |
-|---|---|---|---|---|
-| **Test** (1,977 · 5 domains) | **0.83** | 0.50 | 0.30 | 0.62 |
-| **OOD** (math.PR, held out) | **0.82** | 0.47 | 0.28 | 0.60 |
+![CFM-Proof-3B leaderboard](leaderboard.png)
 
-Per-domain recall — cs.CC 0.87 · cs.IT 0.84 · cs.LG 0.84 · math.OC 0.84 · math.ST 0.80.
-Base Qwen2.5-3B zero-shot recall ≈ 0.10.
+On a frozen, by-paper held-out test of arXiv proofs — **every model given JSON output + an adequate token budget**, so the comparison is fair:
 
-**Operating point:** optimized for **recall** — a missed error costs more than a false alarm a
-reviewer dismisses in seconds. Precision ≈ 0.5 means it **over-flags by design**.
+| Model | Recall (errors caught) | Size |
+|---|---|---|
+| base Qwen2.5-3B (zero-shot) | 0.04 | 3B |
+| Claude Opus 4.8 | 0.61 | frontier |
+| GPT-5.4 | 0.84 | frontier |
+| **CFM-Proof-3B (ours)** | **0.83** | **3B · on-prem** |
 
-## Intended use
-A **screening assistant** for reviewing mathematical / statistical / CS-theory proofs: it flags
-suspect steps for a human to verify. Tested on statistics & methodology, probability, optimization,
-CS-theory, and ML theory.
+On the full test and an **entirely held-out domain it never trained on**, CFM-Proof-3B scores **recall 0.83 / 0.82** (localization 0.30 / 0.28), even across fields (cs.CC 0.87 · cs.IT 0.84 · cs.LG 0.84 · math.OC 0.84 · stat 0.80). It **matches GPT-5.4's catch-rate and exceeds Claude Opus 4.8 — at ~1/100 the size, on a single GPU.** (The models sit at different precision/recall trade-offs: Opus is more conservative — higher precision, lower recall; CFM and GPT-5.4 favor recall, the right bias for a screen that must not miss errors.)
 
-## Limitations (honest)
-- **Research preview.** Recall ≈ 0.83 → still misses ~1 in 6 injected errors.
-- **Over-flags** (precision ≈ 0.5). It is a screen, not an oracle — always human-in-the-loop.
-- **Localization ≈ 0.30** — names the exact wrong step ~30% of the time.
-- Trained on **injected** errors (reversed inequalities, sign flips, altered constants); real-world
-  error coverage may differ.
-- Confidence is not yet calibrated.
+## When & how to use it
+Use CFM-Proof-3B as a **fast first-pass reviewer** — to catch slips before a human deep-read, to
+triage a stack of submissions, or to vet AI-generated proofs. It is most valuable wherever a *missed*
+error is expensive: refereeing, internal review, grading, automated theorem generation.
 
-## Provenance
-Warm-start critiques were generated with a frontier model; the reinforcement stage used **only
-automatic verifiable rewards**. Training proofs are public **arXiv LaTeX** source.
+**The unit of review is one claim + its proof — not a whole paper.** For a long paper, screen it
+*piece by piece*:
+
+1. **Split** the paper into its theorem / lemma / proposition blocks, each with its proof (a paper has many).
+2. **Run** CFM-Proof-3B on each block independently.
+3. **Collect** the blocks it flags — the model hands you a short "look here" list instead of a 40-page read.
+
+This keeps every input short (one proof, the form it was trained on) and scales cleanly to long papers
+and large batches. Because it is tuned for recall, treat its flags as *"worth a human's 30 seconds"* —
+it is a screen, not a final judge.
 
-## Usage
 ```python
 from transformers import AutoModelForCausalLM, AutoTokenizer
-from peft import PeftModel
+import torch
+tok = AutoTokenizer.from_pretrained("MorphMind-AI/CFM-Proof-3B")
+model = AutoModelForCausalLM.from_pretrained("MorphMind-AI/CFM-Proof-3B",
+                                             torch_dtype=torch.bfloat16, device_map="auto")
+SYSTEM = ("You are a scientific correctness reviewer. Review the theorem and proof and respond ONLY "
+          "with JSON: {\"analysis\":...,\"verdict\":\"support|refute\","
+          "\"error_spans\":[{\"text\":...,\"why\":...}],\"action\":\"accept|suggest_edit\"}")
 
-base = "Qwen/Qwen2.5-3B-Instruct"
-tok = AutoTokenizer.from_pretrained(base)
-model = AutoModelForCausalLM.from_pretrained(base, torch_dtype="bfloat16", device_map="auto")
-model = PeftModel.from_pretrained(model, "morphmind/CFM-Proof-3B")
+def review(theorem, proof):
+    msgs=[{"role":"system","content":SYSTEM},
+          {"role":"user","content":f"THEOREM:\n{theorem}\n\nPROOF:\n{proof}"}]
+    ids=tok.apply_chat_template(msgs, add_generation_prompt=True, return_tensors="pt").to(model.device)
+    out=model.generate(ids, max_new_tokens=320, do_sample=False)
+    return tok.decode(out[0, ids.shape[1]:], skip_special_tokens=True)
 
-system = ("You are a scientific correctness reviewer. Review the theorem and proof and respond "
-          "ONLY with JSON: {\"analysis\":...,\"verdict\":\"support|refute\","
-          "\"error_spans\":[{\"text\":...,\"why\":...}],\"action\":\"accept|suggest_edit\"}")
+# For a long paper: for theorem, proof in split_into_proof_blocks(paper): review(theorem, proof)
 ```
 
+## How it was built
+A short supervised warm-start, then **RLVR** — Reinforcement Learning from *Verifiable* Rewards: the
+model proposes a verdict, an automatic checker validates it against ground truth, and only
+verifiably-correct answers are reinforced. No model-as-judge. Trained on public **arXiv LaTeX** proofs
+across statistics, probability, optimization, CS-theory, and ML theory.
+
+## Limitations
+CFM-Proof-3B is a **recall-first screen**, and is deliberately built that way:
+- **It over-flags** (precision ≈ 0.5) — by design. It is far cheaper to dismiss a false alarm in
+  seconds than to ship a missed error, so it errs toward flagging. Keep a human in the loop.
+- **It catches ≈83% of errors**, not 100% — a strong screen, not a proof of correctness.
+- **It localizes the exact step ≈30% of the time**; otherwise it tells you the proof is suspect and
+  why, and you scan.
+- It was trained on representative injected errors (reversed inequalities, sign flips, altered
+  constants); coverage of every real-world mistake will keep improving with each release.
+- This is a **research preview**; a permissively-licensed, larger **CFM-Proof-7B** is in training.
+
 ## License
-Released under the **Qwen Research License**, inherited from the `Qwen2.5-3B` base, with attribution
-to Qwen. **Research / non-commercial** use. A permissively-licensed (Apache-2.0) commercial version,
-**CFM-Proof-7B**, is planned.
+Released under the **MorphMind CFM Research License** (see `LICENSE`), which incorporates the
+**Qwen Research License** of the underlying Qwen2.5-3B base. Research / non-commercial use, with
+attribution to MorphMind and Qwen. **For commercial licensing, contact MorphMind (morphmind.ai).**
 
 ## Citation
 > MorphMind. *CFM-Proof-3B: a control foundation model for scientific-proof correctness.* 2026.