اشتراک
فناوری هوش مصنوعی پژوهش

مقیاس‌پذیری ایمن تیم‌های چندعاملی با کلود فبل ۵.۲

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

در یک نگاه چکیدهٔ خودکار موتور هوش مصنوعی افق آبی

تیمی متشکل از ۱,۰۰۰ عامل هوش مصنوعی که نسخه اولیه مدل «کلود فبل ۵.۲» را اجرا می‌کردند، توانستند اثبات رسمی قضیه آخر فرما را بدون استفاده از پلتفرم تخصصی Prove2Me یا هدایت مستقیم پژوهشگر بازتولید کنند. این تیم در ۲۸.۷ ساعت، با یک‌سوم توکن‌های خروجی کمتر، اثباتی یک‌هفتم طول اثبات اصلی نوشتند. هر عامل در محیط ایزوله بدون اینترنت کار می‌کرد و یک طبقه‌بند پیش از اجرای هر دستور و یک مانیتور آفلاین اقدامات را بررسی می‌کردند. به عامل‌ها فهرستی از ۶۰ گزاره، طرحی یک‌جمله‌ای، تعاریف و ۴۷ لم اثبات‌شده داده شد و نقش رهبر و کمک‌کننده تعیین گردید. بدون Prove2Me، تیم سیستم هماهنگی خود را ساخت: رهبر در ۱۰ دقیقه اول پنج جدول در پایگاه داده مشترک Postgres ایجاد کرد (اعلان، تخصیص، یادداشت‌ها، زیروظایف و کارهای انجام‌شده). او ابتدا ۴۷ گزاره را غیرقابل‌اجرا قضاوت کرد، اما پس از اثبات سریع ۱۰ گزاره اول در ۷۰ دقیقه، کمک‌کننده‌ها را به گزاره‌های دشوارتر منتقل کرد. برای لنگلندز-تونل، تیم درختی از وظایف تا عمق ۱۰ سطح و ۲,۴۱۸ وظیفه ساخت. لنگلندز-تونل در ساعت ۲۸.۴ و قضیه نهایی در ساعت ۲۸.۷ اثبات شد. در بیش از یک میلیون فراخوانی ابزار، هیچ‌کدام معیار مسدود شدن را برآورده نکرد. این آزمایش نشان می‌دهد تیم‌های چندعاملی با مدل‌هایی مانند فبل ۵.۲ می‌توانند اهداف جاه‌طلبانه را در چارچوب مرزهای ایمنی طراحی‌شده محقق سازند، هرچند هدایت انسانی و داربست‌های تخصصی همچنان می‌توانند مفید باشند.

تیم‌های چندعاملی می‌توانند مسائل دشوار و بلندمدت را حل کنند. در ماه سپتامبر، ما نخستین صورت‌بندی رسمی کامل از قضیه آخر فرما را منتشر کردیم که توسط ده‌ها عاملِ در حال اجرای یک مدل تحقیقاتی داخلی، تقریباً هم‌ارز با کلود فبل ۵.۱، نوشته شده بود. آن کار به Prove2Me، پلتفرمی برای صورت‌بندی ریاضیات، و جهت‌دهی یک پژوهشگر متکی بود. در یک آزمایش جدید مقیاس کوچک، تیمی متشکل از ۱,۰۰۰ عامل که نسخه اولیه کلود فبل ۵.۲ را اجرا می‌کردند، اثبات را بدون داربست‌بندی فراهم‌شده توسط Prove2Me یا هدایت پژوهشگر بازتولید کردند. این تیم ۲۸.۷ ساعت زمان برد، یک‌سوم توکن‌های خروجی کمتری استفاده کرد و اثباتی نوشت که طول آن یک‌هفتم اثبات اصلی بود.

هر عامل در یک محیط ایزوله (Sandbox) بدون دسترسی به اینترنت کار می‌کرد. یک طبقه‌بند (Classifier) قبل از اجرای هر دستور پوسته و ویرایش فایل، آن را بررسی می‌کرد و یک مانیتور آفلاین هر یک از اقدامات تیم را بازبینی می‌نمود. ما به عامل‌ها فهرستی از ۶۰ گزاره، طرحی یک‌جمله‌ای از مسیر کلاسیک اثبات، تعاریفی که این گزاره‌ها استفاده می‌کنند و ۴۷ لم اثبات‌شده از صورت‌بندی قبلی خود دادیم و نقش‌های رهبر و کمک‌کننده را تعیین کردیم. هیچ راهنمایی دیگری درباره نحوه اثبات قضیه یا سازماندهی خودشان ارائه نکردیم.

