Cuq — это фреймворк, преобразующий MIR (промежуточное представление Rust) в Coq для формальной семантики и верифицированного перевода Rust-ядер GPU. Проект нацелен на PTX (язык ассемблера NVIDIA) и обеспечивает математически строгую основу для GPU-программирования на Rust.

Фреймворк позволяет формально доказывать свойства GPU-кода и обеспечивает верифицированный перевод из Rust в PTX. Это критически важно для безопасности и надежности вычислений на GPU, где ошибки могут иметь серьезные последствия. Cuq заполняет пробел между высокоуровневым Rust-кодом и низкоуровневым GPU-исполнением, предоставляя формальные гарантии корректности преобразований.

• Проект, который переводит MIR Rust в Coq для формальной верификации ядра CUDA, вызвал бурную дискуссию из-за имени «cuq».
• Участники спорят, звучит ли название как «кук» или «кью-кью»; критика имени превратилась в обсуждение культурных различий.
• Некоторые предлагают переименовать проект в «rocuda», «rocq» или «rocq», чтобы избежать нежелательных коннотаций.
• Автор отвечает, что имя строится на словах CUDA и Coq, и что он не осознавал двусмысленность; вопрос о переименовании остаётся открытым.
• Несмотря на спор, техническая ценность проекта в том, что он может формально верифицировать параллельные вычисления и уменьшить гонки за счёт формального доказательства корректности.

Определение пятого значения функции занятого бобра

Авторы: Коллаборация bbchallenge (Джастин Бланшар и др.)

Аннотация: Мы доказываем, что $S(5) = 47,176,870$ с использованием системы проверки доказательств Coq. Значение занятого бобра $S(n)$ — максимальное число шагов, которое машина Тьюринга с $n$ состояниями и 2 символами может выполнить с нулевой ленты до остановки. Функция $S$ была введена Тибором Радо в 1962 году как один из простейших примеров невычислимой функции. Доказательство включает перебор $181,385,789$ машин Тьюринга с 5 состояниями и определение для каждой из них, останавливается ли она. Наш результат — первое определение нового значения занятого бобра за более чем 40 лет и первое формально верифицированное значение, что демонстрирует эффективность массовых онлайн-исследований (bbchallenge$.$org).

Комментарии: 48 страниц, 17 рисунков

Предметные области: Логика в информатике (cs.LO); Формальные языки и теория автоматов (cs.FL); Логика (math.LO)

Цитирование: arXiv:2509.12337 [cs.LO]

• Результат BB(5) был подтверждён с использованием комбинации исчерпывающего перебора и продвинутых методов анализа (десидеров) для проверки остановки машин Тьюринга.
• Процесс проверки был значительно оптимизирован: большинство машин было отсеяно на ранних этапах, и лишь 183 машины потребовали глубокого моделирования (до 47 млн шагов).
• Исследование является крупным collaborative-проектом с открытым исходным кодом, аналогичным другим сообществам, изучающим клеточные автоматы и гугологию.
• Значение BB(5) само по себе не имеет прямого практического применения и считается чисто академическим достижением, однако разработанные методы могут быть полезны для статического анализа программ и решения проблем остановки.
• Некоторые машины Тьюринга, включая кандидата для BB(6), выполняют вычисления, аналогичные последовательности Коллатца, что представляет отдельный математический интерес.
• Проверка доказательства с помощью Coq требует нескольких часов на обычном компьютере, что несопоставимо с вычислительными затратами на его получение.
• Для машин с большим числом состояний (начиная с BB(6)) прямое вычисление значения считается невозможным из-за его колоссального размера и неразрешимости проблемы остановки в общем случае.