丑寅同墟·星海抉择 Writeup

模型结构

分词器使用如下 62 个字符，并把字符直接映射为其下标：

0123456789abcdefghijklmnopqrstuvwxyzABCDEFGHIJKLMNOPQRSTUVWXYZ

输入长度固定为 16，较短的输入会在末尾补编号 0。模型没有词嵌入层，16 个字符编号会作为浮点数直接进入两层全连接网络：

z = W1 · x + b1
h = ReLU(z)
logits = W2 · h + b2

其中 x 有 16 维，隐藏层 h 有 21 维，输出层有 64 维。输出编号 62 对应 <success>，编号 63 对应 <fail>。

分析输出层

检查输出层权重可以发现，0 至 61 号普通字符的权重均为 0，偏置均为 -10000。<fail> 的权重也全部为 0，偏置为 0.4。只有 <success> 使用了隐藏层：

W2[62] = [1, -10^10, -10^10, ..., -10^10]
b2[62] = -376131.21875

所以成功类别的分数为：

logit_success = h[0] - 10^10 · (h[1] + ... + h[20]) - 376131.21875

隐藏层第 1 至 20 行的权重、偏置都是整数，输入编号也是整数。一旦这些行中有正数，经过 ReLU 后至少为 1，成功分数就会被减去至少 10^10，不可能成为最大值。因此正确输入必须让 20 个拒绝单元全部关闭：

W1[i] · x + b1[i] <= 0,  i = 1, 2, ..., 20

这 20 行就是模型中保存秘密的主体。进一步观察可见，它们构造了 20 个经过目标点的超平面。令所有拒绝单元恰好位于 ReLU 的分界点，得到整数线性方程组：

W1[1:21] · x = -b1[1:21]

系数矩阵为 20 × 16，秩为 16，因此该方程组在实数范围内也只有一个解。使用整数精确运算求解得到：

x = [15, 1, 10, 16, 2, 0, 2, 6, 12, 7, 15, 10, 1, 6, 6, 6]

代回全部 20 个方程后，左侧都严格等于 0。所有编号也都位于分词器的合法范围内。按字符表还原为：

f1ag2026c7fa1666

其中编号 0 位于字符串中间，对应字符 0。由于它后面仍有非零编号，该位置不是末尾补位。

模型验证

把恢复出的编号送回完整模型后，第 1 至 20 个隐藏单元全部为 0，输出分数为：

logit_success = 0.5
logit_fail    = 0.4

最终最大输出编号为 62，解码结果为 <success>。

Exp

#!/usr/bin/env python3

import sys

import numpy as np
import sympy as sp
from safetensors.numpy import load_file


CHARSET = "0123456789abcdefghijklmnopqrstuvwxyzABCDEFGHIJKLMNOPQRSTUVWXYZ"
SUCCESS_ID = 62


def main():
    if len(sys.argv) != 2:
        raise SystemExit("usage: python exp.py <model.safetensors>")

    state = load_file(sys.argv[1])

    weights = state["dense.weight"][1:]
    biases = state["dense.bias"][1:]
    assert np.array_equal(weights, np.rint(weights))
    assert np.array_equal(biases, np.rint(biases))

    matrix = sp.Matrix(weights.astype(np.int64).tolist())
    target = sp.Matrix((-biases).astype(np.int64).tolist())
    assert matrix.rank() == 16

    solutions = sp.linsolve((matrix, target))
    assert len(solutions) == 1
    exact = next(iter(solutions))
    assert all(value.q == 1 for value in exact)

    ids = np.array([int(value) for value in exact], dtype=np.int64)
    assert np.all((0 <= ids) & (ids < len(CHARSET)))
    assert matrix * sp.Matrix(ids.tolist()) == target

    x = ids.astype(np.float32)
    hidden = np.maximum(
        state["dense.weight"] @ x + state["dense.bias"],
        0.0,
    )
    logits = state["lm_head.weight"] @ hidden + state["lm_head.bias"]
    assert np.all(hidden[1:] == 0)
    assert int(np.argmax(logits)) == SUCCESS_ID

    flag = "".join(CHARSET[index] for index in ids)
    print(flag)


if __name__ == "__main__":
    main()