Balansis 1.1.0 · Python · AGPL-3.0 / коммерческая
Компенсированная арифметика, у которой можно проверить каждое число
Balansis — библиотека для вычислений, где обычная арифметика с плавающей точкой прячет потерю точности вместо того, чтобы её показать. Здесь компенсация возвращается вызывающему коду как значение, деление на ноль — это состояние, а не исключение, а алгебра модели доказана в Lean4. Всё, что ниже, измерено и проверено — с указанием, чем и когда.
Задача, ради которой это существует
Скалярное произведение двух векторов длины 1000. Точный ответ известен: он вычислен в рациональной арифметике и равен -4893576300353906275/9223372036854775808 ≈ -0.530562605606728. Слагаемые при этом порядка 1016, и ответ полностью съедается взаимным уничтожением.
import numpy as np
from balansis.core._eft import dot2
a, b = ... # два вектора по 1000 элементов, ±1e8
float(np.dot(a, b)) # -32
float(dot2(a, b)) # -0.5305626056067283 ← ближайший float64 к точному ответу| Метод | Результат | Верных знаков | Абс. ошибка | Время (min) |
|---|---|---|---|---|
| наивный цикл float64 | -32 | 0.0 | 31.4694 | 37.81 мкс |
| numpy.dot (BLAS) | -32 | 0.0 | 31.4694 | 643.0 нс |
| math.fsum над произведениями точная сумма округлённых произведений — ошибка остаётся | -8.37496948242188 | 0.0 | 7.84441 | 51.89 мкс |
| Balansis dot2 (Ogita–Rump–Oishi) two_product ловит ошибку каждого произведения, math.fsum складывает всё точно | -0.530562605606728 | 16 (предел float64) | 4.478e-17 | 87.65 мкс |
| Balansis numpy_integration.compensated_dot_product публичный numpy-мост, внутри тот же dot2 | -0.530562605606728 | 16 (предел float64) | 4.478e-17 | 87.57 мкс |
math.fsum над произведениями не спасает — каждое произведение уже округлено до того, как его сложили. Это и есть класс задач, для которого компенсированная арифметика придумана. Цена: 136× ко времени относительно np.dot.Что такое ACT простым языком
ACT (Absolute Compensation Theory) — модель, в которой число хранится не одним float, а парой «величина + направление», и вместе с результатом операции возвращается то, что обычно молча выбрасывается.
1. Число — это величина и направление
AbsoluteValue(magnitude, direction): неотрицательная величина и знак отдельно. Ноль в этой модели — не «очень маленькое число», а отдельное состояние ABSOLUTE: его нельзя перепутать с остатком, который просто не поместился в мантиссу.
2. Компенсация — возвращаемое значение, а не побочный эффект
Операции возвращают пару (результат, компенсация). Компенсация — мера того, сколько точности пришлось спасать на этом шаге. Обычный float такой информации не отдаёт: вы получаете ответ и не знаете, был ли он получен без потерь или собран из обломков.
3. Деление — это состояние, а не исключение
ExtendedRatio различает три состояния: finite, infinite (со знаком) и indeterminate. Что с этим делать, выбирает вызывающий код политикой raise / propagate / saturate — а не догадками на месте.
4. Под всем этим — классические error-free transformations
Точность даёт не «магия ACT», а известные алгоритмы: two_sum Кнута, two_product Деккера, dot2 Огиты–Румпа–Оиши, суммирование по Ноймайеру. Balansis не изобретает численный метод заново — он выносит его в API и добавляет к нему типы, семантику и доказательства.
Где выигрывает, а где нет
Сайт про математическую честность не может врать про собственные бенчмарки. Ниже — итог реальных прогонов, включая те, где Balansis проигрывает.
| Задача | Кто выигрывает | Измеренный факт |
|---|---|---|
| Плохо обусловленное скалярное произведение | Balansis | оба метода Balansis дают корректно округлённый до ближайшего float64 ответ; три остальных — 0 верных знаков, включая numpy и math.fsum |
| Деление на ноль как типизированное состояние | Balansis | три состояния и три политики против ZeroDivisionError и тихого nan |
| Сумма ряда со взаимным уничтожением | ничья по точности | math.fsum, встроенный sum() и Balansis дают точный ответ; наивный цикл — 0. Balansis при этом 25× медленнее math.fsum |
| Softmax на переполняющих логитах | ничья со стандартным приёмом | сдвиг на максимум в numpy даёт тот же ответ до последнего бита; выигрыш только против наивной реализации, которая возвращает NaN |
| Бухгалтерский ноль на суммах вроде 12345.67 | Decimal, не Balansis | Ledger приводит Decimal к float на входе и повторяет ошибку float; структурный ноль появляется только там, где и float даёт ноль |
| SVD | numpy | бэкенд numpy_gesdd — это буквально numpy; бэкенд act_jacobi в прогоне оказался и медленнее, и чуть менее точен |
| Сигнал о взаимном уничтожении | это не победа | compensated_add(1e16, −1e16) возвращает 2 при точном ответе 0 — величину в один ULP операнда: это флаг риска, а не восстановленное значение |
| Скорость арифметики на объектах | float | compensated_add медленнее сложения float в 87×; примитив two_sum — только в 5.9× (обе цифры за вычетом накладных питоновского вызова) |
| Алгебра модели | Lean4 | 73 теорем проверены ядром Lean 2026-09-08; вне стандартных аксиом Mathlib не используется ничего |
math.fsum, как замену Decimal в бухгалтерии и как обёртку над numpy в линейной алгебре.Куда дальше
Примеры
Восемь задач с выполненными вычислениями: агрегация, скалярное произведение, softmax, бухгалтерский ноль, деление на ноль, SVD.
Бенчмарки
Точность против наивной арифметики и цена этой точности во времени. Включая случаи, где Balansis проигрывает.
Доказательства
73 теорем Lean4: что именно доказано, на какие аксиомы опирается и что доказательства не покрывают.
Установка
pip install balansis, минимальные зависимости, CLI и первые вызовы API.
Честность
Как повторить каждое число на этой странице и где документация самой библиотеки расходится с прогоном.
Исходники
Репозиторий на GitHub и пакет на PyPI. Лицензия AGPL-3.0-only плюс коммерческая.
Время в таблицах — минимум из серии повторов на разделяемом хосте (Intel Xeon (серверный), 8 vCPU); наименьшее время наименее зашумлено, отношения между методами устойчивы, абсолютные значения — нет. Самый быстрый и самый медленный замер сценария скалярного произведения: 643.0 нс и 87.65 мкс.