У рамках значного стрибка у розвитку штучного інтелекту дослідницька група з Пекінського університету розробила систему ІІ, здатну самостійно вирішувати складні, невирішені математичні завдання. Система успішно впоралася з гіпотезою алгебри десятирічної давності, що знаменує перехід від використання ІІ в якості простого помічника до його ролі як автономного дослідника.
Рішення гіпотези алгебри
У центрі цього прориву лежала гіпотеза алгебри, вперше запропонована в 2014 році покійним Деном Андерсоном, колишнім професором Університету Айови. Протягом десяти років ця проблема залишалася відкритим викликом в області комутативної алгебри.
На відміну від попередніх моделей ІІ, що вимагають постійного керівництва з боку людини, ця нова система опрацювала десятиліття математичної літератури, щоб вирішити гіпотезу, і що критично важливо самостійно верифікувала свої результати без втручання людини. Весь процес зайняв лише 80 годин роботи.
Архітектура автономії: Rethlas та Archon
Щоб подолати традиційні обмеження ІІ в математиці, дослідники відійшли від стандартних великих мовних моделей (LLM), які часто схильні до галюцинацій або логічних помилок. Натомість вони створили структуру з двох агентів, призначену для імітації суворого робочого процесу професійних математиків:
- Агент міркувань (Rethlas): Ця система виступає у ролі «мислителя». Вона використовує пошуковик теорем під назвою Matlas для вивчення різних стратегій і математичних шляхів вирішення задачі.
- Агент формалізації (Archon): Як тільки потенційний доказ знайдено, управління переходить до Archon. Використовуючи інструмент LeanSearch, він переводить неформальні міркування у формальний формат, що перевіряється машиною.
- Верифікатор (Lean 4): Система використовує Lean 4 — спеціалізовану мову програмування та інтерактивний помічник за доказом теорем — щоб гарантувати, що доказ математично обґрунтований і не містить помилок.
Чому це важливо: від допомоги до автоматизації
Сучасні тенденції в області ІІ демонструють потужний вектор на навчання моделей математики, проте більшість із них все ще стикаються із «проблемою суворості». У той час як люди здатні писати докази, вони можуть припускатися помилок; в той час як LLM можуть швидко генерувати текст, часто не вистачає логічної точності, необхідної для вищої математики.
Дослідження Пекінського університету усуває цю прогалину шляхом інтеграції роздумів природною мовою з формальною верифікацією. Такий подвійний підхід гарантує, що ІІ не просто «вгадує» відповідь, а вибудовує доказ, правильність якого може бути математично підтверджена.
Більше того, дослідники зазначили, що ІІ продемонстрував унікальну здатність виконувати завдання, які зазвичай вимагають міждисциплінарної співпраці, фактично діючи як група експертів, які працюють у тандемі.
Майбутнє математичних досліджень
Незважаючи на те, що система працювала автономно, дослідники зазначили, що втручання людини все ще може бути прискорювачем. Математик, який направляє агента «Archon», може прискорити процес формалізації, що відкриває шлях до майбутнього, де люди та ІІ працюють у високошвидкісному симбіотичному циклі.
«Ця робота є конкретним прикладом того, як математичні дослідження можуть істотно автоматизуватися за допомогою ІІ», — заявили дослідники.
Висновок
Поєднуючи логічні міркування зі строгою формальною верифікацією, ця нова архітектура виводить ІІ за межі простих обчислень в область автономних наукових відкриттів. Цей прорив прокладає шлях для вирішення ІІ все більш складних завдань у математиці та інших високотехнологічних наукових галузях.
