# Spark-X1
## 论文
[Spark-Prover-X1: Formal Theorem Proving Through Diverse Data Training](https://arxiv.org/abs/2511.13043)

## 模型简介
Spark-X1 系列是科大讯飞星火大模型体系中的深度推理模型系列。Spark-X1 强调数学、逻辑、代码、语言理解和知识问答等复杂推理能力，并采用快思考/慢思考统一的推理模式。当前开源的 Spark-X1 相关模型主要不是通用 base checkpoint，而是基于 Spark-X1 或科大讯飞新一代基础模型微调得到的垂直领域模型，包括数学形式化与定理证明方向的 Spark-Formalizer-X1-7B / Spark-Prover-X1-7B、化学方向的 Spark-Chemistry-X1-13B、科技文献方向的 Spark-Scilit-X1-13B 等。

## 环境依赖
| 软件 | 版本 |
| :------: | :------: |
| DTK | 26.04 |
| Python | 3.10 |
| Transformers | 4.56.1 |
| vLLM | 0.18.1+das.dtk2604 |

推荐使用镜像: 

harbor.sourcefind.cn:5443/dcu/admin/base/custom:vllm0.18.1-ubuntu22.04-dtk26.04-py3.10-20260510-2242

- 挂载地址`-v` 根据实际模型情况修改
```bash
docker run -it \
    --shm-size 60g \
    --network=host \
    --name Spark-X1 \
    --privileged \
    --device=/dev/kfd \
    --device=/dev/dri \
    --device=/dev/mkfd \
    --group-add video \
    --cap-add=SYS_PTRACE \
    --security-opt seccomp=unconfined \
    -u root \
    -v /opt/hyhal/:/opt/hyhal/:ro \
    -v /path/your_code_data/:/path/your_code_data/ \
    harbor.sourcefind.cn:5443/dcu/admin/base/custom:vllm0.18.1-ubuntu22.04-dtk26.04-py3.10-20260510-2242 bash
```
更多镜像可前往[光源](https://sourcefind.cn/#/service-list)下载使用。

关于本项目DCU显卡所需的特殊深度学习库可从[光合](https://developer.sourcefind.cn/tool/)开发者社区下载安装。

## 预训练权重
**请根据`支持的DCU型号`选择对应模型下载，FP8模型仅在BW1100/BW1101上支持，其他型号请勿使用！**
|  模型名称  | 权重大小 | 数据类型 |支持的DCU型号  | 最低卡数需求 |         下载地址          |
|:------:|:----:|:----:|:----------:|:------:|:---------------------:|
| Spark-Formalizer-X1-7B | 7B | BF16 | K100AI,BW1000 |   1   | [ModelScope](https://modelscope.cn/models/iflytek/Spark-Formalizer-X1-7B) |
| Spark-Chemistry-X1-13B | 13B | BF16 | K100AI,BW1000 |   1   | [ModelScope](https://modelscope.cn/models/iflytek/Spark-Chemistry-X1-13B) |
| Spark-Scilit-X1-13B| 13B | BF16 | K100AI,BW1000 |   1   | [ModelScope](https://modelscope.cn/models/iflytek/Spark-Scilit-X1-13B) |

## 数据集
暂无

## 训练
暂无

## 推理
### Transformers
#### 单机推理

**以`Spark-Chemistry-X1-13B`为例**
```python
from transformers import AutoModelForCausalLM, AutoTokenizer
import torch
# Load model and tokenizer
model_name = "/path/to/Spark-Chemistry-X1-13B"
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" : "请回答下列问题:高分子材料是否具有柔顺性主要决定于()的运动能力。\nA、主链链节\nB、侧基\nC、侧基内的官能团或原子?"
  }]

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=8192,
    top_k=1,
    do_sample=True,
    repetition_penalty=1.02,
    temperature=0.7,
    eos_token_id=5,
    pad_token_id=0,
)

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

### vLLM
#### 单机推理
```bash
# serve启动
# 以Spark-Scilit-X1-13B为例
vllm serve /path/to/Spark-Scilit-X1-13B \
    --generation-config vllm \
    --trust-remote-code \
    --dtype bfloat16 \
    --max-model-len 16384 \
    --served-model-name Spark-Scilit-X1-13B

# client访问
curl http://127.0.0.1:8000/v1/chat/completions \
    -H "Content-Type: application/json" \
    -d '{
      "model": "Spark-Formalizer-X1-7B",
      "messages": [
        {
          "role": "user",
          "content": "请回答下列问题:高分子材料是否具有柔顺性主要决定于()的运动能力。\nA、主链链节\nB、侧基\nC、侧基内的官能团或原子?"
        }
      ],
      "temperature": 0,
      "top_p": 1,
      "max_tokens": 512
    }'
```

## 效果展示
<div align=center>
    <img src="./doc/01.png"/>
</div>

### 精度
DCU与GPU精度一致，推理框架：transformers

## 源码仓库及问题反馈
- https://developer.sourcefind.cn/codes/modelzoo/spark-x1

## 参考资料
- https://arxiv.org/pdf/2408.06574
- https://modelscope.cn/models/iflytek/Spark-Formalizer-X1-7B
- https://modelscope.cn/models/iflytek/Spark-Scilit-X1-13B
- https://gitcode.com/ifly_opensource