Финансы, биллинг и риск
Расчёты, которые не портятся молча: остаток округления виден и не теряется, баланс сходится. Для задач, где неверное число стоит денег и проходит аудит.
Компенсированная арифметика на Python
Balansis
В активной разработкеОткрытая библиотека для устойчивых численных вычислений на компенсированной арифметике: потеря точности, деление на ноль и переполнение не портят расчёт молча, а становятся видимым состоянием. Алгебра модели доказана на Lean 4, код на PyPI (1.1.0, AGPL-3.0 или коммерческая лицензия).
Проблема
Обычная арифметика с плавающей точкой молча теряет значащие разряды, когда складывает величины разного масштаба (catastrophic cancellation), и выдаёт nan или inf при переполнении. Сигнала об ошибке нет. Финансовый расчёт, инженерная симуляция или нормализация в машинном обучении дают правдоподобное, но неверное число, и оно уходит дальше по конвейеру.
Почему обычные решения не справляются
Наивная сумма отбрасывает остаток округления без следа. Приёмы компенсации известны давно, но обычно живут в отдельных функциях: без типов, без явных состояний для особых случаев и без формальной проверки. Там, где правильность расчёта нужно показать проверяющему (биллинг, риск, регулируемые расчёты), этого мало.
Как это работает
Каждое сложение сохраняет свой остаток округления и переносит его дальше, а у результата есть тип. Деление на ноль становится явным состоянием: вы выбираете политику, и событие записывается в журнал. В основе лежит экспериментальная вычислительная модель (ACT). Библиотеку мы сравниваем с наивной суммой и не утверждаем, что она точнее других методов компенсации: если нужна только точная сумма, стандартная math.fsum справится так же точно и быстрее. Код открыт. Алгебра модели доказана на Lean 4 над вещественными числами, поведение float64 формально не доказано.
Демо
Технологии
- Python
- Lean 4
- NumPy
- PyPI
- mypy strict
Где это применимо
Инженерные симуляции и нормализация в ML
Сложение величин разного масштаба без потери разрядов и softmax, который не переполняется на больших логитах: вероятности вместо nan.
Регулируемые расчёты
Алгебра модели доказана на Lean 4, и эти доказательства можно предъявить проверяющему. Поведение float64 они не покрывают.
Чем это подтверждается
153 теоремы Lean 4 о модели, без пропусков
Проект доказательств собирается без единого sorry или admit (так в Lean помечают недоказанное). Доказана алгебра модели над вещественными числами, поведение float64 не формализовано. Подсчёт на 05.10.2026.
Как повторить: lake build + grep -r "sorry\|admit" formal/
Потеря разрядов: наивная сумма даёт 93, компенсированная 3333
На задокументированном сценарии наивная сумма float даёт 93, что неверно, а компенсированная 3333, как и эталон на Decimal. Сравнение идёт с наивной суммой; с другими методами компенсации мы библиотеку не сравниваем.
Как повторить: pytest tests/test_documented_scenarios.py
Softmax без переполнения: наивный даёт nan, библиотека даёт вероятности
На больших логитах наивный softmax выдаёт nan, а компенсированный возвращает корректные вероятности с суммой 1.
Как повторить: pytest tests/test_documented_scenarios.py
Тесты: 870 прошли, 0 упали
Набор тестов разрабатываемой версии проходит без падений на чистом Python (на 05.10.2026). Покрытие строк 76 % при собственном пороге проекта 80 %.
Как повторить: pytest
Код открыт, поэтому всё, что выше, можно проверить в репозитории. Открыть код ↗
Интеграция
Библиотека на Python, ставится из PyPI. Встраивается в расчётный слой вместо наивной арифметики там, где потеря точности недопустима.
Посчитать на своих цифрах
Калькулятор AVA считает, окупится ли автоматизация процесса, на ваших цифрах, без формы и без нашей цены. Если не окупится, он так и скажет.
Посчитать окупаемостьРазберём вашу задачу
Опишите задачу своими словами. Если она не решается или не окупится, скажем об этом до начала работ.