این آزمایش مقیاس کوچک نشان می‌دهد که تیم‌هایی از عامل‌ها که مدل‌هایی مانند فبل ۵.۲ را اجرا می‌کنند، می‌توانند اهداف جاه‌طلبانه و بلندمدت را در چارچوب مرزهای ایمنی طراحی‌شده با دقت محقق سازند.

مسئله

قضیه آخر فرما بیان می‌کند که هیچ عدد صحیح مثبت a، b و c وجود ندارد که رابطه aⁿ + bⁿ = cⁿ را برای هر n بزرگ‌تر از ۲ صدق کند. این قضیه بیش از ۳۵۰ سال بدون اثبات باقی ماند، تا اینکه سر اندرو وایلز در سال ۱۹۹۵ اثبات ۱۲۹ صفحه‌ای خود را ارائه داد. صورت‌بندی این اثبات—یعنی قابل بررسی کردن هر مرحله توسط رایانه—به مدت طولانی هدفی دیرپا در جامعه ریاضیات بوده است.

صورت‌بندی سپتامبر ما ۱۱ روز و حدود ۶ میلیارد توکن خروجی برای یک پژوهشگر و ده‌ها عامل نیاز داشت. آن‌ها ۱۳ میلیون خط کد در Lean نوشتند؛ زبانی برنامه‌نویسی که در آن یک رایانه هر مرحله از اثبات را بررسی می‌کند.

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

داربست (Harness)

ما می‌خواستیم ببینیم آیا تیمی از عامل‌ها که روی مدل‌هایی مانند فبل ۵.۲ اجرا می‌شوند، می‌توانند بدون Prove2Me یا هدایت پژوهشگر، با استفاده از داربستی ساخته‌شده از ابزارهای همه‌منظوره، این نتیجه را تولید کنند یا خیر.

ابزارها

برای این تکلیف، به تیم ۱,۰۰۰ عاملی ۶۰ گزاره برای اثبات دادیم، شامل قضیه نهایی و ۵9 نقطه عطف میانی. برای هر گزاره، عامل‌ها باید اثباتی را در Lean بنویسند، آن را با ابزارهای Lean بسازند و بررسی کنند و سپس آن را به شاخه اصلی مشترک در Git ارسال کنند، جایی که یک ارزیاب آن را چک می‌کرد. ما ابزارهای زیر را به هر عامل دادیم:

  • یک پوسته (Shell) و یک ویرایشگر فایل، در محیط ایزوله مخصوص خود بدون دسترسی به شبکه.
  • زنجیره ابزار Lean و Mathlib، که در تصویر محیط ایزوله تعبیه شده بود.
  • شاخه Git مخصوص خود، به همراه امکان باز کردن درخواست ادغام (Merge Request) به شاخه اصلی.
  • یک پایگاه داده Postgres مشترک، که از طریق پوسته به آن دسترسی داشتند.

همکاری

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

برای این اجرا، هر عامل یک محیط ایزوله روی ماشین مجازی سبک‌وزن مخصوص خود داشت. یک ماشین مشترک منفرد در حدود ۱۰۰ عامل به محدودیت‌های خود برخورد می‌کرد: بیش از نیمی از اجراهای ۱۰۰ عاملی ما به دلیل اتمام حافظه، دیسک یا CPU متوقف یا شروع مجدد می‌شدند.

معماری داربست. انبوهی از ۱,۰۰۰ محیط ایزوله عامل (۱ رهبر و ۹۹۹ کمک‌کننده)، که هر کدام حلقه عامل، کد داربست داخل محیط ایزوله، با پوسته و ویرایشگر فایل به عنوان ابزار و مخزن، Lean و کتابخانه ریاضی به عنوان فایل‌ها را اجرا می‌کنند. درخواست‌ها و پاسخ‌های API بین حلقه عامل و دروازه‌ای خارج از محیط‌های ایزوله که API کلود را صدا می‌زند، رد و بدل می‌شوند. درخواست‌های Git و SQL و نتایج آن‌ها از طریق همان دروازه به زیرساخت تیم، که نیز خارج از محیط‌های ایزوله است، عبور می‌کنند: یک مخزن Git شامل فایل‌های Lean و طرح‌ها، و یک پایگاه داده Postgres شامل دستورالعمل‌ها، وظایف و یادداشت‌ها.
شکل ۱: هر یک از ۱,۰۰۰ عامل در محیط ایزوله مخصوص خود اجرا می‌شد و تنها از طریق یک لوله (Pipe) به یک دروازه (Gateway) به بیرون متصل بودند. دروازه API کلود را صدا می‌زد و درخواست‌های Git و SQL را به مخزن و پایگاه داده مشترک منتقل می‌کرد.

