من توليد الحدسيات إلى براهين قابلة للفحص: المتحققات والمواصفات والاكتشاف في البحث العصبي الرمزي

1. كيف يتوزع العمل بين المقترحات العصبية والإغلاق الرمزي

في AlphaGeometry، يوسّع المحرك الرمزي إغلاق الاستدلال انطلاقًا من الكائنات والعلاقات الموجودة، ويقترح النموذج اللغوي عند الحاجة بناءات مساعدة تضيف كائنات جديدة إلى المحرك. يصل هذا التقسيم للعمل فضاء المقترحات غير المقيّد باستدلال مقيّد بالقواعد. ولا تكمن أهميته العلمية في جعل اللغة الطبيعية للنموذج اللغوي تبدو أكثر مصداقية، بل في إدخال المحتوى المولّد ضمن صياغة نحوية وإجراءات فحص محددة. يقترح هذا المقال حفظ كل بناء ومخطط الاستدلال بعد إضافته وسلسلة الاعتماد النهائية، ليتبين للقراء اللاحقين أي كائن جديد أسهم به النموذج فعلًا، وما إذا كان الاستنتاج يعتمد حقًا على ذلك البناء.[1] Solving olympiad geometry without human demonstrations

2. ينبغي فهم الأداء على المعايير المرجعية مع نطاق المسائل القابلة للتعبير

حلّت دراسة AlphaGeometry الأصلية 25 مسألة ضمن IMO-AG-30، لكن هذه المجموعة أُخذت من مسائل قابلة للترجمة إلى لغة هندسية محددة، واستبعدت أنواعًا مثل بعض المتباينات والهندسة التوافقية. تدعم هذه النتيجة قدرته الاستدلالية داخل تلك البيئة الهندسية، ولا يجوز إعادة صياغتها باعتبارها معدل نجاح مماثلًا في المسائل الرياضية العامة. يدعو هذا المقال إلى نشر المسائل الأصلية ونسخها المصوغة صوريًا وأنواع المسائل المستبعدة وقواعد المراجعة البشرية معًا. وحتى لو كان الفاحص صحيحًا تمامًا، فقد تختلف القضية المبرهنة عن المسألة الأصلية إذا أغفلت الصياغة الصورية شروط عدم الانحلال أو استبدلت علاقة الوقوع داخل قطعة مستقيمة بعلاقة الاستقامة المشتركة.[1] Solving olympiad geometry without human demonstrations

3. تتمحور عملية الاكتشاف في FunSearch حول التقييم القابل للتنفيذ

يربط FunSearch توليد البرامج بالنموذج اللغوي بدالة تقييم وقاعدة بيانات للمرشحين وانتقاء الجمهرة، ويستخدم المرشحين ذوي الدرجات المرتفعة لبناء الموجّهات اللاحقة. يتضمن البرنامج بوصفه مخرجًا بنية قابلة للتفسير أكثر مما تتضمنه إجابة منفردة، لكن دالة التقييم تحدد المسألة التي يحسّنها النظام فعليًا. إذا اقتصر التقييم على حالات محدودة، فإن الدرجة المرتفعة تدعم الأداء على تلك الحالات؛ وإذا استوفى البناء الناتج قيودًا قابلة للفحص المستقل، أمكن تكوين أدلة أقوى. يقترح هذا المقال التعامل مع مواصفات المسألة والمقيّم والباحث بوصفها ثلاثة كائنات تُدار إصداراتها على نحو منفصل، وعدم تسمية «اجتياز البرنامج للتشغيل» مباشرةً برهانًا رياضيًا.[2] Mathematical discoveries from program search with large

4. اشتقاق هذا المقال: زيادة أخذ العينات تحسّن احتمال الوجود، ولا تضمن اختيار الإجابة الصحيحة

