---
title: Spark-Formalizer-X1-7B
canonical_url: "https://www.modelscope.cn/models/iflytek/Spark-Formalizer-X1-7B"
md_url: "https://www.modelscope.cn/models/iflytek/Spark-Formalizer-X1-7B.md"
repository: iflytek/Spark-Formalizer-X1-7B
chinese_name: Spark-Formalizer-X1-7B
last_updated: 2025-12-08
license: "Apache License 2.0"
pipeline_tag: text-generation
tasks:
  - text-generation
model_type:
  - spark
architectures:
  - SparkModel
parameters: 7.5B
tensor_type:
  - F32
library_name:
  - pytorch
  - safetensors
frameworks:
  - PyTorch
language:
  - en
downloads: 90
stars: 1
tags:
  - auto-formalization
  - mathematical-translation
  - natural-language-to-formal
  - theorem-formalization
---

# Spark-Formalizer-X1-7B

> Spark-Formalizer-X1-7B - iflytek 在 ModelScope 开源的模型。Model Card for iFLYTEK Spark-Formalizer-X1-7B

iflytek/Spark-Formalizer-X1-7B 是 ModelScope 魔搭社区上的 7.5B 参数text-generation模型，采用 Apache License 2.0 许可。

- **Repository**: iflytek/Spark-Formalizer-X1-7B
- **License**: Apache License 2.0
- **Tasks**: text-generation
- **Parameters**: 7.5B
- **Tags**: auto-formalization, mathematical-translation, natural-language-to-formal, theorem-formalization
- **Downloads**: 90
- **Stars**: 1
- **Last updated**: 2025-12-08

Source: https://www.modelscope.cn/models/iflytek/Spark-Formalizer-X1-7B

---

# Model Card for iFLYTEK Spark-Formalizer-X1-7B

## Model Introduction

**Spark-Formalizer-X1** is a specialized large language model developed by the iFLYTEK team for mathematical auto-formalization. The model excels at translating natural language mathematical problems into precise formal statements, achieving state-of-the-art performance in formal statement generation.

Spark-Formalizer is trained using a comprehensive Two-stage strategy that ensures high accuracy in semantic preservation and syntactic correctness during the translation process.

### Key Features

- **Two-Stage Training Strategy**: Comprehensive training pipeline including pre-training and supervised fine-tuning (SFT)
- **Expert Iteration Framework**: Continuous optimization through iterative data synthesis and model refinement
- **Bidirectional Translation**: Training on both formalization (natural → formal) and unformalization (formal → natural) tasks
- **Multi-task Pre-training**: Training on diverse formal and informal mathematical tasks including:
  - Statement auto-formalization and unformalization
  - Formal code file understanding
  - Tutorial comprehension for tactics and Mathlib
  - Informal mathematics problem solving

## Model Summary

| Parameter                | Spark-Formalizer-X1 |
|--------------------------|------------------|
| Total Parameters         | 7B               |
| Context Length           | 16,384           |
| Training Stages          | Pre-training + SFT |
| Specialization           | Auto-formalization |
| Translation Direction    | Natural language → Formal language |

## Evaluation Results (pass@8)

| Benchmark       | Spark-Formalizer-X1 | Goedel-Formalizer-V2 | Kimina-Formalizer |
|-----------------|------------------|---------------------|-------------------|
| miniF2F-test    | 98.63%       | **99.18%**          | 95.58%            |
| ProofNet-test   | **78.85%**       | 75.81%              | 65.95%            |
| Extract Theorem | **37.50%**           | 37.17%          | 16.00%            |
| College CoT     | **30.17%**       | 27.17%              | 11.50%            |
| ExamFormal-Bench  | **97.68%**       | 97.43%              | 85.32%            |
| **Average**     | **68.57%**       | 67.35%              | 54.87%            |

### Notable Achievements

- **High School & Undergraduate Levels**: Excellent performance on miniF2F-test (98.63%) and ProofNet-test (78.85%)
- **Challenging Translations**: Strong capability on complex college-level problems (College CoT: 30.17%)
- **Cross-domain Proficiency**: Consistent performance across algebra, analysis, geometry, and other mathematical domains

## Training Methodology

### Two-Stage Training Strategy

1. **Pre-training**: Comprehensive training on diverse mathematical data including:
   - Open-source formal datasets
   - High-quality natural-to-formal translation pairs
   - Tutorials and documentation for Mathlib
   - Informal mathematics problems with solutions

2. **Supervised Fine-tuning (SFT)**: Specialized training on curated translation pairs with:
   - Dual deduplication (internal and external)
   - Quality verification through compilation
   - Semantic consistency validation

## Dataset Contributions
We introduce ExamFormal-Bench, a comprehensive benchmark dataset containing 402 problems focusing on formal theorem proving. The dataset covers problems from high school, undergraduate levels, and mathematical competitions, systematically categorized into:

- Analysis
- Geometry
- Algebra
- Probability & Statistics
- Computational Mathematics
- Discrete Mathematics

## Related Models
We also provide Spark-Prover, a specialized model for automated theorem proving that generates complete formal proofs for formal statements. See the Spark-Prover repository for more details.


## Usage
**requirement**
```bash
cd /path/to/Spark-Formalizer-X1-7B
# We recommend using Python 3.10
pip install -r requirements.txt
pip install .
```
**Quickstart**
```python
from modelscope import AutoModelForCausalLM, AutoTokenizer
import torch
# Load model and tokenizer
model_name = "iflytek/Spark-Formalizer-X1-7B"
tokenizer = AutoTokenizer.from_pretrained(model_name,trust_remote_code=True)
model = AutoModelForCausalLM.from_pretrained(
    model_name,
    torch_dtype=torch.float32,
    device_map="auto",
    trust_remote_code=True
)
# Reactive
chat_history = [
  {
    "role" : "user",
    "content" : "求证方程<ret>$$x^2-y^2=1986\\quad(1)$$<ret>无整数解."
  }]

inputs = tokenizer.apply_chat_template(
    chat_history,
    tokenize=True,
    return_tensors="pt",
    add_generation_prompt=True
).to(model.device)

outputs = model.generate(
    inputs,
    max_new_tokens=16384,
    top_k=100,
    do_sample=True,
    repetition_penalty=1.0,
    temperature=0.5,
    eos_token_id=5,
    pad_token_id=0,
)

response = tokenizer.decode(
    outputs[0][inputs.shape[1] :],
    skip_special_tokens=True
)
print(response)
```




**Optional: Convert FP32 Weights to BF16**

The released weights of Spark-Formalizer-X1-7B are stored in FP32 precision.
For inference efficiency, users can optionally convert the weights into bfloat16 (BF16) format.
```python
from modelscope import AutoModelForCausalLM
import torch

model_name = " /path_to/Spark-Formalizer-X1-7B"

# Load FP32 weights
model = AutoModelForCausalLM.from_pretrained(
    model_name,
    torch_dtype=torch.float32, # explicitly FP32
    device_map="auto",
    trust_remote_code=True
)

# Convert to BF16
model = model.to(torch.bfloat16)

#  Save BF16 weights for later fast loading
save_path = "./Spark-Formalizer-X1-7B-bf16"
model.save_pretrained(save_path, safe_serialization=True)
```

 
## License Agreement
iFLYTEK Spark-Formalizer-X1-7B is licensed under Apache 2.0.