2014 dxdy logo

Научный форум dxdy

Математика, Физика, Computer Science, Machine Learning, LaTeX, Механика и Техника, Химия,
Биология и Медицина, Экономика и Финансовая Математика, Гуманитарные науки




Начать новую тему Ответить на тему На страницу Пред.  1, 2
 
 Re: О возможности создания сверхчеловеческого ИИ
Сообщение27.05.2025, 17:55 
Заслуженный участник
Аватара пользователя


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

 Профиль  
                  
 
 Re: О возможности создания сверхчеловеческого ИИ
Сообщение28.05.2025, 20:31 


19/05/25

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

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

 Профиль  
                  
 
 Re: Нейросеть+логический движок для математических доказательств
Сообщение28.05.2025, 23:22 
Заслуженный участник


07/08/23
1510
Oleksandr Rybakov в сообщении #1687906 писал(а):
Сколько таких итераций?

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

 Профиль  
                  
 
 Re: Нейросеть+логический движок для математических доказательств
Сообщение29.05.2025, 00:51 
Заслуженный участник
Аватара пользователя


11/12/05
10432

(Оффтоп)

dgwuqtj в сообщении #1687954 писал(а):
Если это будет дешевле, чем работа математика, пусть считает.
Этак математики скоро без работы останутся

 Профиль  
                  
 
 Re: Нейросеть+логический движок для математических доказательств
Сообщение29.05.2025, 11:07 
Заслуженный участник
Аватара пользователя


20/08/14
9164
Oleksandr Rybakov в сообщении #1687906 писал(а):
Нейросеть прогнала свои триллионы умножений и написала лажу. Движок проверил, сказал нейросети - думай еще. Сколько таких итераций?
Вы сейчас о процессе обучения сети или о применении обученной сети?

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

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

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

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

 Профиль  
                  
 
 Re: Нейросеть+логический движок для математических доказательств
Сообщение30.05.2025, 20:07 


19/05/25

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

 Профиль  
                  
 
 Re: Нейросеть+логический движок для математических доказательств
Сообщение02.06.2025, 09:51 


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

 Профиль  
                  
 
 Re: Нейросеть+логический движок для математических доказательств
Сообщение02.06.2025, 10:07 


14/01/11
3463
Rasool в сообщении #1688443 писал(а):
Дискуссия: если ИИ способен доказать теорему, но человек не может это понять — считается ли это «знанием»?

Джон фон Нейман писал(а):
В математике вы не понимаете вещи. Вы просто привыкаете к ним.

 Профиль  
                  
 
 Re: Нейросеть+логический движок для математических доказательств
Сообщение02.06.2025, 10:23 
Заслуженный участник
Аватара пользователя


20/08/14
9164
Rasool в сообщении #1688443 писал(а):
Дискуссия: если ИИ способен доказать теорему, но человек не может это понять — считается ли это «знанием»?
Тот же вопрос обсуждался в связи с computer-assisted proof. Пообсуждали и успокоились.

Кранц в книге Изменчивая природа математического доказательства писал(а):
Компьютерных доказательств вокруг уже много <…>, так что большая часть математического сообщества принимает их или по крайней мере относится к ним толерантно
Классическое доказательство, конечно, лучше. Но иметь computer-assisted proof лучше, чем не иметь ничего. Думаю, так будет и с результатами ИИ, проверенными пруфчекером.

 Профиль  
                  
 
 Re: Нейросеть+логический движок для математических доказательств
Сообщение02.06.2025, 11:00 
Заслуженный участник


07/08/23
1510
Rasool в сообщении #1688443 писал(а):
если ИИ способен доказать теорему, но человек не может это понять — считается ли это «знанием»?

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

 Профиль  
                  
Показать сообщения за:  Поле сортировки  
Начать новую тему Ответить на тему  [ Сообщений: 25 ]  На страницу Пред.  1, 2

Модераторы: Karan, Toucan, PAV, maxal, Супермодераторы



Кто сейчас на конференции

Сейчас этот форум просматривают: нет зарегистрированных пользователей


Вы не можете начинать темы
Вы не можете отвечать на сообщения
Вы не можете редактировать свои сообщения
Вы не можете удалять свои сообщения
Вы не можете добавлять вложения

Найти:
Powered by phpBB © 2000, 2002, 2005, 2007 phpBB Group