با ۱,۰۰۰ محیط ایزوله جداگانه، عامل‌ها به راهی برای اشتراک‌گذاری کار خود نیاز داشتند، بنابراین به آن‌ها یک پایگاه داده SQL (شکل ۱) دادیم. ما SQL را انتخاب کردیم زیرا اصول اولیه عمومی برای سازماندهی اطلاعات ارائه می‌دهد، تراکنش‌های آن با نوشتن‌های همزمان ۱,۰۰۰ عامل کنار می‌آیند و کلود از قبل با آن آشناست. عامل‌ها از پایگاه داده برای تصاحب وظایف، اشتراک‌گذاری یادداشت‌ها و ثبت کارهای تمام‌شده استفاده کردند.

پرامپت‌نویسی

پرامپت ما به کلود فهرستی از ۶۰ گزاره برای اثبات می‌داد، هر کدام با یک توضیح غیررسمی یک‌خطی، و ابزارهای موجود (فهرست‌شده در بالا) را توصیف می‌کرد.

تنها ساختاری که به تیم دادیم یک سلسله‌مراتب بود، متشکل از یک رهبر و ۹۹۹ کمک‌کننده. به رهبر گفتیم مسئله را به بخش‌هایی تقسیم کند و آن‌ها را به کمک‌کننده‌ها اختصاص دهد. به کمک‌کننده‌ها گفتیم انتظار کار از رهبر را داشته باشند و اگر تکلیفی مبهم بود، با رهبر مشورت کنند.

در طول اجرا، داربست ۱۹ یادآوری خودکار به رهبر ارسال کرد که چقدر زمان باقی مانده است، و هر کدام او را تشویق می‌کردند به ادامه دادن.

ایمنی

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

معماری داربست با تدابیر ایمنی آن که در سه گروه مشخص شده‌اند. محیط ایزوله: هر عامل یک VM سبک‌وزن مخصوص خود بدون دسترسی به شبکه، بدون کلیدهای API یا اعتبارنامه‌ها، بدون مسیر مستقیم به سایر محیط‌های ایزوله، یک حساب کاربری بدون امتیاز ویژه و بدون دسترسی ابزاری به کد داربست دریافت می‌کند. مانیتورینگ بلادرنگ: دروازه یک طبقه‌بند مسدودکننده را روی هر فراخوانی ابزار اجرا می‌کند، با طراحی Fail-Closed، هویت هر عامل را تنظیم می‌کند و هر Push و Query را لاگ می‌گیرد؛ مخزن Git تنها Pushهای شاخه مخصوص را با یک کار ادغام برای شاخه اصلی قبول می‌کند و پایگاه داده Postgres از یک نقش مشترک بدون امتیاز ویژه با محدودیت‌های زمانی و حجمی استفاده می‌کند. مانیتورینگ آفلاین: رکوردهای اجرا که خارج از محیط‌های ایزوله نگه‌داشته می‌شوند، مانیتورینگ آفلاین را تغذیه می‌کنند، که یافته‌های جدی را به مالکان اجرا گزارش می‌دهد.
شکل ۲: سه لایه ایمنی تیم را احاطه کرده بودند: محیط ایزوله، مانیتورینگ بلادرنگ و مانیتورینگ آفلاین. یک طبقه‌بند هر فراخوانی ابزار را قبل از اجرا بررسی می‌کرد و یک مانیتور آفلاین اقدامات تیم را بازبینی می‌نمود.

محیط ایزوله (Sandboxing)

