Могут ли весёлые игры в онлайне решить сложные проблемы с верификацией программного обеспечения, которыми обычно занимаются профессиональные эксперты в программировании? Другими словами, будет ли армия необразованных геймеров лучше, чем профессиональный процесс? Исследователи из Агентства по перспективным оборонным научно-исследовательским разработкам США (DARPA) уверены, что так и есть.
Первые эксперименты показали, что краудсорсинг даже эффективнее, чем предполагалось. Программа под названием Краудсорсинговая формальная верификация (Crowd Sourced Formal Verification, CSFV) началась в декабре 2013 года, и тогда открыли портал Verigames с пятью бесплатными играми на онлайновую верификацию.
Например, на скриншоте вверху изображена игра Paradox, в которой нужно устранить конфликты, изменяя состояние экранных переменных. По достижении установленного результата перед игроком ставят новую задачу на оптимизацию.
Кроме Paradox, есть ещё космическая головоломка Dynamakr для складывания паззла из космического генератора паттернов; битва с инопланетными захватчиками Ghost Map Hyperspaceс целью украсть их расщелины (через которые гады пересекают ткань пространства-времени) и путешествие по средневековой земле монстров Monster Proof с попутным решением головоломок ради обогащения.
В последней пятой игре Binary Fission нужно отсортировать атомные частицы в минимально возможное количество шагов.
На прошлой неделе DARPA объявило об успехе первого этапа программы и вскоре добавить ещё пять игр на сайт.
Из сообщения в блоге DARPA: «Эти [2013] игры транслировали действия игроков в аннотации к программам и помогли экспертам по формальной верификации в создании математических доказательств, которые подтверждают отсутствие важных классов ошибок в языках программирования C и Java. Первоначальный анализ показывает, что дилетанты, которые играли в игры CSFV, создали тысячи тысяч аннотаций».
В общем, геймерский проект оказался очень удачным.
Пожалуй, не следует беспокоиться из-за неизбежно высокого уровня безработицы в роботизированном обществе будущего. Программисты всегда предложат людям интересные и полезные занятия.
Комментарии (11)
sam002
03.06.2015 23:47Ого, Java и Си прошли формальную верификацию! Вот что надо было выносить в заголовок.
ANSI C вроде бы давно верифицирован, т.к. используется и лицензируется в различных ответственных областях, а вот про java на атомных станциях не слышал ещё.
Признаться думал, что все ОО ЯП не проходит формальную верификацию.
Doktor_Gradus
Здесь тревожнее совсем другое. Такие вещи могут привести (не обязательно приведут, но могут привести, в сочетании с другими факторами — повальной автоматизацией всего и вся, например) к тому, что образуется узкая прослойка высококвалифицированных и очень высокооплачиваемых специалистов — технократическая элита.
А все остальные получат образование в рамках упрощённой средней школы; их научат читать, писать и немного считать. А потом посадят на какую-нибудь несложную работу или вообще на пособие с обязанностью играть в такие игры около часа в день.
В фантастике такие сюжеты уже обыгрывались неоднократно.
sortarage
Пардон, а чем это плохо-то? :)
Doktor_Gradus
Ну, любая элита, и технократия тут не исключение, стремится удерживать систему в положении, при котором она сохраняет свою главенствующую роль. По сути, нас ждёт такое цифровое средневековье, которое может продлиться тысячелетиями. Да, оно будет с демократией, правами людей и меньшинств, прогрессом техники и т.д.
Минус в том, что элита обособится, она будет учиться в отдельных школах и университетах. Куда попасть человеку извне, конечно, будет можно, но очень, очень сложно. Фактически, это будет социальный лифт в элиту, потому что элите всё равно нужна новая кровь. Знания, технологии, наука — окажутся в руках узкого круга людей, которые обязательно воспользуются этой возможностью для контроля. Подчеркну, что прогресс техники и науки сохранится (может быть, темпы замедлятся, но, в целом, прогресс сохранится).
Упрощённая же средняя школа редко будет давать самородков, способных осилить такое же обучение, к которому элита будет готова. По сути, школы будут готовить полуграмотный электорат. Людей для обслуживания нужд элиты и выполнения неавтоматизированной работы.
Радует только то, что раньше или позже система всё равно рухнет. Как рухнул рабовладельческий строй, как рухнуло средневековье. Так и тут. Вопрос лишь во времени.
pronvis
coursera.org www.edx.org oyc.yale.edu с вами не согласятся
alizar Автор
По-моему, это основной сценарий, по которому мы и идём. Теоретически, выглядит неплохо, должны быть гармония и счастье.
Но вот мне кажется, что народ никогда не сравниться с уравниловкой, не смогут мирно жить, черти, всё равно будут соседям глотки грызть… :(
Может быть, чтобы не допустить конфликтов, придётся их занять работой больше, чем на 1 час в день, иначе перебьют друг друга.
IRainman
А почему будет уравниловка то?
Лично я вижу тут только хорошее: не будет голодных, нищих, не будет антисанитарии и большинства болезней, будет минимальный доступный всем без необходимости что либо делать уровень жизни включая безопасность, воду и пищу, жилище, образование, медицину и возможность к саморазвитию. У людей появится больше свободного времени на свои проекты, ибо время, что раньше тратили паша на дядю ради заработать три копейки на покушать и оплатить коммунальные услуги пойдёт на пользу себе и, в конечном итоге, обществу. В общем это и есть Цивилизация!
Уравниловки же не будет просто потому, что те кто будет заниматься своими проектами так и будут жить лучше чем те, кто будет сидеть на попе ровно и ничего не делать.
Помимо этого я вообще сомневаюсь, что будет много тех, кто просто будет сидеть на попе ровно ибо это отсутствие самореализации как таковое и оно изнутри очень сильно давит на психику.
Doktor_Gradus
Угу, угу.
Большинство людей не будут делать НИ-ЧЕ-ГО. Они будут есть, пить, развлекаться целыми днями, зависать во вконтактике или в фб.
IRainman
Почему и откуда эта уверенность в том, что люди не будут ничего делать? Ведь вы сейчас просто берёте людей в нынешних условиях, т.е. когда они устали от жизни «совсем» и выхода из этой ситуации нет никакого кроме как просто на всё закрыть глаза и забыться в оставшееся время.
Всё вот это: бесконечное развлечение, алкоголь и «протрачивание» времени в соц. сетях это следствие воздействия среды, а не свойство человека ибо если бы это было свойством человека то уже очень давно остановился бы человек в развитии своём.
У человека есть интерес, у человека есть тяга к исследованиям и куча других хороших качеств, которым надо давать возможность проявится, а не заставлять людей всё своё время тратить на тупую механическую работу ради добывание себе еды и оплату пребывания в бетонной коробке.
Doktor_Gradus
Давайте расставим точки над ?.
Вы говорите об утопии. Об обществе, в котором имеется изобилие всего и для того, чтобы получить доступ к этому всему человеку не нужно сильно напрягаться. Захотел поработать с суперкомпьютером — пошёл поработал с суперкомпьютером. Мне определённо хотелось бы, чтобы человечество достигло такого уровня, когда полностью раскрывается потенциал каждого человека. Но пока это утопия. Может быть когда-нибудь.
Я же говорю об опасности, поджидающей человечество, если оно пойдёт определённым путём. Путём разделения общества на технократическую элиту и большинство. Элита — это всегда меньшинство, в данном случае отобранное, условно говоря, по уровню интеллекта. И есть большинство, которое элите, в общем, не нужно — рабочих лучше заменить роботами — они не болеют, не устают, в отпуска не ходят. Но что-то же с ним надо делать, не устраивать же концлагеря.
И находится простой выход — даём людям минимальное пособие. На это пособие можно оплатить бетонную коробку, купить еду, одежду и ещё чуть-чуть останется на всякие ништяки.
Немножко больше будут зарабатывать те, кто будет работать на работе, трудно поддающейся роботизации и, при этом, не предъявляющей каких-то особых требований к умениям и интеллекту. Такой работы вокруг полным полно.
Как же теперь убедить этих людей, что этого минимума им достаточно? А начать со школы — школа будет давать некоторый минимум знаний, но не более того. Достаточный минимум, чтобы осилить туториал к игрушке — брутфорсеру, типа Fold It и упомянутым в посте.
И как же вы предлагаете человеку, который живёт на минимальные деньги и у которого минимальное образование, раскрывать свой потенциал?
Замечу ещё, что малообразованному человеку легче запудрить мозги маркетологической чушью и впарить ему вещи, которые ему не нужны. Так что корпорациям это выгодно и они вполне могут лоббировать законопроекты, которые в тоге приведут нас к такой модели общества.
И, кстати, из комментариев я вижу, что мы, если не на полпути к такому обществу, то шаги туда уже делаем. Вот это меня и тревожит.
IRainman
Т.е. то, что есть сейчас получается лучше? :) К тому же:
>>что образуется узкая прослойка высококвалифицированных и очень высокооплачиваемых специалистов — технократическая элита.
это всё уже есть сейчас, узкоспециализированные спецы в области науки, инженерии, компьютерных наук, медицины и т.д. :)