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]

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]

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]

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.