شفقنا- یک ابزار هوش مصنوعی چینی موفق شد یک مسئله پیچیده ریاضی را حل کند؛ مسئلهای که دانشمندان طی ده سال گذشته از حل آن ناتوان مانده بودند و نخستینبار در سال ۲۰۱۴ توسط یک ریاضیدان آمریکایی مطرح شده بود.
به گزارش شفقنا؛ وبگاه آرتی عربی نوشت: «تیمی از دانشگاه پکن این سامانه را بهگونهای توسعه داده که بهصورت شبهمستقل عمل میکند؛ به این معنا که با مرور دههها پژوهش ریاضی به راهحل دست یافته و سپس بدون نیاز به دخالت انسانی قابلتوجه، صحت نتایج خود را نیز بررسی کرده است».
مسئله حلشده، یک «حدس جبری» بود که توسط پروفسور دان اندرسون از دانشگاه آیووا مطرح شده و پیش از درگذشت او در سال ۲۰۲۲ همچنان حلنشده باقی مانده بود.
پژوهشگران به سرپرستی «دونگ بن» اعلام کردند که سامانه آنها توانسته این مسئله باز در حوزه «جبر جابجایی» (شاخهای از جبر مجرد که به مطالعه حلقههای جابجایی و ایدهآلهای آنها میپردازد) را حل کرده و بهصورت خودکار اثبات کند؛ دستاوردی که نمونهای عینی از امکان خودکارسازی پژوهشهای ریاضی با استفاده از هوش مصنوعی به شمار میرود.
آنچه این سامانه را متمایز میکند، سرعت بسیار بالای آن نسبت به انسان است؛ بهگونهای که میتواند مسائل پیچیدهای را حل کند که پیشتر نیازمند همکاری گروهی از متخصصان در حوزههای مختلف بود. با این حال، بزرگترین چالش پیش روی پژوهشگران این بود که اثباتهای ریاضی نیازمند دقتی مطلق هستند، در حالی که خروجی مدلهای زبانی بزرگ معمولاً بهدلیل تمایل به «توهمسازی» یا تولید اطلاعات نادرست، از اعتبار کافی برخوردار نیست.
به همین دلیل، تیم چینی سامانهای نوآورانه طراحی کرد که از ترکیب دو عامل (Agent) تشکیل شده است: عامل نخست مسئول استدلال به زبان طبیعی است و عامل دوم وظیفه رسمیسازی نتایج و راستیآزمایی آنها را بر عهده دارد.
این سامانه بر سازوکاری هوشمند مبتنی است که با یک سیستم استدلال به نام «ریثلاس» (Rethlas) آغاز میشود؛ سیستمی که با استفاده از موتور جستوجوی نظریههای ریاضی موسوم به Matlas، راهبردهای حل را بررسی میکند. پس از دستیابی به یک برهان احتمالی، سامانه دوم با نام «آرخون» (Archon) و با بهرهگیری از موتور جستوجوی LeanSearch، آن برهان را به قالبی تبدیل میکند که توسط یک اثباتگر تعاملی به نام «Lean 4» قابل بررسی باشد. این اثباتگر تنها یک ابزار ساده نیست، بلکه یک زبان برنامهنویسی کامل است که کتابخانه آن شامل صدها هزار نظریه و تعریف ریاضی است.
این سامانه توانست در مدت تنها ۸۰ ساعت پردازش، حدس اندرسون را حل کند، آن هم بدون نیاز به قضاوت یا مداخله یک ریاضیدان انسانی. با این حال، پژوهشگران اشاره کردهاند که در صورت هدایت سامانه «آرخون» توسط یک ریاضیدان واقعی، میتوان این فرایند را حتی سریعتر نیز انجام داد.
در نهایت، این تیم تأکید میکند که دستاورد یادشده الگویی امیدوارکننده برای آینده به شمار میرود؛ جایی که سامانههای استدلال غیررسمی و رسمی در کنار یکدیگر کار میکنند تا نتایجی قابلاعتماد و قابلراستیآزمایی تولید شود و در عین حال، نیاز به مداخله انسانی بهطور چشمگیری کاهش یابد.