webAI-Official/TwIL-LM2
webAI-Official/TwIL-LM2 is a 2.53 billion parameter decoder-only transformer model, built from ibm-granite/granite-3.3-2b-instruct. Developed by webAI-Official, it is specifically optimized for formal logic tasks, demonstrating strong performance in areas like Lean formalization and rule induction. The model achieves a macro gate score of 0.4178 on in-domain formal logic benchmarks and offers fast decoding speeds, making it suitable for specialized reasoning applications.
Loading preview...
TwIL-LM2: A Specialized Formal Logic Reasoning Model
TwIL-LM2 is a 2.53 billion parameter model developed by webAI-Official, derived from ibm-granite/granite-3.3-2b-instruct. It is highly specialized for formal logic tasks, including FOL translation, entailment, semantic parsing, Lean formalization, and critique.
Key Capabilities & Performance
- Exceptional Formal Logic Performance: Achieves a macro gate score of 0.4178 on in-domain formal logic benchmarks, ranking fourth among twelve compared models, ahead of larger alternatives like LFM2.5-8B-A1B and Granite-4.1-3B.
- Competitive in Specific Logic Lanes: Ranks fourth on
lean_formalizetoken-F1 (0.5159) and ahead of TwIL-LM3 onrule_induction(0.3292). - High Decoding Speed: Decodes at 21,369 tokens/s on an H100, making it 1.57x faster than TwIL-LM3 due to its Granite architecture base.
- Efficient Resource Usage: With 2.53B parameters, it runs efficiently, including GGUF builds for CPU deployment (e.g., Q4_K_M at 1.44 GiB).
- Long Context Window: Inherits a 131,072-token context window from its base model, though evaluations were conducted with shorter generation budgets.
Limitations & Intended Use
- Not a General Assistant: This model is not designed for general-purpose tasks or strict output formatting. It performs poorly on strict-output metrics (e.g., strict MCQ accuracy 0.0000, strict-7 score 0.1214) and general held-out benchmarks.
- No Safety Tuning: Lacks specific safety tuning or instruction-following alignment beyond its base model.
- Non-Commercial License: Released under the webAI Non-Commercial License ver. 1.0.
TwIL-LM2 is ideal for applications requiring robust performance in formal logic reasoning where speed and specialized accuracy are paramount, rather than broad general knowledge or strict output adherence.