ИИ с Прологом или без?

[Majestio]

Felan, дружище, ты поднял важную тему!

Но прошу тебя дальше не обижаться, если я буду немного резок в своих суждениях

В последнем посте у тебя слишком много букв, которые не совсем по делу! Но ты реально поднял одну из важнейших тем - одновременная работа нейросетки с её обучением. Это сейчас реальная проблема. Если загуглить или занейросетить - то там будет порядка 7-10. Первая из который = "потеря памяти". Раскидаю на пальцах ...

1) Сегодня вы обсуждаете решение проблемы, где в промежуточных решениях не может быть значения от квадратного корня от минус единицы
2) Завтра нейросетка "осилила" математический аппарат комплексных исчислений

Следствие: весь возможный платный месячный контекст обсуждений просто у гауно!!! Ибо нужно делать выводы по вновь обновившимся коэффициентам. Но есть и другие важные, навскидку и без детализации, факты. Cорян, и это от ИИ, мне тупо лениво напрягаться в печатанье букф:

• Catastrophic Forgetting (катастрофическое забывание)
• Дилемма стабильности и пластичности
• Вычислительная стоимость и задержки
• Отсутствие или задержка обратной связи
• Дрейф данных (Concept / Data Drift)
• Нестабильность поведения
• Проблемы масштаба
• Безопасность и контроль

[Felan]

Цитата Majestio @ 06.08.26, 14:06

Но прошу тебя дальше не обижаться, если я буду немного резок в своих суждениях

Я тя по ip вычислю!

Цитата Majestio @ 06.08.26, 14:06

В последнем посте у тебя слишком много букв, которые не совсем по делу!

Тут сложно сказать. Я думал тема началась с технической подоплеки. Как заставить НС объяснить свое поведение хотя бы на прологе. Но не важно как.
Но проблема тут гораздо глубже. И совмещение обучения и работы (как у червяков ) это только край проблемы.

Но вот я и растекся по древу... Пытаясь популярно с налетом технических ньюансов объяснить положение дел. Ну или мое понимание положения дел. Ну на какое-то время назад.

Цитата Majestio @ 06.08.26, 14:06

1) Сегодня вы обсуждаете решение проблемы, где в промежуточных решениях не может быть значения от квадратного корня от минус единицы
2) Завтра нейросетка "осилила" математический аппарат комплексных исчислений

Менно об этом я и говорю. Нет никакого "осилила" есть "аппроксимировала". А если точнее, то "аппроксимировали нейронной сетью".

Цитата Majestio @ 06.08.26, 14:06

Следствие: весь возможный платный месячный контекст обсуждений просто у гауно!!!

Ну это проблемы бизнеса, тут у меня лапки

Цитата Majestio @ 06.08.26, 14:06

Cорян, и это от ИИ, мне тупо лениво напрягаться в печатанье букф:

Честно говоря, хотелось бы общаться с человеком. С тостером я могу и сам дома поговорить.

Цитата Majestio @ 06.08.26, 14:06

Catastrophic Forgetting (катастрофическое забывание)
Дилемма стабильности и пластичности
Вычислительная стоимость и задержки
Отсутствие или задержка обратной связи
Дрейф данных (Concept / Data Drift)
Нестабильность поведения
Проблемы масштаба
Безопасность и контроль

Это все кроме первого вообще про другое.

[Majestio]

Цитата Felan @ 06.08.26, 14:27

Честно говоря, хотелось бы общаться с человеком. С тостером я могу и сам дома поговорить.

Отпуск (первый за 15 лет, дача, водовка) ... щя просто не вижу вариантов Прикинь, я ещо на рыбалку не ездил лет наверное столько =) А вот нащот тостера - ты неправ, ему обидно! Он мне сам сказал =)))

Добавлено 06.08.26, 15:04

Цитата Felan @ 06.08.26, 14:27

Я тя по ip вычислю!

