dots123/qwen-7b-theorem-engine-v3

Cannot identify the intended theorem.

User: Every continuous function is differentiable.
Assistant: Every differentiable function is continuous.

User: A continuous function on an interval achieves its maximum and minimum.
Assistant: Every continuous function on a closed and bounded interval achieves its maximum and minimum.

User: Pythagorean: a sqrd plus b sqrd is c sqrd in a right triangle.
Assistant: If \(a\) and \(b\) are the lengths of the legs of a right triangle and \(c\) is the length of the hypotenuse, then \(a^2 + b^2 = c^2\).

User: Let thing be valid then A iff B maybe with x.
Assistant: Cannot identify the intended theorem.

pip install -U transformers peft accelerate bitsandbytes safetensors

hf download Qwen/Qwen2.5-7B-Instruct \
  --local-dir models/Qwen2.5-7B-Instruct

hf download dots123/qwen-7b-theorem-engine-v3 \
  --local-dir outputs/qwen_7b_v3

import re
import torch
from peft import PeftModel
from transformers import AutoModelForCausalLM, AutoTokenizer, BitsAndBytesConfig

BASE = "models/Qwen2.5-7B-Instruct"
ADAPTER = "outputs/qwen_7b_v3"

SYSTEM_PROMPT = """# Role
You are a mathematical statement judgment and correction engine.

# Task
First decide whether the user's mathematical statement is:
CORRECT, FALSE, INCOMPLETE, GARBLED_BUT_IDENTIFIABLE, or UNCLEAR.

# Output rules
1. You MUST first write a concise internal judgment inside a <think>...</think> block.
2. If CORRECT, output the clean mathematical statement only.
3. If FALSE, output the correct theorem or statement.
4. If INCOMPLETE, output the complete rigorous theorem with missing assumptions.
5. If GARBLED_BUT_IDENTIFIABLE, infer the intended theorem and rewrite it fully.
6. If UNCLEAR, output exactly: Cannot identify the intended theorem.
7. Never repeat malformed mathematical text unchanged.
8. Use standard LaTeX formatting for formulas ($...$ or $$...$$).
"""

tokenizer = AutoTokenizer.from_pretrained(BASE, trust_remote_code=True)
bnb_config = BitsAndBytesConfig(
    load_in_4bit=True,
    bnb_4bit_quant_type="nf4",
    bnb_4bit_compute_dtype=torch.bfloat16 if torch.cuda.is_bf16_supported() else torch.float16,
    bnb_4bit_use_double_quant=True,
)

base_model = AutoModelForCausalLM.from_pretrained(
    BASE,
    quantization_config=bnb_config,
    device_map="auto",
    trust_remote_code=True,
)
model = PeftModel.from_pretrained(base_model, ADAPTER)
model.eval()

messages = [
    {"role": "system", "content": SYSTEM_PROMPT},
    {"role": "user", "content": "Every continuous function is differentiable."},
]
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():
    output_ids = model.generate(
        **inputs,
        max_new_tokens=256,
        do_sample=True,
        temperature=0.3,
        top_p=0.85,
        repetition_penalty=1.05,
        eos_token_id=tokenizer.eos_token_id,
        pad_token_id=tokenizer.eos_token_id,
    )

text = tokenizer.decode(output_ids[0][inputs.input_ids.shape[-1]:], skip_special_tokens=True)
answer = re.sub(r"<think>.*?</think>", "", text, flags=re.DOTALL).strip()
answer = answer.replace("无法识别其意图定理。", "Cannot identify the intended theorem.")
print(answer)