توليد الفرضيات بالـLLM مقابل التحقق من البراهين

في مكان ما بين فنجان القهوة الثاني والثالث، قرأ كثير من منظّري التعقيد مؤخرًا جملة لم يتوقعوا أن يقرأوها أبدًا: خوارزمية حتمية تعدّ الإسنادات المُرضية لأي صيغة منطقية بوليانية في زمن يقارب 2^(n/√(log n)) — أي دون الأسّية (sub-exponential) بالمعنى التقني الدقيق الذي يُبطل فرضية الزمن الأسّي (ETH)، وهي إحدى الافتراضات الأساسية التي يقوم عليها المجال. لم تصدر هذه الادعاءات عن مجموعة جامعية على arXiv، بل جاءت من مختبر ذكاء اصطناعي، وطُوّر البرهان بالتعاون مع نموذج لغوي كبير. مهما كان رأيك في الإعلان، فهو يسجّل اللحظة التي خرج فيها توليد الفرضيات — أي أن تقترح الآلات رياضيات جديدة بدلًا من أن تكتفي بتصحيحها — من مرحلة العروض التجريبية.

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

ما الذي يدّعيه إعلان الرياضيات بالذكاء الاصطناعي فعلًا

لنبدأ بنتيجة التعقيد لأن رهاناتها الأوضح. تقول فرضية الزمن الأسّي تقريبًا إن مسألة 3-SAT لا يمكن حلّها في زمن 2^o(n) — أي لا توجد خوارزمية يمكن أن تكون دون أسّية بشكل ملموس بدلالة عدد المتغيرات. تعتمد المئات من الأوراق البحثية في التعقيد المعلمي والتعقيد الدقيق على ETH لإثبات حدود دنيا؛ وهي من الافتراضات التي يُبنى عليها عقد كامل من نظريات «بشرط ETH». تصف الورقة الجديدة خوارزمية عدّ حتمية لصيغ k-CNF تستخدم مساحة متعددة الحدود وتعمل في زمن 2^(n/(log n)^(1/2+o(1))) مضروبًا في عامل متعدد الحدود. هذا الأس هو o(n)، وهو بالضبط ما تحظره ETH. الخوارزمية ما زالت بطيئة بوحشية — لن يشغّلها أحد على مثال حقيقي — لكنها حاسمة من الناحية التقاربية. إن صحّ البرهان، فإن فرضية هيكلت عشرين عامًا من حجج الحدود الدنيا ستتوقف ببساطة عن الوجود.

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

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

التحقق من البراهين مقابل توليد الفرضيات: مهمتان مختلفتان

بعد إزالة الضجيج، تقوم كل منظومة ذكاء اصطناعي في الرياضيات بواحدة من مهمتين. المهمة الأولى هي التحقق من البراهين: تعطى حجة مرشحة، فتقرر إن كانت صحيحة. المهمة الثانية هي توليد الفرضيات: تعطى مجالًا بحثيًا، فتقترح ما يستحق المحاولة — مبرهنة مساعدة، أو بناءً، أو خوارزمية، أو مثالًا مضادًا. تبدو المهمتان كنصفين لمهارة واحدة، لكنهما ليستا كذلك. إنهما مسألتان حسابيتان مختلفتان، لكل منهما «أوراكل» مختلف، وأنماط فشل مختلفة، وملامح ثقة مختلفة جذريًا، والخلط بينهما هو ما يجعلك إما تثق زيادة عن اللزوم ببيان صحفي، أو تتجاهل تقدمًا حقيقيًا.

للتحقق أوراكل. البرهان المكتوب في Lean إما أن يتجمع مقابل النواة أو لا يتجمع، والنواة لا تهتم بمدى ثقة الكاتب في نفسه. يفشل التحقق بصوت مرتفع، فكتلة تكتيكية مرفوضة لا لبس فيها. أما التوليد فلا أوراكل له. قد تكون الفرضية المقترحة صحيحة، أو خاطئة، أو صحيحة بديهيًا، أو صحيحة لكنها منشورة عام 1987 بترميز مختلف. يفشل التوليد بهدوء، وأنماط فشله اجتماعية: هراء يبدو معقولًا، أو نتائج حقيقية متنكرة في ثوب الجِدّة. تُقاس الجودة هنا بالأهمية والأصالة، وهما خاصيتان يحددهما الذوق البشري لا أي معيار قابل للحسم.

