0x01 模型分析

model_def.py 中定义的模型非常简单：

class ICTFForCausalLM(PreTrainedModel):
    config_class = ICTFConfig

    def __init__(self, config):
        super().__init__(config)
        self.dense = nn.Linear(config.max_position_embeddings, config.hidden_size, bias=True)
        self.act = nn.ReLU()
        self.lm_head = nn.Linear(config.hidden_size, config.vocab_size, bias=True)

    def forward(self, input_ids, **kwargs):
        x = input_ids.float()
        hidden_states = self.dense(x)
        hidden_states = self.act(hidden_states)
        logits = self.lm_head(hidden_states)
        logits = logits.unsqueeze(1)
        return {"logits": logits}

模型的计算流程如下：

输入字符串
    ↓
转换为字符 ID
    ↓
补齐为长度 16 的向量
    ↓
Linear(16 → 21)
    ↓
ReLU
    ↓
Linear(21 → 64)
    ↓
得到 64 个输出分数
    ↓
最终选择分数最高的 token    

Tokenizer 的字符表为：

0123456789abcdefghijklmnopqrstuvwxyzABCDEFGHIJKLMNOPQRSTUVWXYZ

对应关系为：

0-9  →  ID 0-9
a-z  →  ID 10-35
A-Z  →  ID 36-61

另外还有两个特殊 token：

62 → <success>
63 → <fail>

输入长度不能超过 16。长度不足 16 时，会使用 token ID 0 （对应字符 '0'）进行右填充。
因此，模型最终处理的是一个长度为 16 的整数向量：

$x=(x_0,x_1,\dots ,x_{15})$

其中每个元素满足：

$0\le x_i\le 61$

0x02 权重分析

model.safetensors 中只有四组参数：

观察 lm_head 后，可以发现它几乎完全由人工构造的常数组成。

普通字符

对于 token 0 到 61：

weight 全部为 0
bias = -10000

因此这些 token 的分数始终为：

${\mathrm{logit}}_k=-10000$

<fail>

对于 token 63：

weight全部为 0
bias = 0.4

因此：

${\mathrm{logit}}_{fail}=0.4$

<success>

对于 token 62：

W_lm[62] = [1, -1e10, -1e10, ..., -1e10]
b_lm[62] = -376131.21875

因此：

${\mathrm{logit}}_{success}=h_0-10^{10}(h_1+h_2+\cdots +h_{20})-376131.21875$

0x03 理论推导

第一层的输出为：

$z=Wx+b$

对于第 $i$ 个神经元：

$z_i=W_i\cdot x+b_i$

ReLU 的定义为：

$h_i=\mathrm{ReLU}(z_i)=\max (0,z_i)$

也就是说：

• 当 $z_i<0$ 时，$h_i=0$；
• 当 $z_i>0$ 时，$h_i=z_i$。

<success> 的分数为：

${\mathrm{logit}}_{success}=h_0-10^{10}(h_1+h_2+\cdots +h_{20})-376131.21875$

由于 ReLU 的输出不会小于 0，所以：

$h_i\ge 0$

对于 $i=1,\dots ,20$，权重、偏置和输入 ID 都是整数，因此如果 $h_i>0$，则至少有：

$h_i\ge 1$

这样就会产生至少一个惩罚项：

$-10^{10}{h}_i\le -10^{10}$

而第 0 个神经元的最大值只有大约 $1.79\times 10^6$，远远小于 $10^{10}$。因此，只要 $h_1,\dots ,h_{20}$ 中有任何一个大于 0，<success> 的分数就一定会低于 <fail>。

所以必须满足：

$h_1=h_2=\cdots =h_{20}=0$

根据 ReLU 的定义，这等价于：

$W_i\cdot x+b_i\le 0,i=1,\dots ,20$

当后 20 个神经元全部关闭时：

${\mathrm{logit}}_{success}=h_0-376131.21875$

要让 <success> 的分数超过 <fail> 的 0.4，需要：

$h_0-376131.21875>0.4$

因此：

$h_0>376131.61875$

第 0 个神经元的偏置为：

$b_0=311558.71875$

所以：

$W_0\cdot x+311558.71875>376131.61875$

整理得到：

$W_0\cdot x>64572.9$

因为 $W_0\cdot x$ 是整数，所以：

$W_0\cdot x\ge 64573$

因此，成功条件可以总结为：

$\{\begin{array}{ll}{W}_i\cdot x+b_i\le 0,& i=1,\dots ,20\\ W_0\cdot x\ge 64573& \end{array}$

0x04 求解输入

import numpy as np
from safetensors.numpy import load_file
from z3 import Int, Or, Solver, sat


MODEL_PATH = "./model.safetensors"
CHARSET = "0123456789abcdefghijklmnopqrstuvwxyzABCDEFGHIJKLMNOPQRSTUVWXYZ"


weights = load_file(MODEL_PATH)

dense_w = np.rint(weights["dense.weight"]).astype(int)
dense_b = np.rint(weights["dense.bias"]).astype(int)

x = [Int(f"x{i}") for i in range(16)]

solver = Solver()

for value in x:
    solver.add(value >= 0)
    solver.add(value <= 61)


for i in range(1, 21):
    expression = sum(
        int(dense_w[i, j]) * x[j]
        for j in range(16)
    ) + int(dense_b[i])

    solver.add(expression <= 0)


target_expression = sum(
    int(dense_w[0, j]) * x[j]
    for j in range(16)
)

solver.add(target_expression >= 64573)


result = solver.check()
print("result:", result)

if result == sat:
    model = solver.model()

    solution = [
        model.evaluate(value).as_long()
        for value in x
    ]

    print("input IDs:", solution)

    prompt = "".join(CHARSET[i] for i in solution)
    print("answer:", prompt)

运行结果为：

result: sat
input IDs: [15, 1, 10, 16, 2, 0, 2, 6,
            12, 7, 15, 10, 1, 6, 6, 6]

answer: f1ag2026c7fa1666

冰与火的战歌：Windows内核攻防实战高级班！从零到实战，融合AI与Windows内核攻防全技术栈，打造具备自动化能力的内核开发高手。