Заменит ли ИИ математиков?

Заменят ли нас машины? С момента появления искусственного интеллекта (ИИ) люди беспокоились, что компьютеры в конечном итоге (или даже неизбежно!) превзойдут когнитивные способности человека во всех отношениях.

Пионер искусственного интеллекта Оливер Селфридж в телевизионном интервью начала 1960-х годов сказал: «Я убежден, что машины могут и будут думать при нашей жизни», хотя и с оговоркой: «Я не думаю, что моя дочь когда-либо выйдет замуж за компьютер». (По-видимому, нет никакого технического прогресса, настолько абстрактного, чтобы люди не могли чувствовать сексуальное беспокойство по этому поводу.)

Давайте сделаем соответствующий вопрос более личным: заменят ли меня машины? Я математик; Моя профессия часто рассматривается со стороны как очень сложная, но, в конечном счете, чисто механическая игра, в которую играют с фиксированными правилами, такими как шашки, шахматы или го. Это виды деятельности, в которых машины уже продемонстрировали сверхчеловеческие способности.

Некоторые люди представляют себе мир, в котором компьютеры дают нам ответы на все вопросы. Я мечтаю о большем. Я хочу, чтобы они задавали хорошие вопросы.

Но для меня математика отличается: это творческое занятие, которое требует нашей интуиции так же, как и нашей способности к вычислениям. (Честно говоря, шахматисты, вероятно, чувствуют то же самое.) Анри Пуанкаре, математик, который переосмыслил весь предмет геометрии в начале 20-х годовЙ века, настаивал на том, что это будет безнадежно

Попытка заменить свободную инициативу математика механическим процессом любого рода. Для того чтобы получить результат, имеющий какую-либо реальную ценность, недостаточно отшлифовать расчеты или иметь машину для приведения вещей в порядок: значение имеет не только порядок, но и неожиданный порядок. Машина может завладеть голым фактом, но душа факта всегда будет избегать его».

Но машины могут вносить глубокие изменения в математическую практику, не отказываясь от людей. Питер Шольце, лауреат медали Филдса 2018 года (иногда называемой «Нобелевской премией по математике»), глубоко вовлечен в амбициозную программу на границах алгебры и геометрии под названием «конденсированная математика» — и нет, нет никаких шансов, что я попытаюсь объяснить, что это такое в этом пространстве.

Познакомьтесь с ИИ, вашим новым научным сотрудником

Фото: Одержимая фотография через Unsplash

То, что я собираюсь рассказать вам, является результатом того, что Шольце назвал «экспериментом с жидкими тензорами». Сообщество под названием Lean, основанное Леонардо де Моура из Microsoft Research и в настоящее время с открытым исходным кодом и во всем мире, имеет амбициозную цель разработки компьютерного языка с выразительной способностью захватывать всю современную математику. Предлагаемое доказательство новой теоремы, формализованное переводом на этот язык, можно было бы проверить на правильность автоматически, а не ставить свою репутацию на ошибочных человеческих рецензентов.

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

Когда я впервые услышал о Lean, я подумал, что он, вероятно, будет хорошо работать для некоторых простых задач и теорем. Я недооценил его. Так же поступил и Шольце. В своем блоге в мае 2021 года он пишет: «Эксперимент проверил всю часть аргумента, в которой я не был уверен. Я нахожу абсолютно безумным, что интерактивные помощники по доказательствам теперь находятся на том уровне, что в течение очень разумного промежутка времени они могут формально проверить сложные оригинальные исследования».

И вклад машины заключался не только в том, чтобы подтвердить, что Шольце был прав, думая, что его доказательство было обоснованным; он сообщает, что работа по помещению доказательства в форму, которую машина могла бы прочитать, улучшила его собственное человеческое понимание аргумента!

The Liquid Tensor Experiment points to a future where machines, rather than replacing human mathematicians, become our indispensable partners. Whether or not they can take hold of the soul of the fact, they can extend our grasp as we reach for the soul.

За несколько лет до прорыва Пиччирилло тополог по имени Марк Хьюз из Brigham Young попытался создать нейронную сеть, чтобы сделать хорошие предположения о том, какие узлы были разрезаны. Он дал ему длинный список узлов, где ответ был известен, так же, как нейронная сеть обработки изображений получила бы длинный список изображений кошек и фотографий не-кошек.

Для узла Конвея нейронная сеть Хьюза вернула число, очень близкое к 1/2, что говорит о том, что она глубоко не уверена, отвечать ли на 0 или 1. Это завораживает! Нейронная сеть правильно определила узел, который ставил действительно сложную и математически богатую задачу (в данном случае, воспроизводя интуицию, которая уже была у топологов).

Некоторые люди представляют себе мир, в котором компьютеры дают нам ответы на все вопросы. Я мечтаю о большем. Я хочу, чтобы они задавали хорошие вопросы.

Заменит ли ИИ математиков?

1 да

2 нет