تیمهای چندعاملی میتوانند مسائل دشوار و بلندمدت را حل کنند. در ماه سپتامبر، ما نخستین صورتبندی رسمی کامل از قضیه آخر فرما را منتشر کردیم که توسط دهها عاملِ در حال اجرای یک مدل تحقیقاتی داخلی، تقریباً همارز با کلود فبل ۵.۱، نوشته شده بود. آن کار به 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 متوقف یا شروع مجدد میشدند.
با ۱,۰۰۰ محیط ایزوله جداگانه، عاملها به راهی برای اشتراکگذاری کار خود نیاز داشتند، بنابراین به آنها یک پایگاه داده SQL (شکل ۱) دادیم. ما SQL را انتخاب کردیم زیرا اصول اولیه عمومی برای سازماندهی اطلاعات ارائه میدهد، تراکنشهای آن با نوشتنهای همزمان ۱,۰۰۰ عامل کنار میآیند و کلود از قبل با آن آشناست. عاملها از پایگاه داده برای تصاحب وظایف، اشتراکگذاری یادداشتها و ثبت کارهای تمامشده استفاده کردند.
پرامپتنویسی
پرامپت ما به کلود فهرستی از ۶۰ گزاره برای اثبات میداد، هر کدام با یک توضیح غیررسمی یکخطی، و ابزارهای موجود (فهرستشده در بالا) را توصیف میکرد.
تنها ساختاری که به تیم دادیم یک سلسلهمراتب بود، متشکل از یک رهبر و ۹۹۹ کمککننده. به رهبر گفتیم مسئله را به بخشهایی تقسیم کند و آنها را به کمککنندهها اختصاص دهد. به کمککنندهها گفتیم انتظار کار از رهبر را داشته باشند و اگر تکلیفی مبهم بود، با رهبر مشورت کنند.
در طول اجرا، داربست ۱۹ یادآوری خودکار به رهبر ارسال کرد که چقدر زمان باقی مانده است، و هر کدام او را تشویق میکردند به ادامه دادن.
ایمنی
همانطور که قبلاً به اشتراک گذاشتهایم، هیچ لایه دفاعی منفردی برای مهار یک تیم عامل کافی نیست. در این آزمایش، ما محیط ایزوله (Sandboxing) را با مانیتورینگ بلادرنگ و آفلاین ترکیب کردیم تا هر عامل را در ماشین مجازی مخصوص خود بدون دسترسی به شبکه نگه داریم و هرگونه تلاش برای فرار از محیط ایزوله یا دستکاری مانیتورینگ را تشخیص دهیم.
محیط ایزوله (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: یک لاگ از کارهای تمامشده.
رهبر گزارهها را توزیع کرد
پس از اینکه رهبر جداول را ایجاد کرد، سه کار انجام داد. اول، هر گزاره را به یک گروه ۱۶ تا ۱۷ نفره از کمککنندهها با نوشتن ۹۹۹ ردیف در جدول assign، یکی برای هر کمککننده، اختصاص داد. دوم، یک کمککننده در هر گروه را به عنوان کاپیتان تعیین کرد، مسئول برای ارسال یک طرح به جدول notes و تقسیم کار به وظایف برای تصاحب گروه از جدول subtasks. سوم، دستورالعملها را در جدول announce قرار داد و به هر کمککننده گفت که با قضاوت دشواری گزاره خود و ارسال حکم در جدول notes شروع کند.
از پرامپت خود، کمککنندهها میدانستند که پایگاه داده وجود دارد. آنها جدول announce را پیدا کردند و ارزیابیهای خود را شروع کردند. اکثر آنها احکام را در جدول notes ارسال کردند. حدود ۲۷ دقیقه بعد، سه گزاره قبلاً اثبات شده بودند و رهبر احکام ارسالشده را خوانده بود. سپس ۴۷ گزارهای که اکثر کمککنندهها آنها را غیرقابلاجرا در بودجه اجرا قضاوت کرده بودند را کنار گذاشت و تقریباً تمام کمککنندهها را به ۱۰ مورد باقیمانده که فکر میکرد میتوانند تمام کنند، مجدداً اختصاص داد. گروهها از حدود ۱۷ کمککننده به بین ۴۶ تا ۱۳۹ نفر رشد کردند.
هر کمککننده در یک حلقه کار میکرد، که بیشتر آن در دستورات رهبر آمده بود:
- طرح گزاره را در جدول notes پیدا کنید.
- یک وظیفه از جدول subtasks تصاحب کنید.
- اثبات را در Lean بنویسید، آن را با ابزارهای Lean بررسی کنید و به شاخه اصلی در Git ارسال کنید.
- وظیفه را به عنوان انجامشده علامت بزنید.
- یک بهروزرسانی در جدول notes ارسال کنید.
حدود ۴۵ دقیقه بعد، با اثبات حدود پنج مورد از ۱۰ گزاره، رهبر نوشت:
«ظرفیت پردازش تیم بسیار بالاتر از احکام اولیه 'غیرقابلاجرا در بودجه' فرضشده است»
تمام ۱۰ گزاره در حدود ۷۰ دقیقه اثبات شدند.
سپس رهبر کمککنندهها را به گزارههای دشوارتر منتقل کرد
با اتمام آن ۱۰ گزاره اول، رهبر نوشت، «هیچ دلیلی برای بیکاری وجود ندارد»، و کمککنندهها را به گزارههای دشوارتری که ابتدا کنار گذاشته بود، مجدداً اختصاص داد. همانطور که گزارههای بیشتری اثبات میشدند، او همچنان کمککنندهها را به تخصیصهای جدید منتقل میکرد، عمدتاً در شش ساعت اول (به نوشتنها در جدول assign، که به رنگ قرمز در شکل ۴ نمایش داده شده است، توجه کنید).
در ابتدا، رهبر به کاپیتانها دستور داد کار را به وظایف در جدول subtasks تقسیم کنند. همانطور که کار پیش رفت، کمککنندهها مسئولیت بیشتری برای حل هر گزاره پذیرفتند. آنها شروع به نوشتن وظایف کردند، گاهی پس از اینکه کاپیتان درخواست کمک میکرد. تا ساعت ۵.۶، ۷۳ کمککننده ۷۵۶ وظیفه نوشته بودند و تنها ۱۶ نفر از آن کمککنندهها کاپیتان بودند. شکل ۴ نوشتنها (به رنگ قرمز) به جدول subtasks از بسیاری از کمککنندهها را نشان میدهد، هرچند اکثر این نوشتنها برای تصاحب یک وظیفه یا علامتگذاری آن به عنوان انجامشده بود. کمککنندههایی که یک وظیفه را تمام کردند، داوطلب کار بیشتر شدند:
«آزاد ... من قطعات را از ابتدا تا انتها تمام میکنم ... یک قطعه عمیق نام ببر ... و من فوراً شروع میکنم»
در ابتدا، رهبر همچنین کمککنندهها را به گزارههای خاص اختصاص میداد. این موضوع شروع به تغییر در ساعت اول کرد و تا ساعت سوم، رهبر به کمککنندههای آزاد گفت، «منتظر من نباشید». این امر به کمککنندههای آزاد اجازه داد کار روی گزارههای مختلف را بدون انتظار برای رهبر بردارند، حتی در حالی که او همچنان تخصیصهای جدید مینوشت.
رهبر تیم را به لنگلندز-تونل اختصاص داد
حدود ساعت ۱۸، تنها چیزی که باقی مانده بود لنگلندز-تونل بود، یک نتیجه کلاسیک که اثبات وایلز به آن متکی است، به علاوه گزارههایی که به آن وابسته بودند و یک گزاره دیگر که تیم در طول راه اثبات کرد. در ابتدای اجرا، کاپیتان وظیفه لنگلندز-تونل بدبینانه بود و تخمین زد که اثبات حداقل ۰.۷ تا ۱ میلیون خط کد Lean نیاز خواهد داشت، با کمتر از ۱٪ شانس تمام شدن در زمان مقرر. رهبر آن گزاره را کنار گذاشت.
با اتمام تقریباً تمام کارهای دیگر، رهبر تمرکز تیم را دوباره روی لنگلندز-تونل گذاشت. در آخرین تخصیص بالا به پایین، او حدود ۷۵۰ کمککننده را به آن گزاره منتقل کرد و نوشت، «شانسهای صادقانه پایین است.»
لنگلندز-تونل بسیار بزرگتر از هر گزاره دیگری بود که عاملها روی آن کار کرده بودند، حدود نه برابر وظایف بیشتر و بیش از دو برابر کد جدید نیاز داشت. کمککنندهها دوباره از جدول subtasks برای تقسیم کار استفاده کردند، اما بسیاری از وظایف اولیه برای تکمیل توسط یک کمککننده به تنهایی بسیار بزرگ بودند.
بنابراین تیم کار را به صورت یک درخت سازماندهی کرد. کاپیتان طرحی ایجاد کرد که گزاره را به ۱۰ حوزه تقسیم میکرد و هر قطعه را به عنوان یک وظیفه فهرست مینمود. یک کمککننده که قطعهای را برای مقابله به تنهایی بسیار بزرگ مییافت، میتوانست آن را تقسیم کند و وظایف کوچکتری را زیر آن اضافه کند. درخت هر زمان که یک قطعه برای یک عامل منفرد بسیار دشوار ثابت میشد، رشد میکرد و در نهایت به ۲,۴۱۸ وظیفه تا عمق ۱۰ سطح رسید (شکل ۵). هر قطعه میتوانست قطعات زیرین خود را فرض کند، بنابراین صدها کمککننده میتوانستند قبل از اثبات آن قطعات، بهصورت موازی کار کنند.
شکل ۶ نشان میدهد که هر کمککننده در طول کل اجرا روی چه چیزی کار کرده است، با کمککنندههایی که در اوایل روی گزارههای زیادی پخش بودند و در انتها روی لنگلندز-تونل جمع شدند. لنگلندز-تونل در ساعت ۲۸.۴ اثبات شد، دنبال شده توسط قضیه نهایی در ساعت ۲۸.۷. سپس رهبر نوشت:
«از همه شما سپاسگزارم: قضیه آخر فرما روی شاخه اصلی است، با هسته بررسیشده توسط بررسیکننده رسمی.»
نتیجهگیریها
این آزمایش مقیاس کوچک به ما اجازه داد مطالعه کنیم که چگونه تیمی از ۱,۰۰۰ عامل از یک تکلیف طولانی و دشوار عبور کردند. با استفاده تنها از Git و یک پایگاه داده مشترک، عاملها جداولی را برای تخصیص نقشها و اشتراکگذاری نتایج طراحی کردند، تیمها تشکیل دادند و یک درخت وظایف ساختند تا دشوارترین گزاره را بشکنند، گزارهای که کاپیتان خودش کمتر از ۱٪ شانس تمام شدن در زمان مقرر را به آن داده بود.
این نتیجه نیاز به داربستها یا پلتفرمهای تخصصی دامنه را از بین نمیبرد. برای مثال، Prove2Me ممکن است همچنان با کمک به عاملها برای کامپایل سریعتر کد Lean و اجازه دادن به آنها برای جستجو و استفاده مجدد از نتایج انسانی، بهرهوری را بهبود بخشد.
هدایت انسانی نیز همچنان میتواند در نقاط خاصی مفید باشد. عاملها تمایل دارند از مسائل دشوار دست بکشند و دشواری آنها را اشتباه قضاوت کنند. در اوایل، کمککنندهها ۴۷ از ۶۰ گزاره را غیرقابلاجرا در بودجه اجرا قضاوت کردند، با این حال تیم به اثبات اکثر آنها ادامه داد. تشویق انسانی در چنین لحظاتی میتواند از توقف زودهنگام عاملها جلوگیری کند.
مرزهای ایمنی طراحیشده با دقت، اعتماد به نفس ما را برای اجرای این آزمایش از همان ابتدا فراهم کردند. کلود میتوانست با هر روشی که انتخاب میکند و با ابزارهایی که ما فراهم کردیم با مسئله مقابله کند، اما تنها داخل یک محیط ایزوله بدون دسترسی به شبکه و تحت دو مانیتور جداگانه.
این نتیجه نیاز به داربستها یا پلتفرمهای تخصصی دامنه را از بین نمیبرد. برای مثال، Prove2Me ممکن است همچنان با کمک به عاملها برای کامپایل سریعتر کد Lean و اجازه دادن به آنها برای جستجو و استفاده مجدد از نتایج انسانی، بهرهوری را بهبود بخشد.
هدایت انسانی نیز همچنان میتواند در نقاط خاصی مفید باشد. عاملها تمایل دارند از مسائل دشوار دست بکشند و دشواری آنها را اشتباه قضاوت کنند. در اوایل، کمککنندهها ۴۷ از ۶۰ گزاره را غیرقابلاجرا در بودجه اجرا قضاوت کردند، با این حال تیم به اثبات اکثر آنها ادامه داد. تشویق انسانی در چنین لحظاتی میتواند از توقف زودهنگام عاملها جلوگیری کند.
مرزهای ایمنی طراحیشده با دقت، اعتماد به نفس ما را برای اجرای این آزمایش از همان ابتدا فراهم کردند. کلود میتوانست با هر روشی که انتخاب میکند و با ابزارهایی که ما فراهم کردیم با مسئله مقابله کند، اما تنها داخل یک محیط ایزوله بدون دسترسی به شبکه و تحت دو مانیتور جداگانه.
ما انتظار داریم این روشها به سرعت تکامل یابند و همانطور که تیمهایی مانند این کار سختتری را بر عهده میگیرند، مرزهای ایمنی اطراف آنها باید همگام باقی بمانند. ما معتقدیم که تیمهای چندعاملی، اگر بهصورت ایمن مقیاسدهی شوند، در سالهای آینده به حل برخی از چالشبرانگیزترین مسائل ما کمک خواهند کرد.