ضرب داخلی int8 با پایتون؛ نقطهٔ صفر، بایاس و مرز انباشت صحیح

پیش از تفسیرِ مصرف منابعِ یک مسیر کم‌دقت، باید بدانیم عددهای صحیح چه چیزی را نمایش می‌دهند. ضربِ مستقیمِ کدهای ورودی و وزن، وقتی نقطهٔ صفرِ ورودی جابه‌جا است، می‌تواند حتی علامت پاسخ را اشتباه کند. این درس یک ضرب داخلیِ کوچک را از کدهای ازقبل‌داده‌شده تا انباشتِ صحیح و بازسازیِ کسری دنبال می‌کند. مدل، دادهٔ واقعی، برد نهفته و زمان‌سنج در آزمایش حضور ندارند.

۱. کد صحیح را از مقدار بازسازی‌شده جدا کنیم

قراردادِ بازسازیِ ورودی چنین است: ابتدا نقطهٔ صفر را از کد کم و سپس در مقیاس ضرب می‌کنیم. بنابراین کدِ مساویِ نقطهٔ صفر، مقدارِ واقعیِ صفر دارد؛ لازم نیست خودِ کد صفر باشد. مشخصات هشت‌بیتی LiteRT این نمایش را تعریف می‌کند. اینجا «واقعی» یعنی مقدارِ بازسازی‌شده طبق قرارداد، نه اندازه‌گیریِ فیزیکی یا ورودیِ اصلیِ پیش از کوانتیزه‌سازی.

ورودیِ تألیفی، کدهای دو، شش و منفی دو، با نقطهٔ صفرِ منفی دو و مقیاسِ یک‌هشتم است. پس مقدارهای بازسازی‌شده یک‌دوم، یک و صفرند. وزن‌ها سه، منفی یک و دو، با نقطهٔ صفرِ صفر و مقیاسِ یک‌چهارم‌اند؛ مقدارهایشان سه‌چهارم، منفی یک‌چهارم و یک‌دوم می‌شوند. همهٔ کمیت‌ها در این مثال بی‌واحدند و معنای ولتاژ یا احتمال ندارند.

هر دو بردار tuple، هم‌طول و دارای یک تا شانزده عضو هستند. کد ورودی int دقیقِ منفی ۱۲۸ تا ۱۲۷ و کد وزن منفی ۱۲۷ تا ۱۲۷ است؛ bool و شناور پذیرفته نیستند. نقطهٔ صفرِ ورودی نیز در بازهٔ کدِ ورودی قرار می‌گیرد. برای وزن، فقط صفرِ صحیح پذیرفته می‌شود؛ منفی ۱۲۸ را هم وارد قراردادِ وزنِ متقارن نمی‌کنیم.

دو مقیاس باید Fraction دقیق، مثبت، حداکثر شانزده و دارای مخرجِ حداکثر ۱۰۲۴ باشند. این کران‌ها انتخابِ تمرین‌اند، نه محدودیتِ همهٔ چارچوب‌ها. کد هیچ مقیاسی را از داده تخمین نمی‌زند؛ ورودی را گرد یا اشباع نمی‌کند و float را بی‌صدا به کسر تبدیل نمی‌کند. مسئله از بعدِ انتخابِ کدها و پارامترها آغاز می‌شود.

۲. ضرب داخلی را پس از کم‌کردن نقطهٔ صفر بسازیم

با وزنِ دارای نقطهٔ صفرِ صفر، جمعِ صحیح برابر مجموعِ حاصل‌ضربِ «کد ورودی منهای نقطهٔ صفرِ ورودی» در «کد وزن» است. در نمونه، ورودیِ مرکز‌شده چهار، هشت و صفر می‌شود. حاصل‌ضرب‌ها دوازده، منفی هشت و صفرند؛ جمعِ صحیح چهار است. مقدارِ مرکز‌شده لازم نیست خودش در بازهٔ int8 بماند؛ برای آن، کدِ ورودی را دوباره محدود نمی‌کنیم.

