2025-11-12T00:52:30.352910

OFP-Repair: Repairing Floating-point Errors via Original-Precision Arithmetic

Tan, Ding, Chen et al.

Errors in floating-point programs can lead to severe consequences, particularly in critical domains such as military, aerospace, and financial systems, making their repair a crucial research problem. In practice, some errors can be fixed using original-precision arithmetic, while others require high-precision computation. Developers often avoid addressing the latter due to excessive computational resources required. However, they sometimes struggle to distinguish between these two types of errors, and existing repair tools fail to assist in this differentiation. Most current repair tools rely on high-precision implementations, which are time-consuming to develop and demand specialized expertise. Although a few tools do not require high-precision programs, they can only fix a limited subset of errors or produce suboptimal results. To address these challenges, we propose a novel method, named OFP-Repair.On ACESO's dataset, our patches achieve improvements of three, seven, three, and eight orders of magnitude across four accuracy metrics. In real-world cases, our method successfully detects all five original-precision-repairable errors and fixes three, whereas ACESO only repairs one. Notably, these results are based on verified data and do not fully capture the potential of OFP-Repair. To further validate our method, we deploy it on a decade-old open bug report from GNU Scientific Library (GSL), successfully repairing five out of 15 bugs. The developers have expressed interest in our method and are considering integrating our tool into their development workflow. We are currently working on applying our patches to GSL. The results are highly encouraging, demonstrating the practical applicability of our technique.

academic

OFP-Repair: إصلاح أخطاء الفاصلة العائمة عبر حسابات الدقة الأصلية

المعلومات الأساسية

معرّف الورقة: 2510.09938
العنوان: OFP-Repair: Repairing Floating-point Errors via Original-Precision Arithmetic
المؤلفون: Youshuai Tan, Zishuo Ding, Jinfu Chen, Weiyi Shang
التصنيف: cs.SE (هندسة البرمجيات)
وقت النشر/المؤتمر: Conference'17, Washington, DC, USA (2025)
رابط الورقة: https://arxiv.org/abs/2510.09938

الملخص

قد تؤدي الأخطاء في برامج الفاصلة العائمة إلى عواقب وخيمة، خاصة في المجالات الحرجة مثل الأنظمة العسكرية والفضائية والمالية. في الممارسة العملية، يمكن إصلاح بعض الأخطاء من خلال حسابات الدقة الأصلية، بينما تتطلب أخطاء أخرى حسابات عالية الدقة. يتجنب المطورون عادة استخدام طرق الدقة العالية لأنها تتطلب موارد حسابية كبيرة. ومع ذلك، يواجه المطورون صعوبة في التمييز بين هاتين الفئتين من الأخطاء، وأدوات الإصلاح الحالية غير قادرة على مساعدتهم في هذا التمييز. لمعالجة هذه التحديات، تقترح هذه الورقة طريقة OFP-Repair التي تحدد الأخطاء القابلة للإصلاح بالدقة الأصلية من خلال حساب رقم الشرط للبرنامج بالنسبة للمدخلات، وتستخدم توسع المتسلسلات لبناء إطار عمل موحد للإصلاح. تظهر النتائج التجريبية تحسنًا بمقدار 3 و7 و3 و8 رتب من حيث الحجم على أربعة مقاييس دقة على التوالي.

السياق البحثي والدافع

تعريف المشكلة

قد تؤدي أخطاء الفاصلة العائمة في الأنظمة الحرجة إلى عواقب كارثية، مثل فشل نظام صواريخ باتريوت وانفجار صاروخ أريان 5. تشير الأبحاث الحالية إلى أن أخطاء الفاصلة العائمة تنقسم بشكل أساسي إلى فئتين:

أخطاء قابلة للإصلاح بالدقة الأصلية: يمكن إصلاحها من خلال إعادة بناء التعبيرات الرقمية بالدقة الأصلية
أخطاء معتمدة على الدقة العالية: يجب استخدام حسابات الفاصلة العائمة عالية الدقة لإصلاحها

قيود الطرق الموجودة

