Llama-3.1-8B-Instruct-Math-Reasoner-4bit

Llama-3.1-8B-Instruct-Math-Reasoner-4bit is a lightweight, high-precision mathematical reasoning and theorem-proving model. It is fine-tuned from Meta's Llama-3.1-8B-Instruct using Unsloth on approximately 160 MB of curated mathematical proofs, lemmas, and multi-step reasoning data.

The model is quantized in 4-bit (NF4) via bitsandbytes, enabling efficient deployment on consumer GPUs (e.g., RTX 3060/4060, T4, V100) while retaining the strong logical coherence of the 8B parameter instruction-tuned architecture.

---

Model Highlights

Feature	Specification
Base Model	unsloth/Meta-Llama-3.1-8B-Instruct-bnb-4bit
Developer / Creator	akazidane
Architecture	Llama 3.1 (8B parameters, GQA, RoPE up to 128k context)
Quantization	4-bit NormalFloat (NF4 via bitsandbytes)
Fine-Tuning Framework	Unsloth + TRL SFTTrainer (QLoRA)
Dataset Volume	~160 MB of structured mathematical proofs & reasoning traces
Primary Focus	Mathematical theorem proving, formal/informal proofs, and step-by-step calculus, algebra, and number theory derivations
License	Meta Llama 3.1 Community License

---

Intended Use & Capabilities

• Rigorous Proof Generation: Generates structured, lemma-driven proofs across abstract algebra, real analysis, topology, number theory, and discrete mathematics.
• Step-by-Step Derivation: Breaks down complex mathematical calculations and solves olympiad-style (AIME/USAMO) problem steps without skipping algebraic transitions.
• Proof Critique & Verification: Helps identify logical gaps, unwarranted assumptions, or algebraic mistakes in existing mathematical arguments.
• Resource-Constrained Environments: Runs comfortably in under 6 GB VRAM during 4-bit inference.

---

Quickstart & Inference

1. Fast Inference with Unsloth (Recommended)

Unsloth provides up to 2x faster inference and significant memory savings:

import torch
from unsloth import FastLanguageModel

max_seq_length = 4096  # Supports up to 128k if required
dtype = None           # Automatically detects Float16 / Bfloat16
load_in_4bit = True    # 4-bit quantization

# 1. Load model and tokenizer
model, tokenizer = FastLanguageModel.from_pretrained(
    model_name="akazidane/Llama-3.1-8B-Instruct-Math-Reasoner-4bit",
    max_seq_length=max_seq_length,
    dtype=dtype,
    load_in_4bit=load_in_4bit,
)

# 2. Enable native fast inference
FastLanguageModel.for_inference(model)

# 3. Format input using the standard Llama 3.1 chat template
messages = [
    {
        "role": "system",
        "content": (
            "You are an expert mathematician. Provide rigorous, step-by-step "
            "mathematical proofs with explicit justification for each deductive step."
        ),
    },
    {
        "role": "user",
        "content": "Prove that every non-trivial subgroup of a cyclic group is cyclic.",
    },
]

inputs = tokenizer.apply_chat_template(
    messages,
    tokenize=True,
    add_generation_prompt=True,
    return_tensors="pt",
).to("cuda")

# 4. Generate proof
outputs = model.generate(
    input_ids=inputs,
    max_new_tokens=1024,
    temperature=0.2,   # Low temperature for logical precision
    top_p=0.9,
    use_cache=True,
)

response = tokenizer.decode(outputs[0][inputs.shape[1]:], skip_special_tokens=True)
print(response)

2. Standard Transformers & BitsAndBytes

You can also run inference via standard Hugging Face transformers:

import torch
from transformers import AutoModelForCausalLM, AutoTokenizer

model_id = "akazidane/Llama-3.1-8B-Instruct-Math-Reasoner-4bit"

tokenizer = AutoTokenizer.from_pretrained(model_id)
model = AutoModelForCausalLM.from_pretrained(
    model_id,
    device_map="auto",
    torch_dtype=torch.bfloat16,
)

messages = [
    {
        "role": "system",
        "content": "You are a mathematical reasoning assistant. Provide structured, formal proofs.",
    },
    {
        "role": "user",
        "content": "Prove that the square root of 2 is irrational using proof by contradiction.",
    },
]

prompt = tokenizer.apply_chat_template(
    messages,
    tokenize=False,
    add_generation_prompt=True,
)

inputs = tokenizer(prompt, return_tensors="pt").to(model.device)

with torch.no_grad():
    outputs = model.generate(
        **inputs,
        max_new_tokens=1024,
        temperature=0.2,
        top_p=0.9,
        do_sample=True,
    )

print(tokenizer.decode(outputs[0][inputs.input_ids.shape[1]:], skip_special_tokens=True))

---

Prompt Template Format

The model follows the standard Llama 3.1 Instruct special token layout:

<|begin_of_text|><|start_header_id|>system<|end_header_id|>

{system_prompt}<|eot_id|><|start_header_id|>user<|end_header_id|>

{user_prompt}<|eot_id|><|start_header_id|>assistant<|end_header_id|>

Recommended System Prompt for Proofs:

"You are an expert mathematician. Formulate rigorous, unambiguous proofs. Define notation clearly, state all lemmas utilized, and proceed step-by-step to the conclusion."

---

Training Details

• Base Architecture: Meta-Llama-3.1-8B-Instruct (4-bit quantized base via Unsloth).
• Fine-Tuning Dataset: ~160 MB corpus consisting of mathematical proof texts, formal axiomatic step sequences, worked contest problems, and chain-of-thought derivations.
• Tuning Method: Parameter-Efficient Fine-Tuning (QLoRA) targeting linear projections (q_proj, k_proj, v_proj, o_proj, gate_proj, up_proj, down_proj).
• Optimization: Unsloth fused cross-entropy and fast Triton attention kernels.

---

Recommended Generation Parameters

For mathematical proof tasks, greedy or low-temperature decoding produces the most consistent and sound logic:

Parameter	Value	Rationale
temperature	0.1 – 0.3	Minimizes hallucinated steps and maintains chain-of-thought rigor
top_p	0.90 – 0.95	Eliminates low-probability divergent tokens
max_new_tokens	1024 – 2048	Grants adequate token budget for multi-step lemmas
repetition_penalty	1.05 – 1.10	Prevents cyclical equations or repetitive algebraic statements

---

Limitations & Best Practices

1. Independent Verification: While the model significantly improves chain-of-thought mathematical rigor, output proofs should be manually checked or passed to an interactive theorem prover (e.g., Lean 4) for mission-critical formal verification.
2. Arithmetic Calculations: Large multi-digit arithmetic or heavy matrix operations may still benefit from pairing with external symbolic engines (e.g., SymPy or WolframAlpha).
3. Domain Coverage: Excels at proof-based mathematics and conceptual derivations; domain-specific applied engineering formulas may require additional context in the prompt.

---

Acknowledgments & Citations

• Base model by the Meta Llama Team.
• Fast training and 4-bit quantization powered by Unsloth AI.
• Fine-tuned and maintained by akazidane.