Open-weight LLMs слабо справляются с верификацией Coq-доказательств: лучшая модель подтвердила лишь 12 из 100 теорем
**⚠️ Status: preprint This article is based on a preprint published on arXiv. The work may not have undergone independent peer review. Conclusions reflect the authors' position.
Кратко: Пилотное исследование на arXiv проверило способность шести open-weight LLM генерировать формальные доказательства для Coq. Моделям дали одну попытку на каждую из 100 теорем из бенчмарка CoqStoq. Лучший результат показала Gemma 4 — 12 успешных доказательств, остальные модели существенно отстали.
Что произошло
Исследователи взяли шесть open-weight LLM: Gemma 4, Llama 3.3, DeepSeek Coder V2 Lite, Qwen 3.5, Mistral Small 3.1 и GPT-OSS. Каждой модели предложили 100 теорем из набора CoqStoq, который основан на реальных Coq-проектах. Температура генерации была установлена на 0, чтобы минимизировать случайность. Каждое сгенерированное доказательство проверялось ядром Coq в исходном окружении проекта. Успешным считалось только доказательство, принятое ядром.
Результаты: Gemma 4 верифицировала 12 из 100 теорем, Llama 3.3 — 8, DeepSeek Coder V2 Lite — 1. Qwen 3.5, Mistral Small 3.1 и GPT-OSS не смогли доказать ни одной теоремы. В сумме было получено 21 успешный результат «модель-теорема», которые покрывают 15 различных теорем.
Что изменилось по сравнению с предыдущей версией
Исследование является пилотным и не имеет прямого предшественника в том же объёме. Однако оно продолжает линию работ по оценке LLM в формальной верификации, ранее проводившихся на других бенчмарках.
Цены и доступность
Все участвовавшие модели являются open-weight, то есть их веса доступны для загрузки и локального запуска. Это позволяет исследователям и разработчикам воспроизводить эксперименты и дообучать модели для повышения точности.
Почему это важно
Формальная верификация с помощью Coq — один из самых надёжных способов доказать корректность программ и математических теорем, но она требует высокой точности. Результаты показывают, что современные open-weight LLM, несмотря на впечатляющие успехи в генерации текста, пока плохо справляются с задачей, где каждое утверждение должно быть строго обосновано. Даже лучшая модель подтвердила лишь 12% теорем, что говорит о необходимости дальнейших исследований.
Для пользователей AI-Sphere
Если вы работаете с формальными методами или используете Coq для верификации кода, имейте в виду: текущие open-weight LLM могут помочь в написании черновиков доказательств, но требуют обязательной проверки. Для серьёзных проектов стоит комбинировать LLM с традиционными инструментами или использовать более мощные проприетарные модели. Следите за обновлениями в карточках моделей на ai-sphere.ru — мы будем добавлять новые бенчмарки и оценки.
Источники