Во вторник 16 декабря 2025 г. пройдет семинар "Теоретическое и экспериментальное программирование" (Руководитель: к.ф.-м.н., с.н.с. Гаранина Н.О., соруководители: к.ф.-м.н., н.с. Кондратьев Д.А., к.ф.-м.н., с.н.с. Ануреев И.С., секретарь: к.ф.-м.н. Шилов Н.В.).
Время проведения: 17.00-18.30 НСК (13.00-14.30 МСК) очно в к. 239 ИСИ СО РАН и онлайн по ссылке.
Анонсы, слайды докладов и другая информация будут доступны в группе телеграм.
Докладчик: Александр Максимович Миллер (студент 4-го курса ММФ НГУ)
Тема: Baldur: как большие языковые модели учатся автоматически доказывать теоремы и исправлять ошибки в Isabelle/HOL.
Baldur — это экспериментальная система автоматизированного доказательства теорем, которая использует большие языковые модели (LLM) для решения задач формальной верификации программ. LLM в Baldur генерирует шаги доказательства, леммы и инварианты, а также предлагает возможные направления доказательства, после чего все сгенерированные элементы проверяются традиционными системами машинной поддержки доказательства. Такой гибридный подход обеспечивает высокую степень автоматизации при сохранении формальной корректности. Baldur эффективно решает задачи анализа безопасности, проверки свойств исполнения и доказательства функциональной корректности программ. Система ориентирована на совместную работу эксперта и модели, обеспечивая прозрачность, трассируемость и воспроизводимость рассуждений. Благодаря использованию больших языковых моделей Baldur ускоряет разработку доверенного программного обеспечения и расширяет возможности автоматического синтеза доказательств.