---

license: other

license_name: webai-non-commercial-1.0

license_link: https://huggingface.co/webAI-Official/TwIL-LM3

base_model: webAI-Official/TwIL-LM3

base_model_relation: quantized

tags:

- gguf

- llama.cpp

- smollm3

- reasoning

- formal-logic

- quantized

- local-llm

language:

- en

pipeline_tag: text-generation

library_name: gguf

---

TwIL-LM3-GGUF

GGUF quantizations of webAI-Official/TwIL-LM3 for local inference with llama.cpp and compatible runtimes. [web:2]

TwIL-LM3 is a 3.08B formal-logic reasoning model built from HuggingFaceTB/SmolLM3-3B via LoRA SFT, checkpoint fusion, WiSE-FT (\(\lambda = 0.25\)), and entropy-weighted GRPO (MGPO, step 2071). It is specialized for FOL translation, entailment, semantic parsing, Lean formalization, and proof critique — not a general chat assistant. [web:2]

| Property | Value |

|---|---|

| Quant repo | NANI-Nithin/TwIL-LM3-GGUF |

| Original weights | webAI-Official/TwIL-LM3 |

| Base | HuggingFaceTB/SmolLM3-3B |

| Parameters | 3.08B |

| Architecture | SmolLM3 decoder-only, 36 layers, hidden 2048 |

| Context | 65,536 tokens (scores reported at 8,192) |

| Vocab | 128,256 |

| Reasoning format | <think>…</think> then the answer |

| Language | English |

| License | webAI Non-Commercial License v1.0 (base SmolLM3 is Apache 2.0) |

Highlights

• In-domain formal-logic macro gate 0.336 → 0.422 vs SmolLM3-3B (+26% relative) while held-out 10-dataset macro also rose (0.7193 → 0.7339). [web:2]
• Structured outputs: FOL, entailment labels, semantic parses, Lean statements and critique. [web:2]
• Short answers: ~564 tokens Track A / ~482 Track B; ~28–33 answers/s in the official BF16 harness — not a GGUF measurement. [web:2]
• Q4_K_M is ~1.78 GiB and is the recommended local default (CPU or ~4 GB VRAM). [web:7]

This is not a general assistant. There is no extra safety or preference tuning beyond SmolLM3; instruction following (IFEval) slightly regressed. [web:2]

Available quants

Pick one .gguf file. Filenames follow the usual TwIL-LM3-<QUANT>.gguf pattern. Official reference sizes from the upstream card: [web:7]

| Quant | Size | Bits/weight | Notes |

|---|---|---|---|

| Q2_K / IQ* | smallest | ~2–3 | Max compression; expect quality loss on FOL/Lean |

| Q3_K_M / Q3_K_S | small | ~3 | Tight RAM; logic tasks degrade first |

| Q4_K_M | 1.78 GiB | 4.96 | Recommended default |

| Q5_K_M | 2.06 GiB | 5.74 | Extra headroom vs Q4_K_M |

| Q5_K_S | ~2.0 GiB | ~5.3 | Slightly smaller Q5 |

| Q6_K | 2.35 GiB | 6.56 | Near-Q8 quality, smaller than Q8 |

| Q8_0 | 3.05 GiB | 8.50 | Near-lossless |

| F16 | 5.73 GiB | 16.00 | Requantize / reference |

Upstream K-quants were made with llama-quantize from F16 without an importance matrix. Published Track A/B numbers are bf16 + vLLM, not these GGUFs — expect small drift, especially at Q4 and below. [web:7]

Quick start

Use greedy decoding and a large generation budget. The model writes a <think> block first; a short n truncates reasoning and tanks accuracy. Packaged sampling defaults are not greedy. [web:2]

llama.cpp

# recommended
llama-cli -hf NANI-Nithin/TwIL-LM3-GGUF:Q4_K_M -cnv --temp 0 -n 2048

# local file
llama-cli -m TwIL-LM3-Q4_K_M.gguf -cnv --temp 0 -n 2048

# OpenAI-compatible server + web UI
llama-server -hf NANI-Nithin/TwIL-LM3-GGUF:Q4_K_M --temp 0 -c 8192 -n 2048

Chat template, <|im_end|> EOS, and BOS are in the GGUF metadata; chat mode should work without extra flags. --jinja if your build needs an explicit template. [web:2][web:8]

Ollama