А я ... а я ... я в ОБСЕ заяву напишу, или ваапще в Федерацию Африканских Сил Специальных Операций!

[Qraizer]

Цитата Felan @ 06.08.26, 13:35

А язык программирования это как ни крути поток данных и поток исполнения.

В Прологе нет потоков данных и исполнения.

Цитата Felan @ 06.08.26, 13:35

Ну типа после слоава "пошел" обычно идет "домой"

Ну это смотря в каком языке. В русском, вот, не уверен.
В целом у тебя всё правильно. Только ты упускаешь мои аргументы о верифицируемости. Цифры сиречь веса ты не верифицируешь без алгоритмов их потребляющих. А код и есть алгоритм. Даже если он декларативный, это всё равно алгоритм, т.б. поведение.

Добавлено 07.08.26, 12:11

Цитата Majestio @ 06.08.26, 14:59

... или ваапще в Федерацию Африканских Сил Специальных Операций!

В моё время говорили "...шилом бритый кампучиец".

[Felan]

Цитата Qraizer @ 07.08.26, 12:08

В Прологе нет потоков данных и исполнения.

Эээ всмысле!? Они в любом языке есть. Это логические вещи. Данные как-то изменяются последовательно, а команды как-то выполняются последовательно... Это они и есть.

Цитата Qraizer @ 07.08.26, 12:08

Ну это смотря в каком языке. В русском, вот, не уверен.

Ну шутка же, Ё-мое.

Цитата Qraizer @ 07.08.26, 12:08

В целом у тебя всё правильно. Только ты упускаешь мои аргументы о верифицируемости. Цифры сиречь веса ты не верифицируешь без алгоритмов их потребляющих. А код и есть алгоритм. Даже если он декларативный, это всё равно алгоритм, т.б. поведение.

Я не упускаю. Я про это и говорил, когда рапрягался про

Цитата Felan @ 06.08.26, 13:35

Веса это просто набор чисел. Они не содержат в себе взаимосвязей. Какое число с каким связано? Для этого надо знать структуру нейронки. А это значит, что надо знать конкретный многочлен. Это для линейной. А если нейронка не линейная (есть связи между непоследовательными слоями, или не дай бог в разных направлениях) то все, приплыли. Без знания архитектыры сети веса можно выкидывать. А язык программирования это как ни крути поток данных и поток исполнения. Да он предствит и стуктуру тоже... но это будет уже в разы сложнее и анализировать 111 Гб это не кнопочку в другой цвет покрасить. Во вторых, проанализировать все это не значит построить карты или восстанивать архитектуру. Это значит конкретно объяснить, как она сделал вывод что на картинке кошка, а не харек, например. А подобные вещи люди то себе не могут объяснить внятно.

думаю мы просто все это немного поразному "понимаем". Но думаю тут можно прийти к общему знаменателю.

Как раз проблема в том, что бы восстановить алгоритм. А это не техническая проблему. Ну ок, будет в алгритме, что-то вроде если числа по индексам между 100Гб и 101Гб стоят такие-то числа то это кошка а не харек. Ну ок. А это сибирская или сфинкс? А, ну тут надо смотреть на 3й Гб и вот такие числа.

И тут плавно приходим к Солярису.

(Если че про гигабайты это я ссылаюсь на твое утверждение о 111Гб)

[Qraizer]

Цитата Felan @ 07.08.26, 13:43

Данные как-то изменяются последовательно, а команды как-то выполняются последовательно...

В Прологе нет. Он декларативный, а не императивный. В Прологе есть правила вывода результатов из исходных данных, но как это делается, не формализуется. Результат валиден, если он не противоречит описанным правилам, а как он получен, никого не волнует. Идеально для мат.методов верификации.

Добавлено 07.08.26, 14:53

Цитата Felan @ 07.08.26, 13:43

Как раз проблема в том, что бы восстановить алгоритм.