لماذا صار التوليد جيدًا بما يكفي ليُعتدّ به فجأة؟ لأن نماذج الاستدلال الحديثة تُدرَّب على سلاسل تفكير طويلة، لا تُدفع إليها بالتوجيه فقط — فالتعلم المعزز بمكافآت قابلة للتحقق، وأغلبها في الرياضيات والبرمجة حيث يمكن فحص الإجابات آليًا، علّم هذه الأنظمة أن تبحث فعلًا في فضاء من الخطوات بدلًا من إكمال تسلسل واحد. التشبيه الذي أنصحك بتذكّره: المدقق مُجمِّع، والمولّد مصمم. كلاهما قيّم. لن تسمح أبدًا للمصمم بأن يعتمد عمله بنفسه.

البرهان الذي لا تستطيع فحصه موعظة، والحدس الذي لا تستطيع اختباره إشاعة.

أين يتفوق التحقق الآلي من البراهين

يتفوق المدقق حيثما توجد حقيقة أرضية صورية، والعمل المراجَع طويل أو مُمل أكثر من أن يدققه إنسان سطرًا سطرًا. أصبحت Lean 4 ومكتبتها المجتمعية Mathlib الساحة المرجعية هنا: تكتب التعريفات والبراهين بلغة برمجة، ونواة صغيرة يمكن تدقيقها منفصلة تقرر إن كانت كل خطوة استدلال قانونية. قاعدة الثقة المطلوبة صغيرة جدًا مقارنةً بجبل الرياضيات المبني فوقها، وهذا بالضبط عدم التماثل الذي تريده.

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

import Mathlib
-- The sum of two even natural numbers is even.
theorem even_add_even {a b : ℕ} (ha : Even a) (hb : Even b) : Even (a + b) := by
rcases ha with ⟨k, rfl⟩   -- a = k + k for some k
rcases hb with ⟨l, rfl⟩   -- b = l + l for some l
exact ⟨k + l, by ring⟩    -- witness k + l; ring closes the algebra

لاحظ ما يوضحه المثال عن تقسيم العمل. الحركة الإبداعية هي اختيار الشاهد k + l؛ وحركة التحقق هي تحقق ring من الجبر. يُجيد البشر والنماذج كلاهما الأولى. ولا تُوثق إلا النواة في الثانية، وهي لا تتعب ولا تتصفح ولا تقيّم بالانطباع. أكثر عناصر الإعلان مصداقية هو بالضبط هذه البوابة: الادعاء بأن ورقة الفيزياء حُجبت حتى اكتمال صياغتها في Lean. إن كانت الرواية دقيقة، فهذا مثال على سير العمل وهو يعمل كما يجب: تقترح الآلة، وتُحكِم الآلة، ويُنتظر البيان الصحفي دوره.

أين يتفوق توليد الفرضيات

يتفوق التوليد حيثما يكون فضاء البحث توافقيًا والتقييم رخيصًا. وضعت DeepMind مع FunSearch في 2023 القالب الأساسي: يقترح نموذج لغوي فرضيات على هيئة برامج، ويقيّمها مقيِّم سريع، وتحتفظ حلقة تطورية بالأفضل. أنتج هذا الإعداد بنى جديدة لمجموعات الأغطية (cap sets) وإرشادات تعبئة (bin-packing) أفضل من عقود من الضبط اليدوي. وطوّر AlphaEvolve الفكرة نفسها أبعد، فكان من نتائجه أنه وفّر عملية ضرب واحدة في خوارزمية ضرب مصفوفات 4×4 ظلّت قائمة منذ زمن Strassen. لا يدّعي أحد أن هذه الأنظمة تفهم الهندسة. ولا تحتاج إلى ذلك. تحتاج إلى أن تقترح، ويحتاج المقيِّم إلى أن يكون أمينًا.

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

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

