Математики вказали на недоліки в оприлюднених OpenAI доведеннях

OpenAI оприлюднила сотні заявлених розв’язань складних математичних задач, однак частина цих матеріалів не відповідає рекомендаціям консультативної групи математиків щодо прозорості та забезпечення людського розуміння результатів. Про це повідомляє TechCrunch.

Лабораторія заявляла, що перед публікацією консультувалася з Advisory Group on Mathematics and Artificial Intelligence — групою дев’яти дослідників із різних установ, яку приймає Інститут перспективних досліджень Принстонського університету. Наприкінці вересня група оприлюднила настанови для розробників передових ШІ-моделей, які працюють із відкритими математичними проблемами.

Рекомендації для розробників ШІ

Серед перших рекомендацій групи було припинити тестування складних математичних задач на закритих моделях. Водночас OpenAI прямо зазначила, що оцінює свої пропрієтарні моделі за допомогою відкритих дослідницьких задач із математики.

Група також наголошувала на необхідності якнайшвидшого оприлюднення результатів і пояснення того, як моделі дійшли висновків. У релізі OpenAI лише 10 із 719 рукописів містили оприлюднені ланцюжки міркувань моделі. Для доведень, які люди ще не розуміють, математики пропонували формалізацію; за даними видання, 42% оприлюднених OpenAI доведень не пройшли цього процесу.

Розбіжності між текстом і кодом

Дослідники з Кембриджського університету та Королівського коледжу Лондона цього тижня опублікували роботу, де звернули увагу на щонайменше дві розбіжності між природномовним поясненням і кодом Lean у розв’язанні OpenAI задачі, похідної від рівнянь Нав’є—Стокса. Lean — мова програмування, яку використовують для формальної перевірки доведень через компіляцію коду.

Автори роботи зазначили, що такі розбіжності самі по собі не спростовують жодне з рішень, але ставлять під сумнів можливість покладатися на автоматичну формалізацію без участі людей. Advisory Group on Mathematics and Artificial Intelligence також радила додавати машинозчитувані метадані, які пов’язують природномовні та формальні версії доведення; у цьому релізі OpenAI таких даних не надала.

Математик Терренс Тао після публікації зауважив, що люди, які ініціюють розв’язання задач за допомогою ШІ, можуть не розуміти результат достатньо, щоб відповідати на запитання, виступати з доповідями чи взаємодіяти з фаховою спільнотою. Професорка математики Гарвардського університету Мелані Вуд сказала, що на момент публікації людського розуміння таких розв’язань може не бути, а робота з їхнім осмисленням лише починається.