qwen-3.5-babel-4b-sft-agent

qwen-3.5-babel-4b-sft-agent

Babel-Formal native-tool supervised fine-tuning of Qwen3.5-4B. This release is five completed epochs ('epoch_4_step_144', zero-based epoch/step numbering; 145 optimizer updates), not the latest checkpoint of a longer run. It uses Qwen's native chat template, reasoning field and 'submit_tactic' tool calls instead of the earlier custom boxed-tactic format.

Training used 904 examples, a 12,288-token sequence cap, global batch size 32 and learning rate 1e-5. Demonstrations submit complete Lean/Rocq tactic proofs; they do not invent verifier feedback. This is SFT, not GRPO or expert iteration. No benchmark score is claimed for this release.

This is a text-only Qwen3_5ForCausalLM: no vision encoder is included. Weights are complete consolidated safetensors, not adapters or rank-local NeMo shards. The tokenizer, native chat template and generation configuration are included. No NeMo installation or custom model code is needed for inference.

Usage

Validated with Transformers 5.5.0. Install transformers and accelerate in a compatible PyTorch environment, then:

from transformers import AutoModelForCausalLM, AutoTokenizer

model_id = "theostos/qwen-3.5-babel-4b-sft-agent"
tokenizer = AutoTokenizer.from_pretrained(model_id)
model = AutoModelForCausalLM.from_pretrained(
    model_id, dtype="auto", device_map="auto",
)
tool = {
    "type": "function",
    "function": {
        "name": "submit_tactic",
        "description": "Submit a tactic block to the Lean or Rocq verifier. The block may contain a complete proof.",
        "parameters": {
            "type": "object",
            "properties": {
                "tactic": {
                    "type": "string",
                    "description": "Tactics only, without theorem declarations or Markdown fences."
                }
            },
            "required": [
                "tactic"
            ]
        }
    }
}
messages = [{
    "role": "user",
    "content": (
        "Derive a Lean 4 tactic proof from the following proof term. "
        "Use submit_tactic to submit the complete tactic proof. "
        "Do not include theorem declarations or Markdown fences in the tactic argument.\n\n"
        "Proof term:\nfun (p : Prop) (h : p) => h\n\n"
        "Dependencies that may be useful:\n"
    ),
}]
inputs = tokenizer.apply_chat_template(
    messages, tools=[tool], enable_thinking=True,
    add_generation_prompt=True, tokenize=True,
    return_tensors="pt", return_dict=True,
).to(model.device)
outputs = model.generate(**inputs, max_new_tokens=1024)
print(tokenizer.decode(outputs[0, inputs["input_ids"].shape[1]:], skip_special_tokens=False))

The native Qwen template serializes tool calls in its XML-style format. Supplying a tool schema does not execute the tool: parse the output and check the tactic proof using Lean or Rocq. Generated proofs can be invalid. See Babel-Formal for the training and verification pipeline. This research model is not a correctness oracle.

Released under Apache 2.0, following the upstream Qwen3.5 model.