初始化项目，由ModelHub XC社区提供模型
Model: webAI-Official/TwIL-LM Source: Original Platform
This commit is contained in:
ModelHub XC
353
README.md
Normal file
353
README.md
Normal file
@@ -0,0 +1,353 @@
|
||||
---
|
||||
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.
|
||||
Reference in New Issue
Block a user