Доклад является продолжением первого доклада, читавшегося в феврале, о property-based тестировании на основе зависимых типов и о библиотеке DepTyCheck. В этом докладе подробнее остановимся на том, что из себя может представлять генератор значений зависимого типа, какие могут быть проблемы с представлением и комбинированием таких генераторов, и что можно сделать, чтобы генератор работал эффективно. Доклад предполагает некоторое знакомство с предыдущим докладом, или хотя бы общее знакомство с функциональным программированием и зависимыми типами.
Доклад может быть интересен людям, которые могут столкнуться с задачей генерации случайных значений с зависимыми типами, а также тем, кто пользуется property-based тестированием, и думает о том, почему в разных языках и библиотеках всё так по-разному. Доклад пытается выстроить некоторую систему вокруг реализации возможностей генерации сложных типов данных.
Iris-Lean это порт Iris на Lean. Я расскажу про то, как Iris-Lean устроен и про то, как различия между Rocq и Lean повлияли на дизайн и использование Iris в Lean. Расскажу про текущие проблемы Iris-Lean, про то, что на данный момент сделано, а что — предстоит сделать. Кроме того, будет показан порт iris-tutorial с Rocq Iris на Iris-Lean.
Расскажу про Aeneas — активно развивающийся фреймворк для верификации программ на Rust. Его главная фишка в том, что, благодаря тому что обращение с памятью контролируется в Rust на уровне типов, код на нём удаётся погрузить внутрь функционального языка почти «как есть». Фреймворк поддерживает перевод Rust в разные системы доказательств — F*, HOL, Rocq и Lean, в докладе я буду использовать Lean.
In my previous talk I laid out the grand plan of formalizing all math using a dependency graph. A key component is a formalization agent powerful enough to autonomously formalize any theorem, provided that all its dependencies are already formalized — this represents adding one more node to the graph of formal mathematics. I will describe my experience with semi-autonomous formalization of a theorem in mathematical physics about equilibrium of plasma, and argue that such an agent is already within reach. No prior math or physics knowledge is assumed. Статья, код.
Доклад посвящён дипломному проекту: генеративному фаззеру для компилятора Scala 3, где AST моделируется зависимыми типами на Idris 2 с использованием DepTyCheck. Код на Idris почти целиком написан AI-агентами — будет показано, как выглядит пайплайн, когда автор управляет агентами вместо того, чтобы писать на зависимых типах руками.
Обсудим, как при таком подходе формулируются спецификации, как контролируется корректность, и что получилось в итоге: найденные баги в компиляторе Scala 3, патчи в DepTyCheck и практические ограничения подхода.
Доклад будет интересен тем, кто задаётся вопросом: что происходит, когда формальные методы и LLM-агенты оказываются в одном проекте.
Формальная верификация на базе классических систем типов CiC/MLTT зачастую превращается в затяжную борьбу со стереотипными преобразованиями структур данных и предикатов из-за слишком «жёсткого» определения равенства. Гомотопическая теория типов (HoTT) и её реализация в Cubical Agda призваны решить эту проблему в корне.
В этом докладе я покажу, как принципы унивалентности и тождества структур (SIP) позволяют «бесплатно» переносить теоремы между эквивалентными определениями. Мы рассмотрим, как пропозициональное усечение возвращает в конструктивную логику хорошо знакомое математикам «простое существование», избавляя от возни с лишними деталями реализации. Также мы заглянем в «зоопарк» конечных множеств (по Куратовскому, Бишопу и др). Наконец, на примерах из книги Symmetry авторства Bezem et al мы увидим, как группоидная структура типов превращает множества в классифицирующие пространства групп. Эти механизмы открывают путь к формализации теории высших групп непосредственно в коде, что наделяет современную абстрактную математику вычислимыми свойствами.
Доклад посвящён системе Agentica и построенному в ней агенту для решения бенчмарка ARC-AGI-2. В начале будет коротко объяснено, что такое ARC-AGI, зачем этот бенчмарк был предложен как попытка измерять способность системы осваивать новые правила по малому числу примеров, и чем ARC-AGI-2 отличается от более ранней версии. Также будут кратко затронуты переход к ARC-AGI-3 и другие новости ARC Prize.
Основная часть доклада будет посвящена фреймворку Agentica и тому, как он организует решение задач через персистентную среду исполнения, работает с объектами и типами, и как в нём устроена рекурсивная оркестрация субагентов.
После этого будет подробно рассмотрен Arcgentica как конкретное применение Agentica к задачам ARC-AGI-2. Я покажу, как агент синтезирует функцию преобразования, как проверяет её, каким образом использует рекурсивное делегирование подзадач, и как эта логика отражается в дереве вызовов субагентов на примере решения конкретной задачи.
Hoare Type Theory (HTT) — это библиотека для работы с сепарационной логикой в Coq, построенная в духе денотационной семантики, где в центре внимания — математические, а не операционные свойства мутабельных программ. В отличие от традиционных подходов, которые строят логику поверх конкретной модели кучи, HTT изначально моделирует состояние как абстрактный частичный коммутативный моноид (partial commutative monoid, PCM). Такая основа позволяет единообразно работать с различными PCM и морфизмами между ними непосредственно в рамках стандартной сепарационной логики над кучей.
В докладе я покажу, как этот подход помогает решить известную проблему сепарационной логики — верификацию графовых алгоритмов. Графы плохо поддаются декомпозиции на непересекающиеся компоненты, что исторически делало их верификацию трудоёмкой. Мы используем декомпозицию на так называемые «частичные графы», допускающие висячие рёбра (dangling edges). При этом морфизмы PCM играют роль, аналогичную фрейм-правилу (frame rule): они позволяют локализовать рассуждения в рамках релевантных подграфов, даже если те вложены глубоко в математическую спецификацию.
Эта «контекстуальная локализация» оказывается значительно выразительнее классического фрейминга на уровне троек Хоара. Эффективность подхода видна на примере механизированных доказательств алгоритмов Шорра–Уэйта и Union-Find, каждое из которых умещается примерно в 100 строк — для сравнения, оригинальное доказательство алгоритма Шорра–Уэйта в классической работе Хонгсока Янга занимало около 40 страниц.
Доклад предполагает знакомство с пруф-ассистентом Rocq (aka Coq) и базовыми концепциями сепарационной логики.
Motivated by the humble goal of solving all math, autonomously and reliably, we will discuss two recent papers by the UW Math AI Lab, «Semantic Search over 9 Million Mathematical Theorems» and «Learning to Repair Lean Proofs from Compiler Feedback». Each paper identifies a bottleneck on the road to formalize real mathematical research at scale, and proposes a partial solution. Статья 1, Статья 2.
Работа FunSearch от DeepMind открыла новую парадигму автоматизированных исследований. Допустим дана некоторая задача, для которой можно быстро и автоматически проверить качество решений. FunSearch предлагает решать задачу так:
Такая эволюция направляет креативность нейросети в сторону улучшения метрик. В оригинальной работе, были улучшены оценки в некоторых комбинаторных задачах.
Подход затем развился в работе AlphaEvolve, и на настоящий момент вышло немало работ использующих его в решении математических задач и оптимизации алгоритмов, о которых мы тоже поговорим.
A review of Seed-Prover 1 and 1.5 — LLM-based agents for formal theorem proving in Lean. Both papers were SotA at the time of publication. The talk will specifically focus on test-time scaling strategies, including lemma-decomposition and sketching. Статья 1, Статья 2.
Property-based testing — зарекомендовавший себя подход, позволяющий находить баги, практически неподвластные ручному тестированию, и при правильном использовании значительно сокращающий затраты на качественное тестирование. Для работы подхода нужны генераторы входных данных системы, которую мы тестируем, и часто мы можем получить эти генераторы автоматически или задёшево.
Но что, если у той системы, которую мы хотим тестировать, входные данные очень непростой структуры? Например, хитрые графы с хитрыми отношениями вершин, успешно тайпчекающиеся программы или образы файловых систем? Выясняется, что тут нам могут помочь зависимые типы!
В докладе покажу как генераторы значений зависимых типов могут облегчить сложное тестирование, что сами такие генераторы, на самом деле, сложно, и как с этим можно справиться при помощи деривации. Всё это делается при помощи разработанной мной библиотеки DepTyCheck под язык Idris2.
В докладе я расскажу о серии работ DeepSeek-Prover. На текущий момент это одна из сильнейших систем для формальных доказательств на Lean. В работе множество интересных идей: генерация доказательства целиком, использование больших (600B) моделей для chain-of-thought рассуждений на естественном языке, генерация синтетических данных и обучение с подкреплением. Статья.
Задача поиска формального доказательства в чем-то напоминает игру, где состояния это цели (tactic state), а ходы — это применения тактик или правил вывода. В играх вроде шахмат или го ИИ-методы давно достигли сверхчеловеческого уровня при помощи RL-алгоритма AlphaZero. Я расскажу о статье «HyperTree Proof Search», в которой показано как применить этот метод к доказательству теорем. Дерево вариантов игры при этом заменяется на гипердерево доказательства. Это одна из первых работ по поводу формального доказательств теорем при помощи ИИ, и её идеи лежат в основе современных результатов. Статья.
В докладе рассмотрим практическое применение AutoCorres2 для интеграции C-кода в среду формальной верификации Isabelle/HOL, разберём особенности работы с препроцессированным кодом (по материалам доклада The Next 700 Verified seL4 Platforms — Gerwin Klein, Proofcraft, видео), а также покажем, как использовать Haskell-translator для построения «исполняемой» документации.
В своем докладе я расскажу про работу AlphaGeometry от DeepMind. AlphaGeometry — это система, способная решить 88% задач по геометрии с IMO. Она интересна симбиозом «креативной» нейросети и быстрого механического солвера. Нейросеть по (грубо говоря) рисунку предсказывает новое дополнительное построение, а солвер логически и алгебраически выводит новые факты о текущей конструкции. Все это функционирует внутри домено-специфичного формального языка, разработанного специально под задачу, что позволяет (потенциально) переводить сгенерированные доказательства в другие системы доказательств. Отдельный интерес представляет то, что нейросеть учится без человеческих доказательств, при помощи обучения с подкреплением.