Подборка свежих научных публикаций в области Информатики из библиотеки препринтов arxiv.org.
Публикуется с обязательным указанием ссылок на первоисточники.
2511.01872 Learned Cost Model for Placement on Reconfigurable Dataflow Hardware. Etash Guha, Tianxiao Jiang, Andrew Deng, Jian Zhang, Muthu Annamalai
Хьюристические модели стоимости для размещения и маршрутизации (PnR) в реconfigurable dataflow архитектурах страдают от неточности, высокой трудоемкости разработки и слабой адаптивности к изменениям компилятора. Предлагается data-driven подход на основе GNN: эмбеддинги узлов и ребер графа PnR агрегируются для предсказания throughput регрессором, обученным на эмпирических измерениях, без хьюристик. Это дает 31-52% выше точность предсказаний, 5.6% прирост throughput на моделях BERT/GPT и быструю адаптацию при обновлениях компилятора.
2511.08767 Hey Pentti, We Did (More of) It!: A Vector-Symbolic Lisp With Residue Arithmetic Connor Hanley, Eilene Tomkins-Flanagan, Mary Alexandria Kelly
Статья описывает улучшение “векторного Lisp” — языка программирования, где всё (код, данные) хранится как высокомерные векторы в нейросетях. Раньше числа представлялись списками (медленно: сложение двух больших чисел занимало квадратичное время). Теперь числа кодируют через RHC (остатки по простым модулям в комплексных векторах): уникально, без переноса, операции — простые умножения/экспоненты векторов.
ScenicProver — это фреймворк для проверки “умных” систем (LE-CPS), где машины учатся и взаимодействуют с миром (например, автономные авто). Проблема в том, что полная проверка таких систем сложна из-за “чёрных ящиков” (как ML-модели) и реального мира. Вместо проверки всего сразу, фреймворк разбивает систему на компоненты (сенсоры, контроллеры), использует контракты “предположение-гарантия” на расширенном LTL (с выражениями Scenic для сценариев), сочетает доказательства (Lean 4), тесты в симуляторе и предположения (например, от производителей). Генерирует assurance cases — аргументы безопасности с отслеживанием источников.
2511.02164 ScenicProver: A Framework for Compositional Probabilistic Verification of Learning-Enabled Systems. Eric Vin, Kyle A. Miller, Inigo Incer, Sanjit A. Seshia, Daniel J. F
В статье описывается фреймворк для проверки безопасности сложных «умных» систем, которые включают в себя компоненты машинного обучения (Learning-Enabled Systems, LE-CPS) и взаимодействуют с реальным миром (например, автономные автомобили).
Полная проверка таких систем крайне сложна из-за наличия «чёрных ящиков» (ML-моделей) и из-за взаимодействия с непредсказуемой реальной средой.
Фреймворк предлагает композиционный подход к проверке, разбивая систему на части:
Разбиение на компоненты: Вместо проверки всей системы сразу, фреймворк проверяет отдельные компоненты (сенсоры, контроллеры). Контракты: Используются контракты «предположение-гарантия» (assumption-guarantee) на расширенном темпоральном языке логики LTL. Сочетание методов: Объединяет формальные доказательства (с использованием инструмента Lean 4), тестирование в симуляторе (сценарии задаются через Scenic) и предположения (гарантии от производителей). Результат: Генерируются assurance cases (аргументы безопасности) с возможностью отслеживания источников.
На примере системы экстренного торможения в автомобиле фреймворк показал, что, используя гарантии производителей для сенсоров и фокусируя тесты на сложных условиях (дождь, узкие объекты), он позволяет достичь более высокой вероятности безопасности (94.59% против 91.55% при монолитном тестировании) при том же объёме вычислений.
Таким образом, ScenicProver позволяет повысить достоверность и эффективность проверки безопасности систем, основанных на машинном обучении, в реалистичных условиях.
2511.00403 Equality Saturation Guided by Large Language Models. Wentao Peng, Ruyi Ji, Yingfei Xiong
LGuess — это способ заставить ИИ (типа GPT) оптимизировать программы правильно, без ошибок. ИИ не генерирует весь код сам (он часто лажает), а только предлагает “промежуточные цели” — упрощённые версии программы. Между ними работает специальный инструмент (e-graph из equality saturation), который автоматически находит точные шаги переписывания по правилам.
ИИ смотрит на кучу вариантов в графе, выбирает лучший “чекпоинт” (с помощью простой модели вероятностей, которая учится на его же ответах). Процесс в циклах: насыщаем граф, ИИ выбирает цель, повторяем до финала.
2511.06565 FPGA or GPU? Analyzing comparative research for application-specific guidance. Arnab A. Purkayastha, Jay Tharwani, Shobhit Aggarwal (Western New England U, UNC, Citadel)
Обзор исследований сравнивает FPGA и GPU для ускорения приложений. Анализ охватывает HPC AI и компьютерное зрение. Сравнение идет по метрикам пропускная способность задержка энергоэффективность и программируемость.
FPGA подходит для задач с низкой задержкой кастомных пайплайнов и регулярны. нагрузок например встроенное зрение или обработка сигналов. GPU лучше для высокой пропускной способности и нерегулярных параллельных задач таких как обучение глубоких нейронных сетей или обход графов. FPGA выигрывает в энергоэффективности и задержке GPU в масштабируемости и простот использования.
2511.10343 Omnidirectional type inference for ML: principality any way. Alistair O’Brien (University of Cambridge), Didier Rémy (INRIA), Gabriel Scherer (INRIA & IRIF, Université Paris Cité)
Статья посвящена проблеме вывода типов в языке ML. OmniML это система всенаправленного вывода типов для языка ML которая восстанавливает свойство главенства (principality) даже в сложных и хрупких расширениях. Обычный двунаправленный вывод типов слишком строгий и часто отвергает корректный код когда используются продвинутые конструкции такие как: GADTs (Generalized Algebraic Data Types), Полиморфизм высшего ранга, Перегрузка (overloading).
Авторы предлагают подход, основанный на: Динамическом порядке, где ограничения решаются асинхронно с приостановкой сопоставлений., и постепенной конкретизации для обобщения в let, где частичные схемы типов можно конкретизировать и обновлять по мере необходимости.
Это обеспечивает главенственный вывод типов для перегрузки в OCaml и для полиморфизма первого класса делая систему типов более выразительной чем существующие механизмы.
2511.10361 Lazy Linearity for a Core Functional Language. Rodrigo Mesquita, Bernardo Toninho
Статья посвящена тому, как обеспечить линейные типы в функциональных языках с ленивой оценкой (на примере Haskell).
Линейные типы требуют, чтобы ресурс использовался ровно один раз.
Проблема в том, что в ленивых языках синтаксическая линейность (то, как код написан) часто нарушается компилятором при оптимизациях, хотя семантика (то, как код выполняется) может оставаться линейной. Традиционные системы типов такой код отвергают.
Авторы вводят систему Linear Core — это промежуточный язык, который позволяет статически проверять семантическую линейность (ресурс используется ровно раз при выполнении). Доказано, что в этой системе оптимизации компилятора сохраняют линейность.
Это решение делает надежную поддержку линейных типов доступной для ленивых функциональных языков.
Источник: habr.com
