Невзгоды математической тройки при использовании систем компьютерной алгебры: можем ли мы доверять?

Основная информация

• ID статьи: 1312.3270
• Название: Misfortunes of a mathematicians' trio using Computer Algebra Systems: Can we trust?
• Авторы: Antonio J. Durán (Universidad de Sevilla), Mario Pérez (Universidad de Zaragoza), Juan L. Varona (Universidad de La Rioja)
• Классификация: cs.SC (Символьные вычисления), cs.MS (Математическое программное обеспечение)
• Дата публикации: 15 октября 2013 г. (препринт arXiv)
• Ссылка на статью: https://arxiv.org/abs/1312.3270

Аннотация

Системы компьютерной алгебры оказывают значительную помощь в математических исследованиях, однако неожиданные ошибки в программном обеспечении иногда серьёзно влияют на результаты исследований. В качестве примера авторы демонстрируют, как они обнаружили ошибку в Mathematica при вычислении определителей целочисленных матриц: программа не только неправильно вычисляла определитель, но и давала различные результаты при двукратном вычислении одного и того же определителя.

Исследовательский контекст и мотивация

1. Решаемая проблема: Авторы обнаружили серьёзные ошибки в Mathematica при вычислении определителей больших целочисленных матриц, включая неправильные результаты вычислений и получение различных результатов для одного и того же вычисления.
2. Важность проблемы:
   • Математики всё больше полагаются на системы компьютерной алгебры при проведении исследований
   • Ошибочные результаты вычислений могут привести к неправильным математическим выводам
   • Вычисления с большими целыми числами имеют важное применение в криптографии и других областях
3. Ограничения существующих методов:
   • Коммерческие системы компьютерной алгебры являются "чёрным ящиком" с непрозрачными алгоритмами
   • Известные ошибки обычно не разглашаются пользователям
   • Сложно применять современные методы верификации программного обеспечения
4. Исследовательская мотивация: При исследовании расширения результатов Карлина и Сегё по ортогональным многочленам авторы обнаружили, что Mathematica и Maple дали различные результаты вычислений, что привело к глубокому анализу и выявлению систематических ошибок в Mathematica.

Основной вклад

1. Обнаружение и сообщение о серьёзной вычислительной ошибке в Mathematica: при вычислении определителей больших целочисленных матриц получаются неправильные результаты
2. Предоставление воспроизводимого метода генерации ошибок: разработана случайная программа для генерации матриц, вызывающих ошибку
3. Выявление недетерминированного характера ошибки: вычисление определителя одной и той же матрицы может дать различные результаты
4. Постановка вопроса о надёжности систем компьютерной алгебры: инициирование важного обсуждения о том, как доверять этим системам

Подробное описание методов

Процесс обнаружения проблемы

При исследовании определителей Казоратти ортогональных многочленов: $\det \begin{pmatrix} P_{f_1}(a_k) & P_{f_1}(a_{k+1}) & \cdots & P_{f_1}(a_{k+l}) \\ P_{f_2}(a_k) & P_{f_2}(a_{k+1}) & \cdots & P_{f_2}(a_{k+l}) \\ \vdots & \vdots & \ddots & \vdots \\ P_{f_l}(a_k) & P_{f_l}(a_{k+1}) & \cdots & P_{f_l}(a_{k+l}) \end{pmatrix}$

Авторы использовали целые числа для всех примеров, чтобы избежать проблем с плавающей точкой, но обнаружили, что Mathematica и Maple дали различные результаты.

Метод изоляции ошибки

Для изоляции вычислительной проблемы авторы разработали следующий метод генерации матриц, вызывающих ошибку:

1. Генерация базовой матрицы:

   basicMatrix = Table[Table[RandomInteger[{-99, 99}], {i, 1, 14}], {j, 1, 14}]
   

2. Создание больших целых чисел:

   powersMatrix = DiagonalMatrix[{10^123, 10^152, 10^185, 10^220, 10^397,
   10^449, 10^503, 10^563, 10^979, 10^1059, 10^1143, 10^1229, 10^1319, 10^1412}]
   

3. Добавление случайных возмущений:

   smallMatrix = Table[Table[RandomInteger[{-999, 999}], {i, 1, 14}], {j, 1, 14}]
   

4. Конструирование итоговой матрицы:

   bigMatrix = basicMatrix.powersMatrix + smallMatrix
   

Верификация ошибки

Путём многократного вычисления определителя одной и той же матрицы авторы верифицировали ошибку:

a = Det[bigMatrix];
b = Det[bigMatrix];

Результаты показали, что a==b часто возвращает False.

Экспериментальная установка

Тестовая среда

• Версии программного обеспечения: Mathematica 8.0 – 9.0.1
• Операционные системы: Mac и Windows
• Программное обеспечение для сравнения: Maple и Sage в качестве инструментов верификации