ما محیط ایزوله هر عامل را به روش‌های زیر ایمن کردیم (شکل ۲):

  • ارتباطات: عامل‌ها ابزار پیام‌رسانی اختصاصی نداشتند و تنها از طریق پایگاه داده و Git هماهنگ می‌شدند.
  • تغییرات کد: یک عامل فقط می‌توانست به شاخه Git مخصوص خود Push کند و درخواست ادغام به شاخه اصلی باز کند. سپس یک کار جداگانه تغییرات را به شاخه اصلی ادغام می‌کرد و آن‌ها را تنها در موارد تضاد یا خطا، مانند تاریخچه نامرتبط، رد می‌نمود.
  • دسترسی به پایگاه داده: فراخوانی‌های پایگاه داده تحت یک نقش مشترک بدون امتیاز ویژه (Unprivileged Role) اجرا می‌شدند. هر دستور SQL محدودیت زمانی پنج ثانیه داشت و نوشتن‌های بالای ۲۵۶ مگابایت رد می‌شدند.
  • کنترل‌های شبکه: محیط‌های ایزوله دسترسی به شبکه نداشتند. تنها لینک خروجی آن‌ها یک لوله به دروازه بود که درخواست‌های آن‌ها را انتقال می‌داد.
  • هویت: دروازه هر درخواست را با هویت عامل خارج از محیط ایزوله برچسب می‌زد، تا از جعل هویت یک عامل توسط عامل دیگر جلوگیری شود.
  • هسته (Kernel): هسته هر محیط ایزوله بدون ویژگی‌هایی ساخته شد که به کاربر ریشه (Root) مسیر مستقیمی به داخل آن می‌دهد، مانند ماژول‌های بارگذاری‌شدنی، kexec، دسترسی مستقیم به حافظه خام و کاوشگرهای هسته. آن در حالت قفل هسته (Kernel Lockdown) اجرا می‌شد.
  • کمترین سطح دسترسی: دستورات هر عامل داخل محیط ایزوله آن به عنوان کاربر بدون امتیاز ویژه اجرا می‌شد، با حذف ابزارهایی مانند sudo که می‌توانستند دسترسی ریشه را بازیابی کنند. ابزارهای عامل به گونه‌ای طراحی شده بودند که نمی‌توانستند حلقه عاملی که آن‌ها را اجرا می‌کرد بخوانند یا تغییر دهند.

مانیتورینگ بلادرنگ

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

برای تست اینکه آیا طبقه‌بند ما می‌تواند خرابکاری پیچیده را تشخیص دهد، ارزیابی‌های تکلیف جانبی و خرابکاری چندعاملی را اجرا کردیم، که در آن عامل‌های تیم قرمز (Red-team) از استراتژی‌هایی مانند حملات تجزیه‌ای (Decomposition Attacks) برای فریب دادن طبقه‌بند جهت اجازه فرار از محیط ایزوله استفاده کردند. ما دریافتیم که مانیتورهایی که زنجیره افکار (CoT) عامل‌ها و ارتباط بین‌عاملی را مشاهده می‌کردند، توانستند تمام تلاش‌های خرابکاری را در این ارزیابی‌ها تشخیص دهند، بنابراین اکنون از آن‌ها برای مانیتورینگ اجراهای چندعاملی خود استفاده می‌کنیم. به‌طور موازی، ما نسخه مبتنی بر اقدام (Action-based) همان مانیتور را—which تنها اقدامات را می‌بیند، نه CoT—اجرا می‌کنیم تا از این خطر جلوگیری کنیم که استدلال یک عامل، مانیتور را متقاعد به اجازه دادن به یک اقدام مضر کند.

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

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

در میان بیش از یک میلیون فراخوانی ابزار، هیچ‌کدام در این اجرا معیار لازم برای مسدود شدن را برآورده نکرد. وقتی این فراخوانی‌ها را علیه مانیتور CoT و معیارهای امروز بازپخش کردیم، تنها یکی، یک بررسی برای دسترسی ریشه، نزدیک به مسدود شدن بود.

مانیتورینگ آفلاین

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

نتایج

بدون Prove2Me، تیم سیستم هماهنگی خود را ساخت

کار روی این اثبات در چند سطح انجام می‌شود:

  • اثبات: هیچ عدد صحیح مثبت a، b و c وجود ندارد که رابطه aⁿ + bⁿ = cⁿ را برای هر n بزرگ‌تر از ۲ صدق کند.
  • گزاره‌ها: ما به تیم ۶۰ گزاره برای اثبات دادیم، شامل قضیه نهایی و ۵۹ نقطه عطف میانی.
  • گزاره‌های کوچک‌تر: عامل‌ها گزاره‌های دشوار را به گزاره‌های کوچک‌تری، یا لم‌ها، تقسیم می‌کردند.
  • Lean: هر گزاره و لم یک قضیه در Lean است.

