ИИ с Прологом или без?
 |
Наши проекты:
Журнал · Discuz!ML · Wiki · DRKB · Помощь проекту |
|
| ПРАВИЛА | FAQ | Помощь | Поиск | Участники | Календарь | Избранное | RSS |
| [216.73.216.223] |
|
|
Правила раздела:
1. Название темы - краткое описание кто/что против кого/чего
2. В первом сообщении - список параметров, по которым идет сравнение.
3. Старайтесь аргументировать свои высказывания. Фразы типа "Венда/Слюникс - ацтой" считаются флудом.
4. Давайте жить дружно и не доводить обсуждение до маразма и личных оскорблений.
2. В первом сообщении - список параметров, по которым идет сравнение.
3. Старайтесь аргументировать свои высказывания. Фразы типа "Венда/Слюникс - ацтой" считаются флудом.
4. Давайте жить дружно и не доводить обсуждение до маразма и личных оскорблений.
Модераторы: Модераторы, Комодераторы
ИИ с Прологом или без?
|
Сообщ.
#1
,
|
|
  |
Бузнос диас, амигос!
Заинтересовала эта тема, и я решил её обсудить с ИИ. Вот мой вопрос: Цитата Лет 30 назад я ходил на курсы по Искусственному Интеллекту, и там предполагалось использовать язык программирования Prolog за основу. Но, по прошествии этих лет, ИИ начал развиваться на безе нейросетей. Вопрос вот в чём ... Есть расхожая поговорка "все новое - это надёжно забытое старое". С учётом этой поговорки - какова вероятность, что в будущем новые генерации более мощных ИИ будут задействовать не только нейросети, но и концепции Prolog'а? Пусть не в классической его программной реализации, а, допустим, в виде структурированных датасетов? И, о чудо, ИИ дал вполне положительный ответ!!! Тут сам ответ я публиковать не буду - реально лениво. Но прикреплю его в виде файла в формате "raw markdown". Если кто не знает - это обычный текстовой файл с некоторой своей разметкой. Можно читать в обычном текстовом редакторе. Для ценителей форматированного чтения рекомендую CuteMarkEd. И вопрос холивара: будет ли реинкарнация языка программирования Prolog в качестве бестово/топового "компонента" для будущих поколений ИИ??? Прикреплённый файл  AI_Future.md (6.43 Кбайт, скачиваний: 6)
|
|
Сообщ.
#2
,
|
|
|
|
Нет.
Но как некую базу знаний на стероидах можно попробовать. P.S. твой md попозже прочту. |
|
Сообщ.
#3
,
|
|
 |
Врятли. Суть обучения нейросети - подбор параметров к нееоей функции. А тут получится просто второй этаж - подбор параметров к функции подборанных параметров.
|
|
Сообщ.
#4
,
|
 |
Не ну нормально ж. Сначала нейронка генерит сама себе Прологовый код, обучается, т.с., потом его исполняет.
 |
