OpenAI опублікувала 719 математичних робіт, створених за допомогою ШІ. Однак математики розкритикували компанію за недостатню перевірку результатів. Зокрема, дослідники виявили розбіжності між текстовим поясненням і програмним кодом одного з доведень, повідомляє TechCrunch.
Чому математики критикують підхід OpenAI
OpenAI використовує власні ШІ-моделі для розв’язання складних математичних задач, над якими працюють науковці. Цього тижня компанія опублікувала сотні отриманих результатів, щоб їх могла оцінити математична спільнота.
Перед публікацією OpenAI консультувалася з експертною групою AGMAI, до якої входять дев’ять дослідників із різних наукових установ.
Наприкінці вересня група представила рекомендації для компаній, які використовують ШІ в математичних дослідженнях.
Головна ідея рекомендацій полягає в тому, що недостатньо просто отримати відповідь на складну задачу. Потрібно також переконатися, що люди можуть перевірити доведення, зрозуміти його та пояснити іншим.
OpenAI виконала частину цих вимог. Зокрема, компанія відкрито опублікувала результати та надала інформацію про те, як моделі їх отримали.
Проте детальні записи процесу міркування ШІ були доступні лише для 10 із 719 рукописів. Крім того, 42% доведень не пройшли формалізацію — перевірку за допомогою спеціальних програмних інструментів.
AGMAI також рекомендувала не використовувати закриті ШІ-моделі для перевірки їхніх математичних можливостей на складних відкритих задачах. OpenAI продовжила застосовувати саме такий підхід.
Це викликало питання щодо того, наскільки надійними є опубліковані результати та хто має відповідати за їхню подальшу перевірку.
Розбіжності між текстом і кодом
Окремі питання до підходу OpenAI виникли після публікації дослідження математиків Кембриджського університету та Королівського коледжу Лондона.
Науковці проаналізували доведення, яке ШІ запропонував для задачі, пов’язаної з рівняннями Нав’є — Стокса. Ці рівняння описують складний рух рідин і газів.
Зазвичай ШІ спочатку описує математичне доведення звичайною мовою, а потім перетворює його на програмний код мовою Lean, щоб перевірити правильність результату.
Однак під час такого переведення можуть виникати помилки або змінюватися зміст окремих тверджень.
Дослідники виявили щонайменше дві розбіжності між текстовим поясненням OpenAI та відповідним кодом Lean.
Це не означає, що доведення обов’язково неправильне. Проте такі розбіжності ставлять під сумнів можливість повністю довіряти автоматичній перевірці, яку виконує сам ШІ.
Автори дослідження наголошують, що математичні результати, створені моделями, повинні проходити таку саму незалежну експертну перевірку, як і роботи людей.
AGMAI також рекомендувала OpenAI публікувати спеціальні машинозчитувані дані, які дозволяють зіставляти текстові пояснення з формальними доведеннями. У новому наборі робіт компанія цього не зробила.
Чому участь математиків залишається важливою
Математик Теренс Тао звернув увагу на проблему використання ШІ людьми, які не можуть самостійно пояснити отримані результати.
За його словами, деякі користувачі моделей зосереджуються лише на розв’язанні конкретної задачі, не заглиблюючись у відповідну математичну галузь. Через це вони не завжди здатні відповісти на запитання інших дослідників або пояснити доведення на наукових заходах.
Професорка математики Гарвардського університету Мелані Вуд також наголосила, що після отримання результату від ШІ робота математиків лише починається.
На відміну від традиційних наукових публікацій, такі результати можуть з’являтися без достатнього розуміння з боку людини.
Подальша перевірка потрібна не лише для пошуку помилок, а й для того, щоб нові математичні знання можна було використовувати в інших дослідженнях.