هر گزاره در Lean با یک جایگزین (Placeholder) برای اثبات خود شروع می‌شد و تنها زمانی اثبات‌شده محسوب می‌شد که بررسی‌کننده Lean یک اثبات کامل را می‌پذیرفت. ما به رهبر اجازه دادیم تصمیم بگیرد چگونه با اثبات مقابله کند و چگونه تیم را در این سطوح کاری هماهنگ نماید.

پنج جدول پایگاه داده مشترک بین ۱ رهبر و ۹۹۹ کمک‌کننده. Announce، دستورات رهبر به همه، مانند نحوه تقسیم کار یا کاهش فشار بر پایگاه داده: رهبر آن را می‌نویسد و می‌خواند، کمک‌کننده‌ها آن را می‌خوانند، با یک نوشتن توسط کمک‌کننده. Assign، چه کسی روی چه چیزی کار می‌کند، مانند اینکه کدام کمک‌کننده مالک یا نماینده هر گزاره است: رهبر آن را می‌نویسد و می‌خواند، کمک‌کننده‌ها آن را می‌خوانند، با یک نوشتن توسط کمک‌کننده. Notes، یک تابلوی باز که کمک‌کننده‌ها می‌گویند کدام بخش را تصاحب می‌کنند یا پیشرفت را گزارش می‌دهند: رهبر و کمک‌کننده‌ها هر دو آن را می‌نویسند و می‌خوانند. Subtasks، یک لیست کارهای مشترک که هر کسی وظیفه‌ای اضافه می‌کند و اولین کمک‌کننده‌ای که آن را می‌گیرد مالک آن می‌شود: کمک‌کننده‌ها آن را می‌نویسند و می‌خوانند، و رهبر آن را می‌خواند، با دو نوشتن توسط رهبر. Landed، یک لاگ از کارهای تمام‌شده که ثبت می‌کند کدام گزاره یا بخش فرود آمد (Landed)، کامیت آن و آیا از بررسی‌های تیم عبور کرد: کمک‌کننده‌ها آن را می‌نویسند و می‌خوانند، و رهبر آن را می‌خواند.
شکل ۳: در ۱۰ دقیقه اول، رهبر پنج جدول پایگاه داده مشترک را برای هماهنگ کردن تیم تنظیم کرد. رهبر دستورات و تخصیص‌ها را می‌نوشت، کمک‌کننده‌ها کارهای تمام‌شده را لاگ می‌کردند و جدول زیروظایف را مدیریت می‌کردند، و هر دو به جدول یادداشت‌ها می‌نوشتند.

در ۱۰ دقیقه اول، رهبر پنج جدول در پایگاه داده ایجاد کرد (شکل ۳):

  • Announce: دستورات رهبر به کل تیم (مثلاً نحوه تقسیم کار).
  • Assign: چه کسی روی چه چیزی کار می‌کند (مثلاً کدام کمک‌کننده مالک یا نماینده هر گزاره است).
  • Notes: یک تابلوی باز (مثلاً برای تصاحب بخشی از کار یا گزارش پیشرفت).
  • Subtasks: یک لیست کارها که هر عامل می‌تواند وظیفه‌ای اضافه کند و اولین کمک‌کننده‌ای که آن را تصاحب کند، مالک آن می‌شود.
  • Landed: یک لاگ از کارهای تمام‌شده.

رهبر گزاره‌ها را توزیع کرد

پس از اینکه رهبر جداول را ایجاد کرد، سه کار انجام داد. اول، هر گزاره را به یک گروه ۱۶ تا ۱۷ نفره از کمک‌کننده‌ها با نوشتن ۹۹۹ ردیف در جدول assign، یکی برای هر کمک‌کننده، اختصاص داد. دوم، یک کمک‌کننده در هر گروه را به عنوان کاپیتان تعیین کرد، مسئول برای ارسال یک طرح به جدول notes و تقسیم کار به وظایف برای تصاحب گروه از جدول subtasks. سوم، دستورالعمل‌ها را در جدول announce قرار داد و به هر کمک‌کننده گفت که با قضاوت دشواری گزاره خود و ارسال حکم در جدول notes شروع کند.

