О проверке

[TonitaN]

Уже удалось соединить парсер и formalize? Вопрос также к чату, удалось ли подключить парсер.

[stewkk]

Уже удалось соединить парсер и formalize?

Контроллер для этого есть, но надо допилить интерфейс (телеграм бота / TUI). Я cмогу этим заняться только завтра =(

[TonitaN]

Непонятно, почему именно вы (сдаёте два варианта?)

По базе знаний - просьба, кто уверен в своей БЗ, сделать PR только с вашими вопросами. Иначе очень сложно проверять.

[TonitaN]

part2.json
Вторая часть (не всё) проверенных ответов.

Вижу дальше, что начинается очень много дублей. Лемма о накачке в (условно) 5 вариантах, теорема Клини так же. Если написано нормально, выкидывать не надо. Но засчитать дубли я не могу, по факту всё это - синонимы, которые можно было бы породить аугментацией одного развёрнутого ответа по теме.

[TonitaN]

Дальше:
part3.json

Ещё дальше видны дубли и очевидное талгатство: например, ответ про протокол Долева-Яо ) Сами разберитесь, пожалуйста, я не понимаю, почему должна не спать и проверять 234 kB сплошного текста из-за того, что вы просто за две минуты сделали пасту из лекций (моих и не только), не подумав о том, какой вклад она внесёт в базу знаний.

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

[stewkk]

Уже удалось соединить парсер и formalize? Вопрос также к чату, удалось ли подключить парсер.

Бот готов: https://t.me/stewkk_lab1bot
ПР: #68

Захостил на своем подкроватном сервере =)

[TonitaN]

@stewkk , бот пока только для теории? UPD: Увидела меню, сори.

(@ark2016 , по запросу теорема Майхилла-Нероде опять галлюцинации, причём добавление уточнения "для регулярных языков" делу не помогает: по итогу описывается что-то промежуточное между ней и теоремой Клини. Пока не добавили это в БЗ, или что?)

[TonitaN]

Ответ модели на "теорему Клини" ниже. Тут видно, что модель файн-тюнили, но к чему это привело - см. далее))

Теорема Клини утверждает, что множество языков, принимаемых детерминированным конечным автоматом (ДКА) совпадает с множеством языков, принимаемых академическими регулярными выражениями (ТФЯ). 

Это означает, что любой язык, который может быть описан ДКА, также может быть описан ТФЯ, и наоборот. 

Эта теорема важна в теории формальных языков, поскольку она позволяет переводить языки между ДКА и ТФЯ без потери информации.

[TonitaN]

А вот тут мне вообще непонятно, как такое могло произойти, потому что запрос почти в точности скопирован из ответов @BaldiSlayer . Уже есть сомнения в какой-либо адекватности файн-тюна.

является ли язык Дика (язык правильных скобочных последовательностей) регулярным?
------------------------------------------------------------------------------------------------------
Да, язык Дика (язык правильных скобочных последовательностей) является регулярным. 
Это можно доказать, например, с помощью регулярного выражения, 
представляющего язык всех правильных скобочных последовательностей. 
Одно из возможных регулярных выражений для языка Дика имеет вид:

(?(R)R)((.|(?(R)\1))(?(R)\2))

Здесь `R` означает рекурсивное выражение для скобок, которое можно записать как:

(*[)]|[()]

Таким образом, язык Дика является подмножеством языка, 
описываемого этими регулярными выражениями, и, следовательно, является регулярным.

В то же время, иногда появляются теховские теги, ну явно не из самой модели (я их даже узнаю), и сокращения типа ТФЯ не к месту. Значит, всё-таки БЗ учитывается, но вот как... Нужно проверять, что с метриками, и добавлять синтетические данные, не рассчитывая, что "модель и так умная".

[TonitaN]

По режиму TRS: у меня всегда ответ такой ---

Ошибка при обработке запроса: Post "http://formalize:8081/trs/formalize": POST http://formalize:8081/trs/formalize giving up after 3 attempt(s)

Попытки были просто (поскольку не сказано, где вводить интерпретации, а в код я заглянуть не успела)

f(x) = x

И

f(x) = x
-------
f(x) = x + 1

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

[stewkk]

По режиму TRS: у меня всегда ответ такой ---

Ошибка при обработке запроса: Post "http://formalize:8081/trs/formalize": POST http://formalize:8081/trs/formalize giving up after 3 attempt(s)

Попытки были просто (поскольку не сказано, где вводить интерпретации, а в код я заглянуть не успела)

f(x) = x

И

f(x) = x
-------
f(x) = x + 1

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

Коллеги из команды формалайз давали вот такой пример:

/trs 

Дана система переписывания термов (TRS): f(x)=a, g(x)=f(f(x)), u(x,y)=c(g(x),f(y)). Я интерпретирую её конструкторы так: a=1, f(x)=x2+2*x+1, g(x)=x3, u(x,y)=x+y, c(x,y)=x+y. Доказывает ли моя интерпретация завершимость trs?

На нем все работает, но запросы, которые Вы привели, тоже должны работать. Напишу коллегам =)

[TonitaN]

Мне вовсе не нравится, как модуль formalize реагирует на не тот формат. Как минимум, должен передавать осмысленное сообщение, говорящее пользователю, что лучше пользоваться таким-то форматом ввода (и это их задача, а не чата).

[TonitaN]

@stewkk , какую версию метрики и БЗ вы брали для деплоя? Последнюю? (см. мои комментарии к работе метрик выше для Аркадия - они вообще актуальны?)

[stewkk]

@stewkk , какую версию метрики и БЗ вы брали для деплоя? Последнюю? (см. мои комментарии к работе метрик выше для Аркадия - они вообще актуальны?)

Да, я уже исправляю. Не учел, что сейчас собираю не из main, извините =(

[TonitaN]

Перезапуск показал, что проблемы метрики и БЗ всё те же самые. Буквально те же замечания по тем же запросам.
Или нужно ещё подождать другого перезапуска?

[TonitaN]

Ладно, пока жду вашей отмашки, когда можно выкатывать список претензий Аркадию )