Программирование Го

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

Разумеется, нет. Какая же это свобода воли, если субъект не может сознательно выбрать?

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

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

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

А если вспомнить о такой малюсенькой (по сравнению с ИИ) задачке, которую поставил Ферма .
Сколько времени бились, а ведь стимулировали как .
Проблема ИИ будет обязательно решена - или его создадут, или докажут невозможность его создания. В крайнем случае докажут невозможность доказательства того или этого .

Противоречивое утверждение. Если выбор чем-то обусловлен, значит, на самом деле выбора нет.

Лучше все-таки выражаться несколько точнее, три обоснования я привел.

У человека всегда есть выбор, например, быть или не быть сторонником ИИ. Правда, вне зависимости от этого выбора сам ИИ успешно развивается

Да как же, попросите у авторов Чинука, они обязательно дадут вам кучу DVD дисков с вычислениями, программой и логическое обоснование первых двух. Предостережение!: на проверку может не хватит сил, как не хватило 4 лет (!!) 12 мировым экспертам на проверку якобы доказательства Томасом Халесом гипотезы Кеплера (1611). Томас рассердился и пригрозил, что не позже, чем через 20-ти человеколет докажет компьютером, что его доказательство Кеплера компьютером не содержит ошибки :d . Прикол в том, что такое почти смехотворное развитие , уже бывало: несколько лет тому назад сотрудник лондонского офиса компании Майкрософт наконец доказал компьютером, что доказательство компьютером теоремы о 4-ёх красках правильное :/

См. выше.

Вы несколько некорректно сместили акценты. Доказательство "четырёх красок" ни у кого сомнений давно не вызывало; объявившееся формальное доказательство безусловно интересно с точки зрения формальных методов верификации, но всем остальным в общем-то до лампочки.

Что касается верификации, то там уже передоказали целую кучу гораздо менее интересной, а порой и вовсе тривиальной ерунды. Работа такая.

Всё-таки многие "традиционные" математики чувствовали себя неуютно оттого, что нельзя было проверить самому карандашом на бумаге "четыре краски" из-за непосильного числа вариантов раскрашивания. Доказательство бесспорно интересно тем насколько логически обозримо и не вызывает сомнений ядро, из которого таким же обозримым и бесспорным образом выводят заключение теоремы.

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

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

Если так уж задуматься, то трудно отличить живую от неживой материи)
Но это уж если очень глубоко задуматься, почитать Пелевина, Кастанеду, помедитировать...

Вы невнимательны.

Это не обоснование, а пожелание.

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

Спасибо за обсуждение.

А оно и сейчас нельзя - самому, карандашом на бумаге... В этом смысле - да - задача ещё "открыта", посмотреть на некомпьютерное доказательство было бы крайне любопытно. Но никто пока такого не предоставил.

конечно превосходят! я о себе более высокого мнения, чем об автомате.

Во всяком случае у Джонатана Шэффера есть, разумеется, вся существенная и достаточная информация, чтобы восстановить и прокрутить на компьютере доказательство во всей его полноте. А вот будет ли психологически и логически убедительным такое доказательство зависит от того, кто проверяет: эксперт ли он, не слишком громоздкое и запутанное ли само доказательство? Если да, то придётся проверять опять компом, как на примере 4-ёх красок. Проверка компом будет окончательной и за пределами любых сомнений.

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

Такой путь "проверки" доказательства/программы ничейности никогда не выдаст вердикта, ибо черт знает - может следующий раз Чинук проиграет. Доказательство командой Джонатана Шэффера логическое, поддерживаемое вычислениями и претендует на полноту и окончательность. Можно проверить лишь исчерпывающим тотальным перебором или ... таким же логическим путём, каким в 2005 компьютер подтвердил теорему о 4-ёх красках.

Не думаю, что стоит искать доказательство 4-ёх красок "карандашом" . Из-за неупорядоченности (хаоса) пространства вариантов раскрашивания такое доказательство вряд ли возможно. Недаром понадобилась помощь компа счётом, дабы одолеть плохую структуру задачи. Формальная верификация компьютером (2005) существующего до этого также компьютерного доказательства несомненно интересна тем насколько логически обозримо и не вызывает сомнений ядро, из которого таким же обозримым и строгим образом компьютер подтвердил правильность прежнего (опять компьютерного) доказательства.

В каком смысле пожелание? :whistling:

Чем примечательна якобы свобода воли/выбора, обязательно ли такая свобода несовместима с объективным (то бишь материальным по Ленину ) характером той же воли/(само)сознания?

Знаете, Хайдук... На ИШФ я бы скорее всего ответил матом - не со зла и не для того, чтобы обидеть, а просто мне это кажется наиболее уместным ответом на ваш "хаос". На самом деле не так уж и много таких доказательств, которые в какой-то момент сводятся к компьютерному перебору. А "пространство вариантов" в теории графов почти всегда такое - "неупорядоченное" и с "плохой структурой". Хотя искать доказательство "четырёх красок" карандашом, совершенно без компьютерного перебора, действительно, вряд ли стоит - есть более интересные и полезные занятия.

Что касается формальной верификации, то тут есть небольшая закавыка: нельзя доказать корректность самого "верификатора". Уйти от этого никуда нельзя, потому продаётся это в промышленность под довольно странным соусом: например, "верификатор" корректен с вероятностью 97% (такую цифру я слышал про PVS). Что это значит, я никогда не понимал, и продолжаю не понимать до сих пор. До этого я был уверен в справедливости теоремы на 100%, теперь нужно домножать на 0.97.

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

Да, Хайдук, про хаос уже не смешно

Начиная с 1976, когда Апел и Хакен впервые предложили своё компьютерное доказательство, со временем начали все более и более привыкать к и обозревать доказательство, в 1997 появилось опять-таки полагающееся на вычисления компом упрощение Робертсона-Сеймура-Томаса и т.д. Так что ко времени появления (2005) компьютерного вердикта правильности 4-ёх красок уже был, конечно, некоторый консенсус среди экспертов.

Формальная верификация компом это принципиальное дело. Некая теорема верна, потому что эксперты согласились, что она верна. Однако мы не знаем где тот порог, когда эксперты перестанут соглашаться. По-видимому, якобы доказательства гипотезы Кеплера или ничейности чекерсов Чинуком выходят далеко за пределы логических способностей экспертов и компьютерной проверки на корректность этим якобы доказательствам не миновать. Разумеется, логическая база, от которой стартует компьютер, не должна вызывать сомнений, она должна быть обозримой и строгой по мнению экспертов.

И мне не смешно, Дан, но ничего не поделаешь - математикой (как и шахматами , и самим большущим миром) рулит хаос.

Life is tough and then you die

Да какой консенсус?! Статья Сеймура и Ко чиста и прозрачна как слеза ребёнка. Компьютерный перебор каждый может сделать сам, особого ума на это тоже не требуется. Ссылка на "экспертов" здесь справедлива ровно настолько, насколько она справедлива ко всем остальным статьям. Да, читатель должен быть "в теме", но читатель всегда должен быть "в теме", иначе никак - начала арифметики надо изучать надо в других местах и по другим источникам. Таков уж наш жестокий мир.

Может, когда и будет принципиальным...

Только не бывает длинных и запутанных доказательств, для которых нельзя придумать короткое и простое доказательство. Только они и попадают в великую книгу The Book.

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

Даже больше: сами формулировки теорем должны быть такими, что без бутылки и хорошего парсера не разобраться. Вот только кому это интересно?

Да, громоздкие вычисления неструктурированных задач теоретически неинтересны, но часто являются практически важными :wassat:

Я не спорю насчёт 4-ёх красок - кому слеза ребёнка, а кому мутная вода , такое в принципе субъективно и не знаешь когда выдет за пределы башки и/или терпения. Если начнёшь проверять карандашом, голова помутнеет и не будешь уверен что проверил и чего не проверил в море бесчисленных и хаотических вариантов. Как раз такое случилось на 4-ом году с 12-ью "экспертами", проверяющими Кеплера :d . Программы, осуществляющие перебор, имеют массу тупых подвохов вроде упомянутых Вами кейз-сплитс, в которых можно безнадёжно утонуть. Поэтому упражнение по формальной верификации 4-ёх красок имеет своё значение. Могло происходить примерно так: брали небольшой участок проверяемых рассуждений/вычислений и пытались сделать того заведомо корректными механизмами вывода из заведомо корректного стартового ядра проверяющего компа; если не удавалось в разумном времени, брали еще меньший участок. В конце концов добрались до заключительного утверждения 4-ёх красок, то бишь нашли дедуктивный путь от стартового, заведомо корректного ядра до цели. Стало быть, цель оказалась достижимой заведомо корректным путём, что и требовалось доказать.