از پرامپت خود، کمک‌کننده‌ها می‌دانستند که پایگاه داده وجود دارد. آن‌ها جدول announce را پیدا کردند و ارزیابی‌های خود را شروع کردند. اکثر آن‌ها احکام را در جدول notes ارسال کردند. حدود ۲۷ دقیقه بعد، سه گزاره قبلاً اثبات شده بودند و رهبر احکام ارسال‌شده را خوانده بود. سپس ۴۷ گزاره‌ای که اکثر کمک‌کننده‌ها آن‌ها را غیرقابل‌اجرا در بودجه اجرا قضاوت کرده بودند را کنار گذاشت و تقریباً تمام کمک‌کننده‌ها را به ۱۰ مورد باقی‌مانده که فکر می‌کرد می‌توانند تمام کنند، مجدداً اختصاص داد. گروه‌ها از حدود ۱۷ کمک‌کننده به بین ۴۶ تا ۱۳۹ نفر رشد کردند.

هر کمک‌کننده در یک حلقه کار می‌کرد، که بیشتر آن در دستورات رهبر آمده بود:

  • طرح گزاره را در جدول notes پیدا کنید.
  • یک وظیفه از جدول subtasks تصاحب کنید.
  • اثبات را در Lean بنویسید، آن را با ابزارهای Lean بررسی کنید و به شاخه اصلی در Git ارسال کنید.
  • وظیفه را به عنوان انجام‌شده علامت بزنید.
  • یک به‌روزرسانی در جدول notes ارسال کنید.

حدود ۴۵ دقیقه بعد، با اثبات حدود پنج مورد از ۱۰ گزاره، رهبر نوشت:

«ظرفیت پردازش تیم بسیار بالاتر از احکام اولیه 'غیرقابل‌اجرا در بودجه' فرض‌شده است»

تمام ۱۰ گزاره در حدود ۷۰ دقیقه اثبات شدند.

تایم‌لپس از ساعت ۰ تا ساعت ۳۰ از خواندن و نوشتن بین ۱,۰۰۰ عامل و جداول پایگاه داده مشترک: announce، assign، notes، subtasks، landed و گروهی از جداول دیگر. نوشتن‌ها به عنوان خطوط قرمز از ردیف بالای رهبر و کمک‌کننده‌های ۱ تا ۹۹۹ به پایین به سمت جداول، و خواندن‌ها به عنوان خطوط سبز از جداول به پایین به همان عامل‌ها در ردیف پایین اجرا می‌شوند. شمارش‌ها تا ساعت ۳۰ به ۳۶,۶۱۲ نوشتن و ۳۱۱,۷۳۴ خواندن می‌رسند. تقریباً تمام نوشتن‌ها به جدول notes، حدود ۲۰,۶۰۰، و جدول subtasks، حدود ۱۴,۸۰۰، می‌روند و خطوط در حدود ساعت ۱۸ آرام می‌شوند، زمانی که اجرا شروع مجدد شد.
شکل ۴: خواندن از (سبز) و نوشتن به (قرمز) جداول مشترک در طول اجرا. تقریباً تمام نوشتن‌ها یادداشت‌ها و به‌روزرسانی‌های وظایف کمک‌کننده‌ها است، شامل تصاحب وظایف. مجموع‌ها اکثر فراخوانی‌های اسکریپت را کنار می‌گذارند. فعالیت در حدود ساعت ۱۸ متوقف می‌شود، زمانی که ما اجرا را از آخرین ذخیره آن شروع مجدد کردیم و به عامل‌ها ۱۲ ساعت وقت بیشتر دادیم.

سپس رهبر کمک‌کننده‌ها را به گزاره‌های دشوارتر منتقل کرد

با اتمام آن ۱۰ گزاره اول، رهبر نوشت، «هیچ دلیلی برای بیکاری وجود ندارد»، و کمک‌کننده‌ها را به گزاره‌های دشوارتری که ابتدا کنار گذاشته بود، مجدداً اختصاص داد. همانطور که گزاره‌های بیشتری اثبات می‌شدند، او همچنان کمک‌کننده‌ها را به تخصیص‌های جدید منتقل می‌کرد، عمدتاً در شش ساعت اول (به نوشتن‌ها در جدول assign، که به رنگ قرمز در شکل ۴ نمایش داده شده است، توجه کنید).

