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

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

Кроме того, когда читают какую-либо статью, гораздо важнее понять сами аргументы, чем просто удостоверится в их корректности. Если какая-то машина скажет, что всё правильно, всё равно будут пытаться понять.

Что касается "кэйз-сплитов", то это мой мозг не приспособлен к большому их количеству, а вот тот же Сеймур ориентируется в них как рыба в воде. (Из нескольких докладов, посвящённых доказательству "perfect graph theorem", я для себя понял лишь одно - читать и разбираться в этом бесполезно.) Вот когда и Сеймур заблудится - вот тогда, значит, и пришла пора компьютеров.

Бесспорно, однако в счётых переборных задачах вряд ли осталось что-нибудь стОящее понять: хаос везде одинаково безинтересен, лишь бы не мог вдруг запустить некоторый живучий порядок.

:d
Дело верификатора предостеречь от тупых ошибок, потому что тупых ошибок он не делает по конструкции (безошибочного логического автомата). А тупые ошибки вероятнее всего в счётных переборных задачах, притом их нельзя заметить из-за их локального (случайного, вполне могли бы быть верными взамен! ) характера и отсутствия сколько-нибудь общих ориентиров как раз по причине внутренней хаотичности проблемы.

Пришлось припомнить свою краткую пересписку с Georges Gonthier, французом, кто в 2005 подтвердил компом корректность уже существующего доказательства (при помощи компа) 4-ёх красок. Надеюсь Генна как эксперт разъяснит следующее деликатное, имхо, обстоятельство: существует неизбежная и каверзная проблема, состоящая в том, что уровень строгости и надёжности языка и средств оригинального доказательства как правило всегда ниже максимальных стандартов проверяющего компа-верификатора. Приходится как-то переводить оригинальные выкладки и вычисления на безукоризненный язык верификатора. Однако при этом принципиально невозможно быть уверенными, что сохраняем смысл и цель оригинальных, менее строгих выводов и рассуждений! :/ В конце концов мы как-то должны надёжно и строго обеспечить, что проверяем и доказываем именно то, что хочем - теорему 4-ёх красок - а не что-нибудь другое :d

Поэтому в переписке с Жоресом я заключил, что в пределах его максимально строгого логического ядра должно было уже имелась формулировка того (утверждения теоремы о 4-ёх красках), чего требовалось доказать. Переносить участки, даже коротенькие, из оригинального нестрогого доказательства недопустимо - девственная строгость ядра верификатора тут же и безвозвратно теряется. Почти наверняка уже существующее нестрогое доказательство использовалось лишь в качестве гида куда направлять заведомо строгие, но целиком и полностью собственные, внутренние выводы из заведомо строгого ядра верификатора. В конце концов верификатору удалось прорубить свой собственный дедуктивный путь к своей собственной формулировке утверждения теоремы о 4-ёх красках! :| Разумеется, мы полагаем, что все это время имели почти зеркальное соответствие между старым доказательством-гидом и новым, максимально строгим и формальным, однако факта этой "очевидной" и убедительной эквивалентности двух доказательств доказать строго никак нельзя! :/ Перевод из одной, менее строгой модели в другую, каким бы взаимно-однозначным ни казался, остаётся лишь символом веры, но не больше - ничто не может гарантировать сохранения смысла и содержания, которые остаются плохо определенными один к другому, одной модели к другой

Жаль, конечно, что Генне или остальным компьютерным хакерам не приспичило потусоваться в прецизионной игре, приходится самому трястись в трансе :|

Чрезвычайно важно НЕ трогать исходного логического ядра на протяжении проверки верификатором некоторой громоздкой и запутанной (неупорядоченной, хаотической) работы вроде 4-ёх красок, упаковки пушечных ядер (проблема Кеплера), решения чекерсов, шахмат и т.п. Разумеется, само ядро верификатора не гарантировано от внутренних протоворечий или неадекватности цели, но добиться большего даже Всевышнему претит - по крайней мере ядро должно быть обозримо для экспертов и не вызывать их сомнений. Любое дальнейшее дополнение/изменение ядра, не говоря уже о множественности таких дополнений/изменений, чревато нечаянным и потенциально фатальным снижением стандартов строгости, ведущим к незаметным ошибкам или подмене смысла и целей (не знаем что и к чему делаем) в условиях коварного хаоса громоздкой и запутанной задачи. Благо комп никогда не ошибётся в малом числе непосредственно обозримых простым глазом правил дедуктивного вывода, выявленных ещё Фреге, Расселом и Уайтхедом.

Какие-то подвижки были за последние пол-года в программировании ГО?)

Интересно, а есть игры, которые сложнее и интереснее, чем Го?)

Шахматы :|

Шахматы намного прощще, или вы не в курсе?

А в чем измерять сложность?

Футбол не формализуем, а значит не является игрой в понимании теории игр.

В данном случае - числом возможных позиций)

WinPooh


Сферический кёрлинг и дартс в вакууме)

