Axiom Math، استارتاپی با ارزش ۱.۶ میلیارد دلار، در ۵ نوامبر ۲۰۲۶ اعلام کرد که پروژه Stacks را به‌طور رسمی صحت‌سنجی کرده است. Stacks یکی از بزرگ‌ترین مجموعه‌های ریاضی‌ای است که هرگز توسط انسان نوشته شده — از جبر سطح دانشگاهی تا پیشرفته‌ترین ایده‌های هندسه و نظریه اعداد. ناوگان عامل‌های هوش مصنوعی Axiom حدود ۷٬۶۵۴ صفحه این کتابخانه را به تقریباً ۱۶ میلیون خط کد بررسی‌شده رایانه‌ای در زبان Lean ترجمه کرده‌اند.
چرا Stacks و چرا حالا؟#
Johan de Jong، ریاضی‌دان دانشگاه کلمبیا، پروژه Stacks را در ۲۰۰۵ به‌عنوان یک مرجع متن‌باز آغاز کرد. Peter Woit، همکار او در کلمبیا، Stacks را با کتاب‌های مشهور Bourbaki مقایسه می‌کند و می‌گوید «چیز دیگری واقعاً قابل مقایسه با آن وجود ندارد.»
صحت‌سنجی رسمی یعنی بازنویسی اثبات‌ها به‌صورت کد در زبان Lean و بررسی خط‌به‌خط آن‌ها با یک proof assistant. اگر اثبات قبول شود، ریاضی‌دانان می‌توانند مطمئن باشند که از نظر منطقی درست است. همین روش در طراحی تراشه و یافتن باگ در نرم‌افزارهای حساس هم استفاده می‌شود.
مشکل اصلی Stacks، درهم‌تنیدگی تعریف‌ها و قضایا بود. هر نتیجه به نتایج قبلی وابسته است، مثل یک درخت خانوادگی. Carina Hong، مدیرعامل ۲۵ ساله Axiom که از دوره دکتری ریاضی دانشگاه Stanford انصراف داده و شرکت را در مارس ۲۰۲۵ تأسیس کرده، می‌گوید: «چیزهای بزرگ و چیزهای ظریف در زندگی با هم جور نمی‌شوند.» او در مارس ۲۰۲۵ یک دور Series A به مبلغ ۲۰۰ میلیون دلار به رهبری Menlo Ventures جذب کرد.
روش کار: عامل‌های خودگردان با ساختار شل#
تیم Axiom به عامل‌هایش یک سلسله‌مراتب شل داد و آن‌ها را به‌صورت موازی به کار گرفت. Ashvin Swaminathan از اعضای تیم فنی Axiom می‌گوید: «عامل‌ها خودشان کار پیدا می‌کردند و کارهایی که می‌توانستند موازی انجام دهند را شناسایی می‌کردند.» Axiom همچنین مدل‌های مخصوص خود را برای ریاضیات آموزش داد — رویکردی که Hong می‌گوید استارتاپ‌های صحت‌سنجی دیگر آن را انتخاب نکرده‌اند.
Swaminathan می‌گوید هندسه جبری تا پیش از این یک «سیاه‌چاله بزرگ» در ریاضیات صوری بود: «محققانی که می‌خواستند کار جدید در هندسه جبری را با Lean بررسی کنند، تقریباً چیزی برای ساختن روی آن نداشتند. حالا دارند.»
تحلیل تحریریه: این خبر برای سازندگان ایجنت یعنی چه؟#
اگر همین حالا با عامل‌های هوش مصنوعی نرم‌افزار می‌سازید، این خبر مستقیماً ابزار شما را تغییر نمی‌دهد. اما یک پیش‌فرض را جابه‌جا می‌کند: Axiom استدلال می‌کند که صحت‌سنجی ریاضی، زیرساخت قابل‌استفاده‌مجددی است که عامل‌ها می‌توانند روی آن سازه بسازند. اگر این ادعا درست باشد، مسئله «هوش مصنوعی کد بی‌کیفیت تولید می‌کند» فقط با مدل‌های قوی‌تر حل نمی‌شود — بلکه با لایه‌های صوری‌شده‌ای حل می‌شود که عامل‌ها مجبورند از آن‌ها عبور کنند تا به نتیجه برسند.
نکته احتیاطی: Hong از همه شرکت‌های کدنویسی خواسته که در این مقیاس صحت‌سنجی کار کنند. این یک چالش عمومی است، نه یک محصول آماده. هنوز مشخص نیست چه ابزار یا APIای از Axiom در دسترس توسعه‌دهندگان بیرونی قرار می‌گیرد.
منبع: TechCrunch AI
دیدگاهها
برای گذاشتن دیدگاه وارد شو
دیدگاهها فقط از حسابهای کاربری پذیرفته میشوند.
ورود / ثبتنامهنوز دیدگاهی ثبت نشده — اولین نفر باش.