إذا افترضنا أن كل مرشح مستقل صحيح باحتمال p، فإن احتمال وجود مرشح صحيح واحد على الأقل بين n من العينات يساوي 1−(1−p)^n. تصف هذه العلاقة تغطية مجموعة المرشحين، لكنها لا تتضمن أيّهم سيختاره المتحقق. إذا كان الترابط بين المرشحين قويًا، فإن افتراض الاستقلال يبالغ في تقدير الفائدة؛ وإذا أصدر المتحقق قبولًا خاطئًا، فقد تؤدي زيادة العينات أيضًا إلى زيادة فرص اجتياز المرشحين الخاطئين. يرسم الشكل التغطية واحتمال الاجتياز الخاطئ معًا باستخدام قيم صريحة لـ p ومعدل القبول الخاطئ. وهو لا يقدّر أداء أي مبرهن آلي فعلي، بل يوضح وجوب الإبلاغ عن ميزانية البحث مع قواعد الاختيار والتحقق.作者分析与复核建议 / Author analysis

5. تحليل هذا المقال: ينبغي تحسين ميزانيتي التحقق والاقتراح معًا

لتكن ميزانية الوقت الكلية B، وتكلفة كل اقتراح cg، وتكلفة كل فحص cv؛ عندئذ لا يتجاوز عدد المرشحين المفحوصين بالكامل الجزء الصحيح الأدنى من B/(cg+cv). قد يقلل المتحقق الأكثر تعقيدًا القبول الخاطئ، لكنه يقلل عدد المرشحين الممكن فحصهم؛ وقد يولّد المقترح الأسرع أيضًا أعدادًا كبيرة من الكائنات المكررة. يقترح هذا المقال اعتماد «الأدلة الصالحة القابلة لإعادة التنفيذ المكتسبة لكل وحدة ميزانية» بوصفها النتيجة النهائية المستهدفة، وتسجيل تكاليف التوليد وإزالة التكرار والتحقق والشهادة النهائية كلًّا على حدة. إن وصف سرعة التمرير الأمامي للنموذج وحدها بأنها تسريع للاكتشاف يُغفل مراحل التوسيع الرمزي أو الترجمة البرمجية أو إعادة التنفيذ المستقلة التي قد تكون الأكثر استهلاكًا للوقت.作者分析与复核建议 / Author analysis

6. المثال المضاد في هذا المقال: الاختبارات المحدودة لا تثبت الصحة على مدخلات غير محدودة

لأي مجموعة منتهية من نقاط الاختبار، يمكن بناء كثير حدود يساوي صفرًا عند جميع تلك النقاط، ولا يساوي صفرًا عند نقاط أخرى. ومن ثم، لا يضمن اجتياز دالة مرشحة لجميع العينات المحدودة استيفاءها الخاصية نفسها على مجال غير محدود. يستخدم هذا المقال نقاط الاختبار 0 و1 و2 و3 ومربع كثير حدود لبناء منحنى توضيحي: يجتاز الاختبارات تمامًا عند نقاطها، وينحرف سريعًا خارجها. لا ينفي هذا المثال المضاد قيمة التجارب العددية، بل يقتضي تسمية الأدلة بدقة. فللاستقصاء الشامل على مجال منتهٍ والبناء القابل للتحقق والبرهان الصوري والاختبار التجريبي درجات مختلفة من القوة المنطقية، ولا يجوز حجبها تحت وسم موحد هو «اجتاز التحقق».作者分析与复核建议 / Author analysis

7. لفحص البرهان أيضًا حدود تتعلق بالمواصفات والقاعدة الموثوقة

