مبارزه استارتاپ Axiom Math با محتوای بی‌کیفیت هوش مصنوعی؛ راستی‌آزمایی یکی از بزرگ‌ترین مراجع تاریخ ریاضیات با ایجنت‌ها

به نظر می‌رسد هوش مصنوعی هر هفته یک مسئله جدید ریاضی را حل می‌کند. تنها در ماه گذشته، شرکت OpenAI به‌تنهایی ۷۱۹ مقاله منتشر کرد که ادعا می‌کردند راه‌حل برخی از دشوارترین مسائل این حوزه را یافته‌اند. با این حال، حتی بررسی‌های کامپیوتری نیز ممکن است دچار خطا شوند. پس از سال‌ها مواجهه با محتوای بی‌کیفیت و سرهم‌بندی‌شده هوش مصنوعی (AI slop)، طبیعی است که بپرسیم آیا قرعه بعدی به نام ریاضیات خواهد افتاد یا خیر.

استارتاپ Axiom Math معتقد است که ریاضیات می‌تواند از این سرنوشت بگریزد؛ نه با کاهش سرعت پیشرفت، بلکه با تکیه بر شالوده‌ای محکمتر. این استارتاپ ۱.۶ میلیارد دلاری می‌خواهد زیرساختی تاییدشده و معتبر بسازد که ایجنت‌های هوش مصنوعی بتوانند برای نوشتن نرم‌افزار و در نهایت انجام پژوهش‌های علمی به آن تکیه کنند.

روز چهارشنبه، این شرکت اعلام کرد که پروژه Stacks Project، یکی از بزرگ‌ترین مجموعه‌های ریاضی نوشته‌شده به دست بشر را به‌طور رسمی راستی‌آزمایی و فرموله (Formalize) کرده است. ریاضی‌دانان جایگاه ویژه‌ای برای مجموعه Stacks قائل هستند؛ پیتر وویت (Peter Woit)، ریاضی‌دان دانشگاه کلمبیا، مدعی شده است که «هیچ اثر دیگری واقعاً قابل مقایسه با آن نیست» و این پروژه را با «کتاب‌های مشهور بورباکی (Bourbaki)» مقایسه کرده است؛ مجموعه‌ای که در قرن بیستم ریاضیات را از پایه بازسازی کرد.

یوهان دو یونگ (Johan de Jong)، همکار وویت در دانشگاه کلمبیا، پروژه Stacks Project را در سال ۲۰۰۵ به‌عنوان یک مرجع متن‌باز آغاز کرد. از آن زمان تاکنون، ریاضی‌دانان پیوسته در توسعه آن مشارکت داشته‌اند و دستاوردهای آن را از جبر سطح دانشگاهی تا پیشرفته‌ترین مفاهیم در حوزه‌های جبر، هندسه و نظریه اعداد گسترش داده‌اند.

اکنون ناوگان ایجنت‌های هوش مصنوعی این شرکت، حدود ۷,۶۵۴ صفحه از این کتابخانه بزرگ را به نزدیک به ۱۶ میلیون خط کدِ بررسی‌شده توسط کامپیوتر ترجمه کرده‌اند.

فرموله‌سازی رسمی ریاضیات، روشی برای اطمینان از سلامت و استحکام ساختار زیربنایی آن است. در این فرآیند، ریاضی‌دانان اثبات‌ها را در قالب کد در زبان برنامه‌نویسی ویژه‌ای به نام Lean بازنویسی می‌کنند و برنامه‌ای موسوم به «دستیار اثبات» (Proof Assistant)، کدها را خط‌به‌خط بررسی می‌کند. اگر اثبات از این فیلتر عبور کند، ریاضی‌دانان می‌توانند مطمئن باشند که ساختار آن از نظر منطقی کاملاً بی‌نقص است.

