353 lines
13 KiB
Markdown
353 lines
13 KiB
Markdown
---
|
|
language:
|
|
- en
|
|
library_name: peft
|
|
pipeline_tag: text-generation
|
|
base_model: HuggingFaceTB/SmolLM2-1.7B-Instruct
|
|
license: other
|
|
license_name: webai-non-commercial-license-ver.-1.0
|
|
license_link: https://huggingface.co/webAI-Official/webAI-ColVec1-4b/blob/main/LICENSE.md
|
|
tags:
|
|
- formal-logic
|
|
- reasoning
|
|
- lora
|
|
- peft
|
|
- gguf
|
|
- llama.cpp
|
|
- smollm2
|
|
- twil-lm
|
|
---
|
|
|
|
# TwiL-LM(1.7B)
|
|
|
|
TwiL-LM(1.7B) is a parameter-efficient LoRA adapter for
|
|
[SmolLM2-1.7B-Instruct](https://huggingface.co/HuggingFaceTB/SmolLM2-1.7B-Instruct).
|
|
It is designed for formal-logic tasks including first-order logic (FOL)
|
|
translation, entailment classification, multiple-choice reasoning, semantic
|
|
parsing, Lean assistance, and procedural reasoning.
|
|
|
|
## Model details
|
|
|
|
- **Developed by:** webAI Intelligence Lab
|
|
- **Model repository:** [webAI-Official/TwIL-LM](https://huggingface.co/webAI-Official/TwIL-LM)
|
|
- **Model type:** Decoder-only Transformer with a PEFT LoRA adapter
|
|
- **Base model:** SmolLM2-1.7B-Instruct
|
|
- **Language:** English
|
|
- **License:** webAI Non-Commercial License ver. 1.0
|
|
- **LoRA configuration:** rank 64, alpha 128, dropout 0.0, no bias
|
|
- **Context window:** 8,192 tokens, inherited from the base model
|
|
- **Runtime parameters:** 1,783,728,128 total, consisting of approximately
|
|
1.711B backbone parameters and 72.35M LoRA parameters
|
|
- **Release formats:** PEFT adapter and optional GGUF artifacts
|
|
|
|
This is an adapter, not an independently trained foundation model. Use it with
|
|
the exact base checkpoint and tokenizer listed above.
|
|
|
|
## Model description
|
|
|
|
TwiL-LM adds a relatively small set of trainable weights to SmolLM2-1.7B-Instruct.
|
|
The adapter was trained on a proprietary multi-task corpus engineered for formal
|
|
logic, multi-step deduction, and mathematical reasoning. The corpus combines
|
|
examples from 47 reasoning sources with filtered synthetic examples.
|
|
|
|
In the evaluation described below, TwiL-LM achieved a macro-primary score of
|
|
**0.361**, compared with **0.185** for the unadapted SmolLM2-1.7B base. It led
|
|
the sub-2B models included in this comparison. This result is specific to the
|
|
reported formal-logic suite and should not be interpreted as a general measure
|
|
of intelligence or performance on all reasoning tasks.
|
|
|
|
## Intended uses
|
|
|
|
### Direct use
|
|
|
|
- Translating English statements into first-order logic.
|
|
- Classifying whether a conclusion follows from a set of premises.
|
|
- Answering multiple-choice logic questions.
|
|
- Parsing natural language into structured representations.
|
|
- Drafting or critiquing Lean formalizations with external verification.
|
|
- Research and experimentation on small formal-reasoning models.
|
|
|
|
### Downstream use
|
|
|
|
The model can be integrated into systems that combine language-model generation
|
|
with symbolic solvers, theorem provers, schema validators, or human review.
|
|
Downstream developers should validate outputs for their target domain and retain
|
|
the license and safety restrictions of both this adapter and its base model.
|
|
|
|
### Out-of-scope uses
|
|
|
|
- Autonomous medical, legal, financial, or safety-critical decisions.
|
|
- Treating generated FOL or Lean as verified without running an appropriate
|
|
checker or theorem prover.
|
|
- Unsupervised deployment where logically incorrect or fabricated output can
|
|
cause material harm.
|
|
- Uses prohibited by the webAI Non-Commercial License or the base-model license.
|
|
- Impersonation, deceptive systems, autonomous weaponry, or surveillance that
|
|
targets protected classes.
|
|
|
|
## Training details
|
|
|
|
### Training data
|
|
|
|
The training corpus is proprietary and is not currently published as a Hugging
|
|
Face dataset. It was assembled from 47 reasoning sources and augmented with
|
|
synthetic examples. Samples were normalized into a shared schema, filtered for
|
|
structural quality, deduplicated, and checked using a two-stage LLM verification
|
|
process. Synthetic data can still contain undetected errors, stylistic artifacts,
|
|
or verifier preferences.
|
|
|
|
Because the complete training corpus and all source-level mixture weights are not
|
|
public, independent reproduction and contamination auditing are limited. Users
|
|
should account for this limitation when comparing results or deploying the model.
|
|
|
|
### Training procedure
|
|
|
|
- **Method:** Supervised fine-tuning with PEFT LoRA
|
|
- **Rank:** 64
|
|
- **Alpha:** 128
|
|
- **Dropout:** 0.0
|
|
- **Bias:** none
|
|
- **Target modules:** `q_proj`, `k_proj`, `v_proj`, `o_proj`, `gate_proj`,
|
|
`up_proj`, and `down_proj`
|
|
- **Task type:** `CAUSAL_LM`
|
|
|
|
Optimizer settings, learning-rate schedule, epoch count, random seed, training
|
|
hardware, wall-clock time, and energy consumption are not documented in the
|
|
current release artifacts. These should be added when verified records become
|
|
available.
|
|
|
|
|
|
|
|
## Evaluation
|
|
|
|
### Formal-logic evaluation
|
|
|
|
The in-domain evaluation used held-out samples with up to 200 rows per objective
|
|
and greedy decoding. The reported macro-primary score is an equal-weight average
|
|
over the eligible objectives. `mcq_answer` and `procedural` use
|
|
`max(accuracy, loose_match)`. `lean_prove` and perplexity corpora are excluded
|
|
from the macro score.
|
|
|
|
|
|
|
|
|
|
|
|
The broader comparison includes checkpoints with different parameter counts,
|
|
training procedures, and adaptation methods. It is useful for context but is not
|
|
a controlled architecture or scaling study.
|
|
|
|
|
|
|
|
TwiL-LM performs best on entailment labeling (**0.655**) and improves FOL
|
|
translation (**0.235**, compared with approximately zero for the base). Lean
|
|
formalization, Lean proving, and procedural reasoning remain weak.
|
|
|
|
### Out-of-Distribution (OOD) evaluation
|
|
|
|
OOD transfer was measured on GSM8K, ARC-Challenge chain-of-thought,
|
|
ARC-Challenge 25-shot log-likelihood (`acc_norm`), and LogicBench BQA.
|
|
|
|
|
|
|
|
Compared with SmolLM2-1.7B, TwiL-LM improves LogicBench BQA
|
|
(**0.590 vs 0.563**) but is lower on GSM8K (**0.380 vs 0.413**), ARC-C
|
|
chain-of-thought (**0.463 vs 0.587**), and ARC-C 25-shot log-likelihood
|
|
(**0.460 vs 0.490**).
|
|
|
|
|
|
|
|
These results indicate mixed transfer outside the formal-logic training
|
|
distribution. Larger general reasoning models remain stronger on several OOD
|
|
benchmarks.
|
|
|
|
### Throughput evaluation
|
|
|
|
|
|
|
|
The formal-logic run generated 422,627 tokens in 1,152.34 generation seconds,
|
|
or **366.8 aggregate tokens per second**. The configuration used a maximum of
|
|
1,024 new tokens per example. Outputs averaged 264.1 new tokens; the median was
|
|
92 tokens, the 90th percentile was 1,024 tokens, and 16.1% of outputs reached the
|
|
generation limit.
|
|
|
|
This is aggregate evaluation throughput, not single-request latency or a
|
|
controlled serving benchmark. It depends on hardware, precision, backend,
|
|
batching, prompt length, output length, and stopping behavior. The comparison
|
|
runs did not consistently control all of these variables, so the figure should
|
|
not be used to claim that LoRA intrinsically accelerates generation.
|
|
|
|
### Evaluation limitations
|
|
|
|
- The formal-logic suite includes custom tasks and metrics and is not a standard
|
|
Hugging Face benchmark dataset.
|
|
- Some comparison checkpoints used different output limits and evaluation runs.
|
|
- The evaluation primarily covers English.
|
|
- The current records do not provide confidence intervals or repeated-seed
|
|
variance.
|
|
- Exact-match metrics can penalize semantically equivalent formal expressions.
|
|
- The training corpus is not public, limiting independent contamination checks.
|
|
|
|
Structured Hub evaluation files are not included because the internal suite is
|
|
not registered as a Hugging Face Benchmark and the available records do not
|
|
contain verified task IDs for the OOD benchmarks. The scores above are therefore
|
|
reported in the card rather than submitted as verified Hub leaderboard results.
|
|
|
|
## How to use
|
|
|
|
### Installation and authentication
|
|
|
|
The model repository may require access approval. Install the dependencies and
|
|
authenticate with the Hugging Face Hub:
|
|
|
|
```bash
|
|
pip install -U torch transformers peft accelerate huggingface_hub
|
|
hf auth login
|
|
```
|
|
|
|
### Transformers with PEFT
|
|
|
|
```python
|
|
import torch
|
|
from peft import PeftModel
|
|
from transformers import AutoModelForCausalLM, AutoTokenizer
|
|
|
|
base_id = "HuggingFaceTB/SmolLM2-1.7B-Instruct"
|
|
adapter_id = "webAI-Official/TwIL-LM"
|
|
|
|
tokenizer = AutoTokenizer.from_pretrained(base_id)
|
|
base_model = AutoModelForCausalLM.from_pretrained(
|
|
base_id,
|
|
torch_dtype="auto",
|
|
device_map="auto",
|
|
)
|
|
model = PeftModel.from_pretrained(base_model, adapter_id)
|
|
model.eval()
|
|
|
|
messages = [
|
|
{
|
|
"role": "user",
|
|
"content": "Translate to first-order logic: All cats are mammals.",
|
|
}
|
|
]
|
|
input_ids = tokenizer.apply_chat_template(
|
|
messages,
|
|
tokenize=True,
|
|
add_generation_prompt=True,
|
|
return_tensors="pt",
|
|
).to(model.device)
|
|
|
|
with torch.inference_mode():
|
|
output_ids = model.generate(
|
|
input_ids,
|
|
max_new_tokens=256,
|
|
do_sample=False,
|
|
)
|
|
|
|
new_tokens = output_ids[0, input_ids.shape[-1]:]
|
|
print(tokenizer.decode(new_tokens, skip_special_tokens=True))
|
|
```
|
|
|
|
Use the base model's tokenizer and chat template. Loading the adapter over a
|
|
different base checkpoint is unsupported and can cause incorrect output or tensor
|
|
shape errors.
|
|
|
|
### llama.cpp with GGUF
|
|
|
|
Download the model repository:
|
|
|
|
```bash
|
|
hf download webAI-Official/TwIL-LM --local-dir TwIL-LM
|
|
```
|
|
|
|
If the release contains a GGUF LoRA adapter, apply it to a GGUF converted from
|
|
the matching SmolLM2-1.7B-Instruct base:
|
|
|
|
```bash
|
|
llama-cli \
|
|
-m /path/to/smollm2-1.7b-instruct-f16.gguf \
|
|
--lora TwIL-LM/smollm2-lorav1-ps-lora-f16.gguf \
|
|
-p "Translate to FOL: All cats are mammals." \
|
|
-n 256
|
|
```
|
|
|
|
If the release contains a merged GGUF, use it without `--lora`:
|
|
|
|
```bash
|
|
llama-cli \
|
|
-m TwIL-LM/smollm2-lorav1-ps-merged-Q4_K_M.gguf \
|
|
-p "Translate to FOL: All cats are mammals." \
|
|
-n 256
|
|
```
|
|
|
|
GGUF filenames can vary between releases. Confirm the downloaded filenames
|
|
before running these commands.
|
|
|
|
## Files and formats
|
|
|
|
- `adapter_model.safetensors`: PEFT LoRA weights, approximately 289 MB.
|
|
- `adapter_config.json`: PEFT configuration that identifies the required base
|
|
model.
|
|
- `smollm2-lorav1-ps-lora-f16.gguf`: optional GGUF LoRA adapter, approximately
|
|
145 MB.
|
|
- Merged GGUF variants may be provided as FP16 (approximately 3.42 GB), Q8_0
|
|
(1.82 GB), Q5_K_M (1.23 GB), or Q4_K_M (1.06 GB).
|
|
|
|
Availability and filenames can vary by release. Quantized GGUF variants may not
|
|
match the evaluation quality reported for the original adapter; validate the
|
|
selected artifact on the target workload.
|
|
|
|
## Limitations, risks, and biases
|
|
|
|
- **Not a verifier:** Plausible-looking FOL or Lean output can be syntactically or
|
|
semantically wrong. Use a symbolic solver, Lean/Mathlib, or expert review.
|
|
- **Narrow specialization:** The adapter is designed for formal logic, not as a
|
|
replacement for a general-purpose assistant.
|
|
- **Mixed OOD performance:** Improvements on LogicBench do not transfer
|
|
consistently to GSM8K or ARC-Challenge.
|
|
- **Small-model capacity:** Long reasoning chains, deeply nested quantifiers,
|
|
complex rule induction, and long formal contexts can fail or hallucinate.
|
|
- **Synthetic-data artifacts:** Synthetic examples and LLM verification can
|
|
introduce systematic style, content, or verifier bias.
|
|
- **English-first:** Performance in other languages is not established.
|
|
- **Base-model inheritance:** The adapter retains the base model's limitations,
|
|
biases, and potential for unsafe or inaccurate content.
|
|
- **Context limit:** Inputs near 8,192 tokens leave less room for generation and
|
|
can be truncated by serving frameworks.
|
|
- **Quantization effects:** Q4 and Q5 builds may change formal-token generation
|
|
and exact-match accuracy.
|
|
- **No uncertainty calibration:** Scores do not establish that model confidence
|
|
corresponds to correctness.
|
|
|
|
## Environmental impact
|
|
|
|
Training-energy use, hardware type, training duration, datacenter region, and
|
|
carbon emissions were not recorded in the available release artifacts. No
|
|
emissions estimate is provided. Inference impact varies with hardware, precision,
|
|
quantization, sequence length, and utilization.
|
|
|
|
## License
|
|
|
|
The model weights are distributed under the
|
|
[webAI Non-Commercial License ver. 1.0](https://huggingface.co/webAI-Official/webAI-ColVec1-4b/blob/main/LICENSE.md).
|
|
Review that license and the
|
|
[SmolLM2 base-model terms](https://huggingface.co/HuggingFaceTB/SmolLM2-1.7B-Instruct)
|
|
before use. The license applied to source code in this repository does not
|
|
override the model-weight license.
|
|
|
|
## Citation
|
|
|
|
```bibtex
|
|
@misc{twil_lm_1_7b,
|
|
title = {TwiL-LM(1.7B) Formal-Logic LoRA},
|
|
author = {webAI Intelligence Lab},
|
|
year = {2026},
|
|
url = {https://huggingface.co/webAI-Official/TwIL-LM}
|
|
}
|
|
```
|
|
|
|
## Contact
|
|
|
|
For model questions, licensing requests, or reports of harmful behavior, use the
|
|
Community tab of the
|
|
[webAI-Official/TwIL-LM](https://huggingface.co/webAI-Official/TwIL-LM)
|
|
repository. |