Tech Meridian ← К СУЩНОСТЯМ
PROМОЙ MERIDIAN EN

КОМПАНИЯ · ENTITY #19364

Lean

Хронология связанных событий, источники и контекст из новостной базы.

ХРОНОЛОГИЯ СОБЫТИЙ

3

RESEARCH · 1 ИСТОЧН. · arXiv cs.AI

Агентный пайплайн на базе Gemini автономно обнаружил и формально проверил в Lean новые ускорения для 11 машин Busy Beaver (BB(6))

В препринте arXiv:2610.22603v1 описан агентный пайплайн на базе Gemini, объединяющий распознавание паттернов, автоматическую генерацию гипотез, неформальное рассуждение и формальное доказательство в Lean для автономного поиска компактных, похожих на Коллатца ускорений шагов исполнения машин Тьюринга. Система нашла и формально проверила новые ускорения для одиннадцати машин BB(6), которые авторы предварительно пометили как «Cryptids» — машины с точными компактными описаниями, но с нерешённым вопросом останова.

7.0

RESEARCH · 1 ИСТОЧН. · arXiv cs.AI

Статья на arXiv: обратная связь проверяющего одновременно помогает и мешает самовосстановлению в формальных доказательствах

Новая статья на arXiv (arXiv:2610.22698v1) исследует самовосстановление с обратной связью проверяющего в системе доказательств Lean на моделях Qwen3.6-27B и DeepSeek-Prover-V2-7B на задачах MiniF2F. Авторы обнаружили, что показ неудачного доказательства часто снижает успех и усиливает копирование ошибки, тогда как для Qwen показ сообщения компилятора иногда восстанавливает результаты; при этом ни одна проверенная стратегия обратной связи не превосходит простое повторное пробование с инструкцией при равных токен-бюджетах.

6.0

RESEARCH · 1 ИСТОЧН. · arXiv cs.AI

Статья на arXiv: корректирующая обратная связь снижает обнаружение контрпримеров спецификации в Verus/Rust

Препринт на arXiv (arXiv:2610.20676v1) показывает, что корректирующая обратная связь по корректности может подавлять обнаружение программ, которые формально соответствуют контракту, но нарушают задуманное поведение. На 12 задачах Verus/Rust и четырёх семейств моделeй при одинаковых бюджетах вызовов автономное (без обратной связи) обнаружение более чем вдвое увеличивает долю сертифицированных свидетельств по сравнению с корректирующей петлёй IntentShield (59,0% против 27,1%); фазовое (phase-separated) выполнение достигает такого же суммарного выхода без повторного использования ответов, а сохранение этих свидетельств даёт более эффективный ремонт спецификаций (Phase-Revised: 81,3% успешных реализаций против IS-Revised: 62,5%). Эффект не воспроизводится в доступных оценках Dafny и Lean, что указывает на эмпирические границы для изучённого рабочего процесса Verus/Rust.

6.0