مهندسان نیز از ایده مشابهی به نام «راستی‌آزمایی رسمی» (Formal Verification) برای تأیید صحت عملکرد طراحی تراشه‌های خود استفاده می‌کنند و پژوهشگران در فرانسه نیز از این روش برای کشف باگ‌ها در نرم‌افزار محاسبه کمک‌هزینه‌های خانواده بهره برده‌اند.

برای مجموعه‌ای به عظمت Stacks Project، بررسی تک‌تک قضیه‌ها تنها بخشی از کار است. قضیه‌ها و تعاریف موجود در Stacks به یکدیگر گره خورده‌اند و هر کدام بر پایه موارد پیشین بنا شده‌اند. درست مانند یک شجره‌نامه خانوادگی، بسیاری از نتایج در Stacks به قضیه‌های قبلی خود بازمی‌گردند.

همین پیوستگی پیچیده باعث شده بود که تیم Axiom در ابتدا نسبت به موفقیت پروژه مطمئن نباشد. اعضای تیم باید تمامی این ارتباطات را در دل حدود ۱۶ میلیون خط کد زبان Lean بدون هیچ آسیبی حفظ می‌کردند.

کارینا هونگ (Carina Hong)، مدیرعامل Axiom در این باره می‌گوید: «در زندگی، چیزهای بسیار بزرگ و چیزهای بسیار ظریف معمولاً با هم سازگار نیستند. مجموعه Stacks گردآوری نتایجی است که شالوده ریاضیات را تشکیل می‌دهند. در چنین پروژه‌ای، قضیه‌ها باید با یکدیگر همخوانی داشته باشند و متناقض نباشند؛ تعاریف نباید با هم در تضاد قرار بگیرند.»

این مدیرعامل ۲۵ ساله، دوره دکتری ریاضیات در دانشگاه استنفورد را نیمه‌کاره رها کرد و در مارس ۲۰۲۵ این شرکت را بنیان گذاشت. شرکت Axiom در ماه مارس موفق شد در دور سرمایه‌گذاری سری A به رهبری شرکت Menlo Ventures، مبلغ ۲۰۰ میلیون دلار سرمایه جذب کند.

هونگ در ادامه افزود: «ما مطمئن نبودیم که کدنویسی شهودی (Vibe Coding) بتواند زیبایی و ظرافت مجموعه Stacks را حفظ کند.»

برای به سرانجام رساندن این پروژه، تیم تحقیقاتی ساختار منعطفی را برای ایجنت‌های خود تعریف کرد و به آن‌ها اجازه داد تا به‌طور موازی فعالیت کنند. آشوین سوامیناتان (Ashvin Swaminathan)، عضو کادر فنی Axiom، توضیح می‌دهد: «ما در پروژه Stacks یک سلسله‌مراتب ایجاد کردیم، اما ساختار آن به گونه‌ای نبود که دیکته کند هر ایجنت دقیقاً چه کاری انجام دهد. ایجنت‌ها خودشان وظایف را پیدا می‌کردند و بخش‌هایی را که امکان کار موازی روی آن‌ها وجود داشت، تشخیص می‌دادند.»

شرکت Axiom هم‌چنین مدل‌های اختصاصی خود را طوری آموزش داده است که در ریاضیات مهارت بالایی داشته باشند؛ رویکردی که به گفته هونگ، اکثر استارتاپ‌های دیگر در حوزه راستی‌آزمایی به سراغ آن نرفته‌اند. در ابتدا، تیم به یکی از متخصصان داخلی زبان Lean تکیه کرد تا نوعی «ذوق و سلیقه انسانی» را به ایجنت‌ها بیاموزد. به گفته هونگ، ایجنت‌ها به‌مرور زمان خودشان این ظرافت و سلیقه را فرا گرفتند.

