Пандорум и верификация

[moonwalker72]

Смотрю фильм "Пандорум". Корень всех зол -- в перенаселенности, из-за которой отправляют колонистов к звезде с землеподобной планетой -- это впрочем только фон, не более. Разве через 150 лет население учетверится? Вообще-то в серьёзной статье я читал об опровержении гипотезы Мальтуса -- население пока растет, но скорость этого роста год от года все падает. Там есть еще одна засада в идее фильма, связанная с модификацией генома компьютерной системой корабля исключительно с благими намерениями: повысить выживаемость при дефиците еды воды и кислорода -- при этом люди мутируют в кровожадных карликов. К счастью, не все, но большинство или мутировало или было сожрано. Так вот засада -- в стратегии принятия решений. Сейчас читаю интересную работу по практической формальной верификации программных систем -- методологии model checking, способной находить ошибки, принципиально не обнаруживаемые тестами. Так вот, если модель действий компьютера (разумеется нечеткая и нестрогая, как и любой ИИ) допускает состояние вырождения популяции, то миссия колонизации автоматически проваливается. Люди выживают благодаря собственным врожденным способностям и устойчивости собственной иммунной системы и генома к болезням -- а так же того факта, что они не попали в "окно зла" -- предыдущей вахты-поколения( которая мутировала-сожрана) и с помощью удачного сочетания восстановления памяти-знаний-навыков (опять же, для отдельно взятого человека-организма игральные кости легли удачно) то выходит, что выживание особи само по себе -- это ее судьба. Разумеется, можно назвать это заслугой, но в той же степени, в которой например удалось ни разу не упасть в гололед зимой какого-то года. Здесь есть неустранимый случайный элемент, порождаемый незнанием и который посему не может быть предусмотрен никакой формальной спецификацией модели, и следовательно, поведение верифицированной системы в таких критических точках будет с точки зрения неизмеримо более гибкого живого организма более или менее однотипным. Для него данная система, формально (не в уничижительно-переносном, а именно в математическом смысле) заботящаяся о выживании человека, может сыграть как друга так и врага. А так...если компьютерные системы будут добиваться безусловного выживания несмотря ни на что, то выйдет "Клетка для орхидей" -- то есть особи перестанут быть людьми но и кровожадность уйдет, как порождающая неблагоприятность в нейтральной среде (хотя бы в смысле истечения ресурсов -- живого мяса), они превратятся в овощей. Возможно, надо освободиться от тела, тогда исчезнет и лезвие ножа, по которому приходится порой ходить -- необходимость выжить. Но есть и еще один момент -- если человек рассматривается исключительно как жрущее животное, то неустойчивость стратегии будет завсегда клониться к каннибалам. Вопрос только в масштабе работы модели -- если человек предоставлен сам себе, то неизвестно что лучше: оставить как есть, или оптимизировать за кулисами. Это на самом деле может стать частью формальных требований -- выживание потерявших разум монстров означает проигрыш стратегии колонизации. Так что допускаю, что имела место просто неумная выдумка сценариста.