Forwarded from Covalue
Нашел качественную диссертацию с обзором состояния дел в model checking на 2010й год:
Weißenbacher, [2010] "Program Analysis with Interpolants"
Вкратце идею проверки моделей можно описать так: мы хотим автоматически верифицировать программы, для этого мы аппроксимируем их моделями, то есть автоматами или системами переходов с конечным набором состояний, задаём спецификацию (обычно в какой-то разновидности пропозициональной темпоральной логики) и с помощью поисковых алгоритмов и эвристик исчерпывающе перебираем состояния модели, проверяя что для них всех спецификация верна.
Концептуально этот подход описывается теорией моделей (одним из двух основных разделов логики, второй - это теория доказательств, на которой основана теория типов и proof assistants). Интересно, что в моделчекинге примерно раз в декаду сменяется доминирующая парадигма, в целом его таймлайн выглядит примерно так:
* 1980е - зарождение самой идеи MC из работ Эдмунда Кларка по вычислению неподвижных точек для систем доказательств в предикат-трансформерах, использование BDD для компактификации состояний
* 1990е - дальнейшее ужатие состояний через partial order reduction, появление предикат-абстракции и CEGAR - методов автоматического конструирования моделей из набора assertions о программе
* 2000е - SAT/SMT-революция и уход от BDD, быстрая аппроксимация через интерполяцию Крейга
* 2010е - Аарон Брэдли изобретает семейство алгоритмов PDR (property directed reachability), где процесс построение инварианта чередуется и взаимодействут с построением контрпримера, взаимно усекая пространства поиска
* 2020е - ажиотаж вокруг техник из машинного обучения
Первые три декады и основные их идеи расписаны в первых двух с половиной главах диссертации (вторая половина третьей и четвертая главы более технические).
#automatedreasoning
Weißenbacher, [2010] "Program Analysis with Interpolants"
Вкратце идею проверки моделей можно описать так: мы хотим автоматически верифицировать программы, для этого мы аппроксимируем их моделями, то есть автоматами или системами переходов с конечным набором состояний, задаём спецификацию (обычно в какой-то разновидности пропозициональной темпоральной логики) и с помощью поисковых алгоритмов и эвристик исчерпывающе перебираем состояния модели, проверяя что для них всех спецификация верна.
Концептуально этот подход описывается теорией моделей (одним из двух основных разделов логики, второй - это теория доказательств, на которой основана теория типов и proof assistants). Интересно, что в моделчекинге примерно раз в декаду сменяется доминирующая парадигма, в целом его таймлайн выглядит примерно так:
* 1980е - зарождение самой идеи MC из работ Эдмунда Кларка по вычислению неподвижных точек для систем доказательств в предикат-трансформерах, использование BDD для компактификации состояний
* 1990е - дальнейшее ужатие состояний через partial order reduction, появление предикат-абстракции и CEGAR - методов автоматического конструирования моделей из набора assertions о программе
* 2000е - SAT/SMT-революция и уход от BDD, быстрая аппроксимация через интерполяцию Крейга
* 2010е - Аарон Брэдли изобретает семейство алгоритмов PDR (property directed reachability), где процесс построение инварианта чередуется и взаимодействут с построением контрпримера, взаимно усекая пространства поиска
* 2020е - ажиотаж вокруг техник из машинного обучения
Первые три декады и основные их идеи расписаны в первых двух с половиной главах диссертации (вторая половина третьей и четвертая главы более технические).
#automatedreasoning
Вкратце оформление документов на ребёнка
По свежей памяти решил записать шпаргалку для действий после рождения ребёнка :)
Думаю вне Москвы соответствующие пункты аналогично через региональные центры госуслуг/сайты/ведомства делаются.
1. Свидетельство о рождении – получить в роддоме.
2. Добавить карточку ребёнка каждому родителю на Госуслугах (не обязательно/автоматически)
– Идентификационные номера присваиваются автоматически
* СНИЛС – приходит в email;
* ИНН – отображается в карточке госуслуг.
– Маткапитал приходит автоматически.
– Формальный номер полиса ОМС присваивается автоматически (пока не работает, см. п.6).
Прим. На Госуслугах, Мосуслугах и ФНС можно сделать ребёнку отдельный личный кабинет. Делать этого не следует.
3. Штамп о гражданстве на свидетельство (оформление наличие гражданства по рождению) – лично через любой МФЦ (взять свой паспорт и свидетельство ребёнка).
4. Добавить ребёнка в учётку каждого родителя на Мосуслугах.
5. Прописать ребёнка через Госуслуги.
6. Выбрать страховую компанию ОМС через Госуслуги.
7. Прикрепить ребёнка к поликлинике через Мосуслуги.
8. Запрос детской кухни (при желании – 12 литров молока и 4 литра сока в месяц для мамы или, альтернативно, смесь для ребёнка)
8.1. Подать заявление на получение питания через Мосуслуги
8.2. Записаться к педиатру через Госуслуги. Ребёнка можно не брать, попросить нажать кнопку для молочной кухни. Заодно откроют направления на специалистов по достижению 1 мес.
8.3. Подать заявление на получение QR-кода для пункта выдачи через Мосуслуги.
9. Получить доступ к мед. карте ребёнка через Мосуслуги. Карта станет доступна через lk.emias.mos.ru.
10. Получить три пособия ~20к каждое (не считая помощи для малоимущих и совсем копеечных)
– "Компенсация взамен получения подарочного комплекта для новорожденных" – для Москвы (если отказались от "Собянинской коробки" в роддоме)
– "Единовременная компенсация при рождении (усыновлении) ребёнка" – для Москвы
– "Единовременное пособие при рождении ребёнка" – для РФ (если работаете по ТК – через работодателя)
По свежей памяти решил записать шпаргалку для действий после рождения ребёнка :)
Думаю вне Москвы соответствующие пункты аналогично через региональные центры госуслуг/сайты/ведомства делаются.
1. Свидетельство о рождении – получить в роддоме.
2. Добавить карточку ребёнка каждому родителю на Госуслугах (не обязательно/автоматически)
– Идентификационные номера присваиваются автоматически
* СНИЛС – приходит в email;
* ИНН – отображается в карточке госуслуг.
– Маткапитал приходит автоматически.
– Формальный номер полиса ОМС присваивается автоматически (пока не работает, см. п.6).
Прим. На Госуслугах, Мосуслугах и ФНС можно сделать ребёнку отдельный личный кабинет. Делать этого не следует.
3. Штамп о гражданстве на свидетельство (оформление наличие гражданства по рождению) – лично через любой МФЦ (взять свой паспорт и свидетельство ребёнка).
4. Добавить ребёнка в учётку каждого родителя на Мосуслугах.
5. Прописать ребёнка через Госуслуги.
6. Выбрать страховую компанию ОМС через Госуслуги.
7. Прикрепить ребёнка к поликлинике через Мосуслуги.
8. Запрос детской кухни (при желании – 12 литров молока и 4 литра сока в месяц для мамы или, альтернативно, смесь для ребёнка)
8.1. Подать заявление на получение питания через Мосуслуги
8.2. Записаться к педиатру через Госуслуги. Ребёнка можно не брать, попросить нажать кнопку для молочной кухни. Заодно откроют направления на специалистов по достижению 1 мес.
8.3. Подать заявление на получение QR-кода для пункта выдачи через Мосуслуги.
9. Получить доступ к мед. карте ребёнка через Мосуслуги. Карта станет доступна через lk.emias.mos.ru.
10. Получить три пособия ~20к каждое (не считая помощи для малоимущих и совсем копеечных)
– "Компенсация взамен получения подарочного комплекта для новорожденных" – для Москвы (если отказались от "Собянинской коробки" в роддоме)
– "Единовременная компенсация при рождении (усыновлении) ребёнка" – для Москвы
– "Единовременное пособие при рождении ребёнка" – для РФ (если работаете по ТК – через работодателя)
Одиннадцать вопросов ИИ (для изучения математики и всего прочего)
Меня часто спрашивают...
Говорят, в эпоху модерна важно было наизусть знать основные факты, в эпоху постмодерна – где их найти. А в эпоху больших лингвистических моделей – как наиболее эффективно извлекать информацию по ходу диалогов на естественном языке.
В связи с этим решил описать свою "познавательную стратегию", направленную на ускорение обучения с применением LLM-ок. Применяю в основном в изучении математики, примеры соответствующие.
Общий план знакомства с новой концепцией такой:
1. Основные определения и алгоритмы
2. Связь с другими предметными областями через общие математические объекты
3. Допущения, нюансы, пресуппозиции
4. Перепроверка
Вопросы, которые задаю LLM-ке на каждом шаге соответственно, приведены далее. Стоит иметь в виду, что по-русски все современные LLM дают ответы значительно более низкого качества, перевод дан для удобства.
Основные определения и алгоритмы
1. Что такое X / What is X?
Пример: что такое сигмоида?
Вариации:
– Я всё ещё не понимаю X / I still don't understand X.
– О чем здесь речь / What's described here?
2. Напиши формулу для X / Write formula for X.
Пример: напиши формулу сигмоиды.
И наоборот:
– Объясни по-русски / Explain in plain English.
3. Как X делается по шагам / How X is performed, step-by-step?
Пример: как делается градиентный спуск, по шагам?
Связь с другими областями
4. Как связаны X и Y / How X implies Y?
Пример: как связаны MLE и лосс-функция логистической регрессии?
5. Объясни X, не упоминая Y / Explain X without referring to Y.
Пример: объясни логистическую регрессию, не упоминая GLM.
6. Объясни X с точки зрения Y / Explain X from the perspective of Y.
Пример: объясни MLE с точки зрения статистики.
7. X это то же, что Y / Is X the same as Y?
Пример: эквивариантность (equivariance) это то же, что естественное преобразование (natural transformation)?
(Прим.: один из вопросов, показывающих кардинальное превосходство LLM-ок над поисковыми системами в данной области. Выдачу гугла надо фильтровать и разбирать, LLM-ка сразу даёт резюме.)
Допущения, нюансы, пресуппозиции
8. Почему должно быть X / Why must be X?
Пример: почему в логистической регрессии log-odds должны линейно зависеть от признаков?
9. Что обычно упускают, рассказывая об X / What is usually omitted, when they speak of X?
Пример: что обычно упускают, рассказывая о логистической регрессии?
10. Какие базовые предпосылки X / What are basic assumptions of X?
Пример: какие базовые предпосылки логистической регрессии?
Перепроверка
11. Является ли этот конспект/решение корректным / Is this cheatsheet/solution correct?
Говорят, в эпоху модерна важно было наизусть знать основные факты, в эпоху постмодерна – где их найти. А в эпоху больших лингвистических моделей – как наиболее эффективно извлекать информацию по ходу диалогов на естественном языке.
В связи с этим решил описать свою "познавательную стратегию", направленную на ускорение обучения с применением LLM-ок. Применяю в основном в изучении математики, примеры соответствующие.
Общий план знакомства с новой концепцией такой:
1. Основные определения и алгоритмы
2. Связь с другими предметными областями через общие математические объекты
3. Допущения, нюансы, пресуппозиции
4. Перепроверка
Вопросы, которые задаю LLM-ке на каждом шаге соответственно, приведены далее. Стоит иметь в виду, что по-русски все современные LLM дают ответы значительно более низкого качества, перевод дан для удобства.
Основные определения и алгоритмы
1. Что такое X / What is X?
Пример: что такое сигмоида?
Вариации:
– Я всё ещё не понимаю X / I still don't understand X.
– О чем здесь речь / What's described here?
2. Напиши формулу для X / Write formula for X.
Пример: напиши формулу сигмоиды.
И наоборот:
– Объясни по-русски / Explain in plain English.
3. Как X делается по шагам / How X is performed, step-by-step?
Пример: как делается градиентный спуск, по шагам?
Связь с другими областями
4. Как связаны X и Y / How X implies Y?
Пример: как связаны MLE и лосс-функция логистической регрессии?
5. Объясни X, не упоминая Y / Explain X without referring to Y.
Пример: объясни логистическую регрессию, не упоминая GLM.
6. Объясни X с точки зрения Y / Explain X from the perspective of Y.
Пример: объясни MLE с точки зрения статистики.
7. X это то же, что Y / Is X the same as Y?
Пример: эквивариантность (equivariance) это то же, что естественное преобразование (natural transformation)?
(Прим.: один из вопросов, показывающих кардинальное превосходство LLM-ок над поисковыми системами в данной области. Выдачу гугла надо фильтровать и разбирать, LLM-ка сразу даёт резюме.)
Допущения, нюансы, пресуппозиции
8. Почему должно быть X / Why must be X?
Пример: почему в логистической регрессии log-odds должны линейно зависеть от признаков?
9. Что обычно упускают, рассказывая об X / What is usually omitted, when they speak of X?
Пример: что обычно упускают, рассказывая о логистической регрессии?
10. Какие базовые предпосылки X / What are basic assumptions of X?
Пример: какие базовые предпосылки логистической регрессии?
Перепроверка
11. Является ли этот конспект/решение корректным / Is this cheatsheet/solution correct?
Forwarded from Гиперкаталог
Сегодня в 20:30 традиционный пятничный стрим. Будем допрашивать автора блога metaprogramming про групповую динамику, обучение гопатычей и экономику.
YouTube
HYPERTV: стрим номер 15. Разведдопрос: метапрограминг.
Сегодня цепляемся и допытываем автора канала https://t.iss.one/metaprogramming на разные темы: от, собственно, программирования до психологии. Гостя предупредили, что хотим поговорить про последние байки о ИИ, которые газлайтят пользователей и сводят их с ума…