(←) предыдущая запись ; следующая запись (→)
М.С. дополняет меня: оказывается, французский налоговый кодекс написан на специальном языке программирования — https://github.com/MLanguage/mlang
И напоминает, что существуют всякие системы проверки логического вывода типа Coq. Вообще есть большая движуха на стыке математики и компьютерных наук, посвящённая формальной верификации программ, проверке доказательств итд.
И удивительным образом, есть движуха, стыкующая математическую логику и базы данных (дескрипционная логика активно используется в графовых БД)
upd:
А ещё М.С. разумно говорит, что для систем построения доказательств больше верит в агентные модели — те, которые тренируются решать некоторую задачу и сами корректируют свои ошибки на основе удачных и неудачных решений (например, всякие автопилоты, управление роботами и боты для компьютерных игр так обучают), чем в Large Language Model.
(5/5)