Does the Proof Prove It That Way? Faithful Formalization of Elements Proofs
تقدم هذه الورقة نظام Pistis، وهو نظام وكيل موجه من قِبل أوراكل يتميز باستراتيجية بحث مبتكرة تسمى "OrderDecompose" تولد براهين رسمية أمينة بلغة Lean لعناصر إقليدس عبر مواءمة الاستدلال باللغة الطبيعية بدقة مع التكتيكات الرسمية، متفوقة بذلك على النماذج المرجعية السابقة في السرعة، ومعدل النجاح، وتفضيل البشر والنماذج اللغوية الكبيرة، مع تحديد الفجوات في الحجج الرياضية بفعالية.
البحث الأصلي مرخَّص بموجب CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). هذا شرح مولَّده بالذكاء الاصطناعي للبحث أدناه. لم يكتبه المؤلفون ولم يصادقوا عليه. وللتحقق من الدقة التقنية، يرجى الرجوع إلى البحث الأصلي. اقرأ إخلاء المسؤولية الكامل
لطالما اعتمدت الرياضيات على لغتين متمايزتين. إحداهما هي اللغة الطبيعية التي نستخدمها لشرح الأفكار، وسرد القصص، ومشاركة الرؤى؛ وهي لغة مرنة، غنية بالسياق، وغالبًا ما تتخطى خطوات تبدو بديهية للقارئ البشري. أما الأخرى فهي اللغة الرسمية لمساعدي الإثبات، وهي أنظمة حاسوبية صارمة تتحقق من كل خطوة منطقية لضمان أن النتيجة صحيحة بشكل لا يقبل الجدل. لعقود من الزمن، عمل الباحثون على ترجمة اللغة الأولى إلى الثانية، وهي عملية تسمى "الأتمتة الصورية" (autoformalization). كان الهدف بسيطًا: أخذ برهان مكتوب بشري وتحويله إلى كود يمكن للحاسوب التحقق منه. لكن مشكلة حرجة ظلت قائمة؛ فقد كان بإمكان الحاسوب إنتاج برهان صحيح تقنيًا، ومع ذلك لا يشبه الحجة البشرية التي ألهمته بأي شكل من الأشكال. قد يحل الحاسوب المشكلة باستخدام مسار مختلف تمامًا، مخفيًا الاستدلال الأصلي خلف جدار من الاختصارات المؤتمتة. خلق هذا فجوة بين الحقيقة والفهم؛ فإذا لم يتبع برهان الحاسوب خطوات الإنسان، فلا يمكننا استخدامه للتحقق مما إذا كان استدلال الإنسان سليمًا بالفعل، كما لا يمكننا الوثوق به ليعلمنا كيف يعمل الاستدلال.
لقد تصدى فريق من الباحثين لهذه الفجوة الآن بنظام جديد صُمم لجعل برهان الحاسوب مخلصًا لعملية التفكير الأصلية للإنسان. أطلقوا على نظامهم اسم "بيستيس" (Pistis)، وهو اسم مستمد من الكلمة اليونانية القديمة التي تعني الإيمان أو الثقة. طبق الباحثون هذا النظام على الكتب الثلاثة الأولى من كتاب "العناصر" لإقليدس، وهو نص هندسي تأسيسي كُتب قبل أكثر من ألفي عام. يوضح عملهم أنه من الممكن ترجمة هذه الحجج القديمة إلى لغة حاسوبية حديثة دون فقدان المنطق الأصلي، مع الكشف أيضًا عن أخطاء خفية في النص ظلت غير ملحوظة لقرون.
كان التحدي الجوهري الذي واجهه الفريق هو أن اللغة الطبيعية ومنطق الحاسوب يعملان بإيقاعات مختلفة. قد يقول البرهان البشري: "لنفترض أن هذا صحيح"، ثم يمضي قدمًا، متوقعًا من القارئ ملء الفجوة. أما الحاسوب، فيتطلب أن يتم ذكر وتبرير كل خطوة بشكل صريح. غالبًا ما كانت محاولات ترجمة البراهن تسمح للحاسوب بملء هذه الفجوات بمنطقه الخاص، مما يؤدي فعليًا إلى إعادة كتابة الحجة لتسهيل حلها آليًا. وكانت النتيجة برهانًا يعمل بنجاح ولكنه يفشل في عكس قصد المؤلف البشري. بُني "بيستيس" لمنع حدوث ذلك. فبدلاً من مطالبة الحاسوب بإيجاد أي طريقة ممكنة لإثبات العبارة، يجبر النظام الحاسوب على اتباع المسار المحدد للإنسان، جملة بجملة.
ولتحقيق ذلك، طور الباحثون طريقة تقسم عملية الترجمة إلى مرحلتين متمايزتين. أولاً، تقوم "مرحلة التعيين" (mapping phase) بتحليل النص ذي اللغة الطبيعية وتقسيمه إلى تسلسل من الخطوات الصغيرة والذرية؛ حيث تحدد بالضبط ما تدعيه كل جملة وما هي الافتراضات التي تعتمد عليها، مما يخلق قالبًا صارمًا يجب على الحاسوب اتباعه. ثانيًا، تحاول "مرحلة الملء" (filling phase) إثبات كل من هذه الخطوات الصغيرة بشكل فردي. يستخدم النظام استراتيجية بحث متخصصة تمنع الحاسوب من اتخاذ اختصارات أو القفز للأمام. وإذا لم يستطع الحاسوب إثبات خطوة معينة باستخدام الأدوات والمراجع ذاتها التي ذكرها النص البشري، فإنه لا يجد ببساطة طريقة أخرى لحل المشكلة، بل يقوم بدلاً من ذلك بالإبلاغ عن المشكلة، كاشفًا أن الحجة البشرية الأصلية قد تحتوي على ثغرة أو جزء مفقود.
أثبت هذا النهج فاعلية ملحوظة عند اختباره على هندسة إقليدس. أنتج الباحثون براهين رسمية لـ 92 قضية عبر الكتب الثلاثة الأولى. وعند مقارنة هذه البراهين الجديدة بالمحاولات السابقة، كان الفرق صارخًا؛ فقد تمت برمجة البراهين الجديدة بسرعة أكبر بـ 33 ضعفًا، وهو تحسن كبير في الكفاءة يشير إلى أن الطريقة الجديدة تتجنب الحسابات الثقيلة والبطيئة للأنظمة القديمة. والأهم من ذلك، فضل الخبراء البشريون مخرجات النظام الجديد بفارق كبير. في دراسة معماة، وجد المراجعون أن البراهين الجديدة أكثر شفافية وتمثل حجج الكتاب المدرسي الأصلي بشكل أفضل. كما وافق قاضٍ يعمل بالذكاء الاصطناعي، تم تدريبه لتقييم جودة الترجمة، على ذلك، مفضلًا البراهين الجديدة على القديمة بنسبة تزيد عن خمسة إلى واحد.
بعيدًا عن مجرد ترجمة النص، عمل النظام كمتحقق صارم كشف عن عيوب حقيقية في المادة المصدرية. نظرًا لأن النظام يصر على اتباع المنطق البشري بدقة، فإنه لا يمكنه إخفاء الأخطاء. في إحدى الحالات، حدد النظام خطأً في الاستشهاد في ترجمة حديثة لإقليدس؛ حيث أشار النص إلى قضية تتعلق بقطع خط في المنتصف، لكن الاستشهاد أشار إلى قضية تتعلق بقطع زاوية. رصد النظام هذا عدم التطابق، موضحًا أن الترجمة ربطت الفكرة الخاطئة بالخطوة الخاطئة. وفي حالة أخرى، وجد النظام فجوة في استدلال إقليدس نفسه حيث تُرك سيناريو معين دون معالجة. تمكن الباحثون من إثبات أن الحجة الأصلية كانت غير مكتملة رسميًا، وهو اكتشاف كان من الصعب القيام به بدون أداة تلتزم بالهيكل الأصلي بصرامة.
يوحي نجاح "بيستيس" بأن الصياغة الرسمية الوفية ليست مجرد تمرين تقني، بل هي أداة قوية للتحقق من المعرفة البشرية. فمن خلال إجبار الحاسوب على السير في نفس المسار الذي سلكه الإنسان، يمكن للنظام التأكد مما إذا كان الاستدلال صامدًا أو أين ينهار. وجد الباحثون أن طريقتهم يمكنها قبول الحجج الصحيحة، ودحض الحجج غير الصحيحة، وتحديد مكان الخطأ في البرهان بدقة. تمتد هذه القدرة إلى ما وراء الهندسة القديمة؛ إذ صُمم الإطار ليعمل مع أي حجة رياضية مكتوبة بلغة طبيعية. يظهر العمل أننا لسنا مضطرين للاختيار بين مرونة الشرح البشري وصرامة التحقق الآلي؛ إذ يمكن الحصول على كليهما، بشرط أن يتم توجيه الآلة لاحترام الصوت والمنطق البشري الأصلي.
كما سلطت الدراسة الضوء على حدود التكنولوجيا الحالية. فبينما عمل النظام بشكل جيد مع الكتب الثلاثة الأولى لإقليدس، لم يستطع التعامل مع كل قضية في الكتب اللاحقة دون توجيه بشري إضافي. تطلبت بعض القضايا مفاهيم هندسية لا يعرف النظام الحاسوبي كيفية التعامل معها بعد، مثل قياس طول خط منحني. أشار الباحثون إلى أن نظامهم يعتمد على إنسان أو ذكاء اصطناعي متقدم ليعمل كـ "عراف" (oracle)، يتحقق من أن التعيين الأولي للنص صحيح. وهذا يعني أن العملية ليست آلية بالكامل بعد، لكنها تقلل بشكل كبير من مقدار العمل اليدوي المطلوب مقارنة بالطرق السابقة.
في نهاية المطاف، تقدم الورقة معيارًا جديدًا لكيفية تفاعلنا مع البراهين الرياضية في عصر الذكاء الاصطناعي. إنها تتجاوز السؤال حول ما إذا كان بإمكان الحاسوب إثبات نظرية ما، لتنتقل إلى السؤال الأكثر عمقًا: هل يفهم الحاسوب الحجة؟ من خلال ضمان أن البرهان الرسمي يعكس الحجة ذات اللغة الطبيعية خطوة بخطوة، خلق الباحثون أداة يمكنها التحقق من الاستدلال الكامن وراء النتيجة، وليس النتيجة نفسها فقط. يتيح ذلك للرياضيين والطلاب الثقة في أن الحاسوب لا يجد حلاً فحسب، بل يتبع حقًا منطق الشخص الذي كتب البرهان. يقدم هذا العمل مسارًا للمستقبل حيث يعمل البصيرة البشرية والدقة الآلية معًا، مما يحافظ على سلامة الاكتشاف الرياضي مع الاستفادة من قوة التحقق الحديث.
غارق في أبحاث مجالك؟
تصلك نشرة يومية بأحدث الأبحاث المطابقة لكلماتك البحثية المفتاحية — مع ملخصات تقنية، بلغتك.