Математичні розв’язання OpenAI поки не відповідають стандартам цієї галузі

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

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

Дорадча група з питань математики та штучного інтелекту (AGMAI), яку приймає Інститут перспективних досліджень Принстонського університету, складається з дев’яти відомих дослідників із закладів по всьому світу.

Наприкінці вересня організація оприлюднила рекомендації для передових лабораторій, що розв’язують математичні задачі. У заяві щодо останньої добірки доведень AGMAI зазначила, що «зрештою саме математична спільнота має оцінити, наскільки успішно було дотримано наших рекомендацій».

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

Дорадча група не відповіла на запит TechCrunch щодо ретельнішої оцінки останньої добірки доведень OpenAI. Лабораторія явно дотрималася деяких її принципів, зокрема оприлюднила результати якомога швидше та додала інформацію про те, як моделі дійшли своїх висновків. Але не всіх: лише 10 із 719 рукописів містили оприлюднення ланцюжка міркувань моделі.

Для статей, які люди не розуміють, математики запропонували формалізувати доведення, але лише 42% оприлюднених OpenAI доведень пройшли цей процес.

Зрештою, досі не зрозуміло, чи бере OpenAI під час оприлюднення своїх доведень «відповідальність за те, щоб забезпечити подальше людське розуміння», відповідно до принципів AGMAI. AGMAI запропонувала OpenAI допомогти фінансувати роботу математиків-людей, які будуть потрібні, щоб розв’язання лабораторії набули бодай якогось реального значення.

«Задачі автономно розв’язують підказувачі ШІ, які після того, як їхню початкову мету “розв’язано”, не цікавляться ширшою галуззю і недостатньо добре розуміють результати ШІ, щоб відповідати на запитання щодо результату, виступати з доповідями чи іншим чином взаємодіяти з рештою галузі», — написав у соціальних мережах після релізу Теренс Тао, відомий математик, який критикував підхід OpenAI.

Цю проблему ілюструє стаття, оприлюднена цього тижня математиками з Кембриджського університету та Лондонського королівського коледжу, у якій ставиться під сумнів підхід передових лабораторій до цих викликів.

Коли моделі ШІ розв’язують математичні задачі, спочатку вони створюють пояснення «природною мовою», а потім намагаються виразити цей результат мовою програмування Lean, яка теоретично підтверджує точність доведення, компілюючи його як код.

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

Ці розбіжності не обов’язково спростовують жодне з розв’язань, але порушують питання про те, чи можемо ми просто покладатися на моделі у формалізації власних розв’язань без участі людей. Саме тому AGMAI попросила OpenAI «додавати машиночитані метадані, що встановлюють відповідність між природномовними та формальними артефактами», чого передова лабораторія не зробила в цих релізах.

«Через явище неправильних перекладів — висвітлене в цій статті — доведенню природною мовою OpenAI та іншим автоматично формалізованим доведенням у Lean не слід апріорі довіряти без того самого процесу рецензування та перевірки, яким піддаються інші доведення», — доходять висновку автори статті «Втрачені під час перекладу».

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

Коли моделі пропонують розв’язати складну задачу, і вона видає розв’язання, «на момент оприлюднення людського розуміння цього розв’язання немає, і тепер робота лише починається», — розповіла TechCrunch професорка математики Гарвардського університету Мелані Вуд.