2025-11-23T21:58:17.757337

Towards Richer Challenge Problems for Scientific Computing Correctness

Sottile, Tekriwal, Sarracino
Correctness in scientific computing (SC) is gaining increasing attention in the formal methods (FM) and programming languages (PL) community. Existing PL/FM verification techniques struggle with the complexities of realistic SC applications. Part of the problem is a lack of a common understanding between the SC and PL/FM communities of machine-verifiable correctness challenges and dimensions of correctness in SC applications. To address this gap, we call for specialized challenge problems to inform the development and evaluation of FM/PL verification techniques for correctness in SC. These specialized challenges are intended to augment existing problems studied by FM/PL researchers for general programs to ensure the needs of SC applications can be met. We propose several dimensions of correctness relevant to scientific computing, and discuss some guidelines and criteria for designing challenge problems to evaluate correctness in scientific computing.
academic

Auf dem Weg zu umfassenderen Herausforderungsproblemen für die Korrektheit des wissenschaftlichen Rechnens

Grundlegende Informationen

  • Papier-ID: 2510.13423
  • Titel: Towards Richer Challenge Problems for Scientific Computing Correctness
  • Autoren: Matthew Sottile, Mohit Tekriwal, John Sarracino (Lawrence Livermore National Laboratory)
  • Klassifizierung: cs.SE cs.MS
  • Veröffentlichungskonferenz: International Workshop on Verification of Scientific Software (VSS 2025), EPTCS 432
  • Papierlink: https://arxiv.org/abs/2510.13423

Zusammenfassung

Die Korrektheitsprobleme des wissenschaftlichen Rechnens (SC) erhalten zunehmende Aufmerksamkeit in den Gemeinschaften der formalen Methoden (FM) und Programmiersprachen (PL). Bestehende PL/FM-Verifizierungstechniken haben Schwierigkeiten, mit der Komplexität realer Anwendungen des wissenschaftlichen Rechnens umzugehen. Ein Teil des Problems liegt in der fehlenden gemeinsamen Verständigung zwischen der SC- und der PL/FM-Gemeinschaft über maschinenverifizierbare Korrektheitsprobleme und Korrektheitsdimensionen in SC-Anwendungen. Um diese Lücke zu schließen, fordern die Autoren die Etablierung spezialisierter Herausforderungsprobleme auf, um die Entwicklung und Bewertung von FM/PL-Verifizierungstechniken im SC zu leiten. Diese spezialisierten Herausforderungen sollen die bestehenden allgemeinen Programmprobleme, die von FM/PL-Forschern untersucht werden, erweitern und sicherstellen, dass die Anforderungen von SC-Anwendungen erfüllt werden können.

Forschungshintergrund und Motivation

Zu lösende Probleme

  1. Verständnislücke zwischen Gemeinschaften: Mangelndes gemeinsames Verständnis zwischen der Gemeinschaft des wissenschaftlichen Rechnens und der Gemeinschaft der formalen Methoden/Programmiersprachen bezüglich Korrektheitsprobleme
  2. Einschränkungen bestehender Verifizierungstechniken: Bestehende PL/FM-Verifizierungstechniken können die Komplexität realer SC-Anwendungen schwer bewältigen
  3. Unzureichende Herausforderungsprobleme: Mangel an standardisierten Herausforderungsproblemsammlungen, die speziell auf die Korrektheit des wissenschaftlichen Rechnens ausgerichtet sind

Bedeutung des Problems

Anwendungen des wissenschaftlichen Rechnens umfassen komplexe numerische Berechnungen, Parallelverarbeitung, physikalische Modellierung und mehrere andere Ebenen, wobei die Korrektheit direkt die Zuverlässigkeit der Ergebnisse wissenschaftlicher Forschung beeinflusst. Traditionelle Softwareverifizierungsmethoden können die spezifischen Korrektheitsanforderungen des wissenschaftlichen Rechnens oft nicht angemessen abdecken.

Einschränkungen bestehender Ansätze

  • Bestehende formale Verifizierungsherausforderungsprobleme konzentrieren sich hauptsächlich auf allgemeine Programme und fehlt die Komplexität, die für das wissenschaftliche Rechnen spezifisch ist
  • Obwohl die numerische Verifizierungsgemeinschaft verwandte Arbeiten hat, fehlt ein einheitlicher Satz von Herausforderungsproblemen
  • Bestehende Benchmark-Suites konzentrieren sich hauptsächlich auf Leistung statt auf Korrektheit