اگر نقطهٔ صفر را فراموش کنیم، ضربِ خامِ دو در سه، شش در منفی یک و منفی دو در دو، جمعِ منفی چهار می‌دهد. این اختلاف را با افزایش تعداد بیتِ انباشتگر برطرف نمی‌کنیم؛ فرمولِ ورودی غلط است. نوشتنِ شاهدِ دستی با پاسخِ متفاوت کمک می‌کند برنامه‌ای که فقط خروجیِ ظاهراً کوچک دارد، بی‌دلیل درست تلقی نشود.

تعریف DequantizeLinear در ONNX نیز کم‌کردن نقطهٔ صفر و اعمال مقیاس را روشن می‌کند. این منبع برای تفسیرِ کد است؛ عملگرِ ONNX یا مبدلِ مدل را اجرا نکرده‌ایم. مسیرِ این تمرین یک خروجی دارد و یک مقیاسِ وزن برای همان خروجی می‌گیرد؛ چند خروجی و آرایهٔ مقیاسِ محورهای مختلف را پیاده‌سازی نمی‌کند.

۳. بایاس و مرز انباشت سی‌ودوبیتی را روشن کنیم

بایاسِ صحیح در واحدِ انباشتگر تعریف می‌شود. هر واحدِ آن پس از بازسازی برابر حاصل‌ضربِ مقیاسِ ورودی و وزن، یعنی یک‌سی‌ودوم است. پس بایاسِ سه، سه‌سی‌ودومِ بازسازی‌شده اضافه می‌کند؛ سه واحدِ کامل به خروجی اضافه نمی‌کند. در مشخصاتِ Fully Connected در LiteRT، مقیاسِ بایاس از همین حاصل‌ضرب می‌آید؛ بایاسِ این درس تألیفی و ازقبل‌داده‌شده است.

چهار به‌علاوهٔ سه، انباشتِ هفت می‌دهد و بازسازیِ خروجی هفت‌سی‌ودوم است. در مسیرِ غلطِ بدون اصلاح صفر، منفی چهار به‌علاوهٔ سه، منفی یک و خروجیِ منفی یک‌سی‌ودوم می‌شود. این خروجی هنوز عددِ صحیحِ هشت‌بیتیِ تازه نیست. مقیاس و نقطهٔ صفرِ خروجی، گردکردنِ دوباره، محدودسازی، ReLU یا هر تابع فعال‌سازی در مسئله وجود ندارند.

بایاس باید int دقیق در بازهٔ منفی ۲۱۴۷۴۸۳۶۴۸ تا مثبت ۲۱۴۷۴۸۳۶۴۷ باشد. جمعِ نهایی نیز در همین بازه بررسی می‌شود؛ خروج از آن OverflowError می‌دهد و به انتها محدود یا با پیچیدنِ بیت‌ها جایگزین نمی‌شود. دو انتهای بازه پذیرفته‌اند؛ تفاوتِ خطایِ «بایاس نامعتبر» با «جمع نهایی خارج بازه» در کد صریح است.

در این دامنه، قدرمطلقِ هر ورودیِ مرکز‌شده حداکثر ۲۵۵ و وزن حداکثر ۱۲۷ است. با شانزده عضو، قدرمطلقِ مجموعِ حاصل‌ضرب‌ها از ۵۱۸۱۶۰ بیشتر نمی‌شود؛ بایاسِ نزدیکِ انتهای int32 همچنان می‌تواند جمعِ نهایی را خارج کند. پایتون با صحیحِ خودش محاسبه می‌کند و سپس بازه را می‌سنجد؛ رفتارِ سرریز، ترتیبِ انباشت یا اشباعِ هیچ پردازنده‌ای شبیه‌سازی نشده است.

۴. کد را با مسیر کسریِ مستقل مقایسه کنیم

فایل int8_affine_dot.py با Python 3.14.5 و کتابخانهٔ استاندارد اجرا شده است. در مسیرِ اصلی، نخست جمعِ صحیح و بایاس محاسبه و بررسی می‌شوند؛ سپس مقیاس‌ها اعمال می‌شوند. مرجع مستقل، ورودی‌ها و وزن‌ها را جداگانه به کسر بازسازی و حاصل‌ضرب‌های کسری را جمع می‌کند؛ بایاسِ بازسازی‌شده را در پایان جدا می‌افزاید.

