Создатель Lean Лео де Моура: ИИ уже пишет доказательства на 50 млн строк, но доверять им нельзя без машинной проверки
AI, Lean, and the Future of Formal Verification, with Lean Creator Leo de Moura
Лео де Моура, создатель Lean и вице-президент AWS, обсуждает, как ИИ превращает формальную верификацию из удела специалистов в рабочий инструмент. Библиотека Mathlib на 2,5 млн строк создавалась людьми десять лет, а ИИ уже выдаёт доказательства на 50 млн строк, включая 13 млн строк для Великой теоремы Ферма от Anthropic. Ключевой вопрос смещается: главное теперь — спецификации и верность модели коду, а не сам код.
Борис сказал: «Я даже не знаю Lean».
- chamomeal
Что люди думают о тестировании на основе свойств (property-based testing)? Я настроил несколько таких тестов, и это почти как формальная верификация.
Я знаю, что это не одно и то же, но PBT могут отлавливать самые безумные баги, которые я бы никогда не догадался проверить. Всякие штуки с состоянием, межсервисные взаимодействия. Моя единственная претензия к PBT всегда была в утомительной настройке, но LLM решают эту проблему.
В последнее время я не видел особых обсуждений PBT, но в эпоху LLM вы получаете огромную отдачу за свои усилия.
- wbeckler
Я думаю, королевская комбинация — это Lean 4/TLA+/и т.п. плюс ИИ плюс детерминированный генератор. Для больших систем утверждения формальных методов нужно сжимать до понятного человеку размера. Это может происходить, когда утверждения подтверждают точность модели и прикреплённых к ней генераторов кода. Генератор может генерировать доказательства для сгенерированного кода, и человеку нужно только убедиться, что генератор доказуемо порождает корректные утверждения в массовом масштабе.
Именно так формальные методы могут ограничивать ИИ для больших систем.
Мы делаем это в Open Markets Initiative, где мы сгенерировали миллионы строк на Lean 4, TLA+ и Rocq, которые гарантируют точность кода нашего протокола электронных торгов с открытым исходным кодом. Мы не ожидали этого, но Lean-прувер выявил несколько некорректных шагов.
- PandaRider
> ... Но мы ожидаем, что в ближайшие месяцы и годы люди будут гораздо больше сосредотачиваться на спецификациях, на моделях, на свойствах, которые вы хотите видеть у программного обеспечения.
У кого-нибудь есть ресурсы по изучению моделирования для формальной верификации? (Не обязательно на Lean)