۶۰ هزار خط کد تولید شده توسط هوش مصنوعی اکنون در قفس ریاضی سختگیرانهای از تنها ۹۳ خط محصور شدهاند. در ۲۸ ژوئیه ۲۰۲۶، توسعهدهندهای به نام schildep این پروژه را در گیتهاب منتشر کرد تا یک پیادهسازی تأییدشده رسمی (Formally Verified) از تقاطع مشهای هندسه ساختاری سهبعدی (3D CSG mesh intersection) ارائه دهد. هدف این پروژه اثبات این نکته است که حتی وقتی پیادهسازی یک سیستم «جعبه سیاه» است و توسط یک مدل زبانی بزرگ (LLM) نوشته شده، باز هم میتوان صحت مطلق آن را تضمین کرد.
در عصر فعلی که به آن «وایبکدینگ» ([Vibe Coding]) میگویند، برنامهنویسان اغلب بر اساس شهود یا تستهای واحد سطحی به قطعات کد تولید شده توسط AI اعتماد میکنند. طبق گزارش نویسنده پروژه، این رویکرد در هستههای هندسی پیچیده شکست میخورد؛ چراکه موارد خاص و نادر (Edge Cases) — مثل تداخل صفحات همتراز یا برخورد رأس با لبه — تقریباً غیرممکن است که با تستهای رایج جعبه-سیاه شناسایی شوند. با انتقال تأییدیه از سطح کد به سطح مشخصات فنی، این پروژه مرز اعتماد در برنامهنویسی را بازتعریف میکند.
همانطور که در تحلیلهای پیشین ما دربارهی امنیت مدلهای بازمتن اشاره کردیم، مشکل اصلی همواره عدم پیشبینیپذیری خروجیهای AI است. این پروژه با استفاده از Lean 4 — یک زبان برنامهنویسی تابعی و اثباتکننده قضایا — این مشکل را حل کرده است. این رویکرد در واقع متمم تحولاتی است که در مدلهای پیشرفتهتر رخ داده و هزینهٔ اثبات ریاضی نرمافزارها را به قیمت توکن کاهش داده است. نوآوری اصلی در اینجا جداسازی «مشخصات» (Specification - آنچه کد باید انجام دهد)، «پیادهسازی» (Implementation - چگونگی انجام آن) و «اثبات» (Proof - چرا کد درست است) میباشد.
ساختار این سیستم به شرح زیر است:
- مشخصات فنی (Specification): تنها ۹۳ خط کد رسمی است. یک بازبین انسانی فقط باید این خطوط را بخواند تا دقیقاً بداند هسته چه تضمیناتی میدهد.
- پیادهسازی (Implementation): بیش از ۱۰۰۰ خط کد نوشته شده توسط AI است که واقعیتهای پیچیده و «کثیف» هندسه سهبعدی را مدیریت میکند.
- اثباتها (Proofs): بیش از ۶۰ هزار خط اثبات رسمی است که توسط عاملها (Agents) هوش مصنوعی بهطور خودکار نوشته شده تا ثابت کنند پیادهسازی دقیقاً و بدون هیچ انحرافی از مشخصات پیروی میکند.
از آنجا که بررسیکننده Lean این اثباتها را در زمان کامپایل (Compile time) تأیید میکند، بازبین انسانی میتواند ۱۰۰۰ خط پیادهسازی و ۶۰ هزار خط اثبات را بهطور کامل نادیده بگیرد. اگر کد کامپایل شود، از نظر ریاضی تضمین شده است که طبق همان ۹۳ خط مشخصات، درست عمل میکند. این امر به توسعهدهنده اجازه میدهد تا هم پیادهسازی و هم اثباتها را به عنوان یک جعبه سیاه در نظر بگیرد.
برای تأیید این هسته که پیششرطهای «حسن شکل» ورودیها را بررسی کرده و تقاطع را محاسبه میکند، بازبین انسانی تنها نیاز دارد چهار فایل خاص را بررسی کند: CSG/DataStructures.lean ، CSG/Def.lean ، CSG/MeshIntersectWithPreconditionCheck.lean و CSG/WellFormedCheckMsg.lean. مجموع اینها بدون در نظر گرفتن کامنتها، فقط ۹۳ خط است.
بازبین میتواند از بررسی کامل پوشههای CSG/Impl/ و CSG/Proof/ صرفنظر کند. بررسیکننده قطعی Lean تضمین میکند که تمام موارد خاص هندسی مطابق با مشخصات مدیریت شدهاند، بدون اینکه لازم باشد مشخصات تمام این موارد را به صورت تکتک فهرست کند. این فشردهسازی به این دلیل ممکن است که ریاضیات را میتوان بهصورت کلی فرموله کرد، در حالی که پیادهسازی باید با پیچیدگیهای جزئی و موردپسند دستوپنجه نرم کند.
علاوه بر این، امنیت اثباتها با بررسی اصول پذیرفتهشده (Axioms) تأیید میشود. تمام قضایا در این مخزن تنها بر اصول مورد اعتماد [propext, Classical.choice, Quot.sound] تکیه دارند. برای اطمینان از اینکه هیچ تغییر غیرمجازی در پیادهسازی (مانند استفاده از کلمات کلیدی unsafe یا opaque برای پنهان کردن بخشی از کد) وجود ندارد، یک جستوجوی ساده در دایرکتوری CSG/ باید هیچ نتیجهای برای عبارتهایی مثل implemented_by یا extern یا csimp یا skipKernelTC یا partial برنگرداند.
تقاطع مشها بهدلیل مفهوم «حسن شکل» (Well-formedness) بسیار دشوار است. یک مش مثلثی مجموعهای از مثلثهاست که انتظار میرود سطحی بسته ایجاد کند که در خودش فرو نرود (Penetrate). انسانها این مشها را با یک «جرم» (Solid) مرتبط میکنند؛ حجمی در فضای سهبعدی که تمام نقاطی را شامل شود که روی سطح نیستند اما «داخل» مش قرار دارند. این مفهوم از نظر ریاضی توسط شمارش تقاطع پرتوهای علامتدار (Signed ray intersection counting) توصیف میشود.
زبانهای برنامهنویسی متداول نمیتوانند «جرمها» را بهطور صریح بیان کنند زیرا آنها مجموعههای نامتناهی از نقاط هستند. با این حال، Lean اجازه میدهد تقاطع چنین مجموعههای نامتناهی را بهطور صریح تعریف کرد و ثابت کرد که دو مجموعه نامتناهی با هم برابرند. این مدل ریاضی اجازه میدهد تا الزام رسمی زیر برقرار شود: solid (meshIntersect M₁ M₂) = solid M₁ ∩ solid M₂.
پروژه «حسن شکل» را مطابق با ابزارهای واقعی پردازش مش تعریف میکند. یک مش زمانی «حسن شکل» یا درست در نظر گرفته میشود که معیارهای زیر را داشته باشد:
- سطحی آببند (Watertight) باشد.
- جرمی را با تکرار یک (Multiplicity one) محدود کند (با جهتگیری بیرونی منسجم).
- هیچ مثلث تخریبشدهای (Degenerate) نداشته باشد.
- هیچ تداخل داخلی (Self-intersection) نداشته باشد.
یک تسهیل خاص در این تعریف پذیرفته شده است: سطح میتواند در لبهها و رئوس با خود تماس داشته باشد، اما نه در مرکز (Interior) وجوه. سختگیری روی ۲-منیفولد بودن (Strict 2-manifoldness) لازم نیست، زیرا الگوریتمی که همیشه مشهای منیفولد تولید کند از نظر ریاضی غیرممکن است. برای مثال، یک چرخش دقیق از مکعبی با حفرهها میتواند منجر به جرمی شود که در آن دو جزء تنها در یک نقطه با هم تماس دارند و در نتیجه یک سطح غیر-منیفولد ایجاد شود.
پیادهسازیهای متداول با C++ اغلب در پیکربندیهای هندسی خاص شکست میخورند. بر اساس مستندات پروژه، هنگام مقایسه این هسته تأییدشده با یک نسخه غیررسمی C++ که توسط Claude Opus 4.8 نوشته شده بود، یک عامل AI مستقل سه باگ مجزا و بحرانی در نسخه C++ پیدا کرد:
۱. برخورد رأس-وجه (Vertex-Face Collision): پیکربندیهایی که در آن یک رأس از یک مش حسنشکل، همزمان روی یک لبه از بخشی دیگر و یک وجه از مش حسنشکل دیگری قرار میگیرد.
۲. شکست در تقاطع پرتو (Ray Intersection Failures): مواردی که در محاسبات داخلی، زنجیرهای از تستهای تقاطع پرتو همگی دقیقاً به لبههای مثلث برخورد میکنند.
۳. مقیاس ویژگیها (Feature Scaling): پیکربندیهایی که در آن یک وجه بسیار بزرگ توسط چندین ویژگی (Feature) کوچک بریده میشود.
در نسخه تأییدشده، این موارد بهطور ضمنی مدیریت میشوند. مشخصات فنی خروجی را مجبور میکند فارغ از اینکه وجوه همتراز (Coplanar) باشند یا نرمالها در جهت مخالف باشند، نتیجه درست را تولید کند.
مشخصات رسمی تضمین میکند که هسته سناریوهای پیچیدهای را که معمولاً نیاز به تستهای واحد (Unit Testing) بسیار گسترده دارند، مدیریت کند:
تداخلهای همتراز (Coplanar Overlaps)
- اگر دو چهاروجهی وجوههای متداخلی با جهت نرمال یکسان داشته باشند، الگوریتم یک وجه در آن تقاطع ایجاد میکند.
- اگر جهت نرمالها مخالف باشد و هیچ حجمی بین آنها باقی نماند، مشخصات خروجی را «خالی» میکند. این کار از ایجاد آرتیفکتهای رایج «غشای دوگانه» (Double-membrane) که در اپلیکیشنهای تجاری دیده میشود، جلوگیری میکند.
دقت رئوس و مرزها
- جایگذاری رأس: الگوریتم رئوسی که دقیقاً روی سطح مش دیگر قرار دارند را هنگام ایجاد وجوه در هر دو طرف برش، بهدرستی شناسایی و مدیریت میکند.
- مرزهای BVH: وجوههایی که دقیقاً روی مرز یک جعبه احاطهکننده در ساختار شتابدهنده (Bounding Volume Hierarchy) قرار دارند، از طریق نابرابریهای ریاضی دقیق مدیریت میشوند تا خطای شناوری رخ ندهد.
موارد خاص الگوریتمی داخلی
- پرتوتابی (Ray Casting): خطاهای «نامرئی» مانند برخورد دقیق یک پرتو (که برای تشخیص داخل/خارج استفاده میشود) با یک لبه یا عبور همتراز از یک وجه را مدیریت میکند.
- T-junctions: زیرروالهایی (Subroutines) که منجر به ایجاد T-junction میشوند، مجبور میشوند آنها را اصلاح کنند تا خروجی نهایی همچنان «حسن شکل» باقی بماند.
- بررسی پیششرطها: خودِ منطق بررسی حسن شکل نیز تأیید شده است؛ هرگونه خطا در این بخش باعث میشد مشهای معتبر بهاشتباه نامعتبر شناخته شوند.
صحت مطلق هزینهای دارد. این هسته تأییدشده بهطور قابلتوجهی کندتر از پیادهسازیهای پیشرفته (State-of-the-art) است. برای مثال، تقاطع دو مدل «خرگوش استنفورد» با ۷۰ هزار مثلث (که حفرههای پایین آنها برای رعایت آببند بودن بسته شده است)، حدود ۲۴ ثانیه روی یک تراشه M4 Pro تکرشتهای زمان میبرد.
این کندی محدودیت خودِ زبان Lean نیست؛ زیرا نرمافزارهای تأییدشده رسمی در اصل میتوانند به اندازه نرمافزارهای معمولی سریع باشند. بلکه این نتیجهی اجتناب از محاسبات ممیز شناور (Floating-point) شتابیافته سختافزاری است. در حالی که پیادهسازیهای دقیقی مثل CGAL از اعداد اعشاری برای تصمیمگیریهایی که دقت آنها کافی است استفاده میکنند، این پروژه از اعداد گویا (Exact Rationals) استفاده میکند تا هیچ اعتمادی به LLMها و اصول پذیرفتهشده نداشته باشد. استفاده از اعداد اعشاری نیازمند اصول (Axioms) اضافی بود که بازبین انسانی باید به آنها اعتماد میکرد. علاوه بر این، بررسی تمام ورودیها در برابر تعریف «حسن شکل» در زمان اجرا، بخش قابل توجهی از زمان پردازش را میبلعد.
توسعهدهنده از یک فرآیند پالایش گامبهگام با استفاده از عاملها، عمدتاً Claude Opus 4.8 و Fable 5 بهره برد. برخی مراحل بیش از ۲۴ ساعت کار خودکار و مستقل عامل را میطلبید. در این مسیر، استفاده از گردشهای کاری ساختارمند توانسته است نرخ موفقیت عاملهای هوشمند را بهطور چشمگیری افزایش دهد. گردش کار به این شکل تکامل یافت:
- چارچوب ریاضی: ابتدا یک عامل مقالهای از سال ۱۹۹۸ نوشته F. R. Feito و M. Rivero درباره «مدلسازی هندسی بر اساس زنجیرههای سیمپلیکال» را فرموله کرد تا نتیجه وجود ریاضی بدون نیاز به پیادهسازی را به دست آورد (این بخش در
CSG/Legacy/ChainIntersectionExistence.leanیافت میشود). - پیادهسازی اولیه: نسخهای ایجاد و صحت آن ثابت شد (
CSG/Legacy/ChainIntersectionAlgorithm.lean)، هرچند هنوز مشکلاتی مثل مثلثهای متداخل داشت. - الزامات سختگیرانهتر: محدودیتهای جدیدی برای حذف مشکلاتی که در نسخه اول دیده میشد، اضافه شد. در این مرحله برای سادهسازی، محدودیت «موقعیت کلی» (General position restriction) روی ورودیها اعمال شد تا نیازی به مدیریت تمام موارد خاص نباشد.
- حذف محدودیتها: محدودیتهای موقعیت کلی حذف شدند و عامل مجبور شد تمام موارد خاص هندسی را بهدرستی مدیریت کند.
- بهینهسازی: عاملها ساختارهای BVH را برای جلوگیری از پیچیدگی زمانی درجهدو (Quadratic runtime complexity) پیاده کردند. Lean تأیید کرد که این بهینهسازیها همچنان از همان مشخصات فنی اولیه پیروی میکنند.
- پالایش نهایی: مشخصات فنی برای بازبینی انسانی سادهتر و تقویت شد و ساختار نهایی پوشههای
CSG/،CSG/Proof/وCSG/Impl/شکل گرفت.
با وجود صحت کد، این کد «تمیز» نیست. نویسنده اشاره میکند که چون پیادهسازی و اثباتها توسط عاملها بهصورت جعبه سیاه نوشته شدهاند، فاقد طراحی منسجم و معماری که یک معمار انسانی ارائه میدهد، هستند. این وضعیت نوعی «بدهی فنی» (Technical Debt) ایجاد میکند؛ کد کار میکند و اثبات شده است، اما از نظر ساختاری بهینه نیست. این چالشها یادآور این نکته است که چگونه جایگزینی گیتهای مکانیکی با مهندسی پرامپت میتواند نرخ تخطی عاملها از قوانین را کاهش دهد، هرچند کیفیت معماری همچنان یک چالش است.
برخی محدودیتها هنوز فرموله نشدهاند، مانند عملکرد نهایی زمان اجرا یا شیوه دقیق مثلثبندی وجوه خروجی فراتر از شرط حسن شکل (مثلاً ممکن است مشی تولید کند که بیش از حد لازم ریز باشد). این المانها درست به اندازه همان «وایبکدینگ» معمولی، دشوار و غیرقابل کنترل هستند.
این پروژه نخستین پیادهسازی تأیید شده رسمی از تقاطع مشهای سهبعدی CSG است. این کار بر پایه تلاشهای قبلی است اما با آنها تفاوتهای بنیادین دارد:
- Di Vito و Hocking (۲۰۲۱): آنها الگوریتم ادغام چندضلعیها را در محیط PVS برای اشکال دوبعدی تأیید کردند.
- Verified-polygon-intersection: پروژه قبلی همین نویسنده که تقاطع چندضلعیهای دوبعدی را در Lean 4 تأیید میکرد و آن هم بر پایه پیادهسازی و اثبات نوشته شده توسط AI بود.
- Nef Polyhedra در CGAL: اگرچه این سیستم در عمل بسیار دقیق و استوار است، اما عملیات Boolean سهبعدی آن تأیید نشده است و بر اساس تست و استدلال غیررسمی است، نه اثبات ماشینخوان.
این آزمایش نشان میدهد با توانمندتر شدن عاملهای AI در تولید حجم عظیمی از کد، نقش انسان باید از «بازبین کد» (Code Reviewer) به «نویسنده مشخصات فنی» (Specification Author) تغییر کند.
برای جامعه فنی، این موضوع فرض ریسک ذاتی هستههای تولید شده توسط AI را تغییر میدهد. اگر تأییدیه به یک اثباتکننده ماشینخوان (Machine-checked prover) سپرده شود، حجم کد تولید شده توسط AI بیمعنی میشود و تنها کوتاهی، دقت و شفافیت مشخصات فنی اهمیت مییابد.
گام بعدی شما
- مطالعه مستندات زبان Lean 4 برای درک چگونگی تبدیل مشخصات ریاضی به کد اجرایی.
- بررسی مخزن گیتهاب پروژه برای مشاهده نحوه جداسازی فایلهای
Impl(پیادهسازی) ازProof(اثبات). - آزمایش ابزارهای تأیید رسمی در پروژههای حساس که تحمل خطای لبهای (Edge Case) ندارند.
این تنها آغاز ماجراست؛ اثر موجگونهی این رویکرد بر استانداردسازی کدهای تولید شده توسط AI را در گزارش بعدی بررسی خواهیم کرد.
گفتگو