Forschungsmotivation

Inspiriert durch die erfolgreiche Erfahrung von Leistungs-Benchmark-Suites im Bereich des Hochleistungsrechnens (wie NAS Parallel Benchmarks, Mantevo usw.), wird ein ähnliches Herausforderungsproblem-Framework für die Korrektheit des wissenschaftlichen Rechnens etabliert.

Kernbeiträge

  1. Vorschlag von sechs Dimensionen der Korrektheit des wissenschaftlichen Rechnens: Numerik, Datenstrukturen, Domänenmodellierungsstrukturen, Differentialgleichungen, Nebenläufigkeit und Parallelismus, Approximationsschemata
  2. Identifikation von Schlüsselfallen beim Design von Herausforderungsproblemen: Überspecialisierung, „Spielzeug"-Probleme, Vernachlässigung der Besonderheiten des wissenschaftlichen Rechnens usw.
  3. Etablierung des Unterschieds zwischen Herausforderungsproblemen und Benchmark-Tests: Herausforderungsprobleme definieren Ziele und Bewertungskriterien, Benchmark-Tests liefern objektive Messungen
  4. Bereitstellung von Designrichtlinien: Berücksichtigung von Unsicherheit, Trennung von Mathematik und Implementierung, Zulassung ungeprüfter Annahmen usw.

Methodische Details

Aufgabendefinition

Dieses Papier ist ein Positionspapier, das darauf abzielt, ein umfassendes Herausforderungsproblem-Framework für die Korrektheit des wissenschaftlichen Rechnens zu etablieren, anstatt konkrete technische Methoden vorzuschlagen.

Framework-Design

Klassifizierung der Korrektheitsdimensionen

Die Autoren unterteilen die Korrektheit des wissenschaftlichen Rechnens in drei Abstraktionsebenen:

  • Niedrige Ebene: Numerische Berechnungen, traditionelle Datenstrukturen
  • Mittlere Ebene: Modellspezifische Datenstrukturen und Berechnungen
  • Hohe Ebene: Mathematische Abstraktionen, Invarianten physikalischer Systeme

Sechs Kerndimensionen

  1. Numerik (Numerics)
    • Mathematische Operationen und ihre Entsprechung in Hardware/Software-Implementierung
    • Präzisionsprobleme bei Gleitkommaoperationen
    • Herausforderungen bei Algorithmen mit gemischter Präzision
  2. Datenstrukturen (Data Structures)
    • Korrektheit standardisierter Datenstrukturen
    • Strukturtransformationen durch Leistungsoptimierung (z. B. SOA zu AOS-Konvertierung)
    • Garantie semantischer Äquivalenz
  3. Domänenmodellierungsstrukturen (Domain-modeling Structures)
    • Komplexe Datenstrukturen wie Gitter, Graphen
    • Erfüllung physikalischer Systembeschränkungen
    • Hochrangige Invarianten wie Erhaltungssätze
  4. Differentialgleichungen (Differential Equations)
    • Konsistenz zwischen PDEs und physikalischer Modellierung
    • Numerische Stabilität, Kompatibilität von Randbedingungen
    • Wohlgestelltheit (well-posedness)
  5. Nebenläufigkeit und Parallelismus (Concurrency and Parallelism)
    • Kombination mehrerer paralleler Programmiermodelle
    • Gemeinsamer Speicher, Vektorisierung, verteilter Speicher-Parallelismus
    • Ausgleich zwischen Leistung und Korrektheit
  6. Approximationsschemata (Approximation Schemes)
    • Algorithmische Heuristiken
    • Interpolationsmethoden
    • Unterscheidung von numerischen Methoden

Technische Innovationspunkte

  1. Mehrstufige Abstraktionsintegration: Erste systematische Rahmung von Korrektheitsproblemen des wissenschaftlichen Rechnens von niedrigen Implementierungsdetails bis zu hohen physikalischen Beschränkungen
  2. Brückenfunktion zwischen Gemeinschaften: Etablierung einer gemeinsamen Sprache zwischen der Gemeinschaft der formalen Methoden und der Gemeinschaft des wissenschaftlichen Rechnens
  3. Praxisorientierung: Vermeidung von Übertheoretialisierung, Fokus auf praktische Korrektheitsanforderungen in realen Anwendungen