ollama run hf.co/NANI-Nithin/TwIL-LM3-GGUF:Q4_K_M

Docker Model Runner

docker model run hf.co/NANI-Nithin/TwIL-LM3-GGUF:Q4_K_M

Python (llama-cpp-python)

from llama_cpp import Llama

llm = Llama.from_pretrained(
    repo_id="NANI-Nithin/TwIL-LM3-GGUF",
    filename="*Q4_K_M*.gguf",
    n_ctx=8192,
    verbose=False,
)

out = llm.create_chat_completion(
    messages=[{
        "role": "user",
        "content": (
            "Does 'All dogs are mammals. Rex is a dog.' entail 'Rex is a mammal'? "
            "Answer entailment, contradiction, or neutral."
        ),
    }],
    temperature=0.0,
    max_tokens=2048,
)
print(out["choices"]["message"]["content"])

Prompting

Apply the SmolLM3 / chat template. The model emits:

<think>
...chain of thought...
</think>
<final structured answer>

Example tasks it was trained for: [web:2]

• First-order logic translation
• Entailment / contradiction / neutral
• Semantic parsing
• Lean formalization
• Lean proof critique
• Rule induction and procedural reasoning

Keep max_new_tokens ≥ 2048 (4096 if you see truncated </think>). Official eval used greedy, 2048 new tokens, max_seq_len 8192. [web:2]

How the original model was trained

Four stages on SmolLM3-3B: [web:2]

1. LoRA SFT on a synthetic formal-logic corpus (Track A objectives).
2. Checkpoint fusion — average diverse intermediate SFT checkpoints.
3. WiSE-FT: \(W = (1-\lambda)W_{\text{base}} + \lambda W_{\text{ft}}\) with \(\lambda=0.25\) so held-out capability does not collapse.
4. MGPO — entropy-weighted GRPO vs a programmatic verifier; published step 2071.

A sibling without conservative WiSE-FT scored higher in-domain but lost ~12 points held-out and was not released. Post-RL self-distillation (SDFT) hurt both tracks and is not in these weights. [web:2]

Results (original BF16, not this GGUF)

Headline official numbers (greedy, paired harness). Full tables live on the upstream card. [web:2]

| Metric | TwIL-LM3 | SmolLM3-3B |

|---|---|---|

| Track A macro gate | 0.4218 | ~0.336–0.347 |

| Track A 6-lane average | 0.4488 | 0.3296 |

| Track A strict-7 | 0.1971 | 0.1493 |

| Lean formalize token-F1 | 0.5869 | 0.4347 |

| Entailment accuracy | 0.5750 | 0.3750 |

| Semantic parse token-F1 | 0.4416 | 0.4149 |

| Math-corpus PPL (↓) | 3.8229 | 4.0685 |

| Track B 10-dataset CoT macro | 0.7339 | 0.7193 |

These figures are not re-measured on this GGUF repo.

Limitations

• Specialist, not a chatbot. Weak or untested on open chat, code, and tool use (HumanEval / LiveCodeBench / BFCL not reported). [web:2]
• Truncation. ~4.4% of Track A gens hit the 2048-token cap; truncated answers score 0. [web:2]
• Quantization drift. No imatrix; Q2/Q3 will hurt exact-match FOL/Lean more than Q6/Q8.
• Context. 65k is inherited from SmolLM3; official scores used 8k only. [web:2]
• License. Non-commercial terms from webAI apply to the fine-tune; attribute HuggingFaceTB for SmolLM3 (Apache 2.0). [web:2]

Intended use

Local / on-device formal-logic assistance: autoformalization sketches, entailment checks, Lean draft critique, teaching FOL. Research and personal non-commercial use under the upstream license.

Acknowledgements

• webAI — TwIL-LM3 training and evaluation
• HuggingFaceTB — SmolLM3-3B
• llama.cpp — GGUF runtime

Citation

@misc{twil-lm3-gguf,
  title        = {TwIL-LM3-GGUF},
  author       = {Kopparapu, Nithin Sai Kumar},
  year         = {2026},
  howpublished = {\url{https://huggingface.co/NANI-Nithin/TwIL-LM3-GGUF}},
  note         = {GGUF quantization of webAI-Official/TwIL-LM3}
}

Also cite webAI-Official/TwIL-LM3 and HuggingFaceTB/SmolLM3-3B.