Не надо его восстанавливать. Импликации пофику, как получены A и B, она просто говорит, что A → B = F, только при T→F.

Добавлено 07.08.26, 14:57
P.S. По сути в Прологе ты описываешь аксиоматику своей формальной системы, и на этом всё. Все промежуточные теоремы, полагаясь на которые решаются конкретные задачи, внутри Пролог-машины, и она сама их сгенерит, смотря какие понадобились и в каком количестве. Конечно, бывает так, что аксиоматика недостаточна. В конце концов Гёделя никто не отменял. Но формальную систему всегда можно расширить дополнительными аксиомами.

[Felan]

Цитата Qraizer @ 07.08.26, 14:51

В Прологе нет. Он декларативный, а не императивный. В Прологе есть правила вывода результатов из исходных данных, но как это делается, не формализуется. Результат валиден, если он не противоречит описанным правилам, а как он получен, никого не волнует.

Ну, к тому что я пытаюсь сказать это не имеет отношения. Я про логику. И тут как бы вопрос глубины австракции. Мне например не важно как работает ДВС и почему машина доезжает от моего дома до магаза. Жена декларирует "завтра поеду в магаз". И я завтра вижу вксняшку. Но это никак не отменяет что это происходит не магическим образом, а там которетные принципы и действия.

Я про пролог очень мало знаю. Но похоже он напоминает DSL. Верификация это прекрасно. Я думаю что я понимаю о чем ты говоришь. Грубо говоря на картинке мне пофиг как НС определила, что это кошка. Я вижу что это кошка и все. Я проверил, что НС все правильно порешала.

Но это никак не объясняет КАК она это сделала.

Цитата Qraizer @ 07.08.26, 14:51

Не надо его восстанавливать. Импликации пофику, как получены A и B, она просто говорит, что A → B = F, только при T→F.

Это в теории. На практике придется реализовать некую физическую сущьность которая дожна работать в реальном мире и как-то переводит A в B и проверять T.

Я понимаю, что накидали примеров (или нет если без учителя) и на вяходе получили результаты которые выглядят правильно. Но то, как это происходит определить пока невозможно.

Формальная логика как раз позволяет восстановить алгоритм. Просто там посылки надо определять.

Цитата Qraizer @ 07.08.26, 14:51

P.S. По сути в Прологе ты описываешь аксиоматику своей формальной системы, и на этом всё. Все промежуточные теоремы, полагаясь на которые решаются конкретные задачи, внутри Пролог-машины, и она сама их сгенерит, смотря какие понадобились и в каком количестве. Конечно, бывает так, что аксиоматика недостаточна. В конце концов Гёделя никто не отменял. Но формальную систему всегда можно расширить дополнительными аксиомами.

Да я не против. Только примитивы пролога все равно как-то определены. Если это DSL то прекрасно, но как именно внутри пролог-машины определены аксиомы? Как определить новую? Хорош, пусть это не begin if a print c end. Как это работает?

[Majestio]

Цитата Felan @ 07.08.26, 17:18

Я про пролог очень мало знаю. Но похоже он напоминает DSL.

Если коротко: базис языка Пролог составляют факты, правила и запросы, основанные на исчислении предикатов и дизъюнктах Хорна. Программа работает как база знаний, где компьютер ищет логические ответы с помощью поиска с возвратом.

В этом плане я очень даже согласен с Qraizer'ом в плане лёгкости программной верификации сгенерированного ИИ программного кода. Ибо синтаксис Пролога очень простой, разбор будет с минимальными затратами. Даже очень больших "портянок" кода. А вот уже сам процесс верификации - на совести верифицирующего.

Как тут уже не раз упоминалось ... системы на базе нейросетей базируются на многослойной структуре вероятностных коэффициентов, а системы на базе Пролога - на массивах утверждений и фактов. Согласись - второй вариант более просто верифицируем?! Т.е. для каждого предиката можно выделить набор фактов и правила, и их анализировать отдельно. Другой (кстати важный) вопрос - именования ... Скорее всего это будет что-то вроде обфускацируемого кода. Наверное - это одна из главных проблем для человеческого восприятия. Математике и алгоритмам - пофик, а для энд юзера зто будет не проще brainfick'а.

