Математичний прорив OpenAI виявився під питанням — вчені знайшли розбіжність у доказі

Математичний прорив OpenAI почав викликати питання. Вчені порівняли опубліковане доведення по рівняннях Нав'є — Стокса з його алгоритмічною версією Lean і виявили розбіжності: в кількох ключових місцях машинний варіант, перевіряємий на комп'ютері, містить більш слабкі твердження. Це ще не спростування, але ґрунт для сумнівів вже цілком родючий.

Джерело зображення: Thomas T /unsplash.com

За словами математиків, розбіжність зовсім не означає, що доведення невірні або що OpenAI неправильно вирішила задачу, але це ставить під сумнів, чи завжди можна покладатися на математичні результати, згенеровані моделями штучного інтелекту.

«Що потрібно зробити з усіма цими великими доведеннями, створеними на основі мовної моделі, так це те, що їх повинні прочитати люди, і це створює величезне додаткове навантаження на математиків», — повідомив керівник команди Андерс Хансен.

Процес пошуку розбіжностей зайняв у команди близько двох тижнів. При цьому математики використовували підказки ChatGPT. Нагадаємо, що у OpenAI на вирішення задачі пішло 88 годин.

Математики вказали на розбіжність у частині доведення, що називається лемою 8.6. У доведенні на природній мові рівняння в цій частині вимагає, щоб певне значення було менше m + 4, де m — ціле число, а в Lean-версії — менше m + 5, що математично слабше, оскільки допускає більше можливих рішень і не еквівалентно першому.

Уявімо, що вас попросили вирішити рівняння x + 3 = 6, відповіддю на яке є x = 3. Можна написати доведення того, що x має бути менше 4, а також того, що x має бути менше 5. Обидва ці математичні твердження абсолютно вірні, але останнє допускає більше можливих відповідей для x, що робить його математично більш слабким.

За словами Хансена, неправильний переклад міг виникнути через те, що ШІ прагне до того, щоб комп'ютерний код був повністю самосогласованим і не видавав помилок. Якщо в процесі автоматичної формалізації ШІ виявить частину доведення, яка не компілюється, він спробує знайти обхідний шлях, навіть якщо це означає відхилення від доведення, написаного на природній мові.

Кевін Баззард з Імперського коледжу Лондона повідомив, що можна надійно формалізувати в Lean саму формулювання теореми і потім перевірити, чи компілюється доведення. Але це не гарантує, що текстове доведення в PDF коректно передає логіку. Тобто Lean-код може бути внутрішньо узгодженим, але не відповідати тому, що написано в статті. «Я впевнений, що проблема Нав'є — Стокса була вирішена правильно, — говорить Баззард. — Я значно менш впевнений у тому, що доведення, описане текстом, є правильним».

OpenAI повідомила ресурсу New Scientist, що їй відомо про невідповідність між доведенням на природній мові та у вигляді коду, і що це не означає, що жодне з них недійсне.

Хочеш дізнатися більше — читай відгуки