ШІ розв’язує задачі Ердьоша. Що далі?

Лише кілька місяців тому, питання здавалося в основному філософським: якщо штучний інтелект може допомогти вирішити відкриті математичні проблеми, що відбувається з ідеєю людської геніальності?

Це питання вже не є теоретичним. Два недавні досягнення, пов’язані з OpenAI та Google DeepMind, свідчать про те, що штучний інтелект рухається від математичної допомоги до математичної участі. Не в тому сенсі, що ШІ повністю замінює математиків, а в точнішому й важливішому сенсі: він генерує, шукає, перевіряє та іноді відкриває аргументи, які можуть витримати експертну перевірку.

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

Другий розвиток відбувся в дослідників Google DeepMind, які опублікували статтю під назвою “Розширення математичних досліджень за допомогою формального пошуку доведень під керуванням ШІ”. Їх система, AlphaProof Nexus, оцінила генерацію доведень ШІ на відкритих задачах дослідницького рівня і повідомила, що її найсильніший агент самостійно вирішив 9 з 353 відкритих проблем Ердьоша. Вона також довела 44 з 492 відкритих гіпотез з Онлайн-енциклопедії цілочисельних послідовностей.

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

Чому проблеми Ердьоша є серйозним тестом для ШІ

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

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

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

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

OpenAI та прорив у проблемі одиниці відстані

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

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

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

Іншими словами, система, здається, перенесла свою здатність міркувати в незнайоме дослідницьке середовище. Вона не просто запам’ятала відоме доведення. Вона згенерувала результат, який зовнішні математики сприйняли як великий внесок.

Google DeepMind та формальний пошук доведень

Дослідники Google DeepMind у своїй статті розглядають інше, але не менш важливе питання: як зробити математику, згенеровану ШІ, надійною?

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

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

Результат DeepMind особливо важливий, оскільки він пов’язує міркування ШІ з перевіркою. Система не потребує довіри в тому ж сенсі, що й чат-бот природною мовою. Її доведення або компілюється, або ні.

Що це означає для математичних досліджень

Поточний урок полягає в тому, що математики не є застарілими. Це означає, що вузьке місце в математиці може змінитися.

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

• ШІ може досліджувати багато шляхів доведення, перш ніж людина витратить час на один.
• Формальні системи можуть перевіряти кроки, які інакше потребували б повільної експертної перевірки.
• Дослідники можуть використовувати ШІ для пошуку в віддалених математичних підгалузях.

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

Обмеження все ще реальні

Важливо не перебільшувати момент. Система Google DeepMind вирішила 9 із 353 задач Ердьоша, які вона намагалася розв’язати. Це вражаюче, але це також означає, що більшість залишилися невирішеними. Результат OpenAI щодо одиниці відстані є віхою, але це не означає, що кожну знамениту гіпотезу тепер легко довести.

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

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

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

Що далі після того, як ШІ вирішить проблеми Ердьоша?

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

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

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

Глибший наслідок є культурним. Математика завжди цінувала доведення, але вона також цінувала смак: здатність знати, яка проблема має значення, яку абстракцію варто винайти, та який результат змінює форму галузі. Коли пошук доведення стає більш автоматизованим, смак може стати більш важливим, а не менш важливим.

Висновок: Геній переходить до завдань вищого рівня

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

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

Прорив OpenAI щодо одиниці відстані та результати формального пошуку доведення Google DeepMind не закривають книгу про людську математичну креативність. Вони відкривають нову главу, в якій математики можуть працювати з системами, які можуть досліджувати територію швидше, ніж будь-який індивідуальний розум.

Майбутнє математики може не належати тільки людям або машинам. Воно може належати дослідникам, які навчаться спонукати людей і машини мислити разом.