ИИ и формальные доказательства теорем

[DieselMachine]

В ближайшее время в Lean будет формализована вся известная на этот момент математика.
1. Когда это будет сделано, можно ли будет обучить новый математический ИИ только на формализованной математике, целью которого будет только поиск новых доказательств?
2. Будет ли этот математический ИИ искать доказательства лучше или хуже передовых ИИ моделей? Если он будет хуже, то каких ещё данных ему не достаточно для обучения?
3. Вот есть этот математический ИИ, который каким-то способом ищет новые доказательства. Можно ли придумать конкретный алгоритм поиска новых доказательств на Lean, который будет работать лучше чем математический ИИ? Подходит полный перебор всех возможных доказательств, но это слишком долго. Можно ли придумать что-то побыстрее полного перебора, но достаточно эффективное?
4. Верно ли что поиск новых доказательств искусственным интеллектом это просто перебор каким-то способом? Для передовых ИИ? Для математического ИИ? То есть может ли ИИ "придумать" новую идею или теорию как это может сделать человек или нет?

[warlock66613]

DieselMachine в сообщении #1737710 писал(а):

В ближайшее время в Lean будет формализована вся известная на этот момент математика.

Чем ответите, если не будет?

[Ghost_of_past]

(Оффтоп)

warlock66613 в сообщении #1737712 писал(а):

Чем ответите, если не будет?

Особенно в свете того, что наконец-то появились признаки того, что пузырь на рынке ИИ и всего, что с ним связано, перестал надуваться и стоит на грани того, чтобы начать сдуваться. Последние несколько недель активно идет дело, но здесь конечно ничего неожиданного.

[DieselMachine]

Цитата:

Чем ответите, если не будет?

Уже формализованы доказательство теоремы Ферма, классификация простых конечных групп, доказательство гипотез Вейля и весь stacks project, доказательство Перельмана и много чего ещё. А один из главных специалистов по формализации Кевин Баззард даёт оценку в три года. Так что никаких сомнений нет что будет.
А если всё-таки не будет, тогда так: допустим, вся математика формализована в Lean...

[warlock66613]

DieselMachine, я не это спросил.

[DieselMachine]

Цитата:

DieselMachine, я не это спросил.

Тогда я не понял вопроса.

И ещё добавлю вопрос
5. Если модели отдать только самые основные определения: And, Or, Not, Nat, Eq, ... и запустить формулировать теоремы и искать доказательства и обучаться на своих же результатах. То как далеко она сможет продвинуться?

[High-trade]

DieselMachine в сообщении #1737721 писал(а):

Цитата:

DieselMachine, я не это спросил.

Тогда я не понял вопроса.

И ещё добавлю вопрос
5. Если модели отдать только самые основные определения: And, Or, Not, Nat, Eq, ... и запустить формулировать теоремы и искать доказательства и обучаться на своих же результатах. То как далеко она сможет продвинуться?

Математика работает с числами, они же вектора, они же точки.Далее методы работы с ними - функциональный анализ, теория групп итд. And, OR - это действия, они должны над чем-то работать.

-- добавлено через 12 минут --

ИИ - это не поймет, задаст уточняющие вопросы)

[mihaild]

DieselMachine в сообщении #1737710 писал(а):

В ближайшее время в Lean будет формализована вся известная на этот момент математика.

Ниже ответы в предположении, что это в каком-то разумном смысле сделано (хотя есть и мнение, что это в принципе невозможно).

DieselMachine в сообщении #1737710 писал(а):

Когда это будет сделано, можно ли будет обучить новый математический ИИ только на формализованной математике, целью которого будет только поиск новых доказательств?

Можно, конечно, обучить LLM чисто на этих доказательствах в Lean. Как-то работать будет.

DieselMachine в сообщении #1737710 писал(а):

Будет ли этот математический ИИ искать доказательства лучше или хуже передовых ИИ моделей? Если он будет хуже, то каких ещё данных ему не достаточно для обучения?