"""Already-coded integer dot, checked accumulator, exact rational reconstruction."""
from fractions import Fraction
from itertools import product
import json
import platform

INT32_MIN = -(2**31)
INT32_MAX = 2**31 - 1


def affine_dot(qx, qw, zx, sx, sw, bias=0, zw=0):
    for vector, low, high in ((qx, -128, 127), (qw, -127, 127)):
        if type(vector) is not tuple or not 1 <= len(vector) <= 16:
            raise ValueError("vectors must be tuples with 1..16 codes")
        if any(type(v) is not int or not low <= v <= high for v in vector):
            raise ValueError("invalid code type or range")
    if len(qx) != len(qw):
        raise ValueError("input and weight lengths must agree")
    if type(zx) is not int or not -128 <= zx <= 127:
        raise ValueError("input zero point must be an int8 code")
    if type(zw) is not int or zw != 0:
        raise ValueError("symmetric weight zero point must be actual int zero")
    for scale in (sx, sw):
        if type(scale) is not Fraction or not 0 < scale <= 16 or scale.denominator > 1024:
            raise ValueError("scale must be a positive Fraction <=16, denominator<=1024")
    if type(bias) is not int or not INT32_MIN <= bias <= INT32_MAX:
        raise ValueError("bias must be an actual int in the signed int32 range")
    dot = sum((x - zx) * w for x, w in zip(qx, qw))
    accumulator = dot + bias
    if not INT32_MIN <= accumulator <= INT32_MAX:
        raise OverflowError("final accumulator is outside the signed int32 range")
    return {"centered_dot": dot, "accumulator": accumulator,
            "real_output": Fraction(accumulator) * sx * sw}


def dequantized_oracle(qx, qw, zx, sx, sw, bias):
    # Expand each real input/weight before multiplying, no integer-dot helper.
    inputs = tuple(sx * x - sx * zx for x in qx)
    weights = tuple(sw * w for w in qw)
    answer = Fraction(0)
    for x, w in zip(inputs, weights):
        answer += x * w
    return answer + Fraction(bias) * sx * sw


def raises(expected, call):
    try:
        call()
    except expected:
        return True
    return False


def rational(value):
    return {"numerator": value.numerator, "denominator": value.denominator}


