Нейросеть+логический движок для математических доказательств

[Anton_Peplov]

Я Coq не знаю. Возможно, уважаемый george66 сможет помочь.

[Oleksandr Rybakov]

Anton_Peplov в сообщении #1687757 писал(а):

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

Нейросеть прогнала свои триллионы умножений и написала лажу. Движок проверил, сказал нейросети - думай еще. Сколько таких итераций?

[dgwuqtj]

Oleksandr Rybakov в сообщении #1687906 писал(а):

Сколько таких итераций?

Если это будет дешевле, чем работа математика, пусть считает.

[Dan B-Yallay]

(Оффтоп)

dgwuqtj в сообщении #1687954 писал(а):

Если это будет дешевле, чем работа математика, пусть считает.

Этак математики скоро без работы останутся

[Anton_Peplov]

Oleksandr Rybakov в сообщении #1687906 писал(а):

Нейросеть прогнала свои триллионы умножений и написала лажу. Движок проверил, сказал нейросети - думай еще. Сколько таких итераций?

Вы сейчас о процессе обучения сети или о применении обученной сети?

В процессе обучения итераций много. Но это общая ситуация для практически полезных нейросетей. Время их обучения при заданных гиперпараметрах измеряется сутками, а то и в неделями. А потом изменим гиперпараметры и попробуем еще раз, и еще, и еще... Это долгая песня.

Если Вы про применение обученной сети, то пока/если/поскольку она будет доказывать теорему быстрее человека-математика, это будет выгодно.

Вы можете спросить: возможно ли вообще обучить нейросеть доказательству теорем? Я не специалист ни по нейросетям, ни по пруфчекерам, могу только спекулировать. Трудности с математическим доказательством в том, что оно должно быть безупречным. Одна ошибка разрушает все доказательство. Это отличается от обычного использования генеративных нейросетей, когда им достаточно выдать "нечто, похожее на правду".

С другой стороны, доказательство на формальном языке - это набор строк с заданным началом и концом и определенным синтаксисом. Если не ошибаюсь, пруфчекеры устроены так, что соблюдение синтаксиса гарантирует логическую корректность (пусть меня поправят те, кто с ними работал). Каждый может убедиться, что даже туповатая по нынешним меркам GPT-4.1 nano безупречно соблюдает синтаксис русского языка, хотя он запутанный и сложный. Не вижу, почему бы ей не овладеть куда более простым синтаксисом пруфчекера, если бы у нее была достаточно большая обучающая выборка.

[Oleksandr Rybakov]

Триллион умножений это вывод - ответ на вопрос пользователя. Обучение - на много порядков больше.

[Rasool]

В одном телеграм-канале про машинное обучение привели такую статью:
Математика, красота и истина в эпоху ИИ.

Цитата:

Когда-то математическое доказательство считалось вершиной человеческой логики и элегантности. Но ИИ меняет даже это.
В статье https://www.quantamagazine.org/mathematical-beauty-truth-and-proof-in-the-age-of-ai-20250430/ исследуется, как ИИ трансформирует подходы к математике:
ИИ создает доказательства — не просто перебором, а находя закономерности, генерируя гипотезы и даже формируя контрпримеры.
Модели уровня DeepMind уже выигрывают медали на Международной математической олимпиаде.
Красота и элегантность в доказательствах теперь оцениваются не только людьми — ИИ начинает создавать новые формы "математической эстетики".
> “Они разрушают те границы, которые я считал непреодолимыми”
> — Эндрю Грэнвилл, математик
Дискуссия: если ИИ способен доказать теорему, но человек не может это понять — считается ли это «знанием»?

[Sender]

Rasool в сообщении #1688443 писал(а):

Дискуссия: если ИИ способен доказать теорему, но человек не может это понять — считается ли это «знанием»?

Джон фон Нейман писал(а):

В математике вы не понимаете вещи. Вы просто привыкаете к ним.

[Anton_Peplov]

Rasool в сообщении #1688443 писал(а):

Дискуссия: если ИИ способен доказать теорему, но человек не может это понять — считается ли это «знанием»?

Тот же вопрос обсуждался в связи с computer-assisted proof. Пообсуждали и успокоились.

Кранц в книге Изменчивая природа математического доказательства писал(а):

Компьютерных доказательств вокруг уже много <…>, так что большая часть математического сообщества принимает их или по крайней мере относится к ним толерантно

Классическое доказательство, конечно, лучше. Но иметь computer-assisted proof лучше, чем не иметь ничего. Думаю, так будет и с результатами ИИ, проверенными пруфчекером.

[dgwuqtj]

Rasool в сообщении #1688443 писал(а):

если ИИ способен доказать теорему, но человек не может это понять — считается ли это «знанием»?

Если ИИ буквально придумает корректное доказательство на естественном языке, оно вообще ничем не будет отличаться от человеческого. Или речь о том, что такие тексты могут быть слишком длинными для людей? Что-то я сомневаюсь, что с текущими технологиями это возможно. У олимпиадных задач и доказательства вмещаются в страницу, и не надо придумывать десятки определений/лемм.