В данном случае - числом возможных позиций)

Тогда можно взять просто любую игру, где количество позиций бесконечно или даже несчетно. Например, любая антагонистическая игра на квадрате (0,0)-(1,1). Задана некоторая функция f(x,y). Первый игрок выбирает число x из интервала (0,1), второй игрок выбирает число y из того-же интервала. Выигрыш первого (проигрыш второго) дает функция f.

Слава роботам! Убить всех человеков!) (Бендер)

Google just mastered a game that vexed scientists — and their machines — for decades - The Washington Post

Реми Кулом подтверждает:
https://groups.google.com/forum/#!topic/computer-go-archive/_eCHs8_rMfs

Статья в Nature:
https://storage.googleapis.com/deepmind-data/assets/papers/deepmind-mastering-go.pdf

Ну что ж. Тем интереснее.

И там же пишут, что Facebook одновременно достиг больших успехов.
Оригинальный пост Цукерберга https://www.facebook.com/zuck/videos/vb.4/10102619979032811/?type=2&theater

Не слышал этой байки

Почитал, посмотрел... Как-то уж очень шоколадно получается. Но с другой стороны источники очень авторитетные, сторонние подтверждения тоже. Будем посмотреть.

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

Март вообще будет интересным месяцем. Помимо проверки на прочность Гуглобота, в кубке UEC дебютирует Фейсбукбот. Где-то в то же время состоится интересный матч между компьютером и человеком по сёги.

Читаю дальше... Как дилетант, конечно. Но если что, пусть знающие люди поправят.

Общее впечатление такое, что если раньше Го-программы, образно говоря, стояли на одной ноге (поиск, search), то сейчас твердо встанут на вторую (оценка, evalution). В предыдущие годы, где-то начиная с 2006, к Го был адаптирован, и в дальнейшем развит, способ организации поиска называемый MCTS, по-русски Монте-Карло. В то же время, оценку заменял какой-то эрзац на основе UCB и/или паттернов (форм) для выбора направлений симуляции игры (Simulation). Сейчас же предлагается полноценный способ оценки позиции на основе нейронных сетей и способ её интеграции в поиск MCTS. Надеюсь, всё сложится как надо. Кстати, авторы в статье без колебаний заменяют наименование третьей стадии MCTS с Simulation на Evalution.

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

Первая из нейросетей быстрая (2 мкс), но упрощенная. Вторая медленная (3 мс), но относительно точная. На вход они получают позицию для оценки, а на выходе предлагают ходы. Обе сети настраивались на партиях людей с игровых серверов. Третья сеть на выходе выдает не ходы, а оценку позиции. Эта сеть настраивалась уже не на партиях людей, а на партиях второй сети. Любопытно, что для тренировки второй сети (сети ходов) лучше всего подошли партии людей, а для тренировки третьей сети (сети оценки), напротив, больше подошли партии машины, которые она проводила сама с собой. Все три сети встраиваются в поиск MCTS по своеобразной схеме.

Что интересного обнаружилось:
Во первых, играла распределенная версия (1202 CPU и 176 GPU).
Во вторых, у топовой программы Crazy Stone нераспределенная версия выиграла 77% игр с гандикапом в 4 камня, то есть усиление огромное.
Примерная оценка силы программы - 5-6 дан.
В отличии от шахмат, имеет смысл более медленный поиск с более продвинутой оценкой (что логично, так как дерево поиска гораздо больше)
Контроль был 1 час + 30 секунд на ход, при этом при более коротком контроле программа проиграла несколько партий

—- добавлено: 31 янв 2016 —-

Думаю через пару лет они обыграют чемпиона мира

Как я понял, у них оценка вынесена отдельно - на GPU, тогда как поиск запускается на CPU. Так что, похоже, оценка не отбирает вычислительные ресурсы у поиска.

Интересная статья по мотивам недавней победы машины над профи:
http://clubgo.ru

Я вот на этом основывался:

—- добавлено: 1 фев 2016 —-

Я вот на этом основывался:

5 неопубликованных игр были тренеровочными играми в рапид (и из них 2 человек выиграл). Скорее всего на более длинном контроле усиление компа будет еще заметнее.

5-7 лет имхо оптимистичная оценка. Я бы дал человеку года 3.

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

Не покидает меня подозрение, что был ещё один секретный матч, с более сильным игроком. Не стали бы они после Fan Hui'я, вот просто так, сразу же под Седола бросаться. Может быть конечно им от успеха в голову ударило, но куда им было торопиться? Публиковать партии со второго матча (если он был) им пока не с руки, поскольку как сказал Ке Чжие "Конечно, мы не увидим ее слабости всего лишь по пяти партиям, в том числе потому, что оппонент играл столь плохо". А вот игра с более сильным соперником, что-то бы да показала.

У Deep Blue было 100-200 миллионов нпс, они же говорят, что у них же на 3-4 порядка меньше, и это у распределенной версии с тысячей процессоров.

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