تا حالا فکر کردی کامپیوترها چطور می‌تونن بر اساس منطق خودشون کشفیات جدید کنن؟ امروز میخوام باهات درباره یه ایده خفن و تازه صحبت کنم به اسم “Generative Logic” یا همون “منطق زاینده”. حالا اول بذار یه توضیح خودمونی بدم: منطق زاینده یعنی روشی که باهاش میشه به کامپیوتر یه سری تعریف اولیه (که بهش میگن اصل‌های اولیه یا “Axiom”) داد و این سیستم خودش شروع می‌کنه با استفاده از اون‌ها یه عالمه نکته جدید رو به شکل قطعی و بدون شانس و احتمال کشف می‌کنه.
ماجرا از جایی شروع میشه که چیزایی که به رایانه میدیم با یه زبان مدل‌سازی خیلی ساده به اسم “MPL” نوشته میشن. MPL یه زبان برنامه‌نویسی ریاضی خیلی خلاصه هست، طوری که حتی آدمایی که خیلی دنبال پیچیدگی ریاضی نیستن هم می‌تونن اصول اولیه رو توش تعریف کنن.
بعدش چی میشه؟ این تعریف‌ها وارد یه جور شبکه از بلوک‌های منطقی (Logic Blocks یا همون LBها) میشن. هرکدوم از این بلوک‌ها خیلی ساده‌ان و فقط با “پیغام دادن” به همدیگه کار می‌کنن. هر وقت یه چندتا عبارت زیر یه قانون مشخص با هم یکی شن (به این حالت میگن “Unify under an inference rule” یعنی طبق یه قاعده استنتاج چفت هم بشن)، اون موقع خود سیستم یه نتیجه جدید درست می‌کنه و دقیقا نشون میده این نتیجه از کدوم منبع اومده – یعنی کاملاً قابل پیگیری و با مدرک! این مدل، یه “گراف اثبات” می‌سازه که هر کسی هر بخششو خواست بتونه بررسی کنه.
تا اینجای کار با نرم‌افزارش اومدن برنامه معروف ریاضی پئانو (Peano Arithmetic) رو پیاده کردن. یعنی با تعریفای اولیه پئانو که همون اصلای پایه ریاضی برای عدد هست (اصلای پئانو یه سری تعریفای اساسی است که میگه مثلاً عدد صفر وجود داره، هر عددی بعدی‌ای داره، و اینا)، سیستم بدون اینکه خودش چیزی بلد باشه، شروع کرده با همین اصل‌ها کلی نتیجه جدید خودش کشف کرده! از جمله اثباتایی مثل جابجایی و شرکت‌پذیری جمع و ضرب، و توزیع‌پذیری (Associativity و Commutativity و Distributivity یعنی ترتیب یا گروه‌بندی تو جمع و ضرب مهم نباشه و اینا – خلاصه مفاهیم مهم ریاضی که دبیرستان هم باهاش درگیریم).
یه قسمت هیجان‌انگیز دیگه اینه که هر اثبات رو میشه با جزئیاتش به صورت یه فایل HTML خروجی گرفت و بعدش هر قدم استدلال رو میشه جدا جدا دید و بررسی کرد. یعنی دیگه از این شفاف‌تر نمی‌شه!
تازه، برنامه‌نویسای این پروژه گفتن که دارن به این فکر می‌کنن معماریش رو طوری طراحی کنن که هم سخت‌افزار و هم نرم‌افزارش بتونه همزمان و به تعداد بالا (Massively Parallel یعنی کارهای خیلی زیاد رو یک جا) کار کنه. حتی می‌خوان این سیستم رو بعداً با مدل‌های احتمالاتی مثل “مدل‌های زبانی بزرگ” (Large Language Models یا همون LLMها که ChatGPT هم یکی از نمونه‌هاشونه!) ترکیب کنن تا اتوماتیک‌تر بتونه حدس و گمان علمیش رو مطرح کنه یا حتی خودش قضیه‌های جدید بسازه و اثبات کنه!
کدهای پیاده‌سازیش هم رایگان گذاشتن توی گیت‌هاب این پروژه (https://github.com/Generative-Logic/GL/tree/35a111ea9ba53afe051703d6050be0c3923e9724) و یه بایگانی هم دائمیش رو اینجا گذاشتن (https://doi.org/10.5281/zenodo.16408441). خلاصه اگر واقعا به این موضوع علاقه‌مندی یا دوست داری تستش کنی، دستت کاملاً بازه!
در نهایت، بچه‌های این پروژه خیلی استقبال کردن که هر کسی نظر یا همکاری‌ای داشت واردش بشه و با ایده‌هاش به بهتر شدنش کمک کنه. پس اگه دنبال موضوعات نسل جدید هوش منطقی و اتوماسیون ریاضی هستی، این دقیقاً همون چیزیه که باید بری سراغش!
منبع: +