تحدد الورقة ثلاث قيود رئيسية:

القيد 1: تتطلب عمليات الكشف والإصلاح برنامجًا عالي الدقة، وتحويل البرنامج الأصلي إلى نسخة عالية الدقة يتطلب معرفة عميقة بالرياضيات والتحليل الرقمي
القيد 2: عدم وجود نموذج إصلاح موحد للأخطاء القابلة للإصلاح بالدقة الأصلية، حيث تستطيع الأدوات الموجودة التعامل مع جزء فقط من هذه الأخطاء
القيد 3: عدم وجود قدرات تشخيصية لهذه الأخطاء، مما يجعل من الصعب على المطورين تحديد ما إذا كان يمكن إصلاح الخطأ من خلال حسابات الدقة الأصلية

الدافع البحثي

تظهر أبحاث Franco أن المطورين يفضلون استخدام حلول الإصلاح بالدقة الأصلية لأن حلول الدقة العالية تتطلب تكاليف حسابية عالية جدًا. على سبيل المثال، تم إغلاق NumPy issue #1063 بسبب التكاليف العالية للدقة العالية. ومع ذلك، لا تستطيع الأدوات الموجودة مساعدة المطورين على التمييز بين هذين النوعين من الأخطاء.

المساهمات الأساسية

اقتراح طريقة OFP-Repair: أول إطار عمل موحد قادر على الكشف الفعال والإصلاح الفعال للأخطاء القابلة للإصلاح بالدقة الأصلية
إنشاء الأساس النظري: آليات الكشف والإصلاح بالدقة الأصلية بناءً على نظرية رقم الشرط وتوسع متسلسلة تايلور
التحقق التجريبي الواسع: التحقق من فعالية الطريقة على مجموعة بيانات ACESO والأخطاء الحقيقية وتقارير أخطاء GSL التي لم تُحل لمدة عشر سنوات
القيمة التطبيقية العملية: إصلاح ناجح لـ 5 أخطاء طويلة الأمد في GSL مع الحصول على موافقة المطورين

شرح الطريقة

تعريف المهمة

المدخلات: برنامج يحتوي على أخطاء فاصلة عائمة ونطاق المدخلات الذي يثير أخطاء كبيرة
المخرجات:
1. تحديد نوع الخطأ (قابل للإصلاح بالدقة الأصلية مقابل معتمد على الدقة العالية)
2. رقعة إصلاح للأخطاء القابلة للإصلاح بالدقة الأصلية
القيود: لا تعتمد على تطبيق برنامج عالي الدقة

الأساس النظري

تحليل مصادر الأخطاء الكبيرة

تثبت الورقة أن الأخطاء الكبيرة في الفاصلة العائمة تنشأ بشكل أساسي من تأثير الإلغاء (cancellation). عندما يتم طرح رقمي فاصلة عائمة متقاربين تقريبًا، يحدث انخفاض كبير في عدد أرقام الدقة الفعالة. على سبيل المثال:

x = 3.14159265358973, y = 3.14159265358972
الفرق النظري: 1×10^-14
نتيجة حساب الفاصلة العائمة: 1.021405182655144×10^-14
الخطأ النسبي: حوالي 2.14%

التمثيل متعدد الحدود للبرنامج

بناءً على النظريتين التاليتين:

نظرية الحفاظ على الاستمرارية للعمليات الحسابية: العمليات الحسابية للدوال المستمرة تحافظ على الاستمرارية
نظرية Weierstrass للتقريب: يمكن تقريب أي دالة مستمرة بشكل تعسفي باستخدام متعددات حدود

تثبت الورقة أن برامج الفاصلة العائمة يمكن تحويلها إلى تمثيل متعدد الحدود داخل كل مجال فرعي.

خوارزمية الكشف (الخطوة 1)

فكرة التصميم

