2014 dxdy logo

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

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




Начать новую тему Ответить на тему На страницу Пред.  1 ... 4, 5, 6, 7, 8  След.
 
 Re: Критерий истинности в математике
Сообщение04.07.2016, 20:30 


20/09/09
1879
Уфа
epros в сообщении #1134473 писал(а):
Машина-то Тьюринга Вам чем не угодила? Она, в общем-то как раз и определяет то, что в принципе "доказуемо или опровержимо". Так что если Вы хотите чего-то такого, что в принципе недостижимо для машины Тьюринга, то значит собираетесь залезть в область принципиально недоказуемого и неопровержимого.

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

 Профиль  
                  
 
 Re: Критерий истинности в математике
Сообщение04.07.2016, 21:07 
Заслуженный участник
Аватара пользователя


28/09/06
10413
Rasool в сообщении #1135739 писал(а):
Пока профессиональные математики в основном доказывают теоремы с помощью своей головы, а не с помощью компьютера.

И Вы отсюда делаете вывод, что большинство доказанного математиками компьютер доказать не может? Вовсе нет.

 Профиль  
                  
 
 Re: Критерий истинности в математике
Сообщение04.07.2016, 21:32 
Заслуженный участник
Аватара пользователя


20/08/14
8062
Здесь важно не смешивать разные смыслы выражения "компьютер может доказать".

Первый вопрос - можно ли данное математиками неформальное доказательство перевести на язык какой-то "стандартной" формальной теории. Я не в курсе, честно говоря, в чем они там доказывают - в формальной ZFC или еще где-то, но факт в том, что теория не выдумывается специально под эту конкретную теорему - так можно было бы включить ее в список аксиом и дело с концом - а берется стандартная теория со стандартными аксиомами, и на ее языке записывается доказательство. Обычно считается, что на формальный язык можно перевести любое доказательство, хотя Вавилов, например, сомневается, что это можно сделать с топологическими доказательствами, использующими картинки. После того, как формальное доказательство построено, компьютер может проверить его и в этом смысле "доказать" теорему. Другой вопрос, сколько времени у человека займет перевод с неформального языка на формальный. Это очень трудоемкий процесс, и есть даже мнение, что для серьезных теорем практически неподъемный.

Второй вопрос - а может ли компьютер не проверить составленное человеком формальное доказательство, а самостоятельно его найти за разумное время? Здесь пока все плохо, к сожалению. Т.е. алгоритмически никаких проблем - перебираем все доказательства, пока одно из них не окажется доказательством нужного утверждения или противоположного (как завещал вождь и учитель Гедель, на каких-то утверждениях мы зациклимся, но на самом деле таких утверждений еще поискать; их можно конструировать специально, но чтобы интересное нам утверждение по закону подлости оказалось недоказуемым - это вряд ли). Идиллию портит оговорка "за разумное время", потому что ждать $100^{500}$ лет - удовольствие ниже среднего.

 Профиль  
                  
 
 Re: Критерий истинности в математике
Сообщение05.07.2016, 12:39 
Заслуженный участник
Аватара пользователя


28/09/06
10413
Anton_Peplov в сообщении #1135744 писал(а):
Второй вопрос - а может ли компьютер не проверить составленное человеком формальное доказательство, а самостоятельно его найти за разумное время? Здесь пока все плохо, к сожалению.

Полагаю, что вся проблема заключается в нахождении слишком большого количества ненужных человеку доказательств. И истоки её лежат, очевидно, в нашей неспособности внятно сформулировать, какие из доказательств нам нужны, чтобы компьютеру не делать лишней работы. Так что мы сами виноваты, а не компьютеры.

 Профиль  
                  
 
 Re: Критерий истинности в математике
Сообщение05.07.2016, 13:58 
Заслуженный участник
Аватара пользователя


20/08/14
8062
Нет, я говорю вот о чем. Пусть мы точно знаем, что нам нужно доказательство ВТФ. Записываем ВТФ на языке формальной теории. Вопрос: как компьютеру найти доказательство этого утверждения? Сферический алгоритм в вакууме существует: перебирать все конечные строки языка теории, отделять доказательства и проверять, является ли найденное доказательство доказательством ВТФ. Надежды, что этот алгоритм остановится раньше, чем погаснет Солнце, нет совсем никакой.

 Профиль  
                  
 
 Re: Критерий истинности в математике
