Recommended: Q5_K_M for desktop, Q4_K_M for mobile/edge.
About the Model
Two-stage build:
Stage 1 — Coder Teacher Distillation: Qwen3-1.7B distilled from Qwen3-Coder-30B-A3B-Instruct on 6,122 STEM CoT samples. Proof-weighted cross-entropy (2.5x → 1.5x on derivation tokens) + KL divergence at T=2.0. The Coder teacher transfers structured decomposition patterns — sequential logic, state tracking, compositional reasoning — through the softmax landscape.
Stage 2 — Logical Inference SFT: Fine-tuned on KonstantinDob/logic_inference_dataset (~54,607 propositional logic pairs, LOGICINFERENCEe format). The model performs inference first, then concludes. Based on the LogicInference paper by Santiago Ontañón (Google Research).
1./llama-cli -m qwen3-1.7b-coder-distilled-sft-Q4_K_M.gguf \2 -p "### Instruction:\nConsider the premises: If it rains, the ground is wet. It is raining. What can we conclude?\n\n### Response:\n"\3 -n 512 --temp 0.0
llama.cpp Python
python
1from llama_cpp import Llama
23llm = Llama(model_path="qwen3-1.7b-coder-distilled-sft-Q4_K_M.gguf", n_ctx=1024)45output = llm(6"### Instruction:\nIs the following argument valid? All dogs are animals. Some animals are pets. Therefore, all dogs are pets.\n\n### Response:\n",7 max_tokens=512,8 temperature=0.0,9)10print(output["choices"][0]["text"])
Ollama
bash
1echo'FROM ./qwen3-1.7b-coder-distilled-sft-Q4_K_M.gguf'> Modelfile
2ollama create logic-reasoner -f Modelfile
3ollama run logic-reasoner "If all humans are mortal and Socrates is human, what follows?"
LM Studio
Download any GGUF file and load directly in LM Studio.
Prompt Formats
STEM derivation (Stage 1):
Solve the following problem carefully and show a rigorous derivation.
Problem:
[Your problem]
Proof:
### Instruction:
[Your question or logical inference problem]
### Response:
Limitations
1.7B model. Structured reasoning with hard capacity limits. Not a code generator despite the Coder teacher. Not a formal proof verifier. Complex multi-step inferences with many quantifiers may exceed capacity. Always verify critical outputs.
This is a GGUF-quantized variant. The mathematical foundations (Discrepancy Calculus, Topological Knowledge Distillation) are documented in the source model's card. The discrepancy operator $Df(x)$ and BV decomposition that inform the training pipeline are preserved through quantization — the structural boundaries detected by DISC during training are baked into the weights, not dependent on precision.
This is a GGUF-quantized variant. The mathematical foundations (Discrepancy Calculus, Topological Knowledge Distillation) are documented in the source model's card. The discrepancy operator $Df(x)$ and BV decomposition that inform the training pipeline are preserved through quantization — the structural boundaries detected by DISC during training are baked into the weights, not dependent on precision.
The only BF16 collection in the portfolio. While the broader Convergent Intelligence catalog (43 models, 12,000+ downloads) was trained on CPU at FP32 for $24 total compute, the DistilQwen series was trained on H100 at BF16 with a 30B-parameter teacher. Same methodology, premium hardware. This is what happens when you give the pipeline real compute.
All models use proof-weighted knowledge distillation: 55% cross-entropy with decaying proof weights (2.5× → 1.5×), 45% KL divergence at T=2.0. The proof weight amplifies loss on reasoning-critical tokens, forcing the student to allocate capacity to structural understanding rather than surface-level pattern matching.
