Подборка свежих научных публикаций в области Информатики из библиотеки препринтов 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) с векторными представлениями, используемыми в нейронных сетях.

Авторы расширяют уже существующее векторно-символическое кодирование языка Lisp 1.5 для того, чтобы оно могло выполнять арифметические операции. Для этого они внедряют метод Вычислений в Гиперразмерном Пространстве Вычетов (RHC). Этот метод позволяет представлять целые числа уникальными векторами и выполнять арифметику без необходимости в операциях переноса.

Главная цель этой работы — увеличить выразительность состояний нейронных сетей, позво��яя им работать с произвольно структурированными и интерпретируемыми представлениями данных. По мнению авторов, это шаг к созданию более обобщенного и универсального искусственного интеллекта, способного оперировать сложными символьными структурами.

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 — это промежуточный язык, который позволяет статически проверять семантическую линейность (ресурс используется ровно раз при выполнении). Доказано, что в этой системе оптимизации компилятора сохраняется линейность.

Это решение делает надежную поддержку линейных типов доступной для ленивых функциональных языков.

PS: Всем доброй недели!