def main():
    qx, qw = (2, 6, -2), (3, -1, 2)
    sx, sw, zx, bias = Fraction(1, 8), Fraction(1, 4), -2, 3
    answer = affine_dot(qx, qw, zx, sx, sw, bias)
    raw_dot = sum(x * w for x, w in zip(qx, qw))
    wrong_output = Fraction(raw_dot + bias) * sx * sw
    checks = {}
    checks["hand_centered_dot_and_bias_accumulator"] = (
        answer["centered_dot"] == 4 and answer["accumulator"] == 7)
    checks["hand_exact_real_output_and_separate_fraction_oracle"] = (
        answer["real_output"] == Fraction(7, 32) ==
        dequantized_oracle(qx, qw, zx, sx, sw, bias))
    checks["omitting_input_zero_point_gives_negative_wrong_witness"] = (
        raw_dot == -4 and wrong_output == Fraction(-1, 32) and
        wrong_output != answer["real_output"])
    checks["input_codes_equal_zero_point_leave_only_bias"] = (
        affine_dot((-2, -2, -2), qw, zx, sx, sw, bias)["real_output"] == Fraction(3, 32))
    checks["zero_weights_and_zero_bias_reconstruct_zero"] = (
        affine_dot(qx, (0, 0, 0), zx, sx, sw)["real_output"] == 0)
    checks["paired_permutation_and_weight_sign_change"] = (
        affine_dot(qx[::-1], qw[::-1], zx, sx, sw, bias) == answer and
        affine_dot(qx, tuple(-w for w in qw), zx, sx, sw)["centered_dot"] == -4)
    checks["code_and_zero_point_common_shift_preserves_real_inputs"] = (
        affine_dot(tuple(x + 5 for x in qx), qw, zx + 5, sx, sw, bias) == answer)
    checks["scale_change_preserves_integer_sum_and_scales_real_output"] = (
        affine_dot(qx, qw, zx, sx * 2, sw, bias)["accumulator"] == 7 and
        affine_dot(qx, qw, zx, sx * 2, sw, bias)["real_output"] == Fraction(7, 16))
    cases, all_equal = 0, True
    for xs in product((-2, 0, 3), repeat=2):
        for ws in product((-3, 0, 2), repeat=2):
            for zero in (-2, 0, 2):
                for b in (-3, 0, 5):
                    actual = affine_dot(xs, ws, zero, sx, sw, b)["real_output"]
                    expected = dequantized_oracle(xs, ws, zero, sx, sw, b)
                    all_equal = all_equal and actual == expected
                    cases += 1
    checks["all_729_two_element_cases_match_dequantized_fraction_oracle_one_group"] = (
        all_equal and cases == 729)
    checks["int32_both_endpoints_accepted_and_one_step_beyond_rejected"] = (
        affine_dot((0,), (0,), 0, sx, sw, INT32_MIN)["accumulator"] == INT32_MIN and
        affine_dot((0,), (0,), 0, sx, sw, INT32_MAX)["accumulator"] == INT32_MAX and
        raises(OverflowError, lambda: affine_dot((1,), (1,), 0, sx, sw, INT32_MAX)) and
        raises(OverflowError, lambda: affine_dot((-1,), (1,), 0, sx, sw, INT32_MIN)))
    checks["bounded_dot_extremes_and_length16_fit_before_bias"] = (
        affine_dot((127,) * 16, (127,) * 16, -128, sx, sw)["centered_dot"] == 518160 and
        affine_dot((-128,) * 16, (127,) * 16, 127, sx, sw)["centered_dot"] == -518160)
    checks["reject_vector_type_length_and_code_range"] = all(
        raises(ValueError, lambda x=x,w=w: affine_dot(x, w, 0, sx, sw))
        for x,w in (([], (1,)), ((), ()), ((1,) * 17, (1,) * 17), ((1,), (1, 2)),
                    ((True,), (1,)), ((1.0,), (1,)), ((-129,), (1,)), ((128,), (1,)),
                    ((1,), (-128,)), ((1,), (128,)), ((1,), (False,))))
    checks["reject_zero_point_type_range_or_asymmetric_weights"] = (
        all(raises(ValueError, lambda z=z: affine_dot((1,), (1,), z, sx, sw))
            for z in (True, 0.0, -129, 128, 10**400)) and
        all(raises(ValueError, lambda z=z: affine_dot((1,), (1,), 0, sx, sw, zw=z))
            for z in (True, 0.0, -1, 1)))
    checks["reject_invalid_scale_type_sign_bounds_and_denominator"] = all(
        raises(ValueError, lambda scale=scale: affine_dot(qx, qw, zx, scale, sw)) and
        raises(ValueError, lambda scale=scale: affine_dot(qx, qw, zx, sx, scale))
        for scale in (True, 1, 0.125, Fraction(0), Fraction(-1), Fraction(17), Fraction(1, 1025)))
    checks["reject_bias_type_and_outside_int32_without_clamping"] = all(
        raises(ValueError, lambda b=b: affine_dot(qx, qw, zx, sx, sw, b))
        for b in (True, 3.0, Fraction(3), INT32_MIN - 1, INT32_MAX + 1, 10**400))
    checks["scale_endpoints_single_element_and_no_input_mutation"] = (
        affine_dot((127,), (127,), -128, Fraction(1, 1024), Fraction(16))["real_output"] ==
        Fraction(32385, 64) and qx == (2, 6, -2) and qw == (3, -1, 2))
    assert all(type(v) is bool and v for v in checks.values())
    print(json.dumps({
        "python": platform.python_version(),
        "dependencies": {"standard_library_only": True, "litert_executed": False,
                         "tensorflow_executed": False, "onnx_executed": False},
        "input_codes": qx, "weight_codes": qw, "input_zero_point": zx, "weight_zero_point": 0,
        "input_scale": rational(sx), "weight_scale": rational(sw), "bias_integer": bias,
        "bias_real": rational(Fraction(bias) * sx * sw),
        "centered_inputs": tuple(x - zx for x in qx),
        "centered_dot": answer["centered_dot"], "accumulator": answer["accumulator"],
        "real_output": rational(answer["real_output"]),
        "wrong_omitted_zero_point": {"raw_dot":raw_dot,"accumulator":raw_dot+bias,
                                     "real_output":rational(wrong_output)},
        "signed_int32_range": [INT32_MIN, INT32_MAX],
        "absolute_centered_dot_bound": 16 * 255 * 127,
        "independent_oracle": {"two_element_cases":cases,"all_equal":all_equal},
        "checks":checks,
        "limitations":["Input codes and scales are supplied, not learned or quantized here.",
                       "Python ints plus final range rejection do not emulate hardware overflow.",
                       "No output requantization, activation, model, timing, memory-byte or quality result."]
    },ensure_ascii=False,indent=2))


