25 лауреатів медалі Філдса розкритикували підхід ШІ-компаній до математики. Серед них — Марина Вязовська

💡 Усі статті, обговорення, новини про AI — в одному місці. Приєднуйтесь до AI спільноти!

Українська математикиня Марина Вязовська долучилася до заяви 25 лауреатів медалі Філдса про ризики використання ШІ в математиці. Науковців непокоїть, що компанії поспішають оголосити про розв’язання складних задач, залишаючи замало часу для пояснення доказів і належного визнання внеску інших дослідників.

Заяву 11 вересня опублікував у своєму блозі математик Теренс Тао.

Автори пояснюють, що для ШІ-компаній відомі математичні задачі стали способом продемонструвати можливості моделей. Для науки цінність розв’язання полягає також у нових ідеях і методах, які зможуть застосовувати інші дослідники. Щоб цього досягти, математичний доказ потрібно розібрати, обговорити з колегами й зробити зрозумілим для наступних поколінь науковців.

Поспішні публікації можуть ускладнювати цю роботу та породжувати суперечки про авторство і плагіат. Окремо підписанти наголошують на навчанні: самостійна робота над задачами допомагає студентам розвивати навички й учитися ставити нові запитання.

Автори закликають наукову спільноту, ШІ-компанії та суспільство терміново розв’язати ці проблеми. На їхню думку, використання ШІ має сприяти глибшому розумінню математики, зберігати належне визнання внеску дослідників та умови для навчання нових науковців.

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

Марина Вязовська

📌 Контекст

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

За даними OpenAI, група, яка отримала результат, налічувала близько 10 тисяч ШІ-агентів, що працювали паралельно. Пошук зайняв приблизно 88 годин, а формалізація та перевірка доказу в системі Lean — ще 17.

Паралельно над спорідненими задачами працювали професор Нью-Йоркського університету Трістан Бакмастер і математик Левент Алпьоґе, співробітник Anthropic. Бакмастер заявив, що представник OpenAI пропонував йому написати статтю про результат компанії без співавторства Алпьоґе. Він також поставив питання, чи могла модель використати їхні неопубліковані напрацювання, які дослідники завантажували в Codex.

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

Сама Вязовська має досвід співпраці з розробниками математичного ШІ. У 2016 році вона розв’язала задачу про найщільніше пакування куль у восьмивимірному просторі, а невдовзі разом із колегами — у 24-вимірному. У 2022 році дослідниця отримала медаль Філдса, ставши другою жінкою в історії з цією нагородою.

У 2022 році в інтерв’ю DOU Вязовська розповідала про роль програмування в сучасній математиці. За її словами, навіть у «чистій» математиці комп’ютери можуть використовувати як інструмент для перевірки гіпотез, обчислень або доведення результатів. Сама Вязовська також згадувала, що в студентські роки розглядала програмування як альтернативну кар’єру.

У 2024 році вона та математик Сідгарт Харіхаран започаткували проєкт комп’ютерної перевірки цього доказу. Команда переводила його в Lean — систему, яка перевіряє, чи кожен крок логічно випливає з попередніх тверджень. Для цього дослідники підготували докладний план і написали значну частину коду. Про роботу розповіли в EPFL, де працює Вязовська.

Згодом до проєкту долучилася ШІ-система Gauss від Math, Inc. За даними розробників, вона за п’ять днів завершила решту доведень, потрібних для перевірки восьмивимірного випадку. Команда оцінювала, що на цю частину роботи з наявними інструментами знадобилося б ще близько пів року. Після цього Gauss за два тижні формалізувала доказ для 24 вимірів, спираючись на оригінальну наукову статтю.

Все про українське ІТ в телеграмі — підписуйтеся на канал DOU