بناء حلقة تحقق للبراهين المولّدة بالذكاء الاصطناعي

إن أردت فوائد الرياضيات المولّدة آليًا دون الإحراج، فسير العمل أهم من النموذج. هذا هو الخط الذي أشغّله، بالترتيب:

1. وَلِّد على نطاق واسع وبتكلفة منخفضة. التنوع يتفوق على العمق في هذه المرحلة؛ تريد تغطية فضاء الأفكار لا محاولة واحدة مصقولة.
2. أزل التكرار مقابل الأدبيات. الاسترجاع عبر arXiv وMathOverflow يلتقط الفشل الأكثر شيوعًا: فرضية «جديدة» هي في الحقيقة نتيجة معروفة مرتدية ترميزًا غير مألوف.
3. طبّق مرشحات تجريبية رخيصة. اختبر الحالات الصغيرة عدديًا، وابحث حاسوبيًا عن أمثلة مضادة، ودع العبارات الخاطئة بوضوح تموت بسرعة.
4. صُغ الناجيات رسميًا. Lean أو Isabelle أو Rocq — اختر مساعد البراهين الذي تريده، لكن افهم أن هذه الخطوة هي الأغلى، وأن البرهان باللغة الطبيعية مسودة لا نتيجة.
5. مراجعة بشرية للجِدّة والصياغة. هل يهم هذا؟ هل العبارة هي الصحيحة أصلًا؟ النماذج تُحسّن ما يمكن إثباته؛ والبشر يقررون ما يستحق الإثبات.

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

لماذا ما زال علماء الرياضيات البشر يحرسون بوابة الصحة

لا يستطيع أي مُحقِّق أن يخبرك أن مبرهنة مهمة. اختيار المسألة ذوق، والذوق تقنية اجتماعية بُنيت عبر عقود — الندوات، وتقارير المحكّمين، والإجماع البطيء حول أي الأسئلة تفتح الأبواب وأيها طرق مسدودة. وشكّ المجتمع البحثي في إعلانات الشركات ليس حراسة لذاتها؛ إنه جهاز مناعة، وأجهزة المناعة تبالغ أحيانًا تحديدًا لأن عدم التفاعل قاتل.

ثم هناك النسب. تُدرَّب هذه النماذج على أسئلة المجتمع ومسوداته ومنشورات منتدياته، وهذا يفتح احتمالًا مزعجًا: أن يكون «الاكتشاف» المحتفى به إعادة تركيب لأشياء كتبها محكّموه المستقبليون. الخوف من منافسة أداتك لنفسك ليس وسواسًا، بل هو مشكلة في سلسلة نسب البيانات، وإلى أن تستطيع المختبرات إثبات النسب، سيبقى المحكّمون البشر أدوات الكشف عن الانتحال الوحيدة التي تعمل. أضف إلى ذلك سياسة الاعتماد — من يُدعى للتحقق، وأي أسماء تظهر في الإعلان، واتهامات المحاباة — وستفهم لماذا لا يمكن إزالة البوابة البشرية. اختيار خمسة علماء بارزين لتزكية نتيجة هو فعل سياسي بقدر ما هو معرفي.

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

التوصية: ثق بالحلقة، لا بالنموذج

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

عامِل النموذج إذن كشريك مبتدئ غزير الإنتاج، لا حدود لطاقته ولا حكم لديه: كل ما يقدمه يمر عبر مساعد البراهين قبل أن يدخل الورقة، ويمر عبر إنسان ذي ذوق قبل أن يدخل المقدمة. إن كنت باحثًا، فتعلّم مساعد براهين واحدًا بإتقان، فالصياغة الرسمية هي عنق الزجاجة، والأشخاص القادرون على قيادتها على وشك أن يصبحوا مشغولين جدًا. وإن كنت تبني أدوات، فابنِ الحلقة لا العرض التوضيحي. وحين يصل الإعلان الكبير التالي، تجاوز البيان الصحفي، وافتح الورقة الأولية، وتحقق إن كان مستودع Lean موجودًا. الادعاءات التي تصمد هي التي تصل وقد جرى فحصها آليًا.