if __name__ == "__main__":
    main()

شانزده گروهِ نام‌دار، مقدار بولیِ درست داده‌اند. ۷۲۹ ترکیبِ دوبعدی از کدهای کوچک، نقطهٔ صفر و بایاس، در یک گروه با مرجعِ کسری مقایسه شده‌اند. این مجموعه، همهٔ بردارهای طول شانزده یا همهٔ پارامترهای ممکن نیست. پاسخِ دستی، شاهدِ حذفِ نقطهٔ صفر و دو سویِ مرز انباشت نیز مستقل از آن شبکه بررسی شده‌اند؛ اجرای مجدد، گروهِ تازه نیست.

وقتی همهٔ کدهای ورودی با نقطهٔ صفر برابر باشند، سهمِ ضرب صفر و فقط بایاس باقی می‌ماند. جابه‌جاییِ مشترکِ کدها و نقطهٔ صفر، تا وقتی داخل دامنه بمانند، بازسازی را حفظ می‌کند. ترتیبِ جفت‌های ورودی و وزن نیز اگر با هم عوض شود، پاسخ عوض نمی‌شود. افزایشِ مقیاس، بر جمعِ صحیح اثر ندارد ولی خروجیِ بازسازی‌شده را تغییر می‌دهد؛ این خواص جدا آزموده شده‌اند.

۵. درستی حساب را سرعت یا کیفیت مدل ننامیم

این نتیجه فقط سازگاریِ حسابِ اعلام‌شده را برای داده و بررسی‌های موجود نشان می‌دهد. کدها در شیءهای صحیحِ پایتون ذخیره‌اند؛ آرایهٔ واقعی با نوع int8، دستورِ برداریِ سخت‌افزار یا هستهٔ Fully Connected اجرا نمی‌شود. دقتِ کسری نیز درستیِ انتخابِ مقیاس‌ها، خطایِ کوانتیزه‌سازیِ ورودیِ اصلی یا دقتِ پیش‌بینیِ یک مدل را ثابت نمی‌کند.

{
  "python": "3.14.5",
  "dependencies": {
    "standard_library_only": true,
    "litert_executed": false,
    "tensorflow_executed": false,
    "onnx_executed": false
  },
  "input_codes": [
    2,
    6,
    -2
  ],
  "weight_codes": [
    3,
    -1,
    2
  ],
  "input_zero_point": -2,
  "weight_zero_point": 0,
  "input_scale": {
    "numerator": 1,
    "denominator": 8
  },
  "weight_scale": {
    "numerator": 1,
    "denominator": 4
  },
  "bias_integer": 3,
  "bias_real": {
    "numerator": 3,
    "denominator": 32
  },
  "centered_inputs": [
    4,
    8,
    0
  ],
  "centered_dot": 4,
  "accumulator": 7,
  "real_output": {
    "numerator": 7,
    "denominator": 32
  },
  "wrong_omitted_zero_point": {
    "raw_dot": -4,
    "accumulator": -1,
    "real_output": {
      "numerator": -1,
      "denominator": 32
    }
  },
  "signed_int32_range": [
    -2147483648,
    2147483647
  ],
  "absolute_centered_dot_bound": 518160,
  "independent_oracle": {
    "two_element_cases": 729,
    "all_equal": true
  },
  "checks": {
    "hand_centered_dot_and_bias_accumulator": true,
    "hand_exact_real_output_and_separate_fraction_oracle": true,
    "omitting_input_zero_point_gives_negative_wrong_witness": true,
    "input_codes_equal_zero_point_leave_only_bias": true,
    "zero_weights_and_zero_bias_reconstruct_zero": true,
    "paired_permutation_and_weight_sign_change": true,
    "code_and_zero_point_common_shift_preserves_real_inputs": true,
    "scale_change_preserves_integer_sum_and_scales_real_output": true,
    "all_729_two_element_cases_match_dequantized_fraction_oracle_one_group": true,
    "int32_both_endpoints_accepted_and_one_step_beyond_rejected": true,
    "bounded_dot_extremes_and_length16_fit_before_bias": true,
    "reject_vector_type_length_and_code_range": true,
    "reject_zero_point_type_range_or_asymmetric_weights": true,
    "reject_invalid_scale_type_sign_bounds_and_denominator": true,
    "reject_bias_type_and_outside_int32_without_clamping": true,
    "scale_endpoints_single_element_and_no_input_mutation": true
  },
  "limitations": [
    "Input codes and scales are supplied, not learned or quantized here.",
    "Python ints plus final range rejection do not emulate hardware overflow.",
    "No output requantization, activation, model, timing, memory-byte or quality result."
  ]
}