يمكن لفاحص مستقل صغير أن يقلص بدرجة كبيرة نطاق الشيفرة التي يلزم الوثوق بها، لكن لا بد مع ذلك من مراجعة البديهيات والدلالات والنواة الحسابية وترجمة المدخلات. يقترح هذا المقال الفصل بين الأدوات المعقدة المستخدمة أثناء البحث وإعادة تنفيذ الشهادة النهائية: يجوز للبحث استخدام استدلالات إرشادية، بينما يعتمد الاستنتاج النهائي على خطوات واضحة قابلة للفحص. وإذا وُجدت استدعاءات عددية خارجية أو افتراضات غير مبرهنة أو إضافات بشرية بعد انتهاء المهلة، فينبغي إدراجها صراحةً في الشهادة. قبول الفاحص لبرهان يعني صحته بالنسبة إلى المنظومة المعطاة، ولا يعني أن نمذجة المسألة الواقعية الأصلية أو قياسها قد ثبتت صحتهما أيضًا.作者分析与复核建议 / Author analysis

8. تتأثر الدرجات الناتجة عن البحث بسهولة باختيار المقيّم

إن تكرار التحسين وفق المقيّم نفسه يعادل تحويله تدريجيًا إلى هدف تدريب. تستفيد الحلقة المغلقة في FunSearch من هذه الآلية للعثور على برامج أفضل؛ لكن المقارنة البحثية تحتاج أيضًا إلى تثبيت حالات اختبار خارجية أو إلى برهان مستقل للحكم على قابلية الانتقال. يقترح هذا المقال تسجيل جميع جولات البحث وعائلات المرشحين وأوقات تعديل المقيّم، وتخصيص أحجام أو بُنى للحالات لم تشارك في البحث. إذا لم تتحسن طريقة إرشادية إلا على توزيع مألوف، فينبغي وصفها بأنها استراتيجية فعالة لذلك التوزيع، لا بأنها مبرهنة تعمم على أحجام اعتباطية.[2] Mathematical discoveries from program search with large[3] Let's Verify Step by Step

9. ينبغي التمييز في الاكتشافات الجديدة بين قيم عددية جديدة وبناءات جديدة ومبرهنات جديدة

إن رفع الحد السفلي لمسألة منتهية معينة، والعثور على بناء ممكن أفضل، واكتشاف انتظام، وإثبات قضية عامة، كلها نتائج قيّمة، لكن أشكال تسليمها تختلف. يقترح هذا المقال بطاقة اكتشاف تضم المواصفات الأصلية وخط الأساس المعروف والبرنامج المرشح والفحص المستقل ونطاق المدخلات المنطبق والأجزاء غير المبرهنة. إذا تضمن البرنامج المرشح بنية يمكن تفسيرها رياضيًا، فينبغي إدراج الانتظام منفصلًا بوصفه فرضية جديدة، ثم تقديم برهان أو اختبار بأمثلة مضادة. ولا يجوز الادعاء تلقائيًا بأنه حل مسألة رياضية عامة لمجرد أن النموذج ولّد برنامجًا لم يكتبه البشر من قبل.作者分析与复核建议 / Author analysis

10. ينبغي أن تجعل المقارنة القابلة لإعادة الإنتاج الإخفاقات قابلة للتفسير أيضًا

نقترح تسجيل مجموعة مسبقًا بحسب نوع المسألة وتعقيدها، مع مضاهاة الميزانية الكلية للحوسبة والعمل البشري بين المناهج. وتكون النتيجة الأساسية نسبة المسائل التي تنجح إعادة تنفيذ شهاداتها بصورة مستقلة، وتكملها أحجام الشهادات وزمن البحث وإخفاقات الترجمة. وينبغي إحصاء تعذر التعبير، وعدم العثور على حل، ورفض الفحص، ونفاد الموارد، كلًّا على حدة. عندئذ فقط يمكن تحديد ما إذا كان المنهج الجديد يحسّن توليد الكائنات أو القدرة الاستدلالية أو استراتيجية البحث أو معدل الإنجاز الهندسي، بدل اختزال جميع الإخفاقات في وسم «غير محلولة» يصعب تشخيصه.作者分析与复核建议 / Author analysis

ملحق تقني A · يكشف مخطط الاعتماد المساهمة الفعلية للمقترح

