NANI-Nithin commited on
Commit
f160cba
Β·
verified Β·
1 Parent(s): 30b78ba

Create README.md

Browse files
Files changed (1) hide show
  1. README.md +203 -0
README.md ADDED
@@ -0,0 +1,203 @@
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
1
+ ---
2
+ license: other
3
+ license_name: webai-non-commercial-1.0
4
+ license_link: https://huggingface.co/webAI-Official/TwIL-LM3
5
+ base_model: webAI-Official/TwIL-LM3
6
+ base_model_relation: quantized
7
+ tags:
8
+ - gguf
9
+ - llama.cpp
10
+ - smollm3
11
+ - reasoning
12
+ - formal-logic
13
+ - quantized
14
+ - local-llm
15
+ language:
16
+ - en
17
+ pipeline_tag: text-generation
18
+ library_name: gguf
19
+ ---
20
+
21
+ # TwIL-LM3-GGUF
22
+
23
+ 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]
24
+
25
+ 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]
26
+
27
+ | Property | Value |
28
+ |---|---|
29
+ | Quant repo | [`NANI-Nithin/TwIL-LM3-GGUF`](https://huggingface.co/NANI-Nithin/TwIL-LM3-GGUF) |
30
+ | Original weights | [`webAI-Official/TwIL-LM3`](https://huggingface.co/webAI-Official/TwIL-LM3) |
31
+ | Base | [`HuggingFaceTB/SmolLM3-3B`](https://huggingface.co/HuggingFaceTB/SmolLM3-3B) |
32
+ | Parameters | 3.08B |
33
+ | Architecture | SmolLM3 decoder-only, 36 layers, hidden 2048 |
34
+ | Context | 65,536 tokens (scores reported at 8,192) |
35
+ | Vocab | 128,256 |
36
+ | Reasoning format | `<think>…</think>` then the answer |
37
+ | Language | English |
38
+ | License | webAI Non-Commercial License v1.0 (base SmolLM3 is Apache 2.0) |
39
+
40
+ ## Highlights
41
+
42
+ - 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]
43
+ - Structured outputs: FOL, entailment labels, semantic parses, Lean statements and critique. [web:2]
44
+ - Short answers: ~564 tokens Track A / ~482 Track B; **~28–33 answers/s** in the official BF16 harness β€” not a GGUF measurement. [web:2]
45
+ - Q4_K_M is ~**1.78 GiB** and is the recommended local default (CPU or ~4 GB VRAM). [web:7]
46
+
47
+ This is **not** a general assistant. There is no extra safety or preference tuning beyond SmolLM3; instruction following (IFEval) slightly regressed. [web:2]
48
+
49
+ ## Available quants
50
+
51
+ Pick one `.gguf` file. Filenames follow the usual `TwIL-LM3-<QUANT>.gguf` pattern. Official reference sizes from the upstream card: [web:7]
52
+
53
+ | Quant | Size | Bits/weight | Notes |
54
+ |---|---|---|---|
55
+ | Q2_K / IQ* | smallest | ~2–3 | Max compression; expect quality loss on FOL/Lean |
56
+ | Q3_K_M / Q3_K_S | small | ~3 | Tight RAM; logic tasks degrade first |
57
+ | **Q4_K_M** | **1.78 GiB** | **4.96** | **Recommended default** |
58
+ | Q5_K_M | 2.06 GiB | 5.74 | Extra headroom vs Q4_K_M |
59
+ | Q5_K_S | ~2.0 GiB | ~5.3 | Slightly smaller Q5 |
60
+ | Q6_K | 2.35 GiB | 6.56 | Near-Q8 quality, smaller than Q8 |
61
+ | Q8_0 | 3.05 GiB | 8.50 | Near-lossless |
62
+ | F16 | 5.73 GiB | 16.00 | Requantize / reference |
63
+
64
+ 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]
65
+
66
+ ## Quick start
67
+
68
+ 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]
69
+
70
+ ### llama.cpp
71
+
72
+ ```bash
73
+ # recommended
74
+ llama-cli -hf NANI-Nithin/TwIL-LM3-GGUF:Q4_K_M -cnv --temp 0 -n 2048
75
+
76
+ # local file
77
+ llama-cli -m TwIL-LM3-Q4_K_M.gguf -cnv --temp 0 -n 2048
78
+
79
+ # OpenAI-compatible server + web UI
80
+ llama-server -hf NANI-Nithin/TwIL-LM3-GGUF:Q4_K_M --temp 0 -c 8192 -n 2048
81
+ ```
82
+
83
+ 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]
84
+
85
+ ### Ollama
86
+
87
+ ```bash
88
+ ollama run hf.co/NANI-Nithin/TwIL-LM3-GGUF:Q4_K_M
89
+ ```
90
+
91
+ ### Docker Model Runner
92
+
93
+ ```bash
94
+ docker model run hf.co/NANI-Nithin/TwIL-LM3-GGUF:Q4_K_M
95
+ ```
96
+
97
+ ### Python (llama-cpp-python)
98
+
99
+ ```python
100
+ from llama_cpp import Llama
101
+
102
+ llm = Llama.from_pretrained(
103
+ repo_id="NANI-Nithin/TwIL-LM3-GGUF",
104
+ filename="*Q4_K_M*.gguf",
105
+ n_ctx=8192,
106
+ verbose=False,
107
+ )
108
+
109
+ out = llm.create_chat_completion(
110
+ messages=[{
111
+ "role": "user",
112
+ "content": (
113
+ "Does 'All dogs are mammals. Rex is a dog.' entail 'Rex is a mammal'? "
114
+ "Answer entailment, contradiction, or neutral."
115
+ ),
116
+ }],
117
+ temperature=0.0,
118
+ max_tokens=2048,
119
+ )
120
+ print(out["choices"]["message"]["content"])
121
+ ```
122
+
123
+ ## Prompting
124
+
125
+ Apply the SmolLM3 / chat template. The model emits:
126
+
127
+ ```text
128
+ <think>
129
+ ...chain of thought...
130
+ </think>
131
+ <final structured answer>
132
+ ```
133
+
134
+ Example tasks it was trained for: [web:2]
135
+
136
+ - First-order logic translation
137
+ - Entailment / contradiction / neutral
138
+ - Semantic parsing
139
+ - Lean formalization
140
+ - Lean proof critique
141
+ - Rule induction and procedural reasoning
142
+
143
+ Keep `max_new_tokens` β‰₯ 2048 (4096 if you see truncated `</think>`). Official eval used greedy, 2048 new tokens, `max_seq_len` 8192. [web:2]
144
+
145
+ ## How the original model was trained
146
+
147
+ Four stages on SmolLM3-3B: [web:2]
148
+
149
+ 1. **LoRA SFT** on a synthetic formal-logic corpus (Track A objectives).
150
+ 2. **Checkpoint fusion** β€” average diverse intermediate SFT checkpoints.
151
+ 3. **WiSE-FT**: \(W = (1-\lambda)W_{\text{base}} + \lambda W_{\text{ft}}\) with \(\lambda=0.25\) so held-out capability does not collapse.
152
+ 4. **MGPO** β€” entropy-weighted GRPO vs a programmatic verifier; published step **2071**.
153
+
154
+ 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]
155
+
156
+ ## Results (original BF16, not this GGUF)
157
+
158
+ Headline official numbers (greedy, paired harness). Full tables live on the [upstream card](https://huggingface.co/webAI-Official/TwIL-LM3). [web:2]
159
+
160
+ | Metric | TwIL-LM3 | SmolLM3-3B |
161
+ |---|---|---|
162
+ | Track A macro gate | 0.4218 | ~0.336–0.347 |
163
+ | Track A 6-lane average | 0.4488 | 0.3296 |
164
+ | Track A strict-7 | 0.1971 | 0.1493 |
165
+ | Lean formalize token-F1 | 0.5869 | 0.4347 |
166
+ | Entailment accuracy | 0.5750 | 0.3750 |
167
+ | Semantic parse token-F1 | 0.4416 | 0.4149 |
168
+ | Math-corpus PPL (↓) | 3.8229 | 4.0685 |
169
+ | Track B 10-dataset CoT macro | 0.7339 | 0.7193 |
170
+
171
+ These figures are **not** re-measured on this GGUF repo.
172
+
173
+ ## Limitations
174
+
175
+ - **Specialist, not a chatbot.** Weak or untested on open chat, code, and tool use (HumanEval / LiveCodeBench / BFCL not reported). [web:2]
176
+ - **Truncation.** ~4.4% of Track A gens hit the 2048-token cap; truncated answers score 0. [web:2]
177
+ - **Quantization drift.** No imatrix; Q2/Q3 will hurt exact-match FOL/Lean more than Q6/Q8.
178
+ - **Context.** 65k is inherited from SmolLM3; official scores used 8k only. [web:2]
179
+ - **License.** Non-commercial terms from webAI apply to the fine-tune; attribute HuggingFaceTB for SmolLM3 (Apache 2.0). [web:2]
180
+
181
+ ## Intended use
182
+
183
+ 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.
184
+
185
+ ## Acknowledgements
186
+
187
+ - [webAI](https://huggingface.co/webAI-Official/TwIL-LM3) β€” TwIL-LM3 training and evaluation
188
+ - [HuggingFaceTB](https://huggingface.co/HuggingFaceTB/SmolLM3-3B) β€” SmolLM3-3B
189
+ - [llama.cpp](https://github.com/ggerganov/llama.cpp) β€” GGUF runtime
190
+
191
+ ## Citation
192
+
193
+ ```bibtex
194
+ @misc{twil-lm3-gguf,
195
+ title = {TwIL-LM3-GGUF},
196
+ author = {Kopparapu, Nithin Sai Kumar},
197
+ year = {2026},
198
+ howpublished = {\url{https://huggingface.co/NANI-Nithin/TwIL-LM3-GGUF}},
199
+ note = {GGUF quantization of webAI-Official/TwIL-LM3}
200
+ }
201
+ ```
202
+
203
+ Also cite [`webAI-Official/TwIL-LM3`](https://huggingface.co/webAI-Official/TwIL-LM3) and [`HuggingFaceTB/SmolLM3-3B`](https://huggingface.co/HuggingFaceTB/SmolLM3-3B).