Рубрика «проблема остановки»
Реализм против платонизма. Неполнота Гёделя, неразрешимость Тьюринга и физические основания математики
2025-07-08 в 10:51, admin, рубрики: квантовый компьютер, машина Тьюринга, основания математики, платонизм, проблема остановки, проблема разрешимости, тезис Чёрча-Тьюринга, теорема Гёделя, теория множеств
Учёные доказали, что сдерживание сверхинтеллекта — невычислимая задача
2021-03-22 в 8:20, admin, рубрики: AI, Блог компании VDSina.ru, будущее здесь, вред человечеству, ИИ, искусственный интеллект, компьютерная симуляция, научная фантастика, Научно-популярное, обезьянья лапка, обучение, проблема вреда, проблема остановки, программирование этики, сверхинтеллект, Сверхразум, сдерживание ИИ, тезис Чёрча-Тьюринга, три закона робототехники
Обучение искусственного сверхинтеллекта
Идея сверхинтеллекта не даёт покоя учёным. Некоторые высказывают предположение, что сверхинтеллект не обязан благоприятно относиться к людям, может быть к ним равнодушен, не учитывать их интересы. Что делать в такой ситуации? Точнее, как её предотвратить?
Один из вариантов — контролировать действия сверхинтеллекта, разрешая только такие действия, которые идут на благо человечества. К сожалению, теперь выясняется, что это невозможно. Оказалось, что сдерживание сверхинтеллекта — невычислимая задача.
Читать полностью »
Формальная верификация на примере задачи о волке, козе и капусте
2019-04-22 в 12:42, admin, рубрики: 8 ферзей, coq, Isabelle, np, smt, WhyML, z3, верификация программ, вычислительная сложность, для чайников, защита программ, информационная безопасность, логика Хоара, поиск уязвимостей, проблема остановки, решатель, Символьное выполнение, формальная верификация, формальная верификация для чайников, формальные методыНа мой взгляд, в русскоязычном секторе интернета тематика формальной верификации освещена недостаточно, и особенно не хватает простых и наглядных примеров.
Я приведу такой пример из зарубежного источника, и дополню собственным решением известной задачи о переправе волка, козы и капусты на другую сторону реки.
Но вначале вкратце опишу, что из себя представляет формальная верификация и зачем она нужна.
Под формальной верификацией обычно понимают проверку одной программы либо алгоритма с помощью другой.
Это нужно для того, чтобы удостовериться, что поведение программы соответствует ожидаемому, а также обеспечить её безопасность.
Формальная верификация является самым мощным средством поиска и устранения уязвимостей: она позволяет найти все существующие дыры и баги в программе, либо же доказать, что их нет.
Стоит заметить, что в некоторых случаях это бывает невозможно, как например, в задаче о 8 ферзях с шириной доски 1000 клеток: всё упирается в алгоритмическую сложность либо проблему остановки.
Однако в любом случае будет получен один из трёх ответов: программа корректна, некорректна, или же — вычислить ответ не удалось.
В случае невозможности нахождения ответа, зачастую можно переработать неясные места программы, уменьшив их алгоритмическую сложность, для того чтобы получить конкретный ответ да либо нет.
А применяется формальная верификация, например, в ядре Windows и операционных системах беспилотников Darpa, для обеспечения максимального уровня защиты.
Мы будем использовать Z3Prover, очень мощный инструмент для автоматизированного доказательства теорем и решения уравнения.
Причём Z3 именно решает уравнения, а не подбирает их значения грубым брутфорсом.
Это означает, что он способен находить ответ, даже в случаях когда комбинаций входных вариантов и 10^100.
А ведь это всего лишь около дюжины входных аргументов типа Integer, и подобное зачастую встречается на практике.
Задача о 8 ферзях (Взята из англоязычного мануала).