إن ظهور نقطة مساعدة في الرسم النهائي لا يعني أن البرهان يحتاج إليها فعلًا. يمكن تتبع اعتماد الاستدلال عكسيًا انطلاقًا من الاستنتاج المستهدف، وحذف المقدمات والعناصر الوسيطة غير ذات الصلة، ثم إعادة تنفيذ الشهادة المتبقية بصورة مستقلة. تُظهر الأعمال المرتبطة بـ AlphaGeometry أهمية تتبع الاعتماد. يقترح هذا المقال حفظ الشهادات قبل التقليص وبعده مع الشروط المحذوفة؛ وإذا نتجت قضية أكثر عمومية بعد حذف مقدمات، فينبغي إعادة مراجعة شروط النطاق وعدم الانحلال في المسألة الأصلية. إن تبسيط مخطط الاعتماد يوفر خيطًا للاكتشاف، وليس اختصارًا يجيز تجاهل الفروق الدلالية.[1] Solving olympiad geometry without human demonstrations

ملحق تقني B · يغيّر البحث التكيفي العينة الفعالة

يُولَّد المرشحون من البرامج الفائزة في الجولات السابقة، ولذلك تترابط درجاتهم وبُناهم. إن اعتبار جميع المرشحين عينات برنولية مستقلة يبالغ في تغطية البحث؛ كما أن إحصاء الجمهرة النهائية وحدها قد يخفي مقدارًا كبيرًا من الحسابات الفاشلة. يقترح هذا المقال اعتماد تشغيلات البحث المستقلة والمسائل بوصفها الوحدات الإحصائية الأساسية، مع الاحتفاظ بعلاقات النسب وكشف التكرار. ولمقارنة المولّدات، ينبغي تثبيت قواعد التقييم والجمهرة؛ أما مقارنة الأنظمة الكاملة فتقتضي مضاهاة الميزانية الكلية وإجراء دراسات استئصال للمكونات. ينبغي أن يتوافق مستوى الاستقلال الإحصائي مع الادعاء، ولا يجوز الاستعاضة بعدد هائل من المرشحين عن عدد قليل من المسائل المستقلة.[2] Mathematical discoveries from program search with large

ملحق تقني C · تختلف ثغرات المقيّم عن الأمثلة المضادة الرياضية

قد يستغل البرنامج تفاصيل التنفيذ أو الفيض الحسابي أو انتهاء المهلة أو المدخلات غير المفحوصة للحصول على درجة مرتفعة، ولا يشكل ذلك بالضرورة تحسينًا صالحًا للهدف الرياضي. يقترح هذا المقال إجراء فحص دلالي مستقل إلى جانب التشغيل المعزول، واختبار المدخلات الحدّية والمتطرفة والمنظّمة؛ وإذا كانت النتيجة بناءً ممكنًا، فينبغي أيضًا إعادة فحص القيود بتنفيذ برمجي مختلف. يجب تسجيل اكتشاف ثغرة في المقيّم بوصفه عيبًا هندسيًا، ولا يجوز احتسابه اكتشافًا رياضيًا. وفي المقابل، فإن المثال المضاد الصحيح الذي يدحض الحدسية الأصلية نتيجة علمية، ويلزم التمييز الواضح بينهما بالاستناد إلى المواصفات والفحص المستقل.作者分析与复核建议 / Author analysis

ملحق تقني D · للاستقصاء الشامل على مجال منتهٍ حدود واضحة