Надо проверять, но я бы поставил примерно 19:1, что при сравнимых размерах и обучении будет хуже. Потому что, скорее всего, думать сразу в терминах Lean - менее эффективный способ доказывать, чем начинать с чего-то "интуитивного", и дальше формализовывать. А при обучении на формальных доказательствах, машине придется эти "интуитивные" концепции находить самостоятельно.

DieselMachine в сообщении #1737710 писал(а):

Можно ли придумать что-то побыстрее полного перебора, но достаточно эффективное?

У Вас написано "но", но первое и второе направлены в одну сторону, а не в разные.
Вот недавно доказали, что SAT можно решить быстрее, чем перебором. Я не уверен, есть ли линейное сведение поиска доказательств (данного размера) к SAT, но если есть - то есть и поиск доказательств быстрее полного перебора. Есть ли что-то достаточно эффективное для применения на практике - неизвестно.

DieselMachine в сообщении #1737710 писал(а):

Верно ли что поиск новых доказательств искусственным интеллектом это просто перебор каким-то способом? Для передовых ИИ?

Ну разве что в том же смысле, что и поиск доказательств человеком - это "перебор каким-то способом". Люди же тоже пробуют разные идеи.

(Оффтоп)

Ghost_of_past в сообщении #1737713 писал(а):

Последние несколько недель активно идет дело, но здесь конечно ничего неожиданного.

А почему Далио является авторитетом, а Маск - нет?

Ghost_of_past в сообщении #1737713 писал(а):

Особенно в свете того, что наконец-то появились признаки того, что пузырь на рынке ИИ и всего, что с ним связано, перестал надуваться и стоит на грани того, чтобы начать сдуваться

Вы уже закупились SQQQ?

DieselMachine в сообщении #1737721 писал(а):

Если модели отдать только самые основные определения: And, Or, Not, Nat, Eq, ... и запустить формулировать теоремы и искать доказательства и обучаться на своих же результатах.

Что это вообще значит? Какой модели, и что такое "основные определения" и как их "давать" в данном контексте?

High-trade в сообщении #1737727 писал(а):

Математика работает с числами, они же вектора, они же точки

Что это вообще значит?

[Ghost_of_past]

(Оффтоп)

mihaild в сообщении #1737732 писал(а):

А почему Далио является авторитетом, а Маск - нет?

Ну хотя бы по той причине, что Далио - финансист, а Маск наркоман-мизантроп с комплексом бога, наплодивший кучу детей от кучи женщин нет. Хотя вообще не заметить пузырь на рынке мог только слепой: уж больше года, как о рисках пузыря говорят МВФ и Всемирный Банк.

mihaild в сообщении #1737732 писал(а):

Вы уже закупились SQQQ?

Я закупился попкорном. Но попкорн - пустые углеводы, поэтому давайте заменим на протеиновые батончики.

[High-trade]

Цитата:

="mihaild в сообщении #1737732"]Что это вообще значит?

Например - Формула Эйлера, в ней комплексное число - это вектор в полярной системе и точка с двумя ортогональными проекциями.

[DieselMachine]

mihaild в сообщении #1737732 писал(а):

DieselMachine в сообщении #1737721 писал(а):

Если модели отдать только самые основные определения: And, Or, Not, Nat, Eq, ... и запустить формулировать теоремы и искать доказательства и обучаться на своих же результатах.

Что это вообще значит? Какой модели, и что такое "основные определения" и как их "давать" в данном контексте?

Всё что у нас есть - это Lean

structure And (a b : Prop) : Prop where
  intro ::
  left : a
  right : b

inductive Or (a b : Prop) : Prop where
  | inl (h : a) : Or a b
  | inr (h : b) : Or a b

inductive Nat where
  | zero : Nat
  | succ (n : Nat) : Nat

И т. д. Берём все эти основные типы данных, можно прямо всё что идёт стандартом в Lean без Mathlib. Там и простые теоремы есть с доказательствами, например, ассоциативность натуральных чисел. Обучаем на этих данных ИИ и запускаем искать дальше новые определения и теоремы. Как далеко продвинется ИИ?

