استارتاپ Axiom Math با استفاده از هوش مصنوعی به دنبال پاکسازی ریاضی از خطاهای ماشینی

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

این استارتاپ به تازگی اعلام کرده که پروژه «Stacks» را که یکی از بزرگترین مجموعه‌های دانش ریاضی بشری است، به صورت رسمی تایید کرده است. این پروژه که از سال ۲۰۰۵ توسط یوهان دی جونگ آغاز شد، مرجعی برای مباحث پیشرفته از جبر تا هندسه است. تیم Axiom با استفاده از ناوگان عوامل هوش مصنوعی خود، حدود ۷۶۵۴ صفحه از این پروژه را به ۱۶ میلیون خط کد قابل‌بررسی توسط کامپیوتر تبدیل کرده است.

فرآیند تایید رسمی (Formal Verification) به این صورت است که اثبات‌ها در زبان برنامه‌نویسی Lean بازنویسی می‌شوند و یک دستیار اثبات، صحت منطقی آن‌ها را خط به خط بررسی می‌کند. این تکنیک مشابه روشی است که مهندسان برای اطمینان از سلامت طراحی تراشه‌ها یا یافتن باگ‌های نرم‌افزاری حساس استفاده می‌کنند. با این تفاوت که در ریاضیات، هر قضیه بر پایه قضایای پیشین استوار است و کوچکترین خطا می‌تواند کل ساختار را متزلزل کند.

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

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