لا تشكل الاختبارات المحدودة برهانًا على مجال غير محدود، لكن إذا كان مجال المسألة أصلًا مجموعة منتهية محددة بدقة، فيمكن للاستقصاء الشامل أن يوفر دليلًا قويًا، بشرط خلو التعداد من السهو وصحة الفاحص. يقترح هذا المقال تسجيل حجم المجال وقواعد التعداد وإزالة التكرار وتغطية الأجزاء، وتوفير مراجعة مستقلة للعدد الكلي. وإذا استُخدم التناظر للاختزال، فينبغي بيان علاقة التكافؤ واكتمال الممثلين. فلا يجوز تسمية الفحص بالعينة استقصاءً شاملًا، ولا رفض برهان على مجال منتهٍ لمجرد استخدام الحاسوب؛ والمهم هو إمكان التأكد المستقل من النطاق والتغطية.作者分析与复核建议 / Author analysis

11. الخاتمة: تستمد الاكتشافات الآلية قوتها من التزامات قابلة للفحص

تكمن القيمة الأبرز للأنظمة العصبية الرمزية في تسخير القدرة الاستكشافية للنماذج التوليدية لخدمة قيود منطقية أو برمجية واضحة. تبين تحليلات الاحتمال والميزانية والمثال المضاد للاختبارات المحدودة في هذا المقال وجود خطوات لا يمكن تجاوزها بين العثور على مرشح واجتياز التقييم والحصول على برهان. ينبغي أن تتيح المواد المنشورة لقارئ لا يثق بالنموذج التوليدي أن يفحص الاستنتاجات الأساسية، وأن يعرف فئة المسائل التي تنطبق عليها الأدلة. عندئذ تتاح لهذه الاكتشافات فرصة أن تصبح معرفة رياضية قابلة للتراكم والمقارنة والتعميم.作者分析与复核建议 / Author analysis

الصيغ والاشتقاقات الأساسية

مسار المنهج والأدلة

رسوم تحليلية وأمثلة عددية

مثال قابل لإعادة الحساب

عندما يكون p=0.1 وn=20، يبلغ احتمال الصحة مرة واحدة على الأقل نحو 0.878423؛ وتساوي g القيمة 0 عند جميع نقاط 0,1,2,3، لكن g(0.5)=0.87890625؛ فالاختبارات المحدودة لا تثبت خاصية على مجال غير محدود.

مقارنة المناهج

خطة إعادة الفحص والتجارب

1. تثبيت المسألة الأصلية والمواصفات الصورية، ومراجعة شروط عدم الانحلال والنطاق صراحةً.
2. إدارة إصدارات الباحث والمقيّم والفاحص النهائي كلٍّ على حدة.
3. مضاهاة الميزانية الكاملة للحوسبة والعمل البشري، وتسجيل تكاليف التوليد والتحقق.
4. الاحتفاظ بجميع عمليات البحث وعائلات المرشحين، وتجنب احتساب المكررات عينات مستقلة.
5. التحقق باستخدام حالات مستقلة أو إعادة تنفيذ الشهادات، وتسجيل الأجزاء غير المبرهنة على نحو منفصل.
6. التمييز بين تعذر التعبير، وعدم العثور على حل، ورفض الفحص، ونفاد الموارد.
7. الإبلاغ عن درجات الأدلة المختلفة للبناءات والحدود السفلية والانتظامات التجريبية والمبرهنات العامة.
8. تسليم أدلة يمكن إعادة تنفيذها دون استدعاء النموذج التوليدي، وعدم وصف المثال المضاد في هذا المقال بأنه اكتشاف لمبرهنة جديدة.

نطاق الانطباق والقيود

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

أدلة الدراسات الأصلية ونطاق انطباقها

أسئلة بحثية جديرة بالاختبار

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

المصادر الأولية وما يقابلها من ادعاءات

1. Solving olympiad geometry without human demonstrationsTrinh et al. · 2024-01-17IMO-AG-30: 25/30; geometry-language coverage and excluded problem types; author correction noted.
2. Mathematical discoveries from program search with large language modelsRomera-Paredes et al. · 2023Program generation, evaluation function, population database and search; evaluator validity is part of the system.
3. Let's Verify Step by StepLightman et al. · 2023-05-31v1 abstract; process vs outcome supervision