Сообщение05.07.2016, 14:08 
Заслуженный участник
Аватара пользователя


19/12/10
1546
Anton_Peplov в сообщении #1135862 писал(а):
Записываем ВТФ на языке формальной теории. Вопрос: как компьютеру найти доказательство этого утверждения?

Метод резолюций. Хотя это и не сферический метод в вакууме, но фактически эквивалентен решению SAT-проблемы.

Подробности тут: Чень Ч., Ли Р. Математическая логика и автоматическое доказательство теорем.

 Профиль  
                  
 
 Re: Критерий истинности в математике
Сообщение05.07.2016, 14:48 
Заслуженный участник
Аватара пользователя


16/07/14
8355
Цюрих
Anton_Peplov в сообщении #1135744 писал(а):
время? Здесь пока все плохо, к сожалению

Уже для евклидовой геометрии всегда будет всё плохо - задача истинности формул в ней EXPTIME-трудна. Можно только пытаться рассматривать эвристики разного качества.

 Профиль  
                  
 
 Re: Критерий истинности в математике
Сообщение05.07.2016, 19:10 
Заслуженный участник
Аватара пользователя


28/09/06
10413
Хочу сказать всем защитникам преимуществ человеческого разума перед бездушными машинами: Экспоненциальная сложность задачи поиска доказательства для человека такая же непреодолимая проблема, как и для компьютера. И никакая математическая интуиция или другие формы оракулов тут не помогут. Другое дело, что человек вполне может что-нибудь добавить в аксиоматику, если сочтёт это полезным для облегчения доказательства. Компьютер такого делать не станет (если явно ему этого не разрешить).

 Профиль  
                  
 
 Re: Критерий истинности в математике
Сообщение05.07.2016, 19:55 
Заслуженный участник
Аватара пользователя


16/07/14
8355
Цюрих
epros, разве доказано, что $BQP \neq EXPTIME$?

 Профиль  
                  
 
 Re: Критерий истинности в математике
Сообщение05.07.2016, 20:28 
Заслуженный участник
Аватара пользователя


28/09/06
10413
mihaild в сообщении #1135946 писал(а):
epros, разве доказано, что $BQP \neq EXPTIME$?

Я не понял, это намёк на то, что в мозгах математиков - квантовый компьютер? Давайте тогда наймём кого-нибудь из них в криптоаналитики, чтобы с помощью алгоритма Шора за время $N^3$ в уме шифры взламывали. :-)

 Профиль  
                  
 
 Re: Критерий истинности в математике
Сообщение05.07.2016, 20:41 
Заслуженный участник
Аватара пользователя


20/08/14
8062
epros в сообщении #1135940 писал(а):
Экспоненциальная сложность задачи поиска доказательства для человека такая же непреодолимая проблема, как и для компьютера.
Ну Уайлс же не доказывал ВТФ полным перебором строк, похожих на доказательство, нес па? Или он в аксиоматику что-то добавил?:) "А примем-ка мы за аксиому, что ВТФ верна".

У некоторых людей, эта, крутые эвристики есть. Ну очень крутые. Мы плохо пока понимаем, какие именно - если бы понимали и научились воспроизводить, у нас каждый выпускник математического факультета был бы Уайлсом. Так вот именно потому, что мы не понимаем, что это за эвристики, мы не можем их запрограммировать, чтобы они были у компьютера. И пока это так, компьютер в деле поиска математических доказательств, быть может, и не будет проигрывать бухгалтеру тете Маше, но Эндрю Уайлсу точно будет проигрывать.

 Профиль  
                  
 
 Re: Критерий истинности в математике
Сообщение05.07.2016, 21:15 


20/09/09
1879
Уфа
Anton_Peplov в сообщении #1135955 писал(а):
epros в сообщении #1135940 писал(а):
Экспоненциальная сложность задачи поиска доказательства для человека такая же непреодолимая проблема, как и для компьютера.
Ну Уайлс же не доказывал ВТФ полным перебором строк, похожих на доказательство, нес па? Или он в аксиоматику что-то добавил?:) "А примем-ка мы за аксиому, что ВТФ верна".