Тестовые данные

• Размер матриц: 14×14
• Диапазон значений: содержат большие целые числа примерно с 10 000 цифр
• Способ генерации: случайная генерация базовой матрицы с последующим увеличением масштаба через степени и добавлением малых возмущений

Результаты экспериментов

Основные находки

1. Вычислительные ошибки: Mathematica вычисляет полностью неправильные значения определителей
2. Недетерминированность: одна и та же матрица при многократном вычислении даёт различные результаты
3. Зависимость от версии: ошибки появляются в версиях 8 и 9, в версиях 6 и 7 они, похоже, отсутствуют

Конкретный пример

В одном конкретном примере:

• Первое вычисление в Mathematica: N[a] = -3.263388173990166 × 10^9768
• Второе вычисление в Mathematica: N[b] = -8.158470434975415 × 10^9768
• Правильный результат (Maple/Sage): ≈ 1.95124219131987 × 10^9762

Сообщение об ошибке

Авторы сообщили об этой ошибке в Wolfram Research 7 октября 2013 г. (номер случая: CASE:303438), получили подтверждение, однако проблема не была решена в последующих версиях.

Связанные работы

1. Исторические прецеденты: аналогично ошибке деления в процессоре Pentium, обнаруженной Thomas Nicely в 1994 г.
2. Верификация программного обеспечения: упоминаются исследования методов верификации открытых систем компьютерной алгебры
3. Успешные примеры математического программного обеспечения:
   • Доказательство теоремы о четырёх красках (Appel и Haken)
   • Доказательство гипотезы Кеплера (Thomas Hales)
   • Программное обеспечение Kenzo обнаружило ошибки в опубликованных теоремах

Выводы и обсуждение

Основные выводы

1. Проблемы надёжности: даже при символьных вычислениях (целочисленной арифметике) системы компьютерной алгебры могут давать ошибочные результаты
2. Масштаб влияния: ошибки при вычислении больших целых чисел влияют не только на теоретическую математику, но и на прикладные области, такие как криптография
3. Системные проблемы: "чёрный ящик" коммерческого программного обеспечения затрудняет предсказание и предотвращение ошибок

Ограничения

1. Неясные условия срабатывания ошибки: невозможно точно предсказать, какие матрицы вызовут ошибку
2. Специфичность версии: ошибка появляется только в определённых версиях
3. Зависимость от платформы: требуется верификация на различных операционных системах

Будущие направления

1. Разработка более совершенных методов верификации программного обеспечения
2. Повышение прозрачности коммерческого программного обеспечения
3. Установление более совершенных механизмов сообщения об ошибках и их исправления

Глубокая оценка

Преимущества

1. Значительная практическая важность: выявление серьёзных ошибок в широко используемом математическом программном обеспечении
2. Научный метод: верификация через несколько независимых систем обеспечивает надёжность обнаруженных результатов
3. Высокая воспроизводимость: предоставлены подробные методы воспроизведения ошибки
4. Ясное изложение: на фоне конкретного математического исследования живо демонстрируется процесс обнаружения проблемы

Недостатки

1. Ограниченный теоретический анализ: отсутствует глубокий анализ коренных причин возникновения ошибки
2. Отсутствие решений: в основном это сообщение о проблеме, не предлагаются методы предотвращения или обнаружения подобных ошибок
3. Ограниченный диапазон тестирования: сосредоточено в основном на одном типе вычислений (определители больших целочисленных матриц)

Влияние

1. Академическая ценность: напоминает исследователям о надёжности компьютерных доказательств
2. Практическая ценность: важное предупреждение для пользователей, полагающихся на Mathematica при вычислениях с большими целыми числами
3. Улучшение программного обеспечения: побуждает разработчиков обращать внимание на подобные ошибки и их исправление

Применимые сценарии

Результаты этого исследования применимы к:

• Исследованиям, использующим Mathematica для вычисления определителей больших целочисленных матриц
• Криптографическим вычислениям с большими числами
• Математическим исследованиям, требующим высокоточных символьных вычислений
• Оценке надёжности систем компьютерной алгебры

Библиография

В статье цитируются следующие важные работы:

1. Karlin & Szegő (1960/1961) – оригинальное исследование определителей ортогональных многочленов
2. Appel & Haken (1977) – компьютерное доказательство проблемы четырёх красок
3. Hales (2005) – доказательство гипотезы Кеплера
4. Ciaurri & Varona (2006) – ранние исследования надёжности компьютерных вычислений

Хотя эта статья относительно небольшого объёма, она выявляет важную проблему: даже кажущиеся надёжными символьные вычисления могут содержать систематические ошибки. Она напоминает нам о необходимости осторожности при использовании компьютеров в математических исследованиях и подчёркивает важность верификации программного обеспечения и его прозрачности.