|
Сообщ.
#5
,
|
|
|
|
Цитата Qraizer @ сама себе Прологовый код А нафига козе баян? Пролог он же для кожанных. Сама себе она че-нить свое нагенерить должна. |
|
|
Сообщ.
#6
,
|
|
|
Ну так своё и нагенерит. Зато, во-первых, без галюнов, ибо в итоге имеются чёткие правила вместо статистических весов, во-вторых, эти правила поддаются валидации человеком, ибо исходный код на лице. Ну круто же. Та и не только человеком, вообще говоря, можно и математики накрутить с автоматическими доказательствами.
|
|
Сообщ.
#7
,
|
|
|
|
Цитата Qraizer @ во-первых, без галюнов, ибо в итоге имеются чёткие правила вместо статистических весов Это с чего бы вдруг? Галюны не из-за статистических весов, а из-за того, что они специально искажаются. Иначе все это превратиться в обычную формулу. Пусть даже и будет некоторые "интересные" интерполяции и экстраполяции. Цитата Qraizer @ во-вторых, эти правила поддаются валидации человеком, ибо исходный код на лице. Это с чего бы вдруг нейронка, которая сама себе че-то там генерит будет заботитсья о том, что бы какой-то там человек че-то там валидировал!? Да ну даже если и так, сколько там милиардов параметров сейчас у них? Удачи валидировать  |
|
|
Сообщ.
#8
,
|
|
|
Цитата Felan @ Именно из-за статистических весов. Предсказание наиболее вероятного следующего токена – лучше формулы пока не придумали. И да, там простая формула, управляемая коэффициентами. Просто длинная, с кучей слоёв сиречь рекурсий к самой себе. Это не секрет, и не секрет даже сама формула. Вот коэффициенты к ней фикъпоймёшь какие, пока не заклянешь в нутро этих мильярдов параметров.Галюны не из-за статистических весов, а из-за того, что они специально искажаются. Иначе все это превратиться в обычную формулу Цитата Felan @ Запросто. Пролог несложно поддаётся математическому анализу на основе строгой мат.логики. Это не какой-то там условный императивный хаос с его непредсказуемостью в ран-тайм. А стопицод мильярдов параметров – это просто количество, формальные методы легко и быстро на основе импликаций его сворачивают в более простые промежуточные выводы. ...Удачи валидировать Добавлено Цитата Felan @ Не будет. Она этого и не делает. Когда обучается, она это делает себе. Просто мы умные, и когда думаем, что харэ, давай работай, берём и сохраняем их в условный gpt-oss-20b-MXFP4.gguf, куда эти 20 лярдов параметров сливаем. Ну а тут будет не 11 Гб бинарник, а 111 Гб прологового текста. Чи не проблема... Это с чего бы вдруг нейронка, которая сама себе че-то там генерит будет заботитсья о том, что бы какой-то там человек че-то там валидировал!? |
|
Сообщ.
#9
,
|
|
|
|
Цитата Qraizer @ Именно из-за статистических весов. Не-а. Они в время работы не меняются. Я вроде не слышал, что бы сделал сетки которые в процессе обучаются\корректируют свои веса. А следовательно, веса весами, но они всегда постоянные. А вариативность достигается т.н. температурой. Это другое. Цитата Qraizer @ Пролог несложно поддаётся математическому анализу на основе строгой мат.логики Математически там анализировать нечего. Формула известна, коффициенты тоже. Важны вазаимосвязи коэффициентов. И тут две проблемы. На милиарды параметров взаимоотношение кратно больше и смысла взаимоотношения непонятно как определять с учетом того, что оно может и учавствует во множестве "решений". Цитата Qraizer @ Когда обучается, она это делает себе. Просто мы умные, и когда думаем, что харэ, давай работай, берём и сохраняем их в условный gpt-oss-20b-MXFP4.gguf, куда эти 20 лярдов параметров сливаем. Ну а тут будет не 11 Гб бинарник, а 111 Гб прологового текста. Чи не проблема... Ну начнем с придирок  Нейронка сама ничего не делеает. Она не обучается. Ее обучают. Т.е есть стадия обучения (подбор весов, с чего вообще это назвали обучением!?) и стадия работы. Они, пока, не пересекаются. А процессы подбора и расчета ошибки по отношению к нейронке - внешние. Т.е. ничего "она" "себе" не делает.Да, насохраняли этих весов, только как их интерпритировать? Какая принципиальная разница межде слючевыми словами пролога и числами? Ну и в конце внезапно выяснится, что не в человечиских возможностях в серьез ананализировать 111 Гб чего-либо. Будем брать для этого другую нейронку... Упс, походу зациклились Не, ну если я не прав, нухотя бы на треть, про динамические нейронки например, может кто ссылкой кинет? |
|
Сообщ.
#10
,
|
|
|
|
Цитата Felan @ Не, ну если я не прав, нухотя бы на треть, про динамические нейронки например, может кто ссылкой кинет? Хочешь спросить про нейронки - спроси нейронку  Скрытый текст Современные самообучаемые (self-supervised) нейронные сети Модели, которые учатся на неразмеченных данных через pretext-задачи (маскирование, контрастирование, предсказание представлений и т.д.).Эти подходы лежат в основе большинства современных foundation models. |
|
Сообщ.
#11
,
|
|
|
|
Не размеченные данные это давно уже не новость. Речь о том что они либо работают либо учатся. Вроде пока эти два стадии не научились совмещать.
|
|
Сообщ.
#12
,
|
|
|
|
Цитата Felan @ Вроде пока эти два стадии не научились совмещать. Да, читал, есть такое - пока только пытаются. В продакшене такого нету. |
|
|
Сообщ.
#13
,
|
|
|
Цитата Felan @ Ок, придираемся. Я не вижу разницы в том, чтобы после обучения сохранять веса или сохранять прологовый код. Но веса хренпоймишозахрень, а код вполне себе читаемая весчь, которая формально верифицируема сторонними методами, включая с применением математических методов доказательства корректности. Количество при этом не является препятствующим фактором, является хренпоймишохрень, которую верифицировать можно исключительно той самой формулой, то бишь самой нейронкой, этой же самой, которую верифицируем Ну начнем с придирок  .За галюны есть куча версий. Г.о. ссылаются на вероятностный подход как причину, на то они и вероятности. Есть ещё мнения, что дело в том, что нейронки всеми силами пытаются угодить промту, и потому иногда срываются в подтасовки ради с их точки зрения большей значимости "понравиться". Код же, прологовый или какой другой не суть, не будет вероятностным. Ну, по крайней мере я так понимаю отчёт самого AI в стартовом посту. Пролог же тут всплыл тупо по причине, что он декларативный, а не императивный, что некисло так выгоднее в плане его формальной верификации. |
|
Сообщ.
#14
,
|
|
|
|
Цитата Qraizer @ Ок, придираемся. Я не вижу разницы в том, чтобы после обучения сохранять веса или сохранять прологовый код. Вот с этим я с тобой согласен много-много. Но Felan ещй параллельно поднял вторую тему, а ля "работа в продакшене с непрерывным обучением/самообучением". И там, действительно, много реально "острых" подводных камней. Типа (одно из) - "потеря памяти" в процессе пересчета коэффициентов. Там ещо over-дохера аспектов ... но "бесшовная" реализация ИИ в плане обучения и самообучения + продакшен мода - действительно щяс проблемна. ... Но!!! Таки да =) Мы забыли про Prolog!!! Это можно считать "база константных данных". А что может быть красивще? Корень квадратный из минус единицы, да не смешите мои ласты! Хотя к комплексным исчислениям у меня нет негатива, честно. |
|
Сообщ.
#15
,
|
|
|
|
Цитата Qraizer @ Ок, придираемся. Я не вижу разницы в том, чтобы после обучения сохранять веса или сохранять прологовый код. Но веса хренпоймишозахрень, а код вполне себе читаемая весчь, которая формально верифицируема сторонними методами, включая с применением математических методов доказательства корректности. Количество при этом не является препятствующим фактором, является хренпоймишохрень, которую верифицировать можно исключительно той самой формулой, то бишь самой нейронкой, этой же самой, которую верифицируем . Так. Ну, во первых разница есть. Веса это просто набор чисел. Они не содержат в себе взаимосвязей. Какое число с каким связано? Для этого надо знать структуру нейронки. А это значит, что надо знать конкретный многочлен. Это для линейной. А если нейронка не линейная (есть связи между непоследовательными слоями, или не дай бог в разных направлениях) то все, приплыли. Без знания архитектыры сети веса можно выкидывать. А язык программирования это как ни крути поток данных и поток исполнения. Да он предствит и стуктуру тоже... но это будет уже в разы сложнее и анализировать 111 Гб это не кнопочку в другой цвет покрасить. Во вторых, проанализировать все это не значит построить карты или восстанивать архитектуру. Это значит конкретно объяснить, как она сделал вывод что на картинке кошка, а не харек, например. А подобные вещи люди то себе не могут объяснить внятно. А насчет верефецировть это все нейронкой... Цитата Felan @ Будем брать для этого другую нейронку... Упс, походу зациклились Цитата Qraizer @ За галюны есть куча версий. Г.о. ссылаются на вероятностный подход как причину, на то они и вероятности. Есть ещё мнения, что дело в том, что нейронки всеми силами пытаются угодить промту, и потому иногда срываются в подтасовки ради с их точки зрения большей значимости "понравиться". Код же, прологовый или какой другой не суть, не будет вероятностным. Ну, по крайней мере я так понимаю отчёт самого AI в стартовом посту. Пролог же тут всплыл тупо по причине, что он декларативный, а не императивный, что некисло так выгоднее в плане его формальной верификации. Да нет никакой кучи версий. Тут все предельно понятно. Есть многомерная функция. Нейронка это ее приближение неким многочленом. А дальше обычная аппроксимация\интерполяция\экстраполяция. Во время работы веса фиксированы, т.е. аппроксимация задана. А дальше, даем вход, если попали в экстраполированую облатьсь - фантазия\синтез\анализ, а если в интерполированую - знание\анализ\глюк. Самое гавное, что тут категория результата на самом деле определяетя все равно людьми. Если какая-нибдуь нейронка скажет что на картики с кошкой на самом деле 50% собаки, люди не скажут "О боже! Открыт новый вид!" Все скажут "хер вам а не денег" ваша нейронка гавно. В целом достижение нейросетей заключается только в том, что больше не надо искать функции, что сложно и не понятно как. Достаточно взять эпических размеров функцию (всмысле параметров), выбрать какую-нибудь непрерывнцю (функцию активации) модуляцию из ограниченного набора (сигмоида, ступенка че там еще есть это все равно технический момент что бы просто математические методы работали) и старым добрым градиентным спуском (ну или лавандовой модификацией что бы бабок срубить за инновации) подобрать коэффициенты под любую фигню. Ну да иногда помогает с неочевидными зависимостями, и даже может в некоторых случаях создавать результаты по очевидным. Ну типа после слоава "пошел" обычно идет "домой" Короче, я вообще не нейронкофоб. Удобная штука. Но не надо ее во все щели пихать. И уж тем более это не ИИ. Или не Сильный ИИ. Или как там теперь называется тру интеллект? ЗЫЖ Просто я тут не продаю нейронки. Продовал бы, я бы конечно так не богохульствовал |
|
Сообщ.
#16
,
|
|
|
|
Felan, дружище, ты поднял важную тему!
Но прошу тебя дальше не обижаться, если я буду немного резок в своих суждениях В последнем посте у тебя слишком много букв, которые не совсем по делу! Но ты реально поднял одну из важнейших тем - одновременная работа нейросетки с её обучением. Это сейчас реальная проблема. Если загуглить или занейросетить - то там будет порядка 7-10. Первая из который = "потеря памяти". Раскидаю на пальцах ... 1) Сегодня вы обсуждаете решение проблемы, где в промежуточных решениях не может быть значения от квадратного корня от минус единицы 2) Завтра нейросетка "осилила" математический аппарат комплексных исчислений Следствие: весь возможный платный месячный контекст обсуждений просто у гауно!!! Ибо нужно делать выводы по вновь обновившимся коэффициентам. Но есть и другие важные, навскидку и без детализации, факты. Cорян, и это от ИИ, мне тупо лениво напрягаться в печатанье букф: |
|
Сообщ.
#17
,
|
|
|
|
Цитата Majestio @ Но прошу тебя дальше не обижаться, если я буду немного резок в своих суждениях Я тя по ip вычислю!  Цитата Majestio @ В последнем посте у тебя слишком много букв, которые не совсем по делу! Тут сложно сказать. Я думал тема началась с технической подоплеки. Как заставить НС объяснить свое поведение хотя бы на прологе. Но не важно как. Но проблема тут гораздо глубже. И совмещение обучения и работы (как у червяков ) это только край проблемы.Но вот я и растекся по древу... Пытаясь популярно с налетом технических ньюансов объяснить положение дел. Ну или мое понимание положения дел. Ну на какое-то время назад. Цитата Majestio @ 1) Сегодня вы обсуждаете решение проблемы, где в промежуточных решениях не может быть значения от квадратного корня от минус единицы 2) Завтра нейросетка "осилила" математический аппарат комплексных исчислений Менно об этом я и говорю. Нет никакого "осилила" есть "аппроксимировала". А если точнее, то "аппроксимировали нейронной сетью". Цитата Majestio @ Следствие: весь возможный платный месячный контекст обсуждений просто у гауно!!! Ну это проблемы бизнеса, тут у меня лапки Цитата Majestio @ Cорян, и это от ИИ, мне тупо лениво напрягаться в печатанье букф: Честно говоря, хотелось бы общаться с человеком. С тостером я могу и сам дома поговорить. Цитата Majestio @ Catastrophic Forgetting (катастрофическое забывание) Дилемма стабильности и пластичности Вычислительная стоимость и задержки Отсутствие или задержка обратной связи Дрейф данных (Concept / Data Drift) Нестабильность поведения Проблемы масштаба Безопасность и контроль Это все кроме первого вообще про другое. |
|
Сообщ.
#18
,
|
|
|
|
Цитата Felan @ Честно говоря, хотелось бы общаться с человеком. С тостером я могу и сам дома поговорить. Отпуск (первый за 15 лет, дача, водовка) ... щя просто не вижу вариантов Прикинь, я ещо на рыбалку не ездил лет наверное столько =) А вот нащот тостера - ты неправ, ему обидно! Он мне сам сказал =))) Добавлено Цитата Felan @ Я тя по ip вычислю!  А я ... а я ... я в ОБСЕ заяву напишу, или ваапще в Федерацию Африканских Сил Специальных Операций!  |
|
|
Сообщ.
#19
,
|
|
|
Цитата Felan @ В Прологе нет потоков данных и исполнения.А язык программирования это как ни крути поток данных и поток исполнения. Цитата Felan @ Ну это смотря в каком языке. В русском, вот, не уверен. Ну типа после слоава "пошел" обычно идет "домой"  В целом у тебя всё правильно. Только ты упускаешь мои аргументы о верифицируемости. Цифры сиречь веса ты не верифицируешь без алгоритмов их потребляющих. А код и есть алгоритм. Даже если он декларативный, это всё равно алгоритм, т.б. поведение. Добавлено Цитата Majestio @ В моё время говорили "...шилом бритый кампучиец". ... или ваапще в Федерацию Африканских Сил Специальных Операций! |
|
Сообщ.
#20
,
|
|
|
|
Цитата Qraizer @ В Прологе нет потоков данных и исполнения. Эээ всмысле!? Они в любом языке есть. Это логические вещи. Данные как-то изменяются последовательно, а команды как-то выполняются последовательно... Это они и есть. Цитата Qraizer @ Ну это смотря в каком языке. В русском, вот, не уверен. Ну шутка же, Ё-мое. Цитата Qraizer @ В целом у тебя всё правильно. Только ты упускаешь мои аргументы о верифицируемости. Цифры сиречь веса ты не верифицируешь без алгоритмов их потребляющих. А код и есть алгоритм. Даже если он декларативный, это всё равно алгоритм, т.б. поведение. Я не упускаю. Я про это и говорил, когда рапрягался про Цитата Felan @ Веса это просто набор чисел. Они не содержат в себе взаимосвязей. Какое число с каким связано? Для этого надо знать структуру нейронки. А это значит, что надо знать конкретный многочлен. Это для линейной. А если нейронка не линейная (есть связи между непоследовательными слоями, или не дай бог в разных направлениях) то все, приплыли. Без знания архитектыры сети веса можно выкидывать. А язык программирования это как ни крути поток данных и поток исполнения. Да он предствит и стуктуру тоже... но это будет уже в разы сложнее и анализировать 111 Гб это не кнопочку в другой цвет покрасить. Во вторых, проанализировать все это не значит построить карты или восстанивать архитектуру. Это значит конкретно объяснить, как она сделал вывод что на картинке кошка, а не харек, например. А подобные вещи люди то себе не могут объяснить внятно. думаю мы просто все это немного поразному "понимаем". Но думаю тут можно прийти к общему знаменателю. Как раз проблема в том, что бы восстановить алгоритм. А это не техническая проблему. Ну ок, будет в алгритме, что-то вроде если числа по индексам между 100Гб и 101Гб стоят такие-то числа то это кошка а не харек. Ну ок. А это сибирская или сфинкс? А, ну тут надо смотреть на 3й Гб и вот такие числа. И тут плавно приходим к Солярису. (Если че про гигабайты это я ссылаюсь на твое утверждение о 111Гб) |
|
|
Сообщ.
#21
,
|
|
|
Цитата Felan @ В Прологе нет. Он декларативный, а не императивный. В Прологе есть правила вывода результатов из исходных данных, но как это делается, не формализуется. Результат валиден, если он не противоречит описанным правилам, а как он получен, никого не волнует. Идеально для мат.методов верификации. Данные как-то изменяются последовательно, а команды как-то выполняются последовательно... Добавлено Цитата Felan @ Не надо его восстанавливать. Импликации пофику, как получены A и B, она просто говорит, что A → B = F, только при T→F. Как раз проблема в том, что бы восстановить алгоритм. Добавлено P.S. По сути в Прологе ты описываешь аксиоматику своей формальной системы, и на этом всё. Все промежуточные теоремы, полагаясь на которые решаются конкретные задачи, внутри Пролог-машины, и она сама их сгенерит, смотря какие понадобились и в каком количестве. Конечно, бывает так, что аксиоматика недостаточна. В конце концов Гёделя никто не отменял. Но формальную систему всегда можно расширить дополнительными аксиомами. |
|
Сообщ.
#22
,
|
|
|
|
Цитата Qraizer @ В Прологе нет. Он декларативный, а не императивный. В Прологе есть правила вывода результатов из исходных данных, но как это делается, не формализуется. Результат валиден, если он не противоречит описанным правилам, а как он получен, никого не волнует. Ну, к тому что я пытаюсь сказать это не имеет отношения. Я про логику. И тут как бы вопрос глубины австракции. Мне например не важно как работает ДВС и почему машина доезжает от моего дома до магаза. Жена декларирует "завтра поеду в магаз". И я завтра вижу вксняшку. Но это никак не отменяет что это происходит не магическим образом, а там которетные принципы и действия. Я про пролог очень мало знаю. Но похоже он напоминает DSL. Верификация это прекрасно. Я думаю что я понимаю о чем ты говоришь. Грубо говоря на картинке мне пофиг как НС определила, что это кошка. Я вижу что это кошка и все. Я проверил, что НС все правильно порешала. Но это никак не объясняет КАК она это сделала. Цитата Qraizer @ Не надо его восстанавливать. Импликации пофику, как получены A и B, она просто говорит, что A → B = F, только при T→F. Это в теории. На практике придется реализовать некую физическую сущьность которая дожна работать в реальном мире и как-то переводит A в B и проверять T. Я понимаю, что накидали примеров (или нет если без учителя) и на вяходе получили результаты которые выглядят правильно. Но то, как это происходит определить пока невозможно. Формальная логика как раз позволяет восстановить алгоритм. Просто там посылки надо определять. Цитата Qraizer @ P.S. По сути в Прологе ты описываешь аксиоматику своей формальной системы, и на этом всё. Все промежуточные теоремы, полагаясь на которые решаются конкретные задачи, внутри Пролог-машины, и она сама их сгенерит, смотря какие понадобились и в каком количестве. Конечно, бывает так, что аксиоматика недостаточна. В конце концов Гёделя никто не отменял. Но формальную систему всегда можно расширить дополнительными аксиомами. Да я не против. Только примитивы пролога все равно как-то определены. Если это DSL то прекрасно, но как именно внутри пролог-машины определены аксиомы? Как определить новую? Хорош, пусть это не begin if a print c end. Как это работает? |
|
Сообщ.
#23
,
|
|
|
|
Цитата Felan @ Я про пролог очень мало знаю. Но похоже он напоминает DSL. Если коротко: базис языка Пролог составляют факты, правила и запросы, основанные на исчислении предикатов и дизъюнктах Хорна. Программа работает как база знаний, где компьютер ищет логические ответы с помощью поиска с возвратом. В этом плане я очень даже согласен с Qraizer'ом в плане лёгкости программной верификации сгенерированного ИИ программного кода. Ибо синтаксис Пролога очень простой, разбор будет с минимальными затратами. Даже очень больших "портянок" кода. А вот уже сам процесс верификации - на совести верифицирующего. Как тут уже не раз упоминалось ... системы на базе нейросетей базируются на многослойной структуре вероятностных коэффициентов, а системы на базе Пролога - на массивах утверждений и фактов. Согласись - второй вариант более просто верифицируем?! Т.е. для каждого предиката можно выделить набор фактов и правила, и их анализировать отдельно. Другой (кстати важный) вопрос - именования ... Скорее всего это будет что-то вроде обфускацируемого кода. Наверное - это одна из главных проблем для человеческого восприятия. Математике и алгоритмам - пофик, а для энд юзера зто будет не проще brainfick'а. И тем не менее ... В начале топика я намеренно обозначил Пролог не как замену нейросетей, а как дополнение. В моём понимании Пролог можно использовать как "расширения" для нейросетей со 100%-й достоверностью. Понимаю, что это не совсем понятно. Постараюсь объяснить на пальцах... На момент "сегодня" некоторые нейросетки (и мой любимый Grok Pro) определенные выводы не могут сформировать напрямую, они сперва генерируют свой код на Питоне, его там у себя исполняют, и потом выдают результат. Т.е. генерация кода делается в динамике, потом исполнение, и потом анализ результата исполнения. Вот тут и может пригодиться Пролог - как заранее отверифицированные кирпичики макро и микро подзадач. С другой стороны, при очередном обучении нейросети, эти уже верифицированные задачи можно опустить, ибо есть 100% правильная реализация задачи на Прологе (и есть ответственные товарищи), это конечно всё утрировано и совсем концептуально. |
|
Сообщ.
#24
,
|
|
|
|
Цитата Majestio @ Если коротко: базис языка Пролог составляют факты, правила и запросы, основанные на исчислении предикатов и дизъюнктах Хорна. Программа работает как база знаний, где компьютер ищет логические ответы с помощью поиска с возвратом. Эээ ну я тоже могу википедию процетировать. Но тут речь идет о правилах работы с некоторыми обстратными объектами. А как эти объеты определеня в реальности? Ну это как вот у нас есть алгебра. Она описывает формальные правила различных операций с числами. Но как только тебе надо будет рально сложить два числа, например 2 и 3 не в уме, где ты можешь сам оперировать абстратными объектами, а в реальном мире. Например надо построить устройство которое буедт это далать. Внезапно вяснится, что ни двойки, ни тройки не существует. И выходя из дома никто и никогда ни о двойку ни о тройку не спотыкался. В самом примитивном случае, тебе надо вырезать из дерева двойку, тройку, результат, и придумать механиз который будет на входе принимать 2 и 3 а из него будет вываливаться 5. А тут предлагается товарный вагон щепок с обещанием что где-то там есть щепки из которых можно сделать двойку и тройку. Ну по некоторым правилам. И для того что бы их собрать ннадо перелопатить этот вагон коэффициентов. А под верификацией нейросети я понимаю, что надо иметь обстракные правила определения как искать и какиме именно щепки нужны для двойки. И для тройки, пятерки и т.д. Т.е. формальная связь между произвольно заданным объектом и множества щепок из которых он должен быть собран. Как-то так я это вижу.... Цитата Majestio @ В этом плане я очень даже согласен с Qraizer'ом в плане лёгкости программной верификации сгенерированного ИИ программного кода. Ибо синтаксис Пролога очень простой, разбор будет с минимальными затратами. Даже очень больших "портянок" кода. А вот уже сам процесс верификации - на совести верифицирующего. Так, стоять бояться! Я думал с самого начала что мы говорим о верификации нейросети, а не сгенерированного ей кода. Если второе, то че тут изобретать? Тут тесты генеришь и все. Какая разница на каком языке? Мы тогда получается про разное вообще говорим Цитата Majestio @ И тем не менее ... В начале топика я намеренно обозначил Пролог не как замену нейросетей, а как дополнение. В моём понимании Пролог можно использовать как "расширения" для нейросетей со 100%-й достоверностью. Понимаю, что это не совсем понятно. Постараюсь объяснить на пальцах... На момент "сегодня" некоторые нейросетки (и мой любимый Grok Pro) определенные выводы не могут сформировать напрямую, они сперва генерируют свой код на Питоне, его там у себя исполняют, и потом выдают результат. Т.е. генерация кода делается в динамике, потом исполнение, и потом анализ результата исполнения. Вот тут и может пригодиться Пролог - как заранее отверифицированные кирпичики макро и микро подзадач. С другой стороны, при очередном обучении нейросети, эти уже верифицированные задачи можно опустить, ибо есть 100% правильная реализация задачи на Прологе (и есть ответственные товарищи), это конечно всё утрировано и совсем концептуально. Тут я не понял кто на ком стоял. Как то в кучу все. Еще раз, стадии работы и "обучения" принципиально разделены. Нет сейчас принципиальной возможности их совместить. И "обучение" это просто красивый термин, как "большой взрым" или "черная дыра" или "морская свинка", много чего еще что просто так красиво называется. На самом деле это буквально - подбор коэффициентов. Ну прикол в том, что многочле уже задан. И он, по сути всегда один. Просто мотому, что можно поставить нулевые коэффициенты в нужные места и с эмитировать любую струтуру если она плоская (нет прескоков через слои с любом направлении). Все. Подобрали коэффициенты, положили в мешок. Дальше трясем мешок и из него вываливается что-то полезное. Иногда. Иногда нет. Ну да можно в мешок запизать то, что из него до этого вывалилось и потрести опять, вывалится что-то другое, похожее... иногда. Но там некому говорить "спасибо". У нас на презентации успехов использования ИИ один индус радостно сообщил, что теперь он всегда пишет в конце промта "спасибо" Хотя не знаю, может быть |
|
|
Сообщ.
#25
,
|
|
|
Цитата Felan @ Строго формально арифметика выводится из теории множеств. Самый простой метод состоит из единственной аксиомы "Множеством натуральных чисел называется множество ординалов, меньших минимального недостижимого". (На практике так арифметики не формулируют, и на это есть свои причины.) А множества, являющиеся объектом изучения теории множеств, вокруг нас пруд пруди. Так что аксиоматически циферки 2, 3 и 5 легко сопоставляются с реальными сущностями. Внезапно вяснится, что ни двойки, ни тройки не существует. И выходя из дома никто и никогда ни о двойку ни о тройку не спотыкался. В самом примитивном случае, тебе надо вырезать из дерева двойку, тройку, результат, и придумать механиз который будет на входе принимать 2 и 3 а из него будет вываливаться 5. |
|
Сообщ.
#26
,
|
|
|
|
Мне кажется, что для валидации лучше подойдут решения в духе Z3 theorem prover. Можно прикрутить обвязки в виде контрактов, например или ещё чего-то такого.
На прологе замучаешься все это описывать. Добавлено Ну а ещё не забываем про Agda и Coq. |
|
Сообщ.
#27
,
|
|
|
|
Цитата Qraizer @ Строго формально арифметика выводится из теории множеств. Самый простой метод состоит из единственной аксиомы "Множеством натуральных чисел называется множество ординалов, меньших минимального недостижимого". (На практике так арифметики не формулируют, и на это есть свои причины.) А множества, являющиеся объектом изучения теории множеств, вокруг нас пруд пруди. Так что аксиоматически циферки 2, 3 и 5 легко сопоставляются с реальными сущностями. Все правильно. В этом сопоставлении и есть проблема. Просто сопоставление о котором говришь ты для нас с рождения естественное и мы его базируем на "очевидно это кошка одна штука", но как это сопоставление происходит? И, как я пологал, мы говорим про верефикацию _работы_ нейросети, а не сгенерированного ей кода. В первом случае непонятно что с чем и как сопоставлять, а во втором все и так трифиально, даже нейросети для этого не нужны. А тут встает вопрос не сопоставления с сущьностями, а сначала с определением сущьностей как они есть внутри НС. |
|
|
Сообщ.
#28
,
|
|
|
Ну, это непросто, да. Как-никак, самые основы математики. Но и не сказать, что прям сложно. Рассказать? Ординальная арифметика довольно занятная, и мне всегда было интересно, откуда и как все эти школьные азы берутся, которые на уровне математики уже далеко не азы, а вполне себе производные формальные системы.
|
|
Сообщ.
#29
,
|
|
|
|
Цитата Qraizer @ Ну, это непросто, да. Как-никак, самые основы математики. Но и не сказать, что прям сложно. Рассказать? Ну давай. Расскажи, как ты понимаешь, что на одной картинке кошка, а на другой хорек. А если про числа, так это да, это просто. Мы прото постулируем существование пустого множества, а дальше говорим, давайте сопоставим выдуманное нами пустое множество вот этому объекту, не определяя вообще, что такое "этот" и вообще что такое "объект". А так да, все просто. |
|
|
Сообщ.
#30
,
|
|
|
Чуточку сложнее. Постов на 5.
|
|
Сообщ.
#32
,
|
|
|
|
Цитата Qraizer @ откуда и как все эти школьные азы берутся, которые на уровне математики уже далеко не азы, а вполне себе производные формальные системы Не всё так просто, как кажется на первый взгляд Простой пример. В последнем классе средней школы давали формулу объема конуса. Ну воде бы все понятно ... но не говорили откуда она взялась - чисто учи и все. Да, там есть, скажем так, "классические выводы" от Евклида и Архимеда ... Но есть и самый, на мой взгляд простой и правильный вывод - вывод объема тела вращения путем интегрального суммирования.Вычисление числа Пи Почти все вы знаете, что методов было много (вики): Метод Архимеда (~250 г. до н.э.), Мадхава из Сангамаграмы(~1400 г.), Франсуа Виет (1593 г.), Джон Валлис (1655 г.), Джеймс Грегори (1671) и Готфрид Лейбниц (1673) - (1671 / 1673 гг.), Леонард Эйлер (1734–1735 гг.) И о чюдо!!! Сриниваса Рамануджан. Быстросходящиеся ряды (самый известный даёт ~8 знаков на член). Революция в скорости сходимости. Скорость просто тупо на порядок больше!!! На их основе позже появились ещё более быстрые формулы. Да, Qraizer, бывают в нашей жысти "чюды чюдесные". И самое интересное это в том, что не хватает интеллекта (и наверное больше всего фантазии), чтобы это познать. Про Сриниваса я вообще пытаюсь не думать, иначе ощущаю себя просто говном! |
|
|
Сообщ.
#33
,
|
|
|
Чудесатое чудесо? Таких есть у меня много.
Берём металлическую (чтобы воздух не особо влиял) цепочку, держим её в руке в свёрнутом виде с надетым на палец крайним звеном. Вытягиваем руку вперёд. Во второй вытянутой вперёд руке держим ...ну, скажем, бильярдный шар (тоже тяжёленький). Одновременно выпускаем шар падать вниз и свёрнутую с закреплённым неподвижно одним концом цепочку, у которой свободный конец начинает разматываться тоже вниз. В итоге шар внизу, цепочка развёрнута и вертикально висит на пальце. Но что это? Или показалось? Повторяем опыт... нет, не показалось. Цепочка разматывается быстрее, чем падает шар. Повторяем опыт многократно, воспроизводится однозначно. Свободный конец цепочки, закреплённой неподвижно другим концом, падает с ускорением больше g. Ну не чудесато ли? |
|
Сообщ.
#34
,
|
|
|
|
Qraizer, чёт не катит восприятие ( Объясни феномен, плс!
Добавлено Антиоффтопик!!!  Давайте мутить про Пролог в плане AI ... Пожалусто! |
|
|
Сообщ.
#35
,
|
|
|
Объяснить-то несложно, только с Прологом это никак не коррелирует
|
|
Сообщ.
#36
,
|
|
|
|
Цитата Qraizer @ Объяснить-то несложно, только с Прологом это никак не коррелирует Можно и нужно под спойлером. Вот пример, "после вчерашнего": Скрытый текст Теорема Инспекторы ГИБДД святее Понтия Пилата. Доказательство Понтий Пилат, римский прокуратор Иудеи, вынес смертный приговор Иисусу Христу. При этом в деле отсутствовал даже намёк на: Таким образом, Пилат казнил человека, который не нарушал ПДД. Более того — он ещё и руки помыл, демонстрируя полное отсутствие ответственности. Инспектор ГИБДД, напротив: Следствие Инспектор ГИБДД не казнит невиновных в дорожном смысле, не умывает рук и ограничивается административными мерами. Пилат же распял человека, который даже не превысил скорость. Вывод По сравнению с Понтием Пилатом инспекторы ГИБДД — настоящие святые. Они хотя бы ждут, пока вы нарушите правила, прежде чем начинать «крестный путь» в виде протокола. |
1 пользователей читают эту тему (1 гостей и 0 скрытых пользователей)
0 пользователей:
[ Script execution time: 0.1409 ] [ 15 queries used ] [ Generated: 24.08.26, 07:51 GMT ]