ИИ и сложнейшие проблемы мира · Теоретическая информатика · arXiv · 2026-10-23
RAIN: агентная генерация доказательств для верификации ПО на основе Rocq
Оригинальное название: RAIN: Agentic Proof Generation for Rocq-based Software Verification
Построение доказательств для интерактивных средств доказательства теорем трудоёмко, несмотря на строгие гарантии корректности, которые они обеспечивают. Авторы представляют RAIN — лёгкий агент, специализированный на доказательствах, который добавляет к LLM исследование репозитория, итеративное уточнение и обратную связь от проверяющей программы, что позволяет ему находить леммы и пересматривать целые скрипты доказательств. На подмножестве CoqStoq RAIN достиг более 90% успешных доказательств, что как минимум на 24,7% выше существующих базовых методов, и сравнялся с универсальными кодинг-агентами при значительно меньших затратах.