Управлять формальностью/строгостью: надо разбираться с псевдокодами

ailev — 02.01.2022 Вот тут предлагают gradual dependent types: https://deepai.org/publication/approximate-normalization-for-gradual-dependent-types. Я отвечаю на это (разговор был вот тут: https://t.me/typeslife/14799), что это всё попытки изобрести шкалу формальности/строгости, но вот эта попытка не выходит за рамки строгого обсуждения строгости, нестрогое и неформальное, а также полустрогое и полуформальное в этой попытке теряется. Мы же вроде как говорим, когда поминаем "градуальность" о палитре/шкале/спектре/степени формализации (погуглили: "степень формализации" -- это самый частый термин), синоним — уровень строгости. Но по факту там градуальности разных уровней строгости, а не градульность всей шкалы, начиная с уровня строгости разговорного естественного языка.

Формальность описаний/моделей/объяснений, формальность результата описывания/моделирования/исследований -- это про конструктивный объект, времени создания, design-time. А если брать функцию (вычисления по описаниям как данным, время run-time), то речь идёт о точности мышления/вычислений. Для достижения требуемой точности мышления берёшь из палитры/шкалы какой-то формализм/уровень строгости и получаешь для него точность мышления. И тут нужно ещё и заметить про неясности с терминологией: если говорить в терминах точности, то сразу отваливаются все инженеры и естественнонаучники: они не поймут ни слова. Но насчёт формализации их учили, что формализация — это для точности. А саму "точность" для обсуждения этой тематики "строгости" мало кто использует непосредственно.

Формализовывать нужно, но только самое важное -- и тогда уж не жалеть на это сил. Но огромный объём повседневного мышления делается в не слишком формальной форме. И это нужно поддерживать. Какие-то рассуждения на эту тему я приводил недавно в https://ailev.livejournal.com/1598826.html (и там подразделы "Интеллект-стек нужен при недостатке данных/жизненного опыта, а не только компенсации малой вычислительной мощности" и "Неудача формальных представлений интеллект-стека", и "Представление знаний интеллект-стека в не очень строгом/полуформальном/уровня псевдокода виде в человеческой голове", и "От строгости мы не отказываемся, но фронтир сейчас -- хорошие методы работы с нестрогими представлениями").

