شرکت OpenAI مجموعه‌ای شامل ۳۷۲ نتیجه ریاضی جدید را منتشر کرده که توسط یک مدل پیشرفته داخلی این شرکت تولید شده‌اند. هر نتیجه قرار است یک مسئله باز ریاضی را حل کند یا پیشرفت قابل توجهی در مسیر حل آن ارائه دهد. نکته مهم اینکه OpenAI به‌جای انتشار این اثبات‌ها در مجلات علمی سنتی، آن‌ها را همراه با سوابق بازبینی و منابع در GitHub قرار داده و برای بسیاری از نتایج نیز از اثبات رسمی و قابل بررسی توسط ماشین استفاده کرده است.
🔹 شرکت OpenAI تعداد ۳۷۲ نتیجه ریاضی تولیدشده توسط یک مدل پیشرفته داخلی را منتشر کرده است.
🔹 هر نتیجه برای حل یک مسئله باز یا ایجاد پیشرفتی قابل توجه در آن ارائه شده و برخی به الگوریتم‌های مهم و فرضیه ریمان مربوط هستند.
🔹 تقریباً تمام نتایج با یک پرامپت و یک عامل هوش مصنوعی تولید شده‌اند و هر نتیجه به‌طور متوسط حدود سه ساعت محاسبات ChatGPT Pro Thinking مصرف کرده است.
🔹 بسیاری از اثبات‌ها با زبان Lean رسمی‌سازی شده‌اند تا درستی منطقی آن‌ها به‌صورت ماشینی قابل بررسی باشد.
🔹 انتشار نتایج در GitHub و نه مجلات داوری‌شده، بحث‌هایی درباره شیوه ارزیابی حجم عظیم ریاضیات تولیدشده توسط هوش مصنوعی ایجاد کرده است.
شرکت OpenAI اعلام کرده یک مدل پیشرفته داخلی این شرکت موفق به تولید ۳۷۲ نتیجه ریاضی جدید شده است. براساس توضیحات ارائه‌شده، هرکدام از این نتایج باید یک مسئله باز را حل کرده یا پیشرفت قابل توجهی در مسیر حل آن ایجاد کرده باشند.
دامنه نتایج منتشرشده گسترده است و از بهبود الگوریتم‌های مهم کامپیوتری تا پیشرفت‌هایی مرتبط با فرضیه ریمان را شامل می‌شود.
تمام این نتایج در یک مخزن GitHub قرار گرفته‌اند که علاوه بر اثبات‌ها، شامل سوابق بازبینی و تغییرات و همچنین ارجاعات و منابع است.
براساس اعلام OpenAI، تقریباً تمام نتایج از یک پرامپت برای یک عامل هوش مصنوعی به دست آمده‌اند، هرچند برای دستیابی به برخی از آن‌ها چند تلاش لازم بوده است.
این روش تفاوت قابل توجهی با راهکار استفاده‌شده برای مسئله Navier-Stokes دارد. طبق اطلاعات منتشرشده، حل آن مسئله به مجموعه‌ای متشکل از ۱۰ هزار عامل هوش مصنوعی و میلیون‌ها دلار توان محاسباتی نیاز داشت و نتیجه آن نیز چند هفته است که تحت بررسی رسمی قرار دارد.
در مقابل، برای هرکدام از نتایج مجموعه جدید به‌طور متوسط معادل حدود سه ساعت توان محاسباتی ChatGPT Pro Thinking مصرف شده است.
یکی از مهم‌ترین بخش‌های پروژه، استفاده از اثبات رسمی است. بسیاری از اثبات‌های منتشرشده با Lean رسمی‌سازی شده‌اند و OpenAI قصد دارد تعداد بیشتری از نتایج را نیز در آینده به این شکل ارائه کند.
زبان Lean برای نوشتن اثبات‌های ریاضی به شکلی طراحی شده است که درستی منطقی آن‌ها توسط ماشین قابل بررسی باشد. استفاده از چنین روشی در شرایطی اهمیت بیشتری پیدا می‌کند که هوش مصنوعی قادر به تولید حجم بسیار زیادی از نتایج ریاضی باشد.
دلیل این رویکرد تا حد زیادی عملی است. اگر مدل‌های هوش مصنوعی بتوانند صدها یا هزاران نتیجه جدید تولید کنند، بررسی دستی تمام آن‌ها می‌تواند از ظرفیت جامعه ریاضی فراتر برود.
انتشار ۳۷۲ نتیجه ریاضی جدید OpenAI
شرکت OpenAI در کنار نتایج، جزئیاتی درباره روش انجام پروژه نیز منتشر کرده است. این اطلاعات شامل خلاصه‌هایی از فرایند استدلال، آمار مربوط به تعداد مسائل امتحان‌شده توسط مدل و برآورد هزینه محاسباتی می‌شود.
با این حال، تمام جزئیات منتشر نشده‌اند. OpenAI پرامپت‌های مورد استفاده را در دسترس قرار نداده و به‌جای ارائه هزینه محاسباتی هر مسئله به‌صورت جداگانه، تنها میانگین هزینه را اعلام کرده است.
یکی از غیرمعمول‌ترین جنبه‌های این پروژه، شیوه انتشار آن است. OpenAI به‌جای ارسال نتایج به مجلات علمی دارای فرایند داوری همتا، آن‌ها را مستقیماً در GitHub منتشر کرده است.
این تصمیم نشان‌دهنده چالشی است که افزایش سرعت تولید نتایج توسط هوش مصنوعی می‌تواند برای سازوکار سنتی انتشار علمی ایجاد کند. فرایند متعارف داوری مقالات برای بررسی چنین حجم بالایی از نتایج بالقوه جدید طراحی نشده است.
استفاده از GitHub همچنین امکان ثبت تغییرات، اصلاح نتایج و به‌روزرسانی مستمر آن‌ها را فراهم می‌کند، در حالی که رسمی‌سازی اثبات‌ها می‌تواند بخشی از بار بررسی صحت منطقی را از دوش داوران انسانی بردارد.
🔴 همچنین بخوانید: هشدار کارمند سابق OpenAI: مدل‌های هوش مصنوعی ممکن است در دنیای واقعی متفاوت از محیط آزمایش رفتار کنند
شرکت OpenAI برای نحوه انتشار نتایج با گروه مشورتی ریاضیات و هوش مصنوعی در Institute for Advanced Study مشورت کرده و به‌صورت کلی از توصیه‌های عمومی این گروه پیروی کرده است.
این گروه شامل ریاضی‌دانان شناخته‌شده‌ای از جمله Timothy Gowers، برنده مدال فیلدز است.
با این حال، OpenAI پیشاپیش یک محدودیت مهم برای نقش این گروه تعیین کرده است: ریاضی‌دانان می‌توانند درباره نحوه اطلاع‌رسانی و انتشار نتایج مشاوره دهند، اما درباره اینکه این نتایج باید تولید شوند یا سرعت تولید آن‌ها چقدر باشد، نقشی ندارند.
شرکت OpenAI همچنین اعلام کرده است که از کارگاه‌ها و کنفرانس‌های متمرکز بر درک و بررسی نتایج تولیدشده توسط هوش مصنوعی حمایت مالی خواهد کرد.
این شرکت پذیرفته است که کیفیت منابع و نحوه ارائه نتایج همچنان نیاز به بهبود دارد. OpenAI همچنین می‌گوید روی انتشار مسئولانه مدل مورد استفاده کار می‌کند تا دانشمندان بتوانند مستقیماً به قابلیت‌های پیشرفته آن دسترسی داشته باشند.
رسمی‌سازی اثبات‌ها با Lean می‌تواند مشخص کند که یک استدلال از نظر منطقی صحیح است، اما این روش تمام مسائل مربوط به ارزیابی نتایج تولیدشده توسط هوش مصنوعی را برطرف نمی‌کند.
برای مثال، Lean نمی‌تواند تعیین کند که یک نتیجه واقعاً جدید، مهم یا از نظر ریاضی مرتبط است. چنین قضاوت‌هایی همچنان به بررسی و ارزیابی جامعه ریاضی نیاز دارند.
OpenAI بر این فرض است که نتایج منتشرشده مرز دانش انسانی را گسترش می‌دهند، اما اینکه جامعه ریاضی تا چه اندازه با این ارزیابی موافق باشد، همچنان مشخص نیست.
واکنش ریاضی‌دانان به پیشرفت سریع هوش مصنوعی در این حوزه یکسان نیست و از استقبال تا نارضایتی را در بر می‌گیرد.
در نامه سرگشاده‌ای با عنوان «ناهم‌راستایی شدید هوش مصنوعی در ریاضیات»، تعداد ۲۵ برنده مدال فیلدز درباره فاصله میان اهداف صنعت هوش مصنوعی و اهداف علم ریاضیات هشدار داده‌اند.
از نگاه نویسندگان این نامه، حل مسئله صرفاً یک ابزار و شاخص برای هدف اصلی یعنی دستیابی به درک مفهومی و بینش ریاضی است. آن‌ها استدلال می‌کنند که تولید انبوه گزاره‌های صحیح می‌تواند به‌جای خلق ایده‌های جدید، زمینه‌های حاصلخیز برای پژوهش را از بین ببرد و آثار این روند ممکن است به حوزه‌های علمی دیگر نیز گسترش پیدا کند.
تیموتی گاورز هشدار داده است که طی یک تا دو دهه آینده ممکن است حجم ادبیات ریاضی به‌شدت افزایش پیدا کند، در حالی که دیگر جامعه‌ای انسانی وجود نداشته باشد که واقعاً تمام بخش‌های آن را درک کند.
Terence Tao، برنده مدال فیلدز نیز بر اهمیت جنبه انسانی آموزش ریاضی تأکید کرده است. به اعتقاد او، آموزش نسل جدید ریاضی‌دانان باید استفاده از ابزارهای هوش مصنوعی را به‌شدت محدود کند تا یادگیری واقعی و دستیابی به درک عمیق همچنان حفظ شود.
🔴 همچنین بخوانید: اخراج ۳ پژوهشگر ایمنی OpenAI در بحبوحه نگرانی‌های امنیتی هوش مصنوعی
انتشار ۳۷۲ نتیجه ریاضی تولیدشده توسط مدل داخلی OpenAI نمونه‌ای از افزایش سرعت استفاده از هوش مصنوعی در پژوهش‌های ریاضی است. رسمی‌سازی بسیاری از اثبات‌ها با Lean می‌تواند بررسی صحت منطقی آن‌ها را آسان‌تر کند، اما مسائلی مانند اصالت، اهمیت و ارزش مفهومی نتایج همچنان به ارزیابی ریاضی‌دانان نیاز دارند. انتشار مستقیم این مجموعه در GitHub نیز چالش تازه‌ای را برای مدل سنتی داوری علمی مطرح می‌کند؛ به‌ویژه اگر حجم نتایج تولیدشده توسط هوش مصنوعی با همین سرعت افزایش یابد.
به نظر شما در دوره‌ای که هوش مصنوعی می‌تواند صدها اثبات ریاضی تولید کند، معیار اصلی پیشرفت باید تعداد مسائل حل‌شده باشد یا میزان درک و بینش جدیدی که این نتایج برای انسان ایجاد می‌کنند؟
