---
base_model: Qwen/Qwen3.5-2B
library_name: transformers
license: apache-2.0
pipeline_tag: text-generation
tags:
- formal-methods
- theorem-proving
- lean
- rocq
- qwen3.5
- supervised-fine-tuning
---

# qwen-3.5-babel-2b-sft

This is the 2B supervised-fine-tuned checkpoint from
[Babel-Formal](https://github.com/theostos/babel-formal), a research project on
proof-term-to-tactic-script translation between Lean and Rocq.

The checkpoint is derived from [Qwen/Qwen3.5-2B](https://huggingface.co/Qwen/Qwen3.5-2B)
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

```python
from transformers import AutoModelForCausalLM, AutoTokenizer

model_id = "theostos/qwen-3.5-babel-2b-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.