Трансформеры компактнее автоматов, но их логистику невозможно проверить

Исследователи Паскаль Бергстрассер и коллеги предложили новый подход к оценке мощностей трансформеров, введя понятие лаконичности. Они доказали, что эти модели способны описывать формальные языки значительно компактнее, чем традиционные представления вроде конечных автоматов или формул линейно-временной логики LTL. Если переводить суть на человеческий язык, трансформеры обладают невероятной выразительной способностью, укладывая огромные объемы информации в очень маленькие структуры данных. В качестве побочного результата этой работы ученые выявили серьезную проблему с безопасностью. Верификация свойств таких моделей оказалась доказанно неосуществимой в разумные сроки, а сложность задачи сравнима с самой трудоемкой, известной в информатике — класс EXPSPACE. Грубо говоря, задача проверки правильности работы трансформера относится к тем, которые требуют астрономических ресурсов для решения, и на практике их решить невозможно. Авторы считают эту лаконичность ключевым фактором, делающим трансформеры столь мощными инструментами, но одновременно и потенциально опасными из-за непроверяемости их логики.