И тем не менее ... В начале топика я намеренно обозначил Пролог не как замену нейросетей, а как дополнение. В моём понимании Пролог можно использовать как "расширения" для нейросетей со 100%-й достоверностью. Понимаю, что это не совсем понятно. Постараюсь объяснить на пальцах... На момент "сегодня" некоторые нейросетки (и мой любимый Grok Pro) определенные выводы не могут сформировать напрямую, они сперва генерируют свой код на Питоне, его там у себя исполняют, и потом выдают результат. Т.е. генерация кода делается в динамике, потом исполнение, и потом анализ результата исполнения. Вот тут и может пригодиться Пролог - как заранее отверифицированные кирпичики макро и микро подзадач. С другой стороны, при очередном обучении нейросети, эти уже верифицированные задачи можно опустить, ибо есть 100% правильная реализация задачи на Прологе (и есть ответственные товарищи), это конечно всё утрировано и совсем концептуально.

[Felan]

Цитата Majestio @ 08.08.26, 09:54

Если коротко: базис языка Пролог составляют факты, правила и запросы, основанные на исчислении предикатов и дизъюнктах Хорна. Программа работает как база знаний, где компьютер ищет логические ответы с помощью поиска с возвратом.

Эээ ну я тоже могу википедию процетировать. Но тут речь идет о правилах работы с некоторыми обстратными объектами. А как эти объеты определеня в реальности? Ну это как вот у нас есть алгебра. Она описывает формальные правила различных операций с числами. Но как только тебе надо будет рально сложить два числа, например 2 и 3 не в уме, где ты можешь сам оперировать абстратными объектами, а в реальном мире. Например надо построить устройство которое буедт это далать. Внезапно вяснится, что ни двойки, ни тройки не существует. И выходя из дома никто и никогда ни о двойку ни о тройку не спотыкался. В самом примитивном случае, тебе надо вырезать из дерева двойку, тройку, результат, и придумать механиз который будет на входе принимать 2 и 3 а из него будет вываливаться 5.
А тут предлагается товарный вагон щепок с обещанием что где-то там есть щепки из которых можно сделать двойку и тройку. Ну по некоторым правилам. И для того что бы их собрать ннадо перелопатить этот вагон коэффициентов.
А под верификацией нейросети я понимаю, что надо иметь обстракные правила определения как искать и какиме именно щепки нужны для двойки. И для тройки, пятерки и т.д. Т.е. формальная связь между произвольно заданным объектом и множества щепок из которых он должен быть собран.

Как-то так я это вижу....

Цитата Majestio @ 08.08.26, 09:54

В этом плане я очень даже согласен с Qraizer'ом в плане лёгкости программной верификации сгенерированного ИИ программного кода. Ибо синтаксис Пролога очень простой, разбор будет с минимальными затратами. Даже очень больших "портянок" кода. А вот уже сам процесс верификации - на совести верифицирующего.

Так, стоять бояться! Я думал с самого начала что мы говорим о верификации нейросети, а не сгенерированного ей кода. Если второе, то че тут изобретать? Тут тесты генеришь и все. Какая разница на каком языке?

Мы тогда получается про разное вообще говорим

Цитата Majestio @ 08.08.26, 09:54

