CFM-Proof-3B research preview: adapter + model card

README.md

@@ -0,0 +1,85 @@
+---
+license: other
+license_name: qwen-research-license
+license_link: https://huggingface.co/Qwen/Qwen2.5-3B/blob/main/LICENSE
+base_model: Qwen/Qwen2.5-3B-Instruct
+library_name: peft
+pipeline_tag: text-generation
+tags:
+- control-foundation-model
+- scientific-ai
+- proof-verification
+- 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.
+
+*Built by [MorphMind](https://morphmind.ai) · research preview.*
+
+## 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": ...}`.
+
+## Results
+Frozen, by-paper held-out test of arXiv proofs (with injected errors) + an out-of-distribution domain never trained on.
+
+| 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 |
+
+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.
+
+**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**.
+
+## 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.
+
+## 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.
+
+## 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.
+
+## Usage
+```python
+from transformers import AutoModelForCausalLM, AutoTokenizer
+from peft import PeftModel
+
+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")
+
+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\"}")
+```
+
+## 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.
+
+## Citation
+> MorphMind. *CFM-Proof-3B: a control foundation model for scientific-proof correctness.* 2026.

adapter_config.json

@@ -0,0 +1,48 @@
+{
+  "alora_invocation_tokens": null,
+  "alpha_pattern": {},
+  "arrow_config": null,
+  "auto_mapping": null,
+  "base_model_name_or_path": "Qwen/Qwen2.5-3B-Instruct",
+  "bias": "none",
+  "corda_config": null,
+  "ensure_weight_tying": false,
+  "eva_config": null,
+  "exclude_modules": null,
+  "fan_in_fan_out": false,
+  "inference_mode": true,
+  "init_lora_weights": true,
+  "layer_replication": null,
+  "layers_pattern": null,
+  "layers_to_transform": null,
+  "loftq_config": {},
+  "lora_alpha": 64,
+  "lora_bias": false,
+  "lora_dropout": 0.05,
+  "lora_ga_config": null,
+  "megatron_config": null,
+  "megatron_core": "megatron.core",
+  "modules_to_save": null,
+  "peft_type": "LORA",
+  "peft_version": "0.19.1",
+  "qalora_group_size": 16,
+  "r": 32,
+  "rank_pattern": {},
+  "revision": null,
+  "target_modules": [
+    "q_proj",
+    "k_proj",
+    "o_proj",
+    "v_proj",
+    "up_proj",
+    "gate_proj",
+    "down_proj"
+  ],
+  "target_parameters": null,
+  "task_type": "CAUSAL_LM",
+  "trainable_token_indices": null,
+  "use_bdlora": null,
+  "use_dora": false,
+  "use_qalora": false,
+  "use_rslora": false
+}

adapter_model.safetensors

@@ -0,0 +1,3 @@
+version https://git-lfs.github.com/spec/v1
+oid sha256:2229da6a1e61ec16964f44ff04adcf28949b719946db2387e46d33c58ec13ae5
+size 239536272