في عالم التحقق الرسمي، تم إجراء دراسات مكثفة حول كل من آليات صياغة البيانات تلقائيًا (autoformalization) والبحث التلقائي عن الأدلة (automated proof search). على الرغم من أن البحث التلقائي عن الأدلة يمكن أن ينتج برهانًا رسميًا عمليًا، إلا أن البرهان الناتج لا يعكس بالضرورة كيف يصل الاستدلال الطبيعي اللغوي إلى استنتاجاته. أطلق الباحثون مصطلح 'الأمانة' (faithfulness) لوصف هذه الظاهرة.

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

في هذا العمل، تم توضيح مجموعة من الشروط الأساسية الخمسة التي يجب على البرهان الرسمي الموثوق أن يلبيها. وقد تم تقديم أداة جديدة تُعرف بـ 'Pistis'، وهي نظام للبحث عن الأدلة مُوجَّه من قبل وكيل فكري، والذي ينتج براهين رسمية بلغة Lean تلبي تلك الشروط.

في جوهرها، تنفذ 'Pistis' بحثًا مبتكرًا تحت اسم 'OrderDecompose' يحافظ على الأمانة من خلال تتبع اعتمادات الاقتباس ومنع الاختصارات غير الموثوقة. بالإضافة إلى ذلك، تجمع بين البحث عن نفي (refutation search) الذي يكشف عن الفجوات والأخطاء في مصدر البراهين اللغوية الطبيعية. أثبتت 'OrderDecompose' قدرتها على إكمال البراهين التي تعجز الطرق التقليدية عن إنجازها حتى في غضون 12 ساعة، كما أن نتائجها تتجمع أسرع بـ 33 مرة مقارنة بالأعمال السابقة.

تم تطبيق 'Pistis' على الكتب الثلاثة الأولى من عناصر إقليدس، مما أتاح الحصول على أعمال عالية الجودة تحتوي على براهين رسمية موثوقة. ووفقًا لدراسة أجريت بشكل مزدوج مع بروتوكول 'LLM-as-a-judge' استنادًا إلى معايير صارمة، تم تفضيل براهين 'Pistis' على الأعمال السابقة بمقدار 2.89 مرة من قبل مراجعينا البشر، و5.2 مرة من قبل قضاة الذكاء الاصطناعي.

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