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

Тема в разделе "Машинное отделение", создана пользователем WildCat, 11 май 2006.

  1. gennah Учаcтник

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

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

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

    • Участник
    Рег.:
    02.12.2007
    Сообщения:
    4.497
    Симпатии:
    0
    Репутация:
    0
    Оффлайн
    Бесспорно, однако в счётых переборных задачах вряд ли осталось что-нибудь стОящее понять: хаос везде одинаково безинтересен, лишь бы не мог вдруг запустить некоторый живучий порядок.

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

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

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

    • Участник
    Рег.:
    02.12.2007
    Сообщения:
    4.497
    Симпатии:
    0
    Репутация:
    0
    Оффлайн
    Жаль, конечно, что Генне или остальным компьютерным хакерам :D не приспичило потусоваться в прецизионной игре, приходится самому трястись в трансе :|

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

    • Участник
    Рег.:
    06.03.2008
    Сообщения:
    3.792
    Симпатии:
    2
    Репутация:
    0
    Оффлайн
    Какие-то подвижки были за последние пол-года в программировании ГО?)
  6. WinPooh В.М.

    • Команда форума
    Рег.:
    13.02.2006
    Сообщения:
    8.003
    Симпатии:
    1.384
    Репутация:
    51
    Адрес:
    Москва
    Оффлайн
    Подвижки в основном на уровне полировки существующих алгоритмов. Принципиально нового, сравнимого с выходом на сцену Монте-Карло, пока не случилось. Zen прочно утвердился на уровне 1-2 дана КГС...
  7. dan77790 Учаcтник

    • Участник
    Рег.:
    06.03.2008
    Сообщения:
    3.792
    Симпатии:
    2
    Репутация:
    0
    Оффлайн
    Интересно, а есть игры, которые сложнее и интереснее, чем Го?)
  8. Chemer Максим

    • Участник
    Рег.:
    14.09.2006
    Сообщения:
    1.674
    Симпатии:
    0
    Репутация:
    0
    Адрес:
    Запорожье
    Оффлайн
    Шахматы :|
  9. dan77790 Учаcтник

    • Участник
    Рег.:
    06.03.2008
    Сообщения:
    3.792
    Симпатии:
    2
    Репутация:
    0
    Оффлайн
    Шахматы намного прощще, или вы не в курсе?
  10. Mustitz Заслуженный

    • Заслуженный
    • Участник
    Рег.:
    30.09.2006
    Сообщения:
    2.525
    Симпатии:
    116
    Репутация:
    6
    Адрес:
    Киев
    Оффлайн
    А в чем измерять сложность?
  11. WinPooh В.М.

    • Команда форума
    Рег.:
    13.02.2006
    Сообщения:
    8.003
    Симпатии:
    1.384
    Репутация:
    51
    Адрес:
    Москва
    Оффлайн
    Футбол сложнее всего. В нём пространство состояний непрерывно, а в Го и шахматах - дискретно.
  12. Mustitz Заслуженный

    • Заслуженный
    • Участник
    Рег.:
    30.09.2006
    Сообщения:
    2.525
    Симпатии:
    116
    Репутация:
    6
    Адрес:
    Киев
    Оффлайн
    Футбол не формализуем, а значит не является игрой в понимании теории игр.
  13. WinPooh В.М.

    • Команда форума
    Рег.:
    13.02.2006
    Сообщения:
    8.003
    Симпатии:
    1.384
    Репутация:
    51
    Адрес:
    Москва
    Оффлайн
    Хорошо. Тогда пусть будет функциональный морской бой в банаховом пространстве :)
  14. dan77790 Учаcтник

    • Участник
    Рег.:
    06.03.2008
    Сообщения:
    3.792
    Симпатии:
    2
    Репутация:
    0
    Оффлайн

    В данном случае - числом возможных позиций)
  15. dan77790 Учаcтник

    • Участник
    Рег.:
    06.03.2008
    Сообщения:
    3.792
    Симпатии:
    2
    Репутация:
    0
    Оффлайн
    WinPooh


    Сферический кёрлинг и дартс в вакууме)
  16. Mustitz Заслуженный

    • Заслуженный
    • Участник
    Рег.:
    30.09.2006
    Сообщения:
    2.525
    Симпатии:
    116
    Репутация:
    6
    Адрес:
    Киев
    Оффлайн

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

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

    • Команда форума
    Рег.:
    11.02.2006
    Сообщения:
    1.208
    Симпатии:
    22
    Репутация:
    8
    Оффлайн
    Starcraft, или любая другая RTS.

    Из настольных игр к нему ближе Шоги, так как в них больше медленных фигур, чем в шахматах. Есть, кстати, истроические варианты Шоги на больших досках, там точно ничего не просчитать (в течение какого-то времени).

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

    В Старкрафте, например, есть и элементы Го (застройка базы, экспаншены) и Шоги (медленно двигающиеся армии, тратящие некоторое время, чтобы пересечь карту). AI в Старкрафте есть, следовательно он формализуем. Проблема в том что движок закрыт, но можно взять какой-нибудь открытый движок, например TA Spring. Хоть там тоже не идеал, всё-таки AI по идее нужно писать на Си, а не на Луа.
  18. Kirr Администратор

    • Команда форума
    Рег.:
    11.02.2006
    Сообщения:
    1.208
    Симпатии:
    22
    Репутация:
    8
    Оффлайн
    Ну да, ну да.. Шахматы тоже считали сложной игрой, где нужно "понимать", "иметь стратегию", где нужен "интеллект". Пока компьютеры не стали играть сильнее людей. И тут же шахматы оказались тупым счётом вариантов. Так и в футболе будет, только подождать нужно чуть подольше. См. проект RoboCup. Вот победит команда роботов команду людей и тут же выяснится что футбол - это тупая беготня по полю с мячиком. Что тогда людишки придумают, чтобы потешить самолюбие, даже не представляю. Наверное останется только скоростное поедание гамбургеров и другие проявления метаболизма.
  19. dan77790 Учаcтник

    • Участник
    Рег.:
    06.03.2008
    Сообщения:
    3.792
    Симпатии:
    2
    Репутация:
    0
    Оффлайн
    Слава роботам! Убить всех человеков!) (Бендер)
  20. onedrey Ветеран

    • Ветеран
    Рег.:
    01.05.2011
    Сообщения:
    6.275
    Симпатии:
    4.333
    Репутация:
    169
    Оффлайн
    Google just mastered a game that vexed scientists — and their machines — for decades - The Washington Post

    Rom нравится это.
  21. Rom Учаcтник

    • Участник
    Рег.:
    12.02.2012
    Сообщения:
    271
    Симпатии:
    100
    Репутация:
    16
    Оффлайн
  22. onedrey Ветеран

    • Ветеран
    Рег.:
    01.05.2011
    Сообщения:
    6.275
    Симпатии:
    4.333
    Репутация:
    169
    Оффлайн
  23. Комсюк народный модератор

    • Ветеран
    Рег.:
    17.07.2011
    Сообщения:
    8.324
    Симпатии:
    6.970
    Репутация:
    390
    Оффлайн
    не всё Владику некротемы откапывать
    Aprilia нравится это.
  24. onedrey Ветеран

    • Ветеран
    Рег.:
    01.05.2011
    Сообщения:
    6.275
    Симпатии:
    4.333
    Репутация:
    169
    Оффлайн
    12552948_10154405490669918_7293713058915443745_n.jpg

    Не слышал этой байки :)
    дикий муцио, nh2008 и Комсюк нравится это.
  25. WinPooh В.М.

    • Команда форума
    Рег.:
    13.02.2006
    Сообщения:
    8.003
    Симпатии:
    1.384
    Репутация:
    51
    Адрес:
    Москва
    Оффлайн
  26. MS Михаил Семионенков

    • Команда форума
    Рег.:
    10.02.2006
    Сообщения:
    5.749
    Симпатии:
    1.288
    Репутация:
    101
    Оффлайн
  27. Rom Учаcтник

    • Участник
    Рег.:
    12.02.2012
    Сообщения:
    271
    Симпатии:
    100
    Репутация:
    16
    Оффлайн
    Почитал, посмотрел... Как-то уж очень шоколадно получается. Но с другой стороны источники очень авторитетные, сторонние подтверждения тоже. Будем посмотреть.

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

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

    • Участник
    Рег.:
    12.02.2012
    Сообщения:
    271
    Симпатии:
    100
    Репутация:
    16
    Оффлайн
    Читаю дальше... Как дилетант, конечно. Но если что, пусть знающие люди поправят.

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

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

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

    • Участник
    Рег.:
    07.02.2014
    Сообщения:
    487
    Симпатии:
    100
    Репутация:
    15
    Адрес:
    Ришон ле Цион, Израиль
    Оффлайн
    Что интересного обнаружилось:
    Во первых, играла распределенная версия (1202 CPU и 176 GPU).
    Во вторых, у топовой программы Crazy Stone нераспределенная версия выиграла 77% игр с гандикапом в 4 камня, то есть усиление огромное.
    Примерная оценка силы программы - 5-6 дан.
    В отличии от шахмат, имеет смысл более медленный поиск с более продвинутой оценкой (что логично, так как дерево поиска гораздо больше)
    Контроль был 1 час + 30 секунд на ход, при этом при более коротком контроле программа проиграла несколько партий
    --- добавлено: 30 янв 2016 ---
    Думаю через пару лет они обыграют чемпиона мира
  30. Rom Учаcтник

    • Участник
    Рег.:
    12.02.2012
    Сообщения:
    271
    Симпатии:
    100
    Репутация:
    16
    Оффлайн
    Как я понял, у них оценка вынесена отдельно - на GPU, тогда как поиск запускается на CPU. Так что, похоже, оценка не отбирает вычислительные ресурсы у поиска.
  31. Rom Учаcтник

    • Участник
    Рег.:
    12.02.2012
    Сообщения:
    271
    Симпатии:
    100
    Репутация:
    16
    Оффлайн
    Интересная статья по мотивам недавней победы машины над профи:
    http://clubgo.ru
  32. EvgeniyZh Учаcтник

    • Участник
    Рег.:
    07.02.2014
    Сообщения:
    487
    Симпатии:
    100
    Репутация:
    15
    Адрес:
    Ришон ле Цион, Израиль
    Оффлайн
    Я вот на этом основывался:
    --- добавлено: 31 янв 2016 ---
    Я вот на этом основывался:


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

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

    • Участник
    Рег.:
    12.02.2012
    Сообщения:
    271
    Симпатии:
    100
    Репутация:
    16
    Оффлайн
    У Дип Блю, была совсем нетривиальная, для шахматных программ, оценочная функция. Но, да, все равно нейронная сеть должна быть намного сложнее и качественнее. Хотя сравнивать столь разные архитектуры довольно затруднительно.
    Не покидает меня подозрение, что был ещё один секретный матч, с более сильным игроком. Не стали бы они после Fan Hui'я, вот просто так, сразу же под Седола бросаться. Может быть конечно им от успеха в голову ударило, но куда им было торопиться? Публиковать партии со второго матча (если он был) им пока не с руки, поскольку как сказал Ке Чжие "Конечно, мы не увидим ее слабости всего лишь по пяти партиям, в том числе потому, что оппонент играл столь плохо". А вот игра с более сильным соперником, что-то бы да показала.
  34. EvgeniyZh Учаcтник

    • Участник
    Рег.:
    07.02.2014
    Сообщения:
    487
    Симпатии:
    100
    Репутация:
    15
    Адрес:
    Ришон ле Цион, Израиль
    Оффлайн
    У Deep Blue было 100-200 миллионов нпс, они же говорят, что у них же на 3-4 порядка меньше, и это у распределенной версии с тысячей процессоров.

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

    • Участник
    Рег.:
    25.03.2007
    Сообщения:
    287
    Симпатии:
    793
    Репутация:
    42
    Оффлайн

Поделиться этой страницей