И тем не менее ... В начале топика я намеренно обозначил Пролог не как замену нейросетей, а как дополнение. В моём понимании Пролог можно использовать как "расширения" для нейросетей со 100%-й достоверностью. Понимаю, что это не совсем понятно. Постараюсь объяснить на пальцах... На момент "сегодня" некоторые нейросетки (и мой любимый Grok Pro) определенные выводы не могут сформировать напрямую, они сперва генерируют свой код на Питоне, его там у себя исполняют, и потом выдают результат. Т.е. генерация кода делается в динамике, потом исполнение, и потом анализ результата исполнения. Вот тут и может пригодиться Пролог - как заранее отверифицированные кирпичики макро и микро подзадач. С другой стороны, при очередном обучении нейросети, эти уже верифицированные задачи можно опустить, ибо есть 100% правильная реализация задачи на Прологе (и есть ответственные товарищи), это конечно всё утрировано и совсем концептуально.

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

Но там некому говорить "спасибо". У нас на презентации успехов использования ИИ один индус радостно сообщил, что теперь он всегда пишет в конце промта "спасибо" Хотя не знаю, может быть

[Qraizer]

Цитата Felan @ 08.08.26, 17:05

Внезапно вяснится, что ни двойки, ни тройки не существует. И выходя из дома никто и никогда ни о двойку ни о тройку не спотыкался. В самом примитивном случае, тебе надо вырезать из дерева двойку, тройку, результат, и придумать механиз который будет на входе принимать 2 и 3 а из него будет вываливаться 5.

Строго формально арифметика выводится из теории множеств. Самый простой метод состоит из единственной аксиомы "Множеством натуральных чисел называется множество ординалов, меньших минимального недостижимого". (На практике так арифметики не формулируют, и на это есть свои причины.) А множества, являющиеся объектом изучения теории множеств, вокруг нас пруд пруди. Так что аксиоматически циферки 2, 3 и 5 легко сопоставляются с реальными сущностями.

[D_KEY]

Мне кажется, что для валидации лучше подойдут решения в духе Z3 theorem prover. Можно прикрутить обвязки в виде контрактов, например или ещё чего-то такого.

На прологе замучаешься все это описывать.

Добавлено 10.08.26, 08:18
Ну а ещё не забываем про Agda и Coq.

[Felan]

Цитата Qraizer @ 09.08.26, 16:07

Строго формально арифметика выводится из теории множеств. Самый простой метод состоит из единственной аксиомы "Множеством натуральных чисел называется множество ординалов, меньших минимального недостижимого". (На практике так арифметики не формулируют, и на это есть свои причины.) А множества, являющиеся объектом изучения теории множеств, вокруг нас пруд пруди. Так что аксиоматически циферки 2, 3 и 5 легко сопоставляются с реальными сущностями.

Все правильно. В этом сопоставлении и есть проблема. Просто сопоставление о котором говришь ты для нас с рождения естественное и мы его базируем на "очевидно это кошка одна штука", но как это сопоставление происходит? И, как я пологал, мы говорим про верефикацию _работы_ нейросети, а не сгенерированного ей кода. В первом случае непонятно что с чем и как сопоставлять, а во втором все и так трифиально, даже нейросети для этого не нужны.
А тут встает вопрос не сопоставления с сущьностями, а сначала с определением сущьностей как они есть внутри НС.

[Qraizer]

Ну, это непросто, да. Как-никак, самые основы математики. Но и не сказать, что прям сложно. Рассказать? Ординальная арифметика довольно занятная, и мне всегда было интересно, откуда и как все эти школьные азы берутся, которые на уровне математики уже далеко не азы, а вполне себе производные формальные системы.

[Felan]

Цитата Qraizer @ 10.08.26, 19:44

Ну, это непросто, да. Как-никак, самые основы математики. Но и не сказать, что прям сложно. Рассказать?

Ну давай. Расскажи, как ты понимаешь, что на одной картинке кошка, а на другой хорек.

А если про числа, так это да, это просто. Мы прото постулируем существование пустого множества, а дальше говорим, давайте сопоставим выдуманное нами пустое множество вот этому объекту, не определяя вообще, что такое "этот" и вообще что такое "объект". А так да, все просто.

[Qraizer]

Чуточку сложнее. Постов на 5.