تسعى الأنظمة الحديثة للتحويل الآلي (Autoformalization) لأن تكون جسرًا مهمًا بين النظريات الرياضية والبرمجيات، مما يسمح بتحويل المسلمات الرياضية غير الرسمية إلى شيفرات قابلة للاستخدام مع مساعدات الإثبات مثل Lean. ومع ذلك، فإن التحديات تكمن في مؤشرات التقييم الحالية التي قد تقبل الجمل المبرمجة بشكل صحيح ولكنها غير متوافقة في الدلالة، أو ترفض جملًا صحيحة مكتوبة بشكل مختلف.

إلهامًا من نموذج Pass@$k$، تقدم الدراسة الجديدة طريقة SA-Pass (*اختبار التوافق الدلالي*)، التي تختبر الجمل الرسمية باستخدام جمل مساعدة تُسمى *أشباح*، والتي تُحدد المعنى المقصود للجملة. يحصل البيان الذي تم إنشاؤه على كامل النقاط فقط عندما يكون صحيحًا عند الاستخدام، ويستنتج كل شبح (تحقق للأمام)، ويستنتج من مجموعها (تحقق للخلف).

تم تطبيق SA-Pass في ShadowBench، وهو معيار كامل للتحويل الآلي باستخدام Lean 4 يتضمن 178 مسألة من مستوى الدراسات العليا إلى مستوى البحث، تغطي ثماني مجالات رياضية. وقد حقق نموذج Claude Code (Opus 4.8) مع Numina-Lean-Agent معدل تجميع قدره 61.8% ونسبة SA-Pass تصل إلى 11.2%. وعبر النماذج الناتجة من ستة تكوينات تعتمد على النمط، حقق SA-Pass توافقًا ثنائيًا بنسبة 98.8% مع تقييمات الخبراء.

تشير أهمية ShadowBench إلى أنه تم استخدامه كمعيار للمرحلة الرابعة من تحدي AI4Math لعام 2026 في مؤتمر ICML، مما يبرز دوره كأداة رئيسية في تطوير الأساليب الرياضية الآلية.