У некоторых людей, эта, крутые эвристики есть. Ну очень крутые. Мы плохо пока понимаем, какие именно - если бы понимали и научились воспроизводить, у нас каждый выпускник математического факультета был бы Уайлсом. Так вот именно потому, что мы не понимаем, что это за эвристики, мы не можем их запрограммировать, чтобы они были у компьютера. И пока это так, компьютер в деле поиска математических доказательств, быть может, и не будет проигрывать бухгалтеру тете Маше, но Эндрю Уайлсу точно будет проигрывать.

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

 Профиль  
                  
 
 Re: Критерий истинности в математике
Сообщение05.07.2016, 21:19 
Заслуженный участник
Аватара пользователя


16/07/14
8355
Цюрих
epros в сообщении #1135953 писал(а):
Я не понял, это намёк на то, что в мозгах математиков - квантовый компьютер?

Это намек на то, что мы не можем уверенно утверждать, что классический компьютер не уступает мозгу (при стремлении размеров компьютера и мозга к бесконечности:D).

 Профиль  
                  
 
 Re: Критерий истинности в математике
Сообщение05.07.2016, 21:24 
Заслуженный участник
Аватара пользователя


20/08/14
8062
Rasool в сообщении #1135963 писал(а):
В принципе, математик должен сам разрабатывать такие эвристики.
К сожалению, эти эвристики сидят где-то у него в подсознании. Выковырять их оттуда и показать он не может. Он может предъявить доказательство, но не путь, которым пришел к доказательству, потому что важные компоненты этого пути скрыты от него самого. Ну скажет он "я думал о том-то, потом по аналогии о том-то, и неожиданно понял, что..." Что скрыто за этим "неожиданно", и есть загадка. Инсайт (как и творчество в целом) - большая тайна, в том числе для самого творца.

 Профиль  
                  
 
 Re: Критерий истинности в математике
Сообщение05.07.2016, 22:09 
Заслуженный участник
Аватара пользователя


28/09/06
10413
Anton_Peplov в сообщении #1135955 писал(а):
Или он в аксиоматику что-то добавил?:)

А разве нет? Вроде, он доказал её отнюдь не в аксиоматике Пеано первого порядка. То бишь, аксиоматика явно была сильнее, чем минимально необходимая.

Anton_Peplov в сообщении #1135955 писал(а):
"А примем-ка мы за аксиому, что ВТФ верна"

Ну, это вряд ли было бы интересно коллегам. А вот если постулировать какое-нибудь существование какого-нибудь недостижимого кардинального числа или что-то в этом роде, так, глядишь, и станет интересным. :-)

Anton_Peplov в сообщении #1135955 писал(а):
У некоторых людей, эта, крутые эвристики есть. Ну очень крутые. Мы плохо пока понимаем, какие именно

Да ладно, это уже мистикой какой-то попахивает. Найти красивое и неожиданное для многих решение сложной (но разумно сложной) задачи - это одно, а непостижимым образом "угадать" решение NP-полной задачи - это другое.

Anton_Peplov в сообщении #1135955 писал(а):
Так вот именно потому, что мы не понимаем, что это за эвристики, мы не можем их запрограммировать, чтобы они были у компьютера

Разумеется, по незнанию можно компьютер так запрограммировать, что он и простейшую школьную задачу будет вечность решать. Эвристики должны, по крайней мере, существовать в принципе. Для многих задач их, вероятно, просто нет, так что тут никакое подсознание не поможет. Иногда да, проблема в том, как извлечь эффективные эвристики из чьего-то подсознания. Но я не вижу причин, по которым эту проблему следует считать принципиально неразрешимой.

mihaild в сообщении #1135965 писал(а):
не можем уверенно утверждать, что классический компьютер не уступает мозгу

Я бы сказал, что у нас нет никаких оснований утверждать, что компьютер уступает мозгу при эквивалентной производительности и правильных базовых алгоритмах. :wink:

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

Модераторы: Модераторы Математики, Супермодераторы



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

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


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

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