Линейка для чисел: как я собрал каталог из 83 форматов с плавающей точкой — и почему он всё время «не сходится»

Любой, кто дебажил несовпадение точности между двумя реализациями нейросети, знает это чувство: один и тот же matmul на двух устройствах даёт разный результат — баг это или просто bf16 так округлил? Инженеры на разных концах конвейера меряют один результат разными линейками. Я собрал одну линейку с точными насечками — машинно-проверяемый каталог из 83 числовых форматов в 13 кластерах. Для каждого: разрядка битов (знак/экспонента/мантисса), смещение, кодирование inf/NaN/субнормалей и единый якорь проверки 0x47C0. Из одного источника истины генерируются Markdown, JSON, Python, Rust, C и RTL для кремния. Главное в проекте — не размер, а честные статус-метки: 51 формат Verified, 12 Historical, 11 Experimental, 9 Open. И отдельная честная ось — граница RTL: где правило e = round((N−1)/φ²) ещё работающее железо (GF16 проверен вплоть до кремния), а где уже гипотеза (GF512/GF1024 — чистая экстраполяция без единой строки Verilog). Парадокс: самая близкая к φ ступень — наименее проверенная. Внутри — лестница зрелости форматов, связь с IEEE P3109 и реальный баг в умножителе, который нашли только потому, что под форматом есть железо Как устроена линейка

https://habr.com/ru/articles/1051010/

#числовые_форматы #floating_point #GoldenFloat #bfloat16 #FP8 #P3109 #RTL #квантизация #машинное_обучение #числа_с_плавающей_точкой

A new piece of research as part of my group's safe and formally verified numerics project that I am really excited about -- The FLoPS framework, which formalizes the upcoming P3109 standard in Lean. Great work by my PhD students: Tung-Che Chang and Sehyeok Park and collaborator Jay Lim from University of California, Riverside.

The upcoming IEEE-P3109 standard for low-precision floating-point arithmetic can become the foundation of future machine learning hardware and software. Unlike the fixed types of IEEE-754, P3109 introduces a parametric framework defined by bitwidth, precision, signedness, and domain. This flexibility results in a vast combinatorial space of formats -- some with as little as one bit of precision -- alongside novel features such as stochastic rounding and saturation arithmetic.

We have formalized the P3109 standard and discovered new interesting properties of foundational algorithms such as Fast2Sum, Sternbenz, and a floating-point splitting ExtractScalar in the context of P3109.

During this process, we discovered some errors in the draft standard and reported it to the working group (I am member of the P3109 working group). They have been fixed.

See the Github repo of our mechanized proofs in Lean: https://github.com/rutgers-apl/flops

See our technical report:
https://arxiv.org/pdf/2602.15965

On a side note, I was convincingly persuaded to explore Lean by Ilya Sergey when I visited NUS in August 2024. Thanks Ilya for making a compelling case for using Lean while Umang Mathur and Abhik Roychoudhury made the visit possible.

#RutgersCS #RAPL #P3109