YAML Metadata Warning:empty or missing yaml metadata in repo card

Check out the documentation for more information.

xiaolesu/OsmosisProofling-SFT

Experimental checkpoint from "Data Overlap as a Post-Training Hyperparameter for Autoformalization." This is the SFT-only variant (Qwen3-8B, thinking disabled) trained on 20K heterogeneous (natural-language, Lean 4) pairs. See the paper repo for details, results, and all artifacts.

πŸ“„ Paper

This model is part of the experiments in:

SFT-GRPO Data Overlap as a Post-Training Hyperparameter for Autoformalization
Xiaole Su, Kasey Zhang, Andy Lyu
https://arxiv.org/abs/2604.13515

Downloads last month
888
Safetensors
Model size
8B params
Tensor type
BF16
Β·
Inference Providers NEW
This model isn't deployed by any Inference Provider. πŸ™‹ Ask for provider support

Model tree for xiaolesu/OsmosisProofling-SFT

Quantizations
1 model

Paper for xiaolesu/OsmosisProofling-SFT