Штучний інтелект самостійно перевірив доказ одного із найскладніших завдань у математиці — завдання про найміцнішу упаковку сфер у багатовимірному просторі, — подвиг, який приніс українській математиці Марині В’язовській Філдсовську премію 2022 року. Цей рубіж знаменує фундаментальний зсув у тому, як проводяться математичні дослідження, переходячи від ІІ як простого обчислювального інструменту до спільного партнера у міркуваннях.
Еволюціонуюча Роль ІІ в Математиці
Протягом століть математики покладалися на такі інструменти, як абаки, калькулятори та комп’ютери, щоб допомагати у обчисленнях. Однак ці інструменти залишалися продовженням людського інтелекту, ніколи не замінюючи основний процес міркувань. Сучасна поява ІІ в математиці принципово інше: ці системи тепер допомагають не тільки в обчисленнях, а й у самому міркуванні, автоматизуючи багато кроків, що лежать в основі математичних аргументів.
Це зрушення відбувалося поступово. Сучасна математика вже спирається на складні структури та великі каталоги результатів, які жодна людина не може повністю охопити. Комп’ютери вже допомагали у великих доказах, таких як теорема про чотири кольори та гіпотеза Кеплера, але сьогоднішні системи ІІ пропонують новий рівень автономії та надійності, особливо у поєднанні з формальними помічниками для доказу.
Потужність Формальної Верифікації
Мови формальної верифікації, такі як Lean, виражають математичні аргументи в такий спосіб, щоб комп’ютери могли перевіряти кожен крок, забезпечуючи логічну обгрунтованість. На відміну від традиційного математичного листа, Lean вимагає явних визначень та висновків, ретельно перевіряючи кожен етап. Хоча він і нещадний, цей процес виключає приховані припущення та стрибки віри. Результат математично визначено за умови, що доказ пройде перевірку Lean.
За останні кілька років математики створили великі бібліотеки у цих мовах, накопичуючи визначення та перевірені теореми для вирішення все більш складних завдань. Насамперед вузьким місцем був трудомісткий процес перетворення передових доказів у форму, яку перевіряла машина, — завдання, яке могло зайняти місяці чи роки.
Прорив: Доказ В’язовської, Перевірений ІІ
Нещодавня верифікація доказу завдання про щільне пакування сфер у багатовимірному просторі В’язівської демонструє швидкий прогрес у цій галузі. Завдання про щільну упаковку сфер запитує, наскільки щільно можна запакувати ідентичні сфери в просторах будь-якої розмірності. В’язовська вирішила це завдання для восьми та 24 вимірювань, спираючись на роботи, які раніше були завершені лише для одного, двох та трьох вимірювань.
Стартап в області ІІ Math, Inc., використовуючи свій розмірковуючий агент Gauss, відіграв ключову роль у переведенні аргументів В’язовської в код Lean та перевірці кожного кроку. Система ІІ не працювала ізольовано: математики надали первісне креслення та структуру. Однак після налаштування Gauss виконав роботу за лічені дні – завдання, яке дослідники-люди оцінили у місяці.
Майбутнє Математичних Досліджень
Це більше ніж технічне досягнення; це сигналізує про фундаментальне зрушення у тому, як працюють математики. Лауреат Філдсівської премії Теренс Тао припускає, що негайна цінність ІІ полягає в автоматизації стомливих, але концептуально простих завдань, дозволяючи математикам зосередитися на стратегії, а не на бухгалтерії. Цей поділ творчого формування ідей від суворої перевірки є ключовим.
Кевін Баззард з Імперського коледжу Лондона застерігає від покладатися на великі великі мовні моделі, але стверджує, що мови формальної верифікації, такі як Lean, пропонують рішення. Якщо доказ проходить програму, він гарантовано буде дійсним. Основна проблема тепер полягає у переведенні більшої частини сучасної математики в ці формальні бібліотеки, надаючи системам ІІ необхідні концепції для роботи.
Висновок
ІІ не замінює математиків, а перевизначає їх роль. Майбутнє математики, ймовірно, полягатиме у створенні та налаштуванні інструментів, що розширюють людські когнітивні межі, поєднуючи інтуїцію з машинною дисципліною. У міру розширення математики, що перевіряється, зростатиме попит на людей, які можуть ставити правильні питання, створювати нові визначення та розпізнавати справжні ідеї. Партнерство між людським інтелектом та штучним інтелектом стимулюватиме нову еру математичних відкриттів.