Нужно как-то подробней разбираться с псевдокодами, но текущие исследования языков тяготеют или к полному естественному языку и там разбираются с проблемами формальной семантики типа conceptual blending (https://markturner.org/blending.html), и прочими трудностями заведомой интуитивности и неформальности (см., например, тесты SuperGLUE https://super.gluebenchmark.com/, начинавшиеся с тестов Винограда, на которых спотыкались любые "правила понимания"), или к полностью формальному ("математика", ибо это не всегда даже математическая логика, стохастические алгоритмы тоже ведь формальны) описанию на искусственных языках с какой-то чёткой денотационной семантикой.

Псевдокод очевидно более формален, чем просто естественный язык, но по сравнению с кодом он не формальней естественного языка. Вот как с этим работать, зачем людям вообще псеводокоды (в работах по AI ни одна статья без них не обходится, алгоритмы почему-то на псеводокоде дают, а не каком-нибудь языке программирования или естественном языке), можно ли управлять "уровнем псевдокодности" для реализации тех целей, для которых существуют псевдокоды — вот это было бы интересным исследованием.

Ибо даже язык с градуальными типами — это ни разу не шаг к псевдокодам, то есть это в части представления знаний незначимые отклонения от строгой типизации, примерно как из Москвы дома на разных улицах Владивостока, неразличимо близко. Это во Владивостоке они на разных улицах!



Пока мы смотрели на SysMoLan как всяческие варианты eDSL, то всё было плохо и не получалось. Когда мы сказали, что надо сменить класс языка, сделать его "архитектурным языком", где намеренно relax требование к типизации, то всё у нас резко взлетело. Инструкции типа https://ailev.livejournal.com/1594529.html стали восприниматься как руководство к действию, и у нас немедленно студенты начали выполнять массово работы по моделированию/представлению знаний о важном в их предприятиях. У нас в видеоканале школы много докладов на эти темы от выпускников. Вот только последний из них: https://www.youtube.com/watch?v=0_WycjiSbJg

И это после того, как мы серьёзно рассмотрели рассуждения авторов ArchiMate и аналогичные рассуждения John Sowa о важности "недоопределённости типов" (underspecification) для моделирования. Онтологи говорят, что общей для всех случаев жизни онтологии не бывает, "об основаниях не договорились". Эпистемологи тоже говорят, что лучшие наши объяснения непрерывно меняют набор объектов, на которые они режут реальность (хороший тут пример у Дойча: сначала сил в механике не было, потом появилось понятие силы в ньютоновской механике, потом в релятивистской механике понятие силы опять изчезло. О понятии "тепла" и "работы" физики договариваются до сих пор, см., например работу по термодинамике в рамках строительной теории, https://arxiv.org/abs/1608.02625).

То есть утопии типа "общего формального языка описания всего" — это утопии. Поэтому описываем пока всё вообще на естественном языке, который underspecified, и это хорошо (подробно обычно об этом пишет John Sowa). А более важное, что нужно доставать вниманием описываем на уровне псевдокода/псевдострого, а самое-самое важное описываем формально/строго.

Ещё много про неформальность вот в этом тексте: "Кругозорные витамины для жизненного опыта (common sense knowledge graphs для large language models)", https://ailev.livejournal.com/1551283.html.

John Sowa всегда выступал одновременно и за строгую логику как представление онтологий, и за underspecification, поэтому его трудно понимать было. Но мы потихоньку разобрались: важное определяется градуально, а не одним махом. Сначала недоспецифицируется, потом самое важное из этого доспецифицируется, потом из этого самое-самое важное формализуется окончательно.

Работы Ванчурина-Вольфа-Кацнельсона-Кунина и прочее по этой линии (вот тут наши планы исследований в этом направлении: https://ailev.livejournal.com/1601601.html) примерно про то же сейчас. В них показывается, в каком месте в эволюции появляется "цифровость", формальность. Эта "строгость представления" неизбежна, пример этого -- появление RNA и далее DNA. Ибо цифра нужна не для собственно рассуждения, а для неизменного повторения без накопления ошибки, защиты от энтропиии (точной репликации) чего-то важного. И тут уж разделяется генотип "цифряной" и более аналоговый фенотип, и они меняются на разных масштабах времени в ходе эволюции. Вот когда мы работаем с ad hoc моделированием чего-то быстроменяющегося в понимании, нам нужны более "аналоговые" переменные, а когда с чем-то уже закосневшим, то железобетонный контроль типов. Текущие "языки" предлагают только один уровень типизации.

John Sowa приоритет при этом отдаёт естественному языку: он считает, что высказывания на нём можно просто уточнять и уточнять по потребности, и это главная фича естественного языка: снаружи он вроде как неформален, но в использовании можно сколько угодно поднимать уровень формальности. Я считаю, что встречное движение "охвата расширяющегося представления об объекте" идёт и со стороны любителей формальных описаний. Взять хотя бы акаузальное моделирование (вот я писал о тамошних подвижках в связи с цифровыми двойниками, https://ailev.livejournal.com/1549559.html, с тех пор вышел ещё JuliaSim, https://juliacomputing.com/products/juliasim/).

Особенность текущего момента, что нельзя считать, что люди работают с неформальными/нестрогими описаниями, а компьютеры и вычисления со строгими, а с серединой этого спектра, псевдострогими псевдокодами, описаниями "архитектурного уровня формальности" никто и ничто не работает. Нет, совсем нет, и речь идёт тут даже не о работе с нейросетями по пониманию естественного языка. Компьютеры сейчас и с псевдокодом работают. Те же архитектурные моделеры (они таки не совсем рисовалки) поддерживают полуформальное моделирование. При этом людям даётся ещё и инструкция, как поделить вычисления по моделированию (включая работу с типами) по мозгам и кремнию. Формализацию и сопутствующую ей логику люди придумали задолго до компьютеров. И нормально так сами строго вычисляли. Те же доказательства в математике и расчёты в инженерии и физике вполне без компьютеров проводили и сто лет назад тоже. Тезис Тьюринга-Дойча про универсальность машины Тьюринга как раз про то, что если уж вычисляешь, то разница между мозгом математика, машиной Тьюринга из кубиков Лего (есть такие!), компьютером на обычных транзисторах и квантовом компьютере только в достижимости результата по ограничениям в скорости и памяти, но никак не по различию в типах вычислимого. Теоретически всё это одинаково, проблема только в практичности (что для математика "вычислимо" на практике может оказаться "на текущей технике вычислимо за пару миллиардов лет", то есть "не вычислимо").

Вот что явно недообсуждено, так это мысль о многоуровневой объективации (задание объекта не в один присест, выделение объекта из фона не одним жестом), она не так тривиальна. И эта многоуровневость не сводится к тому, что мы просто говорим о нескольких уровнях онтологии (foundational, upper, middle, domain), ибо когда говорят о computational ontology, то подразумевают задание всех этих уровней на одном высоком уровне формальности. По Груберу это ж формализация спецификации предметной области! А тут мы говорим, что чем выше по онтологическим (классы классов) уровням, тем меньше требований к "строгому логическому выводу". И мы тут не про "восхождение от абстрактного к конкретному в несколько шагов" (это всё понятно), мы говорим про что-то вроде "нахождение типа/класса методом градиентного спуска от неформального/нестрогого к формальному/строгому.

И новация тут -- поворот от одномерного "онтологические уровни" с обсуждением подходящей foundation ontology для их выражения и в лучшем случае проблем микротеорий/онтик для решения возникающих неразрешимостей логического/строгого вывода к двумерному "онтологические уровни -- уровни строгости" пониманию. См., например, обсуждения августа 2019 года https://ailev.livejournal.com/1489546.html и сентября 2019 года https://ailev.livejournal.com/1486211.html и https://ailev.livejournal.com/1486407.html по итогам разговоров в чате "Типы в языках программирования, моделирования, представления знаний" и уже упомянутые мной материалы (https://ailev.livejournal.com/1598826.html) по уходу от SysMoLan как строгого языка (классического "языка программирования") и переходу к пониманию его как языка не слишком строгого (архитектурного) моделирования. А ведь в уже 2018 году мы говорили о спектре формальности/строгости, у меня про это подробненько рассказывалось в книжке "Визуальное мышление", вышедшей как раз летом 2018 года, https://ridero.ru/books/vizualnoe_myshlenie/. Но вот потребовалось три года, чтобы это всё довести до практики моделирования.

С псевдокодами и сложностью нужно продолжать разбираться. У нас ещё и язык-то толком не сформирован. Совсем недавно мы говорили о схемах и схемоидах, например. Убрали из речи, ибо кантовские "схемы" путались с "диаграммами" из квадратиков и стрелочек. Или те же вопросы "формальности" против "строгости". Или различие не очень строгих и "статистических" (про корреляции) или "стохастических" (то есть на базе оценок вероятности, но точных) рассуждений.

Нужно уходить от строгой оппозиции формального и неформального, строгого и нестрогого. Нужно научиться управлять строгостью, научиться удерживать свои рассуждения на заданном уровне формальности.

Оставить комментарий

Популярные посты:

• Ранее
• Архив