هاگینگ فیس بیش از ۳۰۰ اثبات ریاضی OpenAI را به محیط‌های متن‌باز یادگیری تقویتی برای آموزش مدل‌های هوش مصنوعی تبدیل کرد
در حالی که جدیدترین اثبات‌های ریاضی OpenAI برای بخش بزرگی از انسان‌ها به‌سادگی قابل درک نیستند، این اثبات‌ها به‌زودی می‌توانند برای آموزش مدل‌های هوش مصنوعی به کار گرفته شوند.
هاگینگ فیس مجموعه‌ای از مسائل ریاضی رسمی OpenAI را به محیط‌های متن‌باز یادگیری تقویتی تبدیل کرده است و به هر کسی که بخواهد مدل هوش مصنوعی خود را آموزش دهد، یک معیار ریاضی آماده و قابل اجرا برای کار ارائه می‌کند.
مجموعه داده جدیدی که با نام openai-math منتشر شده، بخشی از ابتکار FineEnvs هاگینگ فیس است و شامل ۳۶۹ مورد از بخش آزمون است که از رسمی‌سازی‌های Lean 4 شرکت OpenAI استخراج شده‌اند. هر مورد به‌جای یک جفت ثابت پرسش و پاسخ، به‌عنوان یک محیط اجرایی یادگیری تقویتی بسته‌بندی شده است. هر ورودی شامل دستورالعمل، توضیحی درباره چالش اثبات مورد نظر و فراداده‌هایی مانند کلیدواژه‌ها و نسخه طرحواره است؛ ساختاری که به مدل اجازه می‌دهد تلاش خود برای ارائه اثبات را به‌صورت خودکار ارزیابی کند، نه اینکه نتیجه توسط انسان بررسی شود.
urlکلم دِلانگ، هم‌بنیان‌گذار و مدیرعامل هاگینگ فیس، در شبکه X خبر انتشار این مجموعه را اعلام کرد و آن را گامی در جهت تبدیل دستاوردهای پژوهشی بسته به زیرساخت‌های آموزشی مشترک دانست. او گفت این پروژه یک انتشار پژوهشی را به «زیرساخت آموزشی اجرایی برای همه» تبدیل می‌کند و رویکرد گسترده‌تر تبدیل پژوهش‌های باز به محیط‌های قابل ساخت و استفاده را مسیری مهم برای آموزش مدل‌های باز بهتر توصیف کرد. دِلانگ همچنین از یک محدودیت مهم این پروژه سخن گفت: بررسی‌کننده خودکار فقط شکل‌بندی رسمی دقیق اثبات اصلی را می‌پذیرد؛ بنابراین ممکن است یک اثبات از نظر ریاضی درست باشد اما چون ساختار متفاوتی دارد، امتیاز صفر بگیرد. او این انتشار را «اولیه و خام» توصیف کرد، نه یک معیار کامل.
این مجموعه در دسته محیط‌های یادگیری تقویتی هاگینگ فیس قرار گرفته و برچسب‌هایی مانند harbor، reinforcement-learning، code-agent، lean4 و mathlib دارد که به زنجیره ابزار مورد استفاده آن اشاره می‌کنند. Lean 4 یک دستیار اثبات رسمی است و mathlib کتابخانه بزرگ و نگهداری‌شده توسط جامعه برای ریاضیات رسمی‌شده در همین اکوسیستم به شمار می‌رود. این محیط به یکی از آزمون‌های محبوب برای بررسی صحت واقعی اثبات‌های تولیدشده توسط هوش مصنوعی تبدیل شده است؛ زیرا مشخص می‌کند یک اثبات واقعاً درست است یا فقط ظاهری قابل قبول دارد. مسائل این مجموعه نام‌هایی مانند AbhyankarSathaye، AffineBernstein و ArtinCAT0 دارند که نشان‌دهنده سطح پیشرفته و پژوهشی ریاضیات رسمی‌شده توسط OpenAI است.
بسته‌بندی این مسائل به شکل محیط‌های RL سازگار با Harbor اهمیت زیادی دارد، زیرا قابلیت‌هایی فراتر از یک مجموعه داده ثابت از مسائل و پاسخ‌ها ایجاد می‌کند. یک مجموعه ثابت برای ارزیابی مفید است، اما به‌تنهایی نمی‌تواند مدل را آموزش دهد. در مقابل، یک محیط یادگیری تقویتی می‌تواند مستقیماً وارد چرخه آموزش شود: مدل یک اثبات پیشنهاد می‌کند، بررسی‌کننده Lean آن را ارزیابی می‌کند و نتیجه پذیرش یا رد به‌عنوان پاداش به مدل بازگردانده می‌شود. همین سازوکار پایه‌ای، پشت بخشی از پیشرفت‌هایی است که آزمایشگاه‌ها در آموزش تقویتی روی وظایف قابل‌راستی‌آزمایی مانند ریاضیات و کدنویسی گزارش کرده‌اند. انتشار هاگینگ فیس در عمل زیرساخت لازم برای چنین نوع آموزشی روی مجموعه ریاضی OpenAI را متن‌باز می‌کند، نه اینکه فقط خود مسائل را منتشر کند.
این اقدام در ادامه روندی قرار می‌گیرد که در آن آزمایشگاه‌های هوش مصنوعی و پژوهشگران، ریاضیات رسمی را به‌عنوان بستری ارزشمند برای آزمایش توانایی‌های هوش مصنوعی می‌بینند؛ بخشی از دلیل این موضوع، وجود پاداشی شفاف و غیرقابل‌ابهام در اثبات‌های قابل بررسی ماشینی است که دستکاری آن دشوارتر است. این اتفاق همچنین در زمانی رخ می‌دهد که جامعه ریاضی درباره نقش هوش مصنوعی در این حوزه بحث‌های فعالی دارد. urlترنس تائو، برنده مدال فیلدز، اخیراً استدلال کرده است که ریاضیات به سوی دوره‌ای موسوم به «Math 2.0» نزدیک می‌شود؛ دوره‌ای که در آن این رشته باید فراتر از حل صرف مسائل حرکت کند، زیرا ابزارهای هوش مصنوعی در همین وظیفه روزبه‌روز بهتر می‌شوند. انتشارهایی مانند این مجموعه که مستقیماً به سیستم‌های هوش مصنوعی برای حل اثبات‌های رسمی پاداش می‌دهند، در مرکز همین بحث قرار دارند.
در حال حاضر، محیط‌های openai-math همچنان یک نسخه اولیه هستند و مشکل سخت‌گیری بیش از حد بررسی‌کننده، واضح‌ترین شکافی است که جامعه باید آن را برطرف کند. با این حال، این پروژه نمونه‌ای قابل توجه از بازسازی ابزارهای داخلی ریاضی یک آزمایشگاه پیشرو به چیزی است که هر توسعه‌دهنده می‌تواند آن را کپی، بررسی و برای آموزش مدل استفاده کند. این مجموعه آزمونی است برای اینکه آیا «پژوهش باز» می‌تواند به خط لوله‌های آموزشی واقعاً باز و قابل استفاده مجدد تبدیل شود یا فقط به انتشار مقاله‌های معیار محدود باقی می‌ماند.