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

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

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