Lean-доказ OpenAI рівняння Нав'є-Стокса не відповідає версії природною мовою, стверджують математики

Невідповідність між двома доказів

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

Тепер група математиків стверджує, що ці дві версії не відповідають одна одній. Андерс Ганзен з Кембриджського університету та Фабіан Черчелі разом із Олександром Бастуном з Лондонського King's College стверджують, що модель OpenAI неправильно переклала частину доказу під час перенесення в Lean. Дослідники наголошують, що це не означає, що докази неправильні або що OpenAI не вирішила проблему, однак викликає сумніви щодо того, чи завжди можна покладатися на математичні результати, згенеровані ШІ.

Послаблена лема

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

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

Навантаження на перевірку доказів ШІ

Знаходження спотворення виявилося трудомістким. Група попросила ChatGPT знайти можливі невідповідності між двома версіями, а потім вручну перевірила кожну з них. Багато запропонованих невідповідностей після перевірки виявилися хибними. Загалом групі знадобилося приблизно два тижні, щоб встановити справжнє спотворення, тоді як, за словами OpenAI, її агентам знадобилося 88 годин на генерацію доказів.

Проблема особливо актуальна, оскільки OpenAI опублікувала партію з 722 математичних робіт, з яких лише частині супроводжують докази на Lean, які не були перевірені вручну. Кевін Базард з Лондонського Imperial College сказав, що він переконаний, що проблема Нав'є-Стокса вирішена правильно, але значно менш переконаний, що доказ, описаний у PDF, є правильним. Ганзен сказав, що потрібно більше роботи над розробкою надійної техніки автоматизації та що остаточний шлях до цього абсолютно невідомий.

Джерела: newscientist.com