Experimentelle Einrichtung

Als Positionspapier enthält dieser Artikel keine experimentelle Einrichtung im traditionellen Sinne, sondern unterstützt seine Standpunkte durch die Analyse bestehender Benchmark-Suites und Herausforderungsprobleme.

Analyseobjekte

  • Leistungs-Benchmarks: NAS Parallel Benchmarks, Mantevo, Salishan problems, Shonan challenge
  • Korrektheitsherausforderungen: VerifyThis, NSV-3 benchmarks, Gallery of Verified Programs
  • Spezialisierte Benchmarks: FPbench, DataRaceBench, SPEC

Bewertungskriterien

Die Autoren schlagen vor, dass Herausforderungsprobleme folgende Merkmale aufweisen sollten:

  • Abdeckung mehrerer Korrektheitsdimensionen
  • Vermeidung von Überspecialisierung
  • Praktische Relevanz
  • Fokus auf spezifische Anforderungen des wissenschaftlichen Rechnens

Experimentelle Ergebnisse

Statusanalyse

Die Autoren stellen fest, dass bestehende Herausforderungsprobleme folgende Mängel aufweisen:

  1. Unzureichende Abdeckung: Mangel an Graphenalgorithmen, komplexen Darstellungen dünnbesetzter Matrizen usw.
  2. Einfache Datenstrukturen: Unzureichende Abdeckung komplexer Darstellungen dünnbesetzter Matrizen über grundlegende CSR hinaus
  3. Unvollständige mathematische Domänen: Unzureichende Abdeckung grundlegender mathematischer Domänen

Erfolgreiche Fallstudien

Evolutionsverlauf von Leistungs-Benchmarks:

  • Linpack → Livermore Loops → NAS Parallel Benchmarks → Mantevo
  • Schrittweise Zunahme der Komplexität, von einfacher linearer Algebra zu vollständigem Anwendungscode
  • Bewertungsmetriken erweitern sich von reiner Leistung auf Korrektheit und Skalierbarkeit

Verwandte Arbeiten

Entwicklung von Leistungs-Benchmarks

  • Frühe Benchmarks: Linpack konzentriert sich auf Gleitkomma-Rechenleistung
  • Schleifen-Kernel: Livermore Loops testen spezifische Rechenmuster
  • Parallele Benchmarks: NAS Parallel Benchmarks führen Parallelismusüberlegungen ein
  • Anwendungsorientiert: Mantevo bietet Mini-Apps, die realen Anwendungen nahekommen

Korrektheit-Verifizierungsherausforderungen

  • Allgemeine Verifikation: VerifyThis und ähnliche Wettbewerbe bieten grundlegende Herausforderungen
  • Numerische Verifikation: coq-num-analysis, Mathematical Components Library
  • Spezialisierte Domänen: FPbench (Gleitkomma), DataRaceBench (Datenwettläufe)

Verifikation und Validierung (V&V)

  • ASME V&V-Richtlinien bieten Verifikations- und Validierungsstandards für Ingenieurwissenschaften
  • Unterscheidung zwischen Verifikations- (verification) und Validierungsproblemen (validation)

Schlussfolgerungen und Diskussion

Hauptschlussfolgerungen

  1. Die Korrektheit des wissenschaftlichen Rechnens erfordert spezialisierte Herausforderungsprobleme, um die Entwicklung formaler Methoden voranzutreiben
  2. Herausforderungsprobleme müssen sich über Rechenabstraktionsebenen erstrecken und niedrige Implementierungsdetails mit hohen Domänenbeschränkungen integrieren
  3. Es ist notwendig, Überspecialisierung und „Spielzeug"-Probleme zu vermeiden und sich auf praktische Anwendungsrelevanz zu konzentrieren

Einschränkungen

  1. Theoretische Natur: Als Positionspapier fehlen konkrete Beispiele von Herausforderungsproblemen
  2. Implementierungskomplexität: Die Etablierung einer umfassenden Herausforderungsproblemsammlung erfordert interdisziplinäre Zusammenarbeit
  3. Bewertungskriterien: Wie man die Qualität von Herausforderungsproblemen objektiv bewertet, bedarf weiterer Forschung

