Type-Checked Compliance: Deterministic Guardrails for Agentic Financial Systems Using Lean 4 Theorem Proving
تقدم هذه الورقة بروتوكول (Lean-Agent)، وهو نظام تحقق رسمي يستخدم إثبات النظريات عبر لغة (Lean 4) لضمان امتثال إجراءات الذكاء الاصطناعي المالي المستقل للمتطلبات التنظيمية الصارمة رياضياً، مما يستبدل الحواجز الوقائية الاحتمالية غير الكافية بسلامة حتمية وقابلة للتحقق تشفيراً.
البحث الأصلي مرخَّص بموجب CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). هذا شرح مولَّده بالذكاء الاصطناعي للبحث أدناه. لم يكتبه المؤلفون ولم يصادقوا عليه. وللتحقق من الدقة التقنية، يرجى الرجوع إلى البحث الأصلي. اقرأ إخلاء المسؤولية الكامل
تخيل أنك توظف مساعداً آلياً (روبوتاً) عبقرياً، فائق السرعة، ولكنه غير متوقع بعض الشيء لإدارة الشؤون المالية لعائلتك. هذا الروبوت (الذكاء الاصطناعي الوكيل - Agentic AI) يمكنه قراءة الأخبار، والتحقق من أسعار الأسهم، واتخاذ قرار بشراء أو بيع الاستثمارات في أجزاء من الملي ثانية. إنه ذكي للغاية، لكن لديه عيب واحد: هو احتمالي (Probabilistic). وهذا يعني أنه يخمن الإجابة الأفضل بناءً على الأنماط، تماماً مثل طالب يخمن الإجابة في اختبار خيارات متعددة. في بعض الأحيان يكون محقاً، ولكن في أحيان أخرى "يهلوس" ويرتكب خطأً قد يكلفك كل أموالك.
الآن، تخيل أن لديك مديراً صارماً للبنك (المنظم/الرقيب) يقول لك: "لا يمكنك خسارة قرش واحد. يجب أن تتبع كل عملية تداول القانون بدقة، وإلا سنغلق نشاطك".
المشكلة هي؟ لا يمكنك الوثوق بروبوت يعتمد على التخمين لاتباع قوانين صارمة. إذا خمن الروبوت بشكل خاطئ، فستتعرض لغرامة أو تفقد ترخيصك.
تقدم هذه الورقة حلاً يسمى بروتوكول "لين-آيجنت" (Lean-Agent Protocol). فكر في الأمر كبناء حارس أمن رياضي لمساعدك الآلي.
إليك كيف يعمل، باستخدام تشبيهات بسيطة:
1. المشكلة: الروبوت "الذي يخمن" مقابل القانون "الصارم"
- الروبوت (نموذج اللغة الكبير - LLM): تخيل طباخاً يعد وجبات مذهلة ولكنه أحياناً ينسى الوصفة أو يضيف الملح بدلاً من السكر. إنه يعمل بنسبة 99% من الوقت، لكن نسبة الخطأ البالغة 1% تلك خطيرة في عالم التمويل.
- الحل الحالي (القيود القديمة): اليوم، تستخدم الشركات "مرشحات محتوى" تشبه حراس الأمن الذين ينظرون إلى وجه الطباخ ويخمنون: "هممم، يبدو أن هذا الطبق خطير، ربما يجب إيقافه؟". هؤلاء الحراس يخمنون أيضاً، وقد يفوتهم طبق خطير إذا بدا بريئاً.
- حل الورقة البحثية: بدلاً من حارس يخمن، نحن بحاجة إلى آلة حاسبة رياضية تثبت أن الطبق آمن قبل خروجه من المطبخ.
2. الحل: "الحارس الرياضي" (Lean 4)
يستخدم المؤلفون لغة حاسوبية خاصة تسمى Lean 4. لا تنظر إلى Lean 4 كلغة برمجة، بل كـ آلة للحقيقة المطلقة.
- الترجمة (نموذج أرسطو): أولاً، يستخدمون ذكاءً اصطناعياً ذكياً (يسمى "أرسطو") لقراءة القواعد القانونية المملة والمعقدة (مثل "لا تنفق أكثر من 10% من أموالك") وترجمتها إلى معادلات رياضية.
- تشبيه: تخيل ترجمة ملاحظة مكتوبة بخط يد فوضوي إلى صيغة رياضية مثالية وغير قابلة للتغيير.
- التخمين/الفرضية (الطلب): عندما يريد المساعد الآلي إجراء عملية تداول، فإنه لا يقوم بها فحسب. بل يجب عليه تقديم برهان رياضي إلى الحارس.
- تشبيه: يقول الروبوت: "أريد شراء 500 سهم من شركة أبل". الحارس لا يكتفي بالإيماء برأسه، بل يقوم بعملية حسابية:
500 سهم * السعر < 10% من إجمالي رأس المال.
- تشبيه: يقول الروبوت: "أريد شراء 500 سهم من شركة أبل". الحارس لا يكتفي بالإيماء برأسه، بل يقوم بعملية حسابية:
- الحكم:
- إذا كانت الرياضيات صحيحة (True): يفتح الحارس البوابة. وتتم عملية التداول فوراً.
- إذا فشلت الرياضيات (False): يغلق الحارس البوابة بقوة. يتم حظر عملية التداول. لا يوجد تخمين، ولا يوجد "ربما". إنه رفض قاطع.
3. لماذا يعد هذا تغييراً جذرياً؟
تسلط الورقة الضوء على ثلاث قدرات خارقة لهذا النظام:
أ. السرعة (الحارس في الميكروثانية)
كان الناس يعتقدون سابقاً أن البراهين الرياضية بطيئة جداً بالنسبة للتداول عالي السرعة. تثبت الورقة أنه لأن "القواعد" محسوبة مسبقاً، فإن التحقق من عملية تداول واحدة يستغرق 5 ميكروثانية (أي 0.000005 ثانية).
- تشبيه: الأمر يشبه نقطة تفتل لا توقف سيارتك للتحقق من هويتك، بل تمسح لوحة أرقامك وتعرف فوراً ما إذا كان مسموحاً لك بالمرور. إنها أسرع من رمشة عين بشرية.
ب. الإيصال "القابل للتفسير"
إذا تم حظر الروبوت، يحتاج المنظمون والعملاء إلى معرفة لماذا.
- الطريقة القديمة: "الذكاء الاصطناعي قرر أن العملية خطيرة". (غامض ومخيف).
- الطريقة الجديدة: يولد النظام إيصالاً باللغة الإنجليزية البسيطة: "تم حظر التداول لأن التكلفة (9,000)".
- تشبيه: بدلاً من حارس يقول "أنا لا أحب انطباعك"، تطبع الآلة تذكرة تقول: "مخالفة: تجاوزت حد السرعة بمقدار 5 ميل في الساعة".
ج. "السترة الواقية من الرصاص" (بيئة WASM المعزولة)
حتى لو حاول الروبوت خداع النظام أو تعرض للاختراق، فإن عملية التداول الفعلية تحدث داخل بيئة معزولة (Sandbox) من نوع WebAssembly (WASM).
- تشبه: تخيل أن الروبوت حيوان بري. نحن لا نضع حوله سياجاً فحسب، بل نضعه في قفص زجاجي يستحيل كسره مادياً. حتى لو حاول الحيوان عض الزجاج، فلا يمكنه إيذاء أي شخص خارجه. القواعد الرياضية هي الزجاج؛ ولا يمكن للروبوت الهروب منها.
4. التأثير في العالم الحقيقي
تجادل الورقة بأن هذا ليس مجرد نظرية. إنه يشبه كيفية استخدام ناسا للرياضيات لإثبات أن الصاروخ لن ينفجر قبل إطلاقه.
- قواعد SEC و FINRA: هذه هي "قوانين المرور" في التمويل. يثبت هذا النظام، رياضياً، أن الروبوت لا يتجاوز أبداً حد السرعة.
- درس "نايت كابيتال" (Knight Capital): في عام 2012، تسبب خلل في الكمبيوتر في خسارة شركة 440 مليون دولار في 45 دقيقة لأن ضوابط السلامة كانت معيبة. يضمن هذا النظام الجديد أن مثل هذا الخطأ مستحيل رياضياً.
الملخص
بروتوكول "لين-آيجنت" هو بمثابة وضع حزام أمان ووسادة هوائية رياضية لسيارة ذاتية القيادة.
- السيارة (الذكاء الاصطناعي) تقود بسرعة وتتخذ القرارات.
- حزام الأمان (Lean 4) لا يخمن؛ بل يحسب بدقة متى يجب أن ينغلق.
- إذا حاولت السيارة القيادة نحو الهاوية، فإن الرياضيات تثبت أن ذلك مستحيل، وتتوقف السيارة فوراً.
هذا يسمح للبنوك باستخدام ذكاء اصطناعي فائق الذكاء دون القلق من أن الذكاء الاصطناعي قد يكسر القانون عن طريق الخطأ أو يفقد أموال الجميع. إنه يحول "السلامة الاحتمالية" إلى سلامة مضمونة.
غارق في أبحاث مجالك؟
تصلك نشرة يومية بأحدث الأبحاث المطابقة لكلماتك البحثية المفتاحية — مع ملخصات تقنية، بلغتك.