Model card update

README.md

@@ -1,5 +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: LICENSE
+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.
+
+![TwiL-LM data creation, training, and evaluation workflow](card_assets/data_workflow_v2.png)
+
+## 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.
+
+![Macro accuracy compared with base models](card_assets/macro_vs_bases.png)
+
+![Macro accuracy compared across Base and LoRA models](card_assets/macro_vs_bases_and_lora.png)
+
+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 compared with SmolLM2-1.7B by objective](card_assets/objectives_vs_smollm2.png)
+
+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.
+
+![TwiL-LM and SmolLM2-1.7B on OOD benchmarks](card_assets/unseen_benchmarks.png)
+
+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**).
+
+![OOD benchmark macro accuracy for Base, FT, and PS variants](card_assets/unseen_macro_no_gsm8k.png)
+
+These results indicate mixed transfer outside the formal-logic training
+distribution. Larger general reasoning models remain stronger on several OOD
+benchmarks.
+
+### Throughput evaluation
+
+![Aggregate generation throughput](card_assets/throughput.png)
+
+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.