language:

• en license: Apache License 2.0 tags:
• auto-formalization
• mathematical-translation
• natural-language-to-formal
• theorem-formalization pipeline_tag: text-generation tasks:
  • text-generation
  • auto-formalization frameworks: PyTorch

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

Evaluation Results (pass@8)

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

cd /path/to/Spark-Formalizer-X1-7B
# We recommend using Python 3.10
pip install -r requirements.txt
pip install .

Quickstart

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.

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.