Computeralgebrasysteme sind für mathematische Forschung äußerst hilfreich, doch unerwartete Fehler in der Software können die Forschung manchmal erheblich beeinträchtigen. Als Beispiel zeigen die Autoren, wie sie einen Fehler in Mathematica bei der Berechnung von Determinanten ganzzahliger Matrizen entdeckten: Das System berechnete nicht nur die Determinante falsch, sondern lieferte auch bei zweimaliger Berechnung derselben Determinante unterschiedliche Ergebnisse.
Bei der Untersuchung der Casorati-Determinante orthogonaler Polynome:
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}$$ Durch die Verwendung von Ganzzahlen zur Konstruktion aller Beispiele, um Gleitkommafehler zu vermeiden, stellten die Autoren fest, dass Mathematica und Maple unterschiedliche Ergebnisse lieferten. ### Fehlerisolationsmethode Um das Berechnungsproblem zu isolieren, entwickelten die Autoren die folgende Methode zur Erzeugung von Matrizen, die den Fehler auslösen: 1. **Erzeugung der Basismatrix**: ```mathematica basicMatrix = Table[Table[RandomInteger[{-99, 99}], {i, 1, 14}], {j, 1, 14}] ``` 2. **Erstellung großer Ganzzahlen**: ```mathematica 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. **Hinzufügung zufälliger Störungen**: ```mathematica smallMatrix = Table[Table[RandomInteger[{-999, 999}], {i, 1, 14}], {j, 1, 14}] ``` 4. **Konstruktion der endgültigen Matrix**: ```mathematica bigMatrix = basicMatrix.powersMatrix + smallMatrix ``` ### Fehlerverifikation Durch mehrfache Berechnung der Determinante derselben Matrix zur Fehlerverifikation: ```mathematica a = Det[bigMatrix]; b = Det[bigMatrix]; ``` Die Ergebnisse zeigten, dass `a==b` häufig `False` zurückgab. ## Experimentelle Einrichtung ### Testumgebung - **Softwareversionen**: Mathematica 8.0 bis 9.0.1 - **Betriebssysteme**: Mac und Windows - **Vergleichssoftware**: Maple und Sage als Verifikationswerkzeuge ### Testdaten - **Matrixgröße**: 14×14 - **Wertebereich**: Enthält große Ganzzahlen mit etwa 10.000 Ziffern - **Generierungsmethode**: Zufällige Erzeugung der Basismatrix, dann Konstruktion durch Potenzvergrößerung und kleine Störungen ## Experimentelle Ergebnisse ### Hauptergebnisse 1. **Rechenfehler**: Die von Mathematica berechnete Determinante war völlig falsch 2. **Nichtdeterminismus**: Mehrfache Berechnungen derselben Matrix lieferten unterschiedliche Ergebnisse 3. **Versionsabhängigkeit**: Der Fehler trat in den Versionen 8 und 9 auf, die Versionen 6 und 7 schienen nicht betroffen zu sein ### Konkretes Beispiel In einem konkreten Beispiel: - Mathematica erste Berechnung: `N[a] = -3.263388173990166 × 10^9768` - Mathematica zweite Berechnung: `N[b] = -8.158470434975415 × 10^9768` - Korrektes Ergebnis (Maple/Sage): `≈ 1.95124219131987 × 10^9762` ### Fehlermeldung Die Autoren meldeten den Fehler am 7. Oktober 2013 an Wolfram Research (Fall-Nummer: CASE:303438), erhielten eine Bestätigungsantwort, doch das Problem wurde in nachfolgenden Versionen nicht behoben. ## Verwandte Arbeiten 1. **Historische Präzedenzfälle**: Ähnlich dem 1994 von Thomas Nicely entdeckten Pentium-Divisionsfehler 2. **Softwareverifikation**: Erwähnung von Verifikationstechniken für Open-Source-Computeralgebrasysteme 3. **Erfolgreiche Fälle mathematischer Software**: - Beweis des Vier-Farben-Satzes (Appel und Haken) - Beweis der Kepler-Vermutung (Thomas Hales) - Kenzo-Software entdeckte Fehler in veröffentlichten Theoremen ## Schlussfolgerungen und Diskussion ### Hauptschlussfolgerungen 1. **Zuverlässigkeitsprobleme**: Auch bei symbolischen Berechnungen (Ganzzahlarithmetik) können Computeralgebrasysteme Fehler produzieren 2. **Umfang der Auswirkungen**: Fehler bei der Großzahlberechnung beeinflussen nicht nur theoretische Mathematik, sondern auch angewandte Bereiche wie Kryptographie 3. **Systemische Probleme**: Die „Black-Box"-Natur kommerzieller Software macht Fehler schwer vorhersehbar und vermeidbar ### Einschränkungen 1. **Unklare Fehlertrigger-Bedingungen**: Unmöglichkeit, genau vorherzusagen, welche Matrizen den Fehler auslösen 2. **Versionsspezifität**: Der Fehler tritt nur in bestimmten Versionen auf 3. **Plattformabhängigkeit**: Verifikation auf verschiedenen Betriebssystemen erforderlich ### Zukünftige Richtungen 1. Entwicklung besserer Softwareverifikationstechniken 2. Erhöhung der Transparenz kommerzieller Software 3. Etablierung besserer Fehlermeldeungs- und Reparaturmechanismen ## Tiefgreifende Bewertung ### Stärken 1. **Große praktische Bedeutung**: Offenlegung schwerwiegender Fehler in weit verbreiteter mathematischer Software 2. **Wissenschaftliche Methodik**: Verifikation durch mehrere unabhängige Systeme gewährleistet Zuverlässigkeit der Ergebnisse 3. **Hohe Reproduzierbarkeit**: Detaillierte Methoden zur Fehlernachvollziehung bereitgestellt 4. **Klare Darstellung**: Lebendige Präsentation des Fehlerfindungsprozesses vor dem Hintergrund konkreter mathematischer Forschung ### Schwächen 1. **Begrenzte theoretische Analyse**: Keine tiefgehende Analyse der Grundursachen des Fehlers 2. **Mangel an Lösungen**: Hauptsächlich Fehlermeldung, fehlende Methoden zur Prävention oder Erkennung solcher Fehler 3. **Begrenzte Testabdeckung**: Konzentration auf einen spezifischen Berechnungstyp (Determinanten großer ganzzahliger Matrizen) ### Einfluss 1. **Akademischer Wert**: Warnung für Forscher vor Zuverlässigkeitsproblemen bei computergestützten Beweisen 2. **Praktischer Wert**: Wichtige Warnung für Benutzer, die Mathematica für Großzahlberechnungen verwenden 3. **Softwareverbesserung**: Ansporn für Softwareentwickler, solche Fehler ernst zu nehmen und zu beheben ### Anwendungsszenarien Die Ergebnisse dieser Forschung sind anwendbar auf: - Mathematica-Verwendung für Großzahl-Matrixberechnungen in der Forschung - Großzahlarithmetik in der Kryptographie - Mathematische Forschung, die hochpräzise symbolische Berechnungen erfordert - Zuverlässigkeitsbewertung von Computeralgebrasystemen ## Literaturverzeichnis Das Papier zitiert die folgenden wichtigen Werke: 1. Karlin & Szegő (1960/1961) - Originalforschung zu Determinanten orthogonaler Polynome 2. Appel & Haken (1977) - Computergestützter Beweis des Vier-Farben-Problems 3. Hales (2005) - Beweis der Kepler-Vermutung 4. Ciaurri & Varona (2006) - Frühe Forschung zur Zuverlässigkeit von Computerberechnungen --- Obwohl dieses Papier relativ kurz ist, offenbart es ein wichtiges Problem: Selbst scheinbar zuverlässige symbolische Berechnungen können systematische Fehler enthalten. Es erinnert uns daran, dass wir bei der Abhängigkeit von Computern für mathematische Forschung Vorsicht walten lassen müssen, und unterstreicht die Bedeutung von Softwareverifikation und Transparenz.