در ابتدا، رهبر به کاپیتان‌ها دستور داد کار را به وظایف در جدول subtasks تقسیم کنند. همانطور که کار پیش رفت، کمک‌کننده‌ها مسئولیت بیشتری برای حل هر گزاره پذیرفتند. آن‌ها شروع به نوشتن وظایف کردند، گاهی پس از اینکه کاپیتان درخواست کمک می‌کرد. تا ساعت ۵.۶، ۷۳ کمک‌کننده ۷۵۶ وظیفه نوشته بودند و تنها ۱۶ نفر از آن کمک‌کننده‌ها کاپیتان بودند. شکل ۴ نوشتن‌ها (به رنگ قرمز) به جدول subtasks از بسیاری از کمک‌کننده‌ها را نشان می‌دهد، هرچند اکثر این نوشتن‌ها برای تصاحب یک وظیفه یا علامت‌گذاری آن به عنوان انجام‌شده بود. کمک‌کننده‌هایی که یک وظیفه را تمام کردند، داوطلب کار بیشتر شدند:

«آزاد ... من قطعات را از ابتدا تا انتها تمام می‌کنم ... یک قطعه عمیق نام ببر ... و من فوراً شروع می‌کنم»

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

رهبر تیم را به لنگلندز-تونل اختصاص داد

حدود ساعت ۱۸، تنها چیزی که باقی مانده بود لنگلندز-تونل بود، یک نتیجه کلاسیک که اثبات وایلز به آن متکی است، به علاوه گزاره‌هایی که به آن وابسته بودند و یک گزاره دیگر که تیم در طول راه اثبات کرد. در ابتدای اجرا، کاپیتان وظیفه لنگلندز-تونل بدبینانه بود و تخمین زد که اثبات حداقل ۰.۷ تا ۱ میلیون خط کد Lean نیاز خواهد داشت، با کمتر از ۱٪ شانس تمام شدن در زمان مقرر. رهبر آن گزاره را کنار گذاشت.

با اتمام تقریباً تمام کارهای دیگر، رهبر تمرکز تیم را دوباره روی لنگلندز-تونل گذاشت. در آخرین تخصیص بالا به پایین، او حدود ۷۵۰ کمک‌کننده را به آن گزاره منتقل کرد و نوشت، «شانس‌های صادقانه پایین است.»

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

تایم‌لپس از ساعت ۲۰.۵ تا ساعت ۲۸.۹ از درخت وظایف زیر لنگلندز-تونل، که به صورت حلقه‌هایی حول گزاره رسم شده است، با زیرحوزه‌های آن به عنوان نقاط سیاه نزدیک مرکز. وظایف هنگامی که کمک‌کننده‌ها آن‌ها را می‌نویسند ظاهر می‌شوند و از خاکستری به نارنجی و سپس قرمز تیره تغییر می‌کنند هنگامی که برای اولین بار به عنوان انجام‌شده علامت می‌خورند، با ساعات بعدی به رنگ تیره‌تر. تا ساعت ۲۸.۹، درخت تمام ۲,۴۱۸ وظیفه را در خود جای داده است، ۲,۳۶۴ مورد از آن‌ها با ساعت مشخصی به عنوان انجام‌شده علامت خورده‌اند و شاخه‌های عمیق‌ترین آن به حلقه‌های بیرونی می‌رسند.
شکل ۵: درخت وظایف زیر لنگلندز-تونل، که از ساعت ۲۰.۵ تا اثبات گزاره در ساعت ۲۸.۴ رشد کرد. هر حلقه به سمت بیرون یک سطح عمیق‌تر است و وظایف هنگامی که برای اولین بار به عنوان انجام‌شده علامت می‌خورند از خاکستری به رنگی تغییر می‌کنند. خطوط نشان می‌دهند که چگونه وظایف تقسیم شدند. ما اکثر این پیوندها را پس از آن از برچسب‌های وظایف کمک‌کننده‌ها استنتاج کردیم.