Zukünftige Richtungen

  1. Zusammenarbeit mit Experten des wissenschaftlichen Rechnens und der formalen Methoden zur Gestaltung konkreter Herausforderungsprobleme
  2. Etablierung standardisierter Bewertungsrahmen und Messkriterien
  3. Berücksichtigung der Integration von Unsicherheitsquantifizierung und statistischer Modellierung
  4. Erweiterung auf Verifikations- und Validierungsprobleme (V&V)

Tiefgehende Bewertung

Stärken

  1. Genaue Problemidentifikation: Genaue Identifikation der Schlüsselherausforderungen bei der Verifizierung der Korrektheit des wissenschaftlichen Rechnens
  2. Systematisches Framework: Das vorgeschlagene Korrektheitsdimensionen-Framework ist systematisch und umfassend
  3. Praxisorientierung: Vermeidung rein theoretischer Diskussionen, Fokus auf praktische Anforderungen
  4. Interdisziplinäre Perspektive: Effektive Verbindung der Gemeinschaften der formalen Methoden und des wissenschaftlichen Rechnens
  5. Historische Anleihen: Wertvolle Erfahrungen aus der Entwicklungsgeschichte von Leistungs-Benchmarks

Mängel

  1. Mangel an konkreten Beispielen: Keine konkreten Beispiele von Herausforderungsproblemen zur Validierung der Machbarkeit des Frameworks
  2. Unklar Implementierungspfad: Mangel an detaillierter Planung für den Übergang vom theoretischen Framework zu praktischen Herausforderungsproblemsammlungen
  3. Fehlende Bewertungsmechanismen: Mangel an konkreten Mechanismen zur Bewertung der Qualität und Effektivität von Herausforderungsproblemen
  4. Unbekannte Akzeptanz durch die Gemeinschaft: Die Akzeptanzbereitschaft und Beteiligungsabsicht der beiden Gemeinschaften bezüglich dieses Frameworks ist unbekannt

Einflussfähigkeit

  1. Akademischer Wert: Bietet ein wichtiges theoretisches Framework für die Forschung zur Korrektheit des wissenschaftlichen Rechnens
  2. Praktisches Potenzial: Könnte die Entwicklung praktischerer Verifizierungstechniken für formale Methoden fördern
  3. Gemeinschaftsaufbau: Könnte tiefere Zusammenarbeit zwischen den Gemeinschaften des wissenschaftlichen Rechnens und der formalen Methoden fördern
  4. Langfristige Bedeutung: Bietet neue Forschungsrichtungen für die Qualitätssicherung von Softwaresystemen des wissenschaftlichen Rechnens

Anwendungsszenarien

  1. Forschungsleitung: Bietet Forschungsrichtungen für Forscher der formalen Methoden in SC-Anwendungen
  2. Werkzeugentwicklung: Leitet die Gestaltung und Bewertung von Verifizierungswerkzeugen für das wissenschaftliche Rechnen
  3. Bildung und Schulung: Bietet ein systematisches Framework für die Ausbildung in der Korrektheit des wissenschaftlichen Rechnens
  4. Standardisierung: Bietet Referenzen für die Festlegung von Qualitätsstandards für Software des wissenschaftlichen Rechnens

Literaturverzeichnis

Das Papier zitiert 26 wichtige Literaturquellen, die folgende Bereiche abdecken:

  • Leistungs-Benchmarks: NAS Parallel Benchmarks 7,8, Mantevo 11, Linpack 14
  • Formale Verifikation: Gallery of Verified Programs 1,17, VerifyThis 20
  • Numerische Verifikation: coq-num-analysis 6, Mathematical Components 2
  • Spezialisierte Benchmarks: FPbench 12, DataRaceBench 21, SPEC 13
  • V&V-Standards: ASME-Richtlinien 18

Obwohl dieses Papier ein Positionspapier ist, bietet es einen wichtigen theoretischen Rahmen und Entwicklungsrichtungen für das Feld der Verifizierung der Korrektheit des wissenschaftlichen Rechnens. Das vorgeschlagene Sechs-Dimensionen-Korrektheit-Framework und die Designrichtlinien sind von großer Bedeutung für die Förderung der Entwicklung dieses Feldes, erfordern aber nachfolgende Arbeiten zur konkreten Umsetzung und Validierung dieser Ideen.