qwen-3.5-babel-4b-sft
This is the 4B supervised-fine-tuned checkpoint from Babel-Formal, a research project on proof-term-to-tactic-script translation between Lean and Rocq.
The checkpoint is derived from Qwen/Qwen3.5-4B
and fine-tuned on the Babel Lean/Rocq term-to-script training corpus. It is
released as a text-only Qwen3_5ForCausalLM checkpoint: the original
Qwen3.5 wrapper's language-model parameters and tokenizer are retained, while
no vision encoder weights are included.
Loading
from transformers import AutoModelForCausalLM, AutoTokenizer
model_id = "theostos/qwen-3.5-babel-4b-sft"
tokenizer = AutoTokenizer.from_pretrained(model_id, trust_remote_code=True)
model = AutoModelForCausalLM.from_pretrained(
model_id,
dtype="auto",
device_map="auto",
trust_remote_code=True,
)
Use the prompting and verification pipeline in the Babel-Formal repository for Lean/Rocq translation experiments. Generated proof scripts must be checked by the target prover; the model does not guarantee correctness.
Limitations
- This is a research checkpoint specialized for formal-proof translation.
- It is not a general-purpose mathematical correctness oracle.
- Outputs can be syntactically invalid or fail verification.
- The model card does not claim that pretraining-data contamination has been excluded.
License
Apache 2.0, following the upstream Qwen3.5 checkpoint.