عنوان: تئورم ۶ میلیون دلار سرمایه بذری جذب کرد تا «اعتمادپذیری» کدهای تولیدشده توسط هوش مصنوعی را اثبات کند
خلاصه: استارتاپ سانفرانسیسکویی Theorem که از دوره بهاری Y Combinator ۲۰۲۵ بیرون آمده، با جذب ۶ میلیون دلار سرمایه بذری بهسرعت در تلاش است ابزارهای خودکار اثبات رسمی و بررسی صحت (verification) کدهای تولیدشده توسط هوش مصنوعی را به محصولات کاربردی برای شرکتها تبدیل کند. این حرکت در زمانی رخ میدهد که تولید کد توسط مدلهای هوش مصنوعی شتاب گرفته و نگرانیها درباره «شکاف نظارتی» و قابلاعتماد بودن نرمافزارها شدت یافته است.
چرا موضوع مهم است؟
با رشد سریع دستیارهای برنامهنویسی مبتنی بر هوش مصنوعی از سوی شرکتهایی مانند GitHub، Amazon و Google، میلیاردها خط کد بهصورت خودکار تولید میشوند. اما توانایی بررسی و تضمین عملکرد صحیح این کدها به همان سرعت رشد نکرده است. بهعبارت دیگر، مسئله اصلی دیگر نوشتن کد نیست؛ مسئله اعتماد به درستی و ایمنی کدهای تولیدشده است. گسترش این «شکاف نظارتی» میتواند زیرساختهای حیاتی مانند سیستمهای مالی، شبکههای برق و تجهیزات پزشکی را در معرض خطر قرار دهد.
چگونه Theorem این مشکل را حل میکند؟
هسته فناوری Theorem ترکیبی از اثبات رسمی (formal verification) — که با استفاده از روشهای ریاضی نشان میدهد نرمافزار دقیقاً مطابق مشخصه عمل میکند — و مدلهای هوش مصنوعی آموزشدیده برای تولید و بررسی خودکار اثباتهاست. این رویکرد تبدیل فرایندی میکند که historically سالها و نیروی متخصص سطح دکترا میطلبید، به فرایندی که میتواند در هفتهها یا حتی روزها تکمیل شود.
تفکیک کسری اثبات (fractional proof decomposition)
تئورم از رویکردی استفاده میکند که بنیانگذار آن آن را «تفکیک کسری اثبات» نامیده است: بهجای تلاش برای اثبات کامل همه حالات ممکن (که برای نرمافزارهای پیچیده غیرقابلعملی است)، منابع بررسی و اثبات را متناسب با اهمیت هر بخش از کد تخصیص میدهد. این روش امکان میدهد تمرکز بر قسمتهای حساس و بحرانی نرمافزار باشد و در عین حال هزینه محاسباتی و زمانی کاهش یابد.
نتایج فنی و نمونههای عملی
– در یک نمایش فنی بهنام SFBench، Theorem با استفاده از هوش مصنوعی توانست 1,276 مسئله را از زبان اثبات Coq به زبان Lean ترجمه و معادل بودن ترجمهها را بهصورت خودکار اثبات کند؛ کاری که بهگفته شرکت برای تیم انسانی حدود ۲.۷ نفر-سال زمان میبرد.
– این فناوری همچنین توانسته با شناسایی باگهایی که از تستهای معمول عبور کرده بودند، نمونههای واقعی را اصلاح کند.
– یک مطالعه موردی عملی: مشتریای با مشخصه ۱,۵۰۰ صفحه PDF و پیادهسازی قدیمی که دچار نشت حافظه و کرشهای مخفی بود، نیاز به ارتقای عملکرد از ۱۰ مگابیت بر ثانیه به ۱ گیگابیت بر ثانیه داشت. سیستم Theorem با تولید نزدیک به ۱۶,۰۰۰ خط کد تولیدی و تولید یک مشخصه اجرایی فشرده (چند صد خط) و ابزار بررسی برابری (equivalence checker)، پیادهسازی جدید را بدون بازبینی دستی کامل مستقر کرد؛ نتیجه: یک پارسر تولیدی و قابلاعتماد با توان ۱ گیگابیت بر ثانیه.
تفاوت فنی Theorem نسبت به سایرین
در حالی که چندین تیم تحقیقاتی و استارتاپ روی تقاطع هوش مصنوعی و اثبات رسمی کار میکنند، Theorem بر مقیاسپذیریِ «نظارت نرمافزاری» تمرکز کرده است و ابزارهایش را برای تیمهای مهندسی سیستم و لایههای نزدیک به سختافزار توسعه میدهد. معماری این شرکت میتواند وابستگیها و کدهای بینفایلی را مدیریت کند؛ موردی که برای عاملهای کدنویسی معمولی با محدودیتهای پنجرهی زمینهای (context window) دشوار است.
سرمایهگذاری و تیم
Theorem روز سهشنبه اعلام کرد که با هدایت Khosla Ventures، سرمایهای برابر با ۶ میلیون دلار جذب کرده است. دیگر سرمایهگذاران شامل Y Combinator، e14، SAIF، Halcyon و جمعی از سرمایهگذاران فرشتگان از جمله Blake Borgerson و Arthur Breitman هستند. تیم فعلی شرکت کوچک است (حدود ۴ نفر) و قصد دارد با این سرمایه، تیم فنی را گسترش داده، منابع محاسباتی برای آموزش مدلهای اثبات را افزایش دهد و به صنایع جدیدی مانند رباتیک، انرژیهای تجدیدپذیر، رمزارزها و سنتز دارو ورود کند.
پیامدهای امنیتی و سیاستگذاری
تسریع در تولید کد توسط هوش مصنوعی هزینهی کشف و سوءاستفاده از آسیبپذیریها را کاهش میدهد. بههمین دلیل بنیانگذاران Theorem بر نیاز به «دفاع نامتقارن» تأکید دارند: راهکارهایی که بدون افزایش متناسب منابع، محافظت کنند. آنها حتی بیان میکنند که اکنون که اثبات رسمی مقرونبهصرفهتر شده، ممکن است در آینده عدم استفاده از آن برای سیستمهای حیاتی به چشم «بیاحتیاطی شدید» (gross negligence) تعبیر شود. این بحث بهتدریج وارد حوزههای قانونگذاری و استانداردسازی میشود، چرا که زیرساختهای حیاتی بیش از پیش تحت تأثیر نرمافزارهای تولیدشده توسط هوش مصنوعی قرار دارند.
جمعبندی
با ورود Theorem به این حوزه، سیگنالی واضح برای بازار و سیاستگذاران ارسال میشود: موج بعدی توسعه نرمافزار با هوش مصنوعی، تنها افزایش سرعت و تولید کد نیست، بلکه تضمین ریاضیِ درستبودن آن است. اگر مسیر فعلی رشد مدلها ادامه یابد، حضور ابزارهای اثبات رسمی خودکار و مقرونبهصرفه میتواند نقش محوری در حفظ امنیت و کنترلپذیری سامانههای پیچیده ایفا کند. در نهایت؛ ماشینها کد مینویسند — اما اکنون باید کسی یا چیزی بتواند کارشان را بهدرستی بررسی کند.