استخدام نظرية رقم الشرط لتقييم تأثير اضطرابات المدخلات على المخرجات: $\left|\frac{f(x+\Delta x)-f(x)}{f(x)}\right| \approx \left|\frac{\Delta x}{x}\right| \cdot \left|\frac{xf'(x)}{f(x)}\right|$

حيث $\left|\frac{xf'(x)}{f(x)}\right|$ هو رقم الشرط.

تدفق الكشف

استخدام ATOMU للكشف عن أخطاء الفاصلة العائمة الكبيرة
لكل خطأ، حساب رقم الشرط للبرنامج بالنسبة للمدخلات
استخدام التفاضل الرقمي لتقدير المشتقات: $f'(x) \approx \frac{f(x+h)-f(x)}{h}$
إذا كان رقم الشرط أقل من حد معين (مثل 10^5)، يتم تصنيف الخطأ كخطأ قابل للإصلاح بالدقة الأصلية

مثال تحليلي

للدالة $\sin(x+\epsilon) - \sin(x)$ :

رقم الشرط بالنسبة إلى $\sin(x+\epsilon)$ : 9.0132×10^9 (كبير جدًا)
رقم الشرط بالنسبة إلى المدخل $x$ : 3.40 (صغير جدًا)
الخلاصة: يمكن إصلاح هذا الخطأ من خلال حسابات الدقة الأصلية

خوارزمية الإصلاح (الخطوة 2)

مبدأ التصميم

استخدام توسع متسلسلة تايلور لتحويل البرنامج إلى شكل متعدد حدود خالٍ من الإلغاء: $f(x) = \sum_{n=0}^{\infty} \frac{f^{(n)}(a)}{n!}(x-a)^n$

تدفق الإصلاح

اختيار نقطة التوسع (عادة بالقرب من النقطة التي تسبب الخطأ الكبير)
حساب الحدود الأولى من متسلسلة تايلور
بناء رقعة متعددة الحدود تتجنب الإلغاء الأصلي
تحديد عدد حدود التوسع (في الورقة بحد أقصى 10 حدود)

مثال الإصلاح

للدالة $\sin(x+\epsilon) - \sin(x)$ :

توسع تايلور: $\sin(x+\epsilon) = \sin(x) + \cos(x)\epsilon - \frac{\sin(x)}{2!}\epsilon^2 + ...$
بعد حذف حد $\sin(x)$ : $\cos(x)\epsilon - \frac{\sin(x)}{2!}\epsilon^2 + ...$
تحسن الخطأ النسبي من 1.1095×10^-10 إلى 1.6176×10^-16

قيود الطريقة

يتطلب توسع تايلور تقارب الدالة عند نقطة التوسع. عندما تتباعد الدالة عند نقطة التوسع (مثل $norm.ppf(1-q/2)$ في SciPy issue #3545 عندما تقترب $q$ من الصفر)، لا تنطبق الطريقة.

إعداد التجارب

مجموعات البيانات

مجموعة بيانات ACESO: 32 دالة معيارية
- 15 دالة من أبحاث سابقة حول أخطاء الفاصلة العائمة، ثبت أنها قابلة للإصلاح بالدقة الأصلية
- 17 دالة متغيرة تحتوي على استدعاءات مكتبات GSL و ALGLIB
الأخطاء الحقيقية: 5 أخطاء قابلة للإصلاح بالدقة الأصلية جمعتها Franco وآخرون
تقارير أخطاء GSL: تقارير أخطاء مفتوحة من قبل عشر سنوات، تحتوي على 15 خطأ فاصلة عائمة

مقاييس التقييم

استخدام الخطأ النسبي لقياس أخطاء الفاصلة العائمة: $\left|\frac{Result_{approximate} - Result_{true}}{Result_{true}}\right|$

يتم تقييم الحد الأقصى للخطأ المطلق والحد الأقصى للخطأ النسبي بشكل منفصل في المناطق المستقرة والمتناقصة.

الطرق المقارنة

المقارنة الرئيسية مع ACESO، لأنها الأداة الوحيدة الموجودة التي لا تتطلب برنامجًا عالي الدقة للكشف والإصلاح.

تفاصيل التطبيق

البيئة: حاوية Docker، Ubuntu 24.04، معالج Intel i9-13900K، ذاكرة 128GB
الحد الأقصى لحدود متسلسلة تايلور: 10 حدود
حد رقم الشرط: 1×10^5
نصف قطر العينة: 1×10^-5

نتائج التجارب

النتائج الرئيسية

RQ1: تقييم قدرة الكشف

معدل النجاح: في 32 دالة من ACESO، نجحت OFP-Repair في تحديد جميع الأخطاء القابلة للإصلاح بالدقة الأصلية
تحليل رقم الشرط: تتراوح أقصى قيمة لرقم الشرط المحسوبة بين 1.47 والحد الأدنى 0 والمتوسط 0.31، وجميعها أقل بكثير من حد 10^5
دقة المشتقات الرقمية: باستثناء دالة bj_tan، يتراوح الخطأ النسبي بين 0-0.746، مما لا يؤثر على فعالية الكشف

RQ2: تقييم أداء الإصلاح

مقارنة مع ACESO، متوسط التحسن في OFP-Repair على أربعة مقاييس:

المقياس	OFP-Repair	ACESO	مضاعف التحسن
الحد الأقصى للخطأ المطلق في المنطقة المستقرة	4.11×10^-16	2.45×10^-13	3 رتب من حيث الحجم
الحد الأقصى للخطأ النسبي في المنطقة المستقرة	7.47×10^-16	2.74×10^-9	7 رتب من حيث الحجم
الحد الأقصى للخطأ المطلق في المنطقة المتناقصة	2.13×10^-16	2.45×10^-13	3 رتب من حيث الحجم
الحد الأقصى للخطأ النسبي في المنطقة المتناقصة	3.73×10^-15	5.74×10^-7	8 رتب من حيث الحجم

RQ3: التطبيقات الحقيقية

الكشف: نجح في تحديد جميع الأخطاء الخمسة القابلة للإصلاح بالدقة الأصلية في العالم الحقيقي
الإصلاح: نجح في إصلاح 3 أخطاء، بينما أصلحت ACESO واحدًا فقط
الدقة: دقة الدوال المصلحة أفضل بشكل ملحوظ من ACESO

تحليل الحالات: تقارير أخطاء GSL

في تقارير أخطاء GSL التي لم تُحل لمدة عشر سنوات:

حالات الحل الكامل (3 حالات)

دالة gsl_sf_hyperg_0F1:

الخطأ النسبي الأصلي: 1.15×10^198
رقم الشرط: 3.39×10^-210 و 1.01×10^-225 (كلاهما صغير جدًا)
الخطأ النسبي بعد الإصلاح: 1.17×10^-27

حالات التحسن الجزئي (حالتان)

دالة gsl_sf_gamma_inc_Q:

انخفض الخطأ النسبي من 1.60×10^-6 إلى 1.57×10^-7

دالة gsl_sf_ellint_P:

من خلال إعادة بناء الحساب لتجنب الفيض السفلي، انخفض الخطأ النسبي إلى 1.91×10^-9

الأعمال ذات الصلة

كشف أخطاء الفاصلة العائمة

أدوات التحليل الثابت: FPDebug و Verrou و Herbgrind على إطار عمل Valgrind
طرق الكشف الديناميكي: الخوارزميات الجينية وتحليل رقم الشرط والتنفيذ الرمزي وغيرها

إصلاح أخطاء الفاصلة العائمة

الطرق القائمة على التحويل: Herbie و Salsa وغيرها، تعتمد على قوالب محددة مسبقًا، نطاق التغطية محدود
الطرق القائمة على الدقة العالية: AutoRNP وغيرها، تتطلب تطبيق برنامج عالي الدقة كامل
ACESO: الطريقة الوحيدة التي لا تعتمد على برنامج عالي الدقة، لكن تأثير الإصلاح محدود

الخلاصة والنقاش

الاستنتاجات الرئيسية

الكشف الفعال: تستطيع OFP-Repair تحديد الأخطاء القابلة للإصلاح بالدقة الأصلية بدقة، دون الحاجة إلى برنامج عالي الدقة
الإصلاح المتفوق: مقارنة بالطرق الموجودة، تحقق تحسنًا بعدة رتب من حيث الحجم في الدقة
القيمة العملية: تطبيق ناجح في المشاريع الحقيقية مع الحصول على موافقة المطورين

القيود

متطلبات التقارب: يتطلب توسع تايلور تقارب الدالة عند نقطة التوسع
معالجة الفروع: قد تتطلب فروع البرنامج المختلفة استراتيجيات معالجة مختلفة
الدوال المعقدة: قد تتطلب الدوال الرياضية المعقدة جدًا حدودًا توسعية أكثر

الاتجاهات المستقبلية

توسيع الطريقة لتغطية نطاق أوسع من الأخطاء غير المحلولة
تحسين استراتيجية اختيار عدد حدود توسع تايلور
إيجاد حلول بديلة للحالات التي تتباعد فيها الدالة

التقييم المتعمق

المميزات

المساهمة النظرية: إنشاء نظرية كشف الأخطاء القابلة للإصلاح بالدقة الأصلية بناءً على رقم الشرط
القوة العملية: عدم الاعتماد على برنامج عالي الدقة، مما يقلل من عتبة الاستخدام
النتائج الملحوظة: تحقيق تحسن بعدة رتب من حيث الحجم على مقاييس متعددة
التحقق الشامل: التحقق الكامل من المعايير الأكاديمية إلى التطبيقات الحقيقية
الكتابة الواضحة: وصف دقيق للتفاصيل التقنية وتصميم تجريبي معقول

أوجه القصور

نطاق التطبيق: ينطبق فقط على الأخطاء القابلة للإصلاح بالدقة الأصلية، غير فعال للأخطاء المعتمدة على الدقة العالية
قيود الدوال: متطلبات تقارب توسع تايلور تحد من عمومية الطريقة
اختيار المعاملات: اختيار حد رقم الشرط وعدد حدود تايلور يفتقر إلى التوجيه النظري
قابلية التوسع: تحتاج قابلية تطبيق الطريقة على البرامج الكبيرة والمعقدة إلى مزيد من التحقق

التأثير

القيمة الأكاديمية: توفير إطار نظري جديد وأداة عملية لمجال إصلاح أخطاء الفاصلة العائمة
التطبيقات الصناعية: ردود الفعل الإيجابية من مطوري GSL تظهر إمكانية التطبيق العملي
قابلية الاستنساخ: توفير حزمة استنساخ كاملة، مما يسهل الأبحاث اللاحقة

السيناريوهات المناسبة

مكتبات الحوسبة العلمية: مثل GSL و NumPy و SciPy وغيرها من مكتبات الحوسبة الرقمية
الأنظمة الحرجة: مشاكل دقة الفاصلة العائمة في أنظمة الفضاء والطيران والمالية
البحث التعليمي: كأداة تعليمية لتحليل وإصلاح أخطاء الفاصلة العائمة

المراجع

تستشهد الورقة بـ 36 مرجعًا ذا صلة، تغطي الكشف عن أخطاء الفاصلة العائمة وإصلاحها والتحليل الرقمي وجوانب أخرى متعددة، مما يوفر أساسًا نظريًا قويًا للبحث. تشمل المراجع الرئيسية الدراسة المنهجية للأخطاء الرقمية من قبل Franco وآخرين، وأدوات الإصلاح الممثلة مثل ACESO و AutoRNP، والأساس النظري الرياضي ذي الصلة.

التقييم الشامل: هذه ورقة بحثية عالية الجودة في هندسة البرمجيات، تقترح حلاً مبتكرًا لمشكلة مهمة في إصلاح أخطاء برامج الفاصلة العائمة. الطريقة لها أساس نظري قوي، والتحقق التجريبي شامل، وتأثير التطبيق العملي ملحوظ. على الرغم من وجود بعض القيود، فإن الورقة تقدم مساهمة مهمة لتطور هذا المجال.