## Контекст Развитие динамических энергетических систем и систем управления требует высокоточных моделей для проектирования и тестирования стратегий управления, включая супервизорные и резильентные по отношению к неисправностям. **Modelica** широко применяется в этой области, так как это универсальный язык, основанный на математических уравнениях. Однако разработка модулей управления в Modelica требует больших затрат времени и специализированных знаний. Это становится особенно актуально при работе с моделями управления в системах системных управления зданий (Building Control Description Language, BCDL). В данном исследовании рассматривается возможность использования **large language models (LLMs)** для автоматизации генерации модулей управления в BCDL в рамках Modelica Library. Целью подхода является уменьшение времени разработки и упрощение процесса для специалистов. ## Метод Разработанная методология основывается на использовании **LLMs** стандартными **prompt-сценариями** и квалифицированным **library-aware grounding** (учет спецификации внутренних характеристик Modelica Library). Далее, для проверки кодов, генерируемых LLMs, разработана реализация **automated compilation** с использованием **OpenModelica**, и система **human in the loop** для оценки результатов. Использованы данные из 4 базовых логических задач (And, Or, Not, Switch) и 5 контрольных модулей (например, включение/выключение холодильника, регулировка вентилей, управление шахтами вентиляции). Этапы работы включают создание прототипов моделей, их автоматическую компиляцию и оценку результатов. ## Результаты **GPT-4o** в zero-shot режиме не сумел генерировать работающий код Modelica. **Claude Sonnet 4**, с использованием созданных специально структурированных процессов, достиг в **basic logic blocks** успеха в 100%, а в задачах управления модулями - **83%**. В результатах, не удалось выполнить, инженеры уделяли усредненно 1-8 часов на устранение ошибок. Ошибки в выборе модулей (например, And вместо Or) были частыми при использовании **retrieval-augmented generation**, тогда как **hard rule search strategy** позволила избежать таких неточностей. Кроме того, система **human evaluation** показала более высокую точность по сравнению с **AI-based evaluation**, поскольку текущие LLMs не могут анализировать результаты симуляций или проверять корректность поведения системы. Несмотря на это, автоматизированный подход с **LLM-поддержкой** уменьшил среднее время разработки модулей с 10-20 часов до 4-6 часов, что составляет 40-60% экономии времени. ## Значимость Логические модели, сгенерированные с помощью LLMs, могут применяться в сферах проектирования управляемых зданий, а также для моделирования и симуляции энергетических систем. Этот подход позволил существенно сократить время разработки моделей управления,

## Контекст Refactoring — процесс улучшения кода без изменения его внешнего поведения — является важной практикой для повышения качества программного обеспечения. Однако его применение связано с высокими затратами времени и ресурсов. Одним из основных вопросов является понимание, почему разработчики проводят refactoring, и какие метрики могут быть эффективными для оценки этих мотиваций. Это понимание может помочь улучшить использование refactoring в практических задачах и сделать его более эффективным. ## Метод Для исследования мотиваций разработчиков во время refactoring был проведен широкомасштабный анализ данных версий управления кодом с использованием Large Language Models (LLMs). Эти модели использовались для определения основных причин refactoring, а результаты были сравнены с мотивациями, предлагаемыми в современной литературе. Также были использованы различные метрики, отражающие качество кода и его читаемость, для оценки их влияния на мотивации. ## Результаты LLMs показали высокую точность в 80% случаев, согласовываясь с мотивациями, известными из литературы в 47% случаев. Они также добавили детальные пояснения к 22% мотиваций, основываясь на сигнатах, версиях, комментариях и других данных из version control. Основные мотивации включали в себя упрощение кода, повышение читаемости и улучшение структуры. Однако метрики, отражающие качество кода и читаемость, показали слабую корреляцию с мотивациями разработчиков. ## Значимость Полученные результаты могут быть применены в различных областях, таких как анализ качества кода, автоматизированные инструменты для поддержки refactoring и системы мониторинга. Использование LLMs для понимания мотиваций может улучшить возможности для решения проблем принятия решений в коде. Более того, LLM-driven гибридные подходы, сочетающие статистические метрики и локализованные пояснения, могут помочь более систематично оптимизировать refactoring и выравнивать короткосрочные улучшения с длительными целями архитектуры. ## Выводы Результаты исследования показали, что LLM-based модели эффективно идентифицируют мотивации на уровне синтаксиса и семантики кода, но сталкиваются с трудностями при понимании архитектурных мотиваций. Будущие исследования будут сконцентрированы на улучшении моделей для повышения точности в архитектурных задачах и на интеграции LLMs с кодовыми метриками для создания более сильных инструментов для принятия рефакторинг-решений.

#### Контекст Satisfiability Modulo Theory (SMT) solvers являются ключевыми инструментами в области исследований по системам и программированию. Они лежат в основе таких задач, как символьное выполнение и автоматическая проверка. Их достоверность и качество тестовых формул, используемых для выявления ошибок, играют ключевую роль в обеспечении надежности этих систем. Однако современные SMT-решатели постоянно развиваются, что сильно усложняет создание качественных тестов. Ранее разработанные методы показали эффективность на более старых версиях систем, но не могут справиться с новыми функциями, добавляемыми в развивающиеся решатели. Данное исследование ориентировано на решение этой проблемы с помощью нового подхода, использующего Large Language Models (LLM) для генерации тестовых формул. #### Метод Предлагаемый подход, Chimera, представляет собой новую LLM-ориентированную стратегию для fuzzing SMT-решателей. Он отличается двумя основными инновациями. Во-первых, Chimera автоматически извлекает контекст-фри грамматики (CFG) из документации для SMT-теорий, включая расширения, специфичные для каждого способа. Во-вторых, Chimera использует генераторы логических выражений, генерируемые LLMs, для создания термов (логических выражений), которые соответствуют этим грамматикам. Эти термы последуют размещаться в уже существующие структурные шаблоны формул, чтобы обеспечить их синтаксическую корректность и нормативность. Этот подход снижает количество ложных срабатываний и позволяет держать высокую скорость генерации формул. Заметно, что Chimera использует LLMs только один раз в начале, чтобы сгенерировать грамматики, чтобы уменьшить накладные расходы на вычислительной мощности. #### Результаты За счет нового подхода, Chimera позволил выявить 43 багов в двух ведущих SMT-решателях: Z3 и cvc5. Из этих 43, 40 багов уже исправлены разработчиками. Эксперименты показали, что Chimera не только увеличил эффективность тестирования, но и повысил качество тестовых формул, при этом существенно сократив время вычислений. Таким образом, Chimera является эффективным инструментом для тестирования и совершенствования существующих SMT-решателей. #### Значимость Полученные результаты важны для многих областей, таких как формальные методы, автоматизированная проверка, и системы символьного вычисления. Улучшенные методы тестирования могут привести к более надежным и производительным системам. Благодаря инновационной интеграции LLMs, Chimera демонстрирует повышенную эффективность в проверке и генерации тестовых формул. Это позволяет