Формализация как присвоение типов на стеке уровней абстракции
Прирост человеческого знания в ходе эволюции случился по линии осознанной формализации: работы с алгоритмами рассуждений, ведущими к строгим результатам. Строгие — это которые не размываются в ходе длинных цепочек рассуждений. Если результаты носят не строгий/цифровой, а статистический характер, то в длинных цепочках рассуждений ошибка будет накапливаться. Но вот последовательности из строгих рассуждений ты можешь пройти десять тысяч раз по десять тысяч шагов рассуждений каждый проход, и если данные у тебя на входе были одни и те же, то ты получишь десять тысяч раз одинаковый результат. И знание тем самым сможет надёжно накапливаться, не размываться при передачах и хранении.
В онтологической инженерии/(мета)моделировании данных говорят о том, что создаётся «классическое онтологическое описание»/«семантическая сеть»/«semantic network»/«knowledge graph»[1], выраженные в языке логики, для изложения которой был в конечном итоге выбран язык математической логики, то есть язык математики. Строгость обеспечивается математической записью: записывают хорошо изученные объекты и их отношения: множества как классы, экземпляры как элементы множеств, операторы как логические операции. А используется это всё как онтология/мегамодель, то есть набор типов объектов внимания и отношений между ними (в том числе описываемых формулами, которые сами сложные объекты, но в любом случае — используется математический язык составления описаний каких-то физических и ментальных объектов и отношений между ними, или операций создания этих объектов в случае конструктивных описаний, и для этих описаний используется набор математических/ментальных объектов, поведение которых хорошо изучено — тех же множеств, различных видов бесконечностей и т.д.).
Есть несколько подходов к построению knowledge graph/онтологии, они все основываются на многоуровневой типологизации/объективации (объективация: каким образом мы выделяем объекты из фона) M0-M4 примерно по той линии, по которой мы тут это и обсуждаем, хотя и с какими-то вариантами:
- ad hoc**/интуитивно****, онтики**. В произвольных проектах, где потребовалась хоть какая-то формализация: берём объекты внимания as is, делая вид, что это «просто объекты, никаких у них типов нет» (так не бывает, тем не менее). На выходе — онтика, просто перечисление самих объектов и отношений между ними, как это представляется человеку интуитивно, то есть как воспринимается его нейронной сеткой, работающей «без логики», «как у животных» — быстрое мышление S1 по Канеману. Нейронная сетка умеет и разговаривать, безо всякой логики, просто продуцирует какие-то наиболее вероятные высказывания: «Вот это стол — на нём едят, а это стул — на нём сидят».
- как формализуют базы данных в промышленности**,** модели данных**/datamodels** в проектировании баз данных**, справочные данные****/referencedata** в проектировании информационных систем предприятий: берут строгую математическую теорию как foundational ontology, чаще всего это логика первого порядка в каком-то её изводе (их ведь тоже много разных). Эту онтологию (набор математических объектов с хорошо изученными свойствами) используют дальше как язык, на котором описывают объекты и отношения upper ontology — какие-то наиболее общие типы объектов, скажем «сущность»/entity, у которой подтипы «абстрактные объекты», «физические объекты», и так примерно 200 понятий из распространённых философских теорий (например, в онтологии ISO 15926-2 всего 201 такое понятие как upper ontology[2]). А дальше всем объектам онтики из предыдущего пункта (ad hoc/интуитивного описания предметной области/domain) присваиваем эти типы в надежде, что результат будет непротиворечив и более понятен. Мы уже многое знаем про мир, когда выделяем объекты, и вот это присваивание типа, который мы уже знаем — это трассировка/прокидывание этого «общего знания» ко всё более конкретным фрагментам знания. Общее знание — это математика, поведение математических объектов. Присвоение типов какой-то middle онтологии (онтологии широких предметных областей — химии, биологии, юриспруденции и т.д.) как раз уточняет знание об этих предметных областях: даёт возможность строить общие рассуждения. Если известно, что сепулька описывается как математическое множество, то к ней будут применимы одни операции, а если это кортеж, то другие, чем бы эта «сепулька» потом не оказалась. Это основной подход, который используется в инженерии при федерировании данных[3]. И тут возможны варианты: с микротеориями (для учёта противоречивости как в CYC[4] — внутри микротеорий противоречий нет, а между ними могут быть, например, высказывания «Граф Дракула — вампир», «Вампиров не существует» не могут быть логически совместимыми без аппарата микротеорий) по части строения онтологии или без, на базе логики первого порядка или всё-таки порядок логики в некоторых случаях можно пробовать увеличить без потери реальной возможности что-то вывести на ограниченных ресурсах, или даже с потерей (математическая вычислимость оказывается не самым важным фактором в онтологиях), да и сами объекты upper ontology можно очень по-разному выбирать. В любом случае, вся эта формализация «графов знаний» базируется на математическом основании.
- классический подход естественн****ых наук (science), исчисление/calculus. Foundational ontology берётся из «оснований математики» (унивалентные основания математики, логицизм, конструктивизм как раз про это), а upper ontology — это математические объекты, которые затем используются в исчислениях[5]. В самом начале исчисления («как посчитать») трактовались как теории изменений так же, как геометрия была теориями о формах, а алгебра теорией об арифметических операциях. Но затем исчислением начали называть всё подряд, что изучалось методами математики — пропозиционное исчисление/логика утверждений[6], вариационное исчисление, лямбда-исчисление и т.д. По сути исчисление — это более-менее обособленная микротеория на материале математики. Множество, многообразие, поле, интеграл, оператор, уравнение — это типы объектов из оснований математики как уровня, близкого к foundational ontology/мета-мета-мета-модели, upper ontology/мета-мета-модели (помним, что выделение этих уровней абстракции/обобщения более-менее произвольно, в разных школах мысли они могут выделяться по-разному, и эти выделения могут ещё и изменяться во времени, улучшения в понимании мира идут довольно быстро, это раньше надо было ждать сотню лет, чтобы в математике что-то сильно поменялось, сейчас ждать вообще не приходится). После того, как мы построили исчисление, для конкретной предметной области производится моделирование на основе исчисления. Скажем, классическая механика моделируется интегральным и дифференциальным исчислением, компьютерные программы в функциональном подходе — лямбда-исчислением, и т.д. Объектам и отношениям в предметном мире будут соответствовать какие-то математические объекты исчисления, а отношения между ними будут выводиться по математическим формулам, поведение объектов в мире при удачно подобранных формулах будет примерно соответствовать поведению математических объектов в ментальном/математическом/идеальном мире.
- Современный подход естественн****ых наук (новый «треугольник»)****: дробное исчисление/fractionalcalculus[7], группа перенормировки/renormalizationgroup и машинное обучение/machinelearning**.** Все эти дисциплины связаны в какой-то мере с системным мышлением, предполагающим уровни рассмотрения проблемы. Дробное исчисление — это обобщение классического интегрирования и дифференцирования на произвольные (например, реальные или даже комплексные) порядки/степени интегрирования и дифференцирования. При этом порядки/степени понимаются как итерационное применение какого-то линейного оператора дифференцирования к функции. Это исчисление близко связано с работами по фрактальным описаниям. Математические описания с изменениями масштаба как в статистической классической/предквантовой физике и квантовой физике идут на базе субъективной/байесовской и некоммутативной/квантовой теории вероятностей, а также ренормализационной группы/группы перенормировки/renormalization group.[8]. А ещё машинное обучение, которое прежде всего включает в себя обучение представлениям/representation learning[9] и глубокое обучение/deep learning[10] — классы познающих/обучающихся алгоритмов, которые используются при создании программ искусственного интеллекта. В целом речь идёт о чём-то, напоминающем системный подход в физике: используется теория вероятностей, чтобы с какой-то уверенностью отмоделировать события на каком-то масштабе деления физического мира на части, а все невязки затем отмоделировать переходом к моделированию на уровень ниже, и так дальше по уровням (ибо всегда будет какая-то невязка моделирования, но она будет меньше и меньше по мере увеличения числа уровней моделирования). Собственно, речь идёт о математических многоуровневых моделях, как-то отражающих многоуровневость физического мира.
Мы тут не трогаем вопрос о том, что в онтологиях/графах знаний/мегамоделях есть по факту и модели абстрактных/математических объектов, и модели физических объектов — и сразу захватывается букет вопросов о том, как они связаны (мы уже упоминали, что связаны они через информатику/computer science, с этими онтологиями/мегамоделями работает какой-то физически реализованный агент-вычислитель).
В любом случае: для описания объектов и отношений в физическом мире, равно как объектов и отношений в ментальном мире (математических объектов) используются объекты математического мира. Математические описания онтологичны, а «строгость» (работа в правой части спектра формальности мышления) всего-навсего указывает на хорошо изученное поведение математических объектов, используемых для моделирования. Адекватность описаний этими объектами других объектов нужно ещё как-то доказывать, способы доказательств**—** в информатике (которую понимаем как семантику, логику, алгоритмик****у в их тесной взаимосвязи).
При выборе уровня формальности обязательно учитываем трудоёмкость формализации и последующих формальных вычислений (она, конечно, зависит от доступности вычислителя — если у вас есть знакомый живой математик, который готов потратить время на формальные выкладки, или даже математик-AI, то трудоёмкость их вычислений для вас будет ничтожна, но ресурс их всё одно придётся оценить и за него заплатить). Это важно на многих уровнях формальности:
- формальное идеально строгое рассуждение: точный алгоритм, который даст ответ, если плюнуть на ресурсные ограничения (типа «теорема, что нейронная сеть с учётом неограниченной ширины и ограниченной глубиной является универсальным аппроксиматором»[11]). Это очень важный математический результат, только по большому счёту, он для не-математиков неинтересен и бесполезен: количество вычислений для аппроксимации с какой-то даже не очень большой точностью даже очень простых функций настолько велико, что никакой компьютер на Земле за хоть как-то адекватное время с этим не справится. А если нужно именно строить рассуждение, а не просто давать численную оценку какой-то простой функции (скажем, речь идёт об экспертной системе с парой сотен логических правил, причём каждое из них дано в нечёткой логике/fuzzy logic[12]), то формальное идеальное решение «как будет в принципе, строго и однозначно» перестаёт иметь смысл: формулу-то можно иметь, теорему можно доказать, но когда нужно получить конкретное рассуждение для конкретной ситуации с конкретными входными данными, ничего не получится: не хватит вычислительных ресурсов всей Вселенной и тысяч лет вычислений.
- формальное реальное рассуждение: точный алгоритм/формула, которая даст точный ответ (скажем, программа с доказанной правильностью, то есть которая гарантированно не зайдёт в какую-то точку, где она вдруг остановится) в приемлемое время при данной физике вычислений и данном вычислительном ресурсе. Тут проблема в no free lunch theorem[13]: для каждого класса задач нужно будет искать способ/алгоритм рассуждения для той или иной физики рассуждения/вычисления (предварительно доказав, что операции в этой физике вычисления и впрямь соответствуют операциям с ментальными/математическими объектами), иначе не уложиться в ограничение. Но зато ответу можно доверять, он точный/строгий/формальный и при повторении рассуждения будет тем же самым. По большому счёту, ровно вот это называется «точными науками» (математика, физика, химия). По Канеману это соответствует медленному мышлению «по правилам», S2 (но надо учитывать, что для разной физической природы компьютеров время вычисления будет разным, плюс результаты будут сильно зависеть от алгоритма, то есть «правил рассуждения»).
- неформальное рассуждение**😗* неточный алгоритм, который даст максимально точный ответ за заранее заданное время. Или хотя бы постановку задачи для формального решения! Не зря ведь говорят, что «постановка задачи — это половина дела». Формальное же реальное решение потом можно будет получить, обратившись к специализированному вычислителю правильной природы. По факту этот подход эквивалентен тому, как изучают математику с помощью программы Mathematica: программа сможет вывести и подсчитать что угодно, но вы должны сообразить, что нужно сказать программе, чтобы получить корректный результат. Этот подход в машинном обучении сейчас известен как Toolformer[14] или TaskMatrix[15]. По большому счёту этот подход не обсуждается в математике, ибо это предмет алгоритмики. Математическую интуицию (а если речь идёт о расчётах по физике или инженерии, то физическую и инженерную интуицию) вполне можно получить по этому пути, необязательно много возиться с формулами, эту обезьянью работу «вывода по правилам» сделает компьютер. А вот выбрать из тысяч и тысяч потенциально важных объектов внимания объекты внимания правильных типов, чтобы решить задачу в Mathematica или GPT-4 — вот это да, это важно! А дальше — вопрос алгоритмики, какой алгоритм выбрать, чтобы получить ответ заданной точности за отведённое на работу алгоритма время и отведённые ресурсы (например, ресурсы вычислителя смартфона или вычислителя уровня большого датацентра с парой суперкомпьютеров).
Итак, тяжёлую работу формального/строгого/точного рассуждения/вывода/inference будут делать компьютеры, а от людей потребуется только знание математической, физической и так далее (дисциплин интеллект-стека, а затем инженерной, менеджерской, предпринимательской) онтологии с типами, соответствующими объектам внимания. Для наших целей усиления интеллекта достаточно соответствующей предметной интуиции для приблизительных/интуитивных рассуждений с этими объектами внимания, чтобы высказывать догадки. А проверять эти догадки сможет и компьютер, никаких тут вопросов.
Математики так и делают: они доказывают свои теоремы неформально, а достижения теории доказательств только-только начинают (редко!) использовать, причём всё больше и больше в этом полагаются на компьютерные средства[16]. В философской энциклопедии так и пишут[17]: proof theory has so far not become a practical tool for the working mathematician; the applications in mathematics have been rather isolated cases. Recent work on formalizing mathematical proofs with computerized systems, called proof editors, may gradually change this picture. Чуть дальше мы покажем, что с этой проблемой пытаются сработать в рамках работ по унивалентным основаниям математики, где можно пробовать оставить и неформальный стиль доказательств, а в случае особой нужды использовать формальное компьютерное доказательство. Но чтобы это стало надёжно работать, требуется заменить основания математики!
Дальше (как всегда, когда начинаем использовать компьютеры) можно вспомнить, что математическая нотация из терминов, представленных одной буквой и операций, представленных одним знаком, плюс хитрая пространственная (не текстовая, не строчная) вёрстка с дробями и индексами — она нужна как стенография, быстрый и компактный ввод/вывод как раз для долгого формульного вывода. По-другому никак, если работать с карандашом и бумагой. И все привыкли. Как к нотам на пяти линейках с наложенной на них ритмикой и более чем странными «альтерациями», тоже не самое рациональное антикварное нотационное решение. Дальше имеем музыкальные редакторы и математические редакторы, где ввод перьевой с распознаванием картинок или прямо игрой на клавиатуре, а для математики будет разметка в хитромудром редакторе LaTeX. Но современным математикам надо работать с системами типа Wolfram Alpha и Wolfram Mathematica, и там, конечно, никакой особой вёрстки на вводе — используется запись текстом на компьютерном языке. За этим, конечно, будущее.
Вот скандальность и удобство может быть в том, что для разговора о математике использовать вообще тексты вместо привычных формул — возможно, тексты с аннотированием типов, чтобы было проще разбираться с материалом. Привычные формулы оставим прикладному курсу «раздела математики», если приходится его изучать. В курсе математического мышления, который должен быть в интеллект-стеке берём фундаментальное содержание, базовые понятия и их отношения. Считать ничего не будем (это нужно только в прикладных курсах), будем только рассуждать. И необязательно рассуждать точно/строго/формально, но зато рассуждать важно с правильно выбранными для этих рассуждений объектами. Не случайно выбранными, а правильными, соответствующими мета-мета-модели мира, «модели из учебника трансдисциплины» (а в случае оснований математики может быть ещё и мета-мета-мета-модель: язык, на котором рассказывается о языке математики, ещё один или даже пара уровней в многоуровневом построении объектов внимания. «Построение» — это отсылка к конструктивной математике, «определить объект — это задать процедуру/программу его построения из более мелких объектов»).
https://en.wikipedia.org/wiki/Universal_approximation_theorem ↩︎
https://en.wikipedia.org/wiki/Proof_theory (и там смотрите Formal and informal proof) ↩︎
https://plato.stanford.edu/entries/proof-theory-development/ ↩︎