К коту вы относитесь внимательно, вот только кастрация все эти плюсы нивелирует. Лучше бы кошек и продолжили держать, раз уж с полноценным котом справиться не можете. Рекомендую продолжить тренировки. И не удивляйтесь, если кот вас однажды хорошенько покусает в отместку за своё хозяйство.
Я только лишь предупредил читателей, чтобы они не угодили в ту же ловушку.
Такие компании имеют одну общую черту: они обещают различные блага
(золотые горы, сказочные перспективы, долю от дохода), но всегда в будущем,
при этом требуя конкретных действий в настоящем.
Жизненно!
Особенно напрягает, когда заманивают на собеседование и объемное тестовое задание некими очень вкусными условиями, и только после его выполнения (которое может растянуться и на неделю) узнаёшь,
что на самом-то деле зарплата будет вдвое ниже рыночной…
Нейросети, хоть и выдают отличные и превосходящие другие экспертные системы ответы, как правило не предоставляют информацию или алгоритм того, каким образом они этот ответ получили, и являются неким подобием чёрного ящика.
Поэтому важным направлением работы современных исследователей является внесение ясности в работу нейросетей, и визуализация того как они находят решение: habr.com/ru/post/401687
Очень интересно, что здесь нашли применение и формальные методы.
Формальная верификация является отличной альтернативой полному перебору:
она хорошо справляется с астрономическим числом комбинаций входных и выходных данных, при этом ничего не упуская и предоставляя всё то же 100% покрытие всех вариантов.
Хоть формальная верификация и используется уже несколько десятков лет, но её применение в областях, связанных с синтезом алгоритмов и машинным обучением, является ещё очень новым и свежим направлением.
Невозможность изменения контрактов после запуска, а также тот факт,
что на них могут храниться огромные суммы средств, иногда приводят к большим проблемам.
В одном из обновлений разработчики кошелька Parity,
в основе которого лежал смарт-контракт именуемый contract multiowned,
поменяли название его внутренней функции multiowned на initMultiowned.
Казалось бы, небольшое улучшение названия на более красивое…
Но до обновления эта функция совпадала с именем самого контракта,
что означало, что она была конструктором, и могла быть вызвана только один раз, сразу после деплоя.
После обновления, initMultiowned, разумеется, перестала считаться конструктором:
теперь эту функцию мог вызвать любой желающий.
Этот факт и выпал из внимания разработчиков.
А функция важная, так как она назначает всех администраторов кошелька, которые и управляют деньгами.
Исходный код функции до и после
До: // constructor is given number of sigs required to do protected "onlymanyowners" transactions
// as well as the selection of addresses capable of confirming them.
function multiowned(address[] _owners, uint _required) {
m_numOwners = _owners.length + 1;
m_owners[1] = uint(msg.sender);
m_ownerIndex[uint(msg.sender)] = 1;
for (uint i = 0; i < _owners.length; ++i) {
m_owners[2 + i] = uint(_owners[i]);
m_ownerIndex[uint(_owners[i])] = 2 + i;
}
m_required = _required;
}
После: // constructor is given number of sigs required to do protected "onlymanyowners" transactions
// as well as the selection of addresses capable of confirming them.
function initMultiowned(address[] _owners, uint _required) {
m_numOwners = _owners.length + 1;
m_owners[1] = uint(msg.sender);
m_ownerIndex[uint(msg.sender)] = 1;
for (uint i = 0; i < _owners.length; ++i) {
m_owners[2 + i] = uint(_owners[i]);
m_ownerIndex[uint(_owners[i])] = 2 + i;
}
m_required = _required;
}
Последствия печальны: злоумышленник сработал оперативно, и за одну ночь отыскал в сети эфира вообще все существующие кошельки Parity (а это несколько тысяч смарт-контрактов), после чего избавил их от предыдущих хозяев. Общие потери составили около 100 миллионов долларов.
Гарантированно предотвратить подобные инциденты можно, только если писать код с математически доказанной надёжностью.
Но это приводит к десятикратному удорожанию разработки, и выходит далеко за рамки интеллектуальных возможностей подавляющего большинства крипто-деятелей. Почему люди не используют формальные методы
На мой взгляд обойтись всё-таки реально, особенно если отказаться от асинхронности.
А проверить выполнение задания клиент может и сам, даже без уведомлений.
Да, удобство снизится, зато безопасность и отказоустойчивость будут максимальны.
Во всяком случае, если не весь код можно сделать функциональным, то хоть его самую важную часть.
CMS, фреймворки, да и сами языки для веб-программирования содержат большое число различных функций, которые ничего не записывают и не сохраняют промежуточных значений.
Порой там находят опасные уязвимости, так что проверка формальными методами им бы не помешала.
Ботулотоксин, к слову, является самым вредоносным не только среди ядов и нейротоксинов.
По опасности на единицу веса он превосходит даже радиоактивные материалы и любые другие вещества.
Такое ощущение, что советы из статьи положены в основу управления персоналом многих корпораций.
Зачастую наблюдал, как людей оценивают не по качеству кода или числу закрытых тасков, а по тому насколько ловко они развешивают лапшу на митингах.
С грустью констатирую, что в подобных организациях наиболее действенными оказываются советы вроде «побольше кивать на совещаниях» или «трогать языком зуб, чтобы создать умное выражение лица».
Функциональное программирование также хорошо тем, что отлично вписывается в концепцию формальной верификации: например, в нём гораздо меньше проблем с сайд-эффектами.
Это упрощает создание отказоустойчивого софта.
Организаторы хакатонов, к сожалению, чаще всего не заинтересованы в дальнейшем выживании команд, а проводят их с целью пиара или хантинга талантливых разработчиков.
Порой даже устоявшаяся команда после хакатона уменьшается в размере.
Сегодня утром я выложил исходники на github в свободный доступ: github.com/scp1001/hyperbox
Вся логика VM содержится в 2 файлах, hyperbox.php и hyperbox2.php
У меня раньше был разряд по шахматам, и я пробовал писать свои шахматные программы.
Такая форма представления в виде 8 строчек и колонок сразу приходит в голову. Она позволяет проще проверять, какие поля бьёт слон, ладья или ферзь, да и по сути является способом представления геометрии доски в программе.
И в задаче с ферзями это будет банально самая лаконичная запись.
Если взять 64 клетки, то придётся гораздо дольше описывать сами понятия горизонталей и вертикалей.
Это я к тому, что никакой подгонки под задачу нет, а попросту было выбрано самое удобное и быстрое в написании представление.
Но ваша идея мне нравится, если будет свободная минутка, то постараюсь её опробовать и рассказать, справился ли верификатор или нет.
С точки зрения вычисления такая задача будет действительно сложней.
А пока проведём более простой эксперимент:
В такой задаче 40 320 (если не брать в учёт перестановки).
Это факториал от 8.
Если увеличить число ферзей до 20, это даст уже порядка 10^18 вариантов.
Z3Prover при этом всё так же справляется мгновенно.
Добавим нагрузки и увеличим их число до 30, что даст около 10^32 способов расстановки ферзей на доске.
# We know each queen must be in a different row.
# So, we represent each queen by a single integer: the column position
import json
from z3 import *
Q = [ Int('Q_%i' % (i + 1)) for i in range(30) ]
# Each queen is in a column {1, ... 30 }
val_c = [ And(1 <= Q[i], Q[i] <= 30) for i in range(30) ]
# At most one queen per column
col_c = [ Distinct(Q) ]
# Diagonal constraint
diag_c = [ If(i == j,
True,
And(Q[i] - Q[j] != i - j, Q[i] - Q[j] != j - i))
for i in range(30) for j in range(i) ]
solve(val_c + col_c + diag_c)
Z3Prover задумался секунд на 5, но решение выдал.
Вот оно:
Наш замечательный верификатор справляется неплохо, поскольку он использует гораздо более мощные алгоритмы нежели обычный перебор.
Но у Z3Prover, конечно, тоже есть свои пределы, связанные главным образом с тем что в итоге он упирается в проблему P=NP.
При 40 ферзях дать быстрый ответ он уже не смог.
Как ни странно, но в программировании немало и таких миров.
Кроме розовых пони, там порой обитают и единороги: стартапы или компании которые вышли на капитализацию свыше миллиарда долларов.
Приведу цитату из официального сайта той, самой безопасной в мире OS seL4:
seL4 is the world’s only hypervisor with a sound worst-case execution-time (WCET) analysis, and as such the only one that can give you actual real-time guarantees, no matter what others may be claiming. (If someone else tells you they can make such guarantees, ask them to make them in public so Gernot can call out their bullshit.) docs.sel4.systems/FrequentlyAskedQuestions.html#can-i-run-a-real-time-os-in-a-virtual-machine-on-sel4
Они решили вашу проблему, и смогли предсказать (и доказать!) время исполнения кода в самом худшем случае.
В итоге беспилотники Darpa летают не взирая на сайд-эффекты.
Довольно много ICO за прошлые 2 года смогли пробраться на хабр, и утомить читателей своими навязчивыми предложениями купить их монет.
Вот и закономерный результат.
Вместе с тем статьи, вписывающиеся в тематику площадки и освещающие именно технические моменты блокчейна воспринимаются вполне нормально.
Благодарю, удача в этом нелёгком деле мне пригодится!
Остапом, однако, я себя не считаю, а все свои доводы и суждения буду подкреплять работающим кодом.
Нейронные сети уже достаточно хорошо изучены, и в эту сферу сложно привнести что-то новое.
Меня больше интересуют методы синтеза программ только лишь по входным и выходным данным конкретно с помощью SMT/SAT.
Это не моё изобретение, такой подход уже имеет место быть, хоть и не слишком известен.
В одной из следующей статей я намерен осветить и эту тематику, тоже на конкретных примерах.
Машина может сгенерировать исходный код только имея входные и выходные данные.
Для этого обычно применяют нейросети или генетические алгоритмы, но SMT/SAT решатели тоже применяются для этой цели и в некоторых случаях превосходят все другие подходы.
И даже более того, машина в принципе может сгенерировать описание, спецификацию, входные данные и исходный код только лишь имея выходные данные в достаточном количестве.
Но это уже к синтезу программ и алгоритмов относится.
Такие компании имеют одну общую черту: они обещают различные блага
(золотые горы, сказочные перспективы, долю от дохода), но всегда в будущем,
при этом требуя конкретных действий в настоящем.
Особенно напрягает, когда заманивают на собеседование и объемное тестовое задание некими очень вкусными условиями, и только после его выполнения (которое может растянуться и на неделю) узнаёшь,
что на самом-то деле зарплата будет вдвое ниже рыночной…
Поэтому важным направлением работы современных исследователей является внесение ясности в работу нейросетей, и визуализация того как они находят решение: habr.com/ru/post/401687
Очень интересно, что здесь нашли применение и формальные методы.
Формальная верификация является отличной альтернативой полному перебору:
она хорошо справляется с астрономическим числом комбинаций входных и выходных данных, при этом ничего не упуская и предоставляя всё то же 100% покрытие всех вариантов.
Хоть формальная верификация и используется уже несколько десятков лет, но её применение в областях, связанных с синтезом алгоритмов и машинным обучением, является ещё очень новым и свежим направлением.
что на них могут храниться огромные суммы средств, иногда приводят к большим проблемам.
В одном из обновлений разработчики кошелька Parity,
в основе которого лежал смарт-контракт именуемый contract multiowned,
поменяли название его внутренней функции multiowned на initMultiowned.
Казалось бы, небольшое улучшение названия на более красивое…
Но до обновления эта функция совпадала с именем самого контракта,
что означало, что она была конструктором, и могла быть вызвана только один раз, сразу после деплоя.
После обновления, initMultiowned, разумеется, перестала считаться конструктором:
теперь эту функцию мог вызвать любой желающий.
Этот факт и выпал из внимания разработчиков.
А функция важная, так как она назначает всех администраторов кошелька, которые и управляют деньгами.
// constructor is given number of sigs required to do protected "onlymanyowners" transactions
// as well as the selection of addresses capable of confirming them.
function multiowned(address[] _owners, uint _required) {
m_numOwners = _owners.length + 1;
m_owners[1] = uint(msg.sender);
m_ownerIndex[uint(msg.sender)] = 1;
for (uint i = 0; i < _owners.length; ++i) {
m_owners[2 + i] = uint(_owners[i]);
m_ownerIndex[uint(_owners[i])] = 2 + i;
}
m_required = _required;
}
После:
// constructor is given number of sigs required to do protected "onlymanyowners" transactions
// as well as the selection of addresses capable of confirming them.
function initMultiowned(address[] _owners, uint _required) {
m_numOwners = _owners.length + 1;
m_owners[1] = uint(msg.sender);
m_ownerIndex[uint(msg.sender)] = 1;
for (uint i = 0; i < _owners.length; ++i) {
m_owners[2 + i] = uint(_owners[i]);
m_ownerIndex[uint(_owners[i])] = 2 + i;
}
m_required = _required;
}
Последствия печальны: злоумышленник сработал оперативно, и за одну ночь отыскал в сети эфира вообще все существующие кошельки Parity (а это несколько тысяч смарт-контрактов), после чего избавил их от предыдущих хозяев. Общие потери составили около 100 миллионов долларов.
Гарантированно предотвратить подобные инциденты можно, только если писать код с математически доказанной надёжностью.
Но это приводит к десятикратному удорожанию разработки, и выходит далеко за рамки интеллектуальных возможностей подавляющего большинства крипто-деятелей.
Почему люди не используют формальные методы
А проверить выполнение задания клиент может и сам, даже без уведомлений.
Да, удобство снизится, зато безопасность и отказоустойчивость будут максимальны.
Во всяком случае, если не весь код можно сделать функциональным, то хоть его самую важную часть.
CMS, фреймворки, да и сами языки для веб-программирования содержат большое число различных функций, которые ничего не записывают и не сохраняют промежуточных значений.
Порой там находят опасные уязвимости, так что проверка формальными методами им бы не помешала.
По опасности на единицу веса он превосходит даже радиоактивные материалы и любые другие вещества.
Зачастую наблюдал, как людей оценивают не по качеству кода или числу закрытых тасков, а по тому насколько ловко они развешивают лапшу на митингах.
С грустью констатирую, что в подобных организациях наиболее действенными оказываются советы вроде «побольше кивать на совещаниях» или «трогать языком зуб, чтобы создать умное выражение лица».
Это упрощает создание отказоустойчивого софта.
Организаторы хакатонов, к сожалению, чаще всего не заинтересованы в дальнейшем выживании команд, а проводят их с целью пиара или хантинга талантливых разработчиков.
Порой даже устоявшаяся команда после хакатона уменьшается в размере.
github.com/scp1001/hyperbox
Вся логика VM содержится в 2 файлах, hyperbox.php и hyperbox2.php
Такая форма представления в виде 8 строчек и колонок сразу приходит в голову. Она позволяет проще проверять, какие поля бьёт слон, ладья или ферзь, да и по сути является способом представления геометрии доски в программе.
И в задаче с ферзями это будет банально самая лаконичная запись.
Если взять 64 клетки, то придётся гораздо дольше описывать сами понятия горизонталей и вертикалей.
Это я к тому, что никакой подгонки под задачу нет, а попросту было выбрано самое удобное и быстрое в написании представление.
Но ваша идея мне нравится, если будет свободная минутка, то постараюсь её опробовать и рассказать, справился ли верификатор или нет.
С точки зрения вычисления такая задача будет действительно сложней.
А пока проведём более простой эксперимент:
В такой задаче 40 320 (если не брать в учёт перестановки).
Это факториал от 8.
Если увеличить число ферзей до 20, это даст уже порядка 10^18 вариантов.
Z3Prover при этом всё так же справляется мгновенно.
Добавим нагрузки и увеличим их число до 30, что даст около 10^32 способов расстановки ферзей на доске.
Z3Prover задумался секунд на 5, но решение выдал.
Вот оно:
Наш замечательный верификатор справляется неплохо, поскольку он использует гораздо более мощные алгоритмы нежели обычный перебор.
Но у Z3Prover, конечно, тоже есть свои пределы, связанные главным образом с тем что в итоге он упирается в проблему P=NP.
При 40 ферзях дать быстрый ответ он уже не смог.
Кроме розовых пони, там порой обитают и единороги: стартапы или компании которые вышли на капитализацию свыше миллиарда долларов.
Приведу цитату из официального сайта той, самой безопасной в мире OS seL4:
seL4 is the world’s only hypervisor with a sound worst-case execution-time (WCET) analysis, and as such the only one that can give you actual real-time guarantees, no matter what others may be claiming. (If someone else tells you they can make such guarantees, ask them to make them in public so Gernot can call out their bullshit.)
docs.sel4.systems/FrequentlyAskedQuestions.html#can-i-run-a-real-time-os-in-a-virtual-machine-on-sel4
Они решили вашу проблему, и смогли предсказать (и доказать!) время исполнения кода в самом худшем случае.
В итоге беспилотники Darpa летают не взирая на сайд-эффекты.
Вот и закономерный результат.
Вместе с тем статьи, вписывающиеся в тематику площадки и освещающие именно технические моменты блокчейна воспринимаются вполне нормально.
Остапом, однако, я себя не считаю, а все свои доводы и суждения буду подкреплять работающим кодом.
Нейронные сети уже достаточно хорошо изучены, и в эту сферу сложно привнести что-то новое.
Меня больше интересуют методы синтеза программ только лишь по входным и выходным данным конкретно с помощью SMT/SAT.
Это не моё изобретение, такой подход уже имеет место быть, хоть и не слишком известен.
В одной из следующей статей я намерен осветить и эту тематику, тоже на конкретных примерах.
Для этого обычно применяют нейросети или генетические алгоритмы, но SMT/SAT решатели тоже применяются для этой цели и в некоторых случаях превосходят все другие подходы.
И даже более того, машина в принципе может сгенерировать описание, спецификацию, входные данные и исходный код только лишь имея выходные данные в достаточном количестве.
Но это уже к синтезу программ и алгоритмов относится.