بودجهٔ بافرهای سامانهٔ نهفته دربارهٔ اقلام و فرضِ حافظه است؛ آن حساب با بررسیِ معنای کدهای صحیح کامل‌تر می‌شود. راهنمای هزینه و تأخیر استقرار نیز سنجشِ سامانه را در دامنهٔ گسترده‌تر مطرح می‌کند. در این درس هیچ کاهشِ RAM، مصرف انرژی، زمان اجرا یا حفظ کیفیتِ مدل اندازه‌گیری نشده است.

منابع در ۲۵ مهر ۱۴۰۵ خوانده شدند. صفحهٔ LiteRT آخرین به‌روزرسانی را ۲۸ مهٔ ۲۰۲۶ نشان می‌دهد؛ این تاریخِ انتشارِ اولیه نیست. مستنداتِ ONNX نسخهٔ 1.24.0 و نسخهٔ عملگرِ خوانده‌شده ۲۸ است؛ بسته اجرا نشده و تاریخِ انتشارِ همان صفحه معلوم نیست. آموزشِ حاضر خبر تازه یا گواهِ انطباقِ بیتیِ چارچوب‌ها نیست.

پرسش اول: چرا کدِ منفی دو، سهمِ صفر در ضرب دارد؟ پاسخ: نقطهٔ صفرِ ورودی نیز منفی دو است؛ تفاضل صفر می‌شود و مقدارِ بازسازی‌شده صفر است، هرچند خودِ کد صفر نیست.

پرسش دوم: بایاسِ سه چه مقداری به خروجی می‌افزاید؟ پاسخ: سه ضرب‌در یک‌هشتم ضرب‌در یک‌چهارم، یعنی سه‌سی‌ودوم؛ جمعِ نهایی هفت‌سی‌ودوم می‌شود.

پرسش سوم: بیشینهٔ int32 به‌علاوهٔ یک پذیرفته می‌شود؟ پاسخ: خیر؛ جمعِ نهایی یک واحد از حد بیشتر است و OverflowError می‌دهد. پیچیدن یا اشباع، سیاستِ این تابع نیست.

پرسش چهارم: آیا توافقِ مرجع، اجرای سریعِ مدل روی برد را ثابت می‌کند؟ پاسخ: خیر؛ نه مدل و بردی اجرا شده‌اند و نه زمان، حافظهٔ هدف و دقتِ پیش‌بینی سنجیده شده‌اند. آن‌ها آزمایش و قراردادِ جدا می‌خواهند.

منابع و مطالعهٔ بیشتر

• LiteRT؛ نمایش آفینِ کد، وزن متقارن و مقیاس بایاسِ Fully Connected
• ONNX 1.24؛ تعریف DequantizeLinear نسخهٔ عملگر ۲۸

بررسی منابع: ۲۵ مهر ۱۴۰۵. تحلیل‌ها و پیشنهادهای اجرایی، جمع‌بندی نویسنده‌اند.