ایجنت‌های Claude Opus 5.5 الگوریتم جدیدی برای کوتاه‌ترین مسیر ابداع کردند

ده ایجنت هوش مصنوعی یک کران جدید برای کوتاه‌ترین مسیر را به اثبات رساندند

شرکت Vals AI گزارش داده است که ده ایجنت مبتنی بر Claude Opus 5.5 حدود ۱۵ ساعت زمان صرف کرده و با تبادل ۷۳۳ پیام، موفق به طراحی یک الگوریتم کوتاه‌ترین مسیر و اثبات کران پیچیدگی آن در سیستم Lean شدند. الگوریتم حاصل که C-HD نام دارد، فواصل دقیق از یک مبدأ واحد را در گراف‌های جهت‌دار با وزن یال‌های حقیقی و غیرمنفی محاسبه می‌کند.

گزارش منتشرشده، C-HD را به عنوان یک بهبود مجانبی جدید در یک محدوده باریک از چگالی گراف معرفی می‌کند. سیستم Lean قضیه بیان‌شده و مفروضات مجاز آن را تأیید کرده است؛ با این حال، جدید بودن این روش و مقایسه آن با ادبیات پیشین هنوز نیازمند بررسی‌های مستقل و خارجی است.

کران ادعاشده توسط C-HD

مسئله هدف، مسئله استاندارد کوتاه‌ترین مسیر از مبدأ واحد است. با داشتن یک گراف جهت‌دار با n رأس، m یال و وزن‌های غیرمنفی، این الگوریتم باید حداقل وزن مسیر از یک مبدأ به تمام رئوس قابل‌دسترس را برگرداند.

الگوریتم دایجسترا (Dijkstra) با هیپ فیبوناچی در زمان O(m + n log n) اجرا می‌شود. یک مقاله در سال ۲۰۲۵ این کران را برای m ≥ n به O(m log^(2/3) n) بهبود بخشید. همچنین C-HD با کران جدیدتر زیر مقایسه شده است:

O(m * sqrt(log n) + sqrt(m * n * log n * log log n))

این ایجنت‌ها یک مخزن اثبات برای کران زیر در C-HD تولید کردند:

O(n + m + m * log(2 + m/(n+1))
  + m^(1/3) * (n * log(n+2))^(2/3))

این تضمین بهبودیافته زمانی اعمال می‌شود که:

m ≤ n * floor(floor(log₂ n)^(3/4))

برنامه ارائه‌شده این شرط را در زمان اجرا بررسی می‌کند. گراف‌هایی که خارج از این محدوده تأییدشده باشند، از الگوریتم جایگزین و تاییدشده بلمن-فورد (Bellman-Ford) استفاده می‌کنند؛ بنابراین، ادعای پیچیدگی بهبودیافته تنها برای شاخه C-HD صادق است.

یک مزیت مجانبی باریک

بزرگترین مزیت اعلام‌شده برای C-HD در حوالی m ≈ n log^(3/4) n ظاهر می‌شود. در این پروفایل، نسبت بین جملات پیشرو مقایسه‌شده با نرخ (log n)^(1/12) رشد می‌کند که نرخ بسیار کندی است.

برای مثال تئوریک n = 2^1000، نسبت جمله پیشرو حدود 1.78 است. این رقم بیانگر عبارات مجانبی است و نه زمان اجرای واقعی.

چگونه C-HD کارهای تکراری را کنترل می‌کند

الگوریتم C-HD جستجو را از طریق کاوش‌های محلی کراندار، مقایسه‌های اولویت‌دار، درخت‌های جستجو و محورهای انتخابی بازگشتی سازماندهی می‌کند. این روش حسابداری، یک رأس تازه کشف‌شده را به عنوان بخشی از یک جستجوی محلی در نظر می‌گیرد، حتی اگر آن رأس به عنوان یک برگ کاوش‌نشده باقی بماند، زیرا یال ورودی نتوانسته تخمین مسافت فعلی آن را بهبود بخشد.

1. با مبدأ و مرز فعلی رئوس کشف‌شده شروع کنید.
2. یال‌های خروجی را از طریق جستجوهای محلی کراندار کاوش کنید.
3. رئوس تازه کشف‌شده را در محدودیت هر جستجو، از جمله برگ‌های کاوش‌نشده، محاسبه کنید.
4. درخت‌های جستجو بسازید و محورهایی را انتخاب کنید که کار بازگشتی باقی‌مانده را تقسیم کنند.
5. ناورداهای محلی را حفظ کنید که پردازش تکراری را زمانی که یک رأس در چندین جستجو ظاهر می‌شود، محدود می‌کنند.

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

نحوه تقسیم کار بین ایجنت‌ها

شرکت Vals AI ده نمونه از Claude Opus 5.5 را با تنظیمات حداکثر توان مدل اجرا کرد و آن‌ها را از طریق یک تابلوی پیام مشترک به هم متصل نمود. این ایجنت‌ها با نقش‌های از پیش تعیین‌شده شروع به کار کردند، اما با کشف رویکردهای امیدوارکننده یا شناسایی شکست‌ها، کار را بین خود بازتوزیع کردند.

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

• رویکردهای شکست‌خورده را ثبت کنید تا سایر ایجنت‌ها از تکرار آن‌ها جلوگیری کنند.
• پیش از ادغام ادعاهای میانی در نتیجه نهایی، آن‌ها را به چالش بکشید.
• پیش از اعلام موفقیت، یک ساختار قابل‌تکرار در Lean تولید کنید.
• دو بررسی داخلی مجزا روی اثبات پیشنهادی انجام دهید.
• در صورتی که هیچ بهبودی از مرحله راستی‌آزمایی عبور نکرد، نتایج جزئی و سوالات باز را حفظ کنید.

مرز اعتماد اثبات

هسته سیستم Lean بررسی کرد که عبارات ارائه‌شده، قضیه مشخص‌شده را اثبات می‌کنند و ابزار Lean Comparator نیز تأیید کرد که این اثبات، گزاره مورد نیاز را هدف قرار داده و تنها از اصول موضوعه مجاز استفاده کرده است. این فرآیند استنتاج‌های نامعتبر را بدون توجه به میزان اطمینانی که ایجنت در ارائه آن‌ها داشته است، شناسایی می‌کند.

پذیرش هسته، گزاره رسمی را همان‌طور که کدگذاری شده پوشش می‌دهد. بازبین‌های انسانی همچنان باید بررسی کنند که آیا این گزاره صادقانه الگوریتم مورد نظر را نشان می‌دهد، آیا مدل پیچیدگی با ادعاهای مقاله مطابقت دارد و آیا کارهای قبلی پیش از این شامل نتیجه مشابهی بوده‌اند یا خیر.

یک الگوی قابل‌استفاده مجدد برای تحقیقات مبتنی بر ایجنت

برای توسعه‌دهندگانی که سیستم‌های ایجنت طولانی‌مدت می‌سازند، این آزمایش یک معماری ملموس ارائه می‌دهد: چندین کارگر نتایج میانی را به اشتراک می‌گذارند، بازبین‌های متخاصم راه‌حل‌های کاندیدا را بررسی می‌کنند و یک بررسی‌کننده خارجی تصمیم می‌گیرد که آیا خروجی نهایی مشخصات دقیق را برآورده می‌کند یا خیر.

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

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