---
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`](https://huggingface.co/webAI-Official/TwIL-LM3) for local inference with [llama.cpp](https://github.com/ggerganov/llama.cpp) and compatible runtimes. [web:2]

TwIL-LM3 is a **3.08B** formal-logic reasoning model built from [`HuggingFaceTB/SmolLM3-3B`](https://huggingface.co/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`](https://huggingface.co/NANI-Nithin/TwIL-LM3-GGUF) |
| Original weights | [`webAI-Official/TwIL-LM3`](https://huggingface.co/webAI-Official/TwIL-LM3) |
| Base | [`HuggingFaceTB/SmolLM3-3B`](https://huggingface.co/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

```bash
# 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

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

### Docker Model Runner

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

### Python (llama-cpp-python)

```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:

```text
<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](https://huggingface.co/webAI-Official/TwIL-LM3). [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](https://huggingface.co/webAI-Official/TwIL-LM3) — TwIL-LM3 training and evaluation
- [HuggingFaceTB](https://huggingface.co/HuggingFaceTB/SmolLM3-3B) — SmolLM3-3B
- [llama.cpp](https://github.com/ggerganov/llama.cpp) — GGUF runtime

## Citation

```bibtex
@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`](https://huggingface.co/webAI-Official/TwIL-LM3) and [`HuggingFaceTB/SmolLM3-3B`](https://huggingface.co/HuggingFaceTB/SmolLM3-3B).