نتیجه این تلاش، یکی از بزرگ‌ترین خلأهای موجود در ریاضیات فرموله‌شده را پر می‌کند. سوامیناتان می‌گوید: «وقتی به بخش‌های فرموله‌شده در ریاضیات نگاه می‌کنید، یک سیاه‌چاله بزرگ می‌بینید؛ سیاه‌چاله‌ای که حوزه هندسه جبری را در بر می‌گیرد.»

به گفته او، تا پیش از این، پژوهشگرانی که می‌خواستند دستاوردهای جدید حوزه هندسه جبری را با زبان Lean بررسی کنند، پایه و اساس چندانی برای کار نداشتند، اما اکنون این زیرساخت در اختیار آن‌ها قرار دارد.

تیم Axiom استدلال می‌کند که هر نتیجه تاییدشده به یک بلوک سازنده تبدیل می‌شود؛ بنابراین اثبات‌های آینده به‌جای شروع از صفر، می‌توانند بر ریاضیات بررسی‌شده تکیه کنند. ترنس تائو (Terence Tao)، ریاضی‌دان دانشگاه UCLA و برنده مدال فیلدز، این قانون کلی را بسیار ساده‌تر بیان کرده است: «هرچه اثبات‌های فرموله‌شده بیشتری داشته باشید، می‌توانید اثبات‌های فرموله‌شده بیشتری بسازید.»

البته ریاضی‌دانان تنها مخاطبان هدف Axiom نیستند. توسعه‌دهندگان نرم‌افزار مدت‌هاست که برای تضمین عاری بودن کدهای خود از باگ‌ها و حفره‌های امنیتی با چالش روبه‌رو هستند. هرچه ایجنت‌های هوش مصنوعی سهم بیشتری از کدهای جهان را می‌نویسند، این مشکل نیز ابعاد بزرگ‌تری پیدا می‌کند.

استارتاپ Axiom روی این ایده سرمایه‌گذاری کرده است که نرم‌افزارهای آینده نیز درست مانند مجموعه Stacks، باید بر پایه زیرساخت‌های راستی‌آزمایی‌شده بنا شوند.

سوامیناتان در این رابطه می‌گوید: «ما معتقدیم ریاضیات نقطه‌ای است که ساخت این زیرساخت‌ها باید از آنجا آغاز شود و این یک مهارت قابل انتقال است. ایجنت‌ها می‌توانند کدهای ما را بخوانند، آن‌ها را درک کنند و زیرساخت‌های جدیدی بر فراز آن‌ها بسازند. کدهای فرموله‌شده ما در زبان Lean، اکنون بستری است که ایجنت‌ها می‌توانند کار خود را روی آن بنا کنند.»

شیوه‌ای که ایجنت‌های Axiom برای ساخت پروژه Stacks به کار گرفتند، یعنی فعالیت موازی و انتخاب خودکار وظایف، همان روشی است که هونگ انتظار دارد بخش عمده‌ای از فعالیت‌های آینده هوش مصنوعی بر اساس آن پیش برود. او معتقد است که ایجنت‌های هوش مصنوعی برای پرهیز از تولید محتوای بی‌کیفیت و سرهم‌بندی‌شده، به یک مجموعه دانش خوش‌ساخت و قابل استفاده مجدد نیاز خواهند داشت.

هونگ می‌گوید: «ایجنت‌ها باید یک کتابخانه قابل استفاده مجدد در اختیار داشته باشند تا بر پایه آن بسازند و مرزهای دانش را به پیش ببرند. اگر در همان ابتدا با انتخاب‌های مهندسی ضعیف، خروجی‌های بی‌کیفیت تحویل دهید، گسترش دادن این مرزها برای ایجنت‌ها بسیار دشوار خواهد شد.»

هونگ به این رویکرد تا حدی اطمینان دارد که رقبای خود را به چالش می‌کشد و می‌گوید: «من صراحتاً از تمام شرکت‌های فعال در حوزه کدنویسی دعوت می‌کنم که روی فرموله‌سازی و راستی‌آزمایی در چنین مقیاسی کار کنند.»