Энергетика – базис экономики любой страны вне зависимости от технологического уклада. Однако сегодня возникла беспрецедентная ситуация, когда необходимо безотлагательно принимать принципиальные решения по дальнейшему развитию мировой энергетики. Причины обусловлены изменениями климата и разрушением озонового слоя Земли, преобладающий вклад в которые вносит деятельность человека, прежде всего, в сфере энергетики. В докладе дан анализ существующей ситуации и описаны механизмы изменения климата.

Обнаружен рост температуры поверхности Земли, который связывается с глобальным потеплением. Его главной причиной является антропогенная эмиссия парниковых газов, прежде всего, CO2. Основной вклад вносит энергетика на органическом топливе. Показано, что антропогенные выбросы ОРВ (озоноразрушающих веществ) типа фреонов приводят к разрушению озонового слоя Земли и образованию озоновых «дыр» в Антарктике. Разрушение озонового слоя и глобальное изменение климата взаимосвязаны, поскольку ОРВ и их заменители являются сильными парниковыми газами. Глобальное потепление сопровождается существенным ростом экстремальных климатических и погодных явлений.

Особую опасность представляют так называемые переломные моменты (tipping points), которые проявляются при превышении порогового значения параметров системы и могут привести к необратимым катастрофическим последствиям. Показано, что в текущей конфигурации Земля находится в бистабильном (мультистабильном) режиме - могут быть реализованы два асимптотических состояния. Теплое состояние (warm), в котором мы находимся, конкурирует с состоянием снежного кома (snowball). Бистабильность существует благодаря положительной обратной связи лед-альбедо. Необходимо дальнейшее развитие климатических моделей Земли с одновременной организацией систем климатического мониторинга.

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

Мульти-Модальная верификация программ — это процесс проверки соответствия кода его спецификации с использованием как динамических, так и символических методов, а также доказательства его корректности с помощью сочетания автоматических и интерактивных инструментов машинной поддержки. Чтобы таким инструментам можно было доверять, они сами должны сопровождаться формальными доказательствами корректности (soundness), устанавливающими, что любая программа, проверенная ими на соответствие спецификации, не нарушит её условия при исполнении. Инструменты верификации, корректность которых доказана внутри универсального доказательного ассистента с малым доверенным ядром, обычно называются фундаментальными (foundational).

В этом докладе я представлю Loom: платформу, которая упрощает и оптимизирует разработку систем верификации программ, являющихся как Фундаментальными, так и Мульти-Модальными. Наш подход основан на известной идее Монадического Неглубоко Вложения (Monadic Shallow Embedding) семантики исполняемой программы в язык теорем прувера, основанного на логике высшего порядка, в нашем случае — Lean. Мы предоставляем библиотеку Трансформеров Монад (Monad Transformers) для такой семантики, кодирующую различные вычислительные эффекты, включая состояние, расходимость программ, обработка исключений и недетерминизм, а также механизм автоматического вывода соответствующих генераторов корректных условий верификации.

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

Одна из систем верификации, основанная на Loom - язык Velvet. Пользователи могут использовать Velvet для спецификации императивных программ в стиле Dafny и их механической верификации. В рамках соревнования VeHa 2025 язык Velvet получилось успешно применить для задачи верификации алгоритма поиска подстроки.

Слайды будут на английском, выступление - на русском.

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