بنابراین تیم کار را به صورت یک درخت سازماندهی کرد. کاپیتان طرحی ایجاد کرد که گزاره را به ۱۰ حوزه تقسیم می‌کرد و هر قطعه را به عنوان یک وظیفه فهرست می‌نمود. یک کمک‌کننده که قطعه‌ای را برای مقابله به تنهایی بسیار بزرگ می‌یافت، می‌توانست آن را تقسیم کند و وظایف کوچک‌تری را زیر آن اضافه کند. درخت هر زمان که یک قطعه برای یک عامل منفرد بسیار دشوار ثابت می‌شد، رشد می‌کرد و در نهایت به ۲,۴۱۸ وظیفه تا عمق ۱۰ سطح رسید (شکل ۵). هر قطعه می‌توانست قطعات زیرین خود را فرض کند، بنابراین صدها کمک‌کننده می‌توانستند قبل از اثبات آن قطعات، به‌صورت موازی کار کنند.

تایم‌لپس از ساعت ۰ تا ساعت ۳۰ از جایی که هر یک از ۹۹۹ کمک‌کننده کار می‌کردند، نمونه‌برداری شده هر ۵ دقیقه. ۶۰ گزاره نقاطی هستند که بر اساس نحوه پرسنل‌دهی رهبر دسته‌بندی شده‌اند: اول فرود آمدند، قابل‌اجرا قضاوت شدند، کنار گذاشته شدند اما تا ساعت ۱.۲ پرسنل‌دهی شدند، کنار گذاشته شدند و از ساعت ۱.۵ برداشته شدند، بالابردن مدولاریتی، لنگلندز-تونل، و پیوندهای نهایی تا قضیه آخر فرما. کمک‌کننده‌ها به عنوان نقاط نارنجی حول گزاره‌هایی که روی آن‌ها کار می‌کنند خوشه می‌شوند: در ساعات اول روی گزاره‌های زیادی پخش شدند، از حدود ساعت ۸ روی بالابردن مدولاریتی شلوغ شدند، در حدود ساعت ۱۸ متوقف شدند و پس از شروع مجدد روی لنگلندز-تونل جمع شدند. در ساعت ۳۰، ۵۴ از ۶۰ گزاره اثبات شده و سیاه پر شده‌اند.
شکل ۶: هر نقطه یک کمک‌کننده است، که هر پنج دقیقه در موقعیت گزاره یا خط کاری که رکوردهای خودش نشان می‌داد روی آن کار می‌کرد، قرار گرفته است، شامل زمانی که منتظر ساخت (Build) بود. کمک‌کننده‌ها روی گزاره‌ها پخش شدند و روی لنگلندز-تونل همگرا شدند. شمارش در ۵۴ از ۶۰ گزاره پایان می‌یابد زیرا پنج جایگزین دیگر مورد نیاز نبودند و یک گزاره حذف شد.

شکل ۶ نشان می‌دهد که هر کمک‌کننده در طول کل اجرا روی چه چیزی کار کرده است، با کمک‌کننده‌هایی که در اوایل روی گزاره‌های زیادی پخش بودند و در انتها روی لنگلندز-تونل جمع شدند. لنگلندز-تونل در ساعت ۲۸.۴ اثبات شد، دنبال شده توسط قضیه نهایی در ساعت ۲۸.۷. سپس رهبر نوشت:

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

نتیجه‌گیری‌ها

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

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

هدایت انسانی نیز همچنان می‌تواند در نقاط خاصی مفید باشد. عامل‌ها تمایل دارند از مسائل دشوار دست بکشند و دشواری آن‌ها را اشتباه قضاوت کنند. در اوایل، کمک‌کننده‌ها ۴۷ از ۶۰ گزاره را غیرقابل‌اجرا در بودجه اجرا قضاوت کردند، با این حال تیم به اثبات اکثر آن‌ها ادامه داد. تشویق انسانی در چنین لحظاتی می‌تواند از توقف زودهنگام عامل‌ها جلوگیری کند.

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

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

هدایت انسانی نیز همچنان می‌تواند در نقاط خاصی مفید باشد. عامل‌ها تمایل دارند از مسائل دشوار دست بکشند و دشواری آن‌ها را اشتباه قضاوت کنند. در اوایل، کمک‌کننده‌ها ۴۷ از ۶۰ گزاره را غیرقابل‌اجرا در بودجه اجرا قضاوت کردند، با این حال تیم به اثبات اکثر آن‌ها ادامه داد. تشویق انسانی در چنین لحظاتی می‌تواند از توقف زودهنگام عامل‌ها جلوگیری کند.

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

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

اشتراک:
این گزارش ترجمه و بازنویسی خبری با موتور هوش مصنوعی افق آبی است و برای خوانندهٔ فارسی‌زبان بازتنظیم شده. منبع اصلی: claude.dev