High-trade в сообщении #1737727 писал(а):

Математика работает с числами, они же вектора, они же точки

Числа, векторы, точки - всё это определяется как какие-то типы данных в Lean

[mihaild]

DieselMachine в сообщении #1737746 писал(а):

Берём все эти основные типы данных, можно прямо всё что идёт стандартом в Lean без Mathlib. Там и простые теоремы есть с доказательствами, например, ассоциативность натуральных чисел. Обучаем на этих данных ИИ и запускаем искать дальше новые определения и теоремы. Как далеко продвинется ИИ?

Тут нужно отказаться от непонятно что значащего термина ИИ, и указать конкретную модель.
Если брать подобные современным LLM, основанные на трансформерах - то ни на сколько. Хорошо если скобки правильно расставлять научится.

[mathpath]

DieselMachine в сообщении #1737710 писал(а):

4. Верно ли что поиск новых доказательств искусственным интеллектом это просто перебор каким-то способом? Для передовых ИИ? Для математического ИИ? То есть может ли ИИ "придумать" новую идею или теорию как это может сделать человек или нет?

Нет, это не просто перебор.
Нейросеть — это сжатая вероятностная модель, которая интерполирует и обобщает паттерны.
Когда GPT доказывает теорему, он не перебирает — он генерирует наиболее вероятную последовательность токенов, которая «похожа» на доказательство.
Это ближе к ассоциативному мышлению, чем к перебору.

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

[DieselMachine]

Цитата:

Когда GPT доказывает теорему, он не перебирает — он генерирует наиболее вероятную последовательность токенов, которая «похожа» на доказательство.

Ага, понятно. Я имел в виду связку ИИ+Lean когда что-то похожее на доказательство от ИИ отдаётся в Lean, тот отвечает что не компилируется и ИИ делает следующую попытку

Цитата:

Можно ли придумать что-то побыстрее полного перебора, но достаточно эффективное?

Цитата:

Вот недавно доказали, что SAT можно решить быстрее, чем перебором. Я не уверен, есть ли линейное сведение поиска доказательств (данного размера) к SAT, но если есть - то есть и поиск доказательств быстрее полного перебора. Есть ли что-то достаточно эффективное для применения на практике - неизвестно.

Я пожалуй задам вопрос конкретнее. Вот недавно OpenAI выложил доказательство, например, квази-гипотезы Римана. Если допустим у нас есть в формализованном виде вся математика, известная на начало этого года, можно ли придумать алгоритм поиска доказательств, который тоже найдёт доказательство квази-гипотезы Римана, используя только формализованную в Lean математику, за время сравнимое с временем OpenAI.
В общем, только ли ИИ может так эффективно искать доказательства или существует детерминированный алгоритм, который тоже может не хуже?

[mihaild]

DieselMachine в сообщении #1737991 писал(а):

Я имел в виду связку ИИ+Lean когда что-то похожее на доказательство от ИИ отдаётся в Lean, тот отвечает что не компилируется и ИИ делает следующую попытку

Примерно так это и работает. И люди примерно так и работают - что-то пробуют, смотрят, получилось ли, и, если не получилось - пробуют что-то другое.
Вопрос в том, как выбирать, что пробовать. Под "перебором" обычно понимается какой-то очень простой способ выбора, как правило - вообще все строки (или с минимальными ограничениями, накладываемыми грамматикой).

DieselMachine в сообщении #1737991 писал(а):

В общем, только ли ИИ может так эффективно искать доказательства или существует детерминированный алгоритм, который тоже может не хуже?

Современный "ИИ" (LLM) - детерменированный алгоритм. Точнее там при применении и обучении есть некоторые недетерменированные элементы, но их легко сделать детерменированными с небольшой потерей вычислительной эффективности, а случайность заменить псевдослучайностью (как правило это уже сделано).