Собраны новейшие работы в области информатики из препринтов arxiv.org.
Каждая статья сопровождается ссылкой на оригинал.
2511.01872 Learned Cost Model for Placement on Reconfigurable Dataflow Hardware. Etash Guha, Tianxiao Jiang, Andrew Deng, Jian Zhang, Muthu Annamalai
Традиционные эвристические модели расчёта стоимости в системах размещения и маршрутизации для перенастраиваемых потоковых процессоров часто неточны, сложны в разработке и плохо адаптируются к изменениям компилятора. Авторы предлагают data-driven метод на основе графовых нейронных сетей: эмбеддинги узлов и рёбер PnR-графа служат входом для регрессионной модели, обученной на реальных замерах пропускной способности без использования эвристик. Такой подход повышает точность предсказаний на 31–52%, увеличивает throughput на 5,6% для моделей 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», где и данные, и код представляются в виде векторных эмбеддингов. Ранее целые числа кодировались списками, из-за чего операция сложения занимала квадратичное время. В новой схеме числа представляются через систему остатков по простым модулям в комплексных векторах — без переносов, с базовыми операциями умножения и возведения в экспоненту, что ускоряет арифметику и обеспечивает однозначность представления.
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
ScenicProver — фреймворк для композиционного вероятностного верифицирования сложных систем с ML-модулями (LE-CPS), взаимодействующих с реальным миром (например, автономные транспортные средства). Избегая «чёрных ящиков» и неопределённости среды, инструмент делит систему на модули (сенсоры, контроллеры) и применяет контракты «предположение-гарантия» в расширенном LTL. Комбинация формальных доказательств на Lean 4, симуляционных тестов через Scenic и допущений от производителей генерирует аргументы безопасности (assurance cases) с полным трассированием источников. На примере системы экстренного торможения достигнута вероятность безопасности 94,59% против 91,55% при монолитном подходе с тем же объёмом ресурсов.
2511.00403 Equality Saturation Guided by Large Language Models. Wentao Peng, Ruyi Ji, Yingfei Xiong
Представлена LGuess — гибридная структура оптимизации программ, в которой крупные языковые модели (LLM) не генерируют итоговый код, а лишь предлагают упрощённые «контрольные точки». Между ними используется механизм equality saturation с e-графом, автоматически выполняющий точные преобразования по заданным правилам. LLM выбирает оптимальные чекпоинты, опираясь на простую вероятностную модель, обученную на собственных ответах. Итеративный цикл «насыщение графа — выбор цели» ведёт к корректной и эффективной оптимизации.
2511.06565 FPGA or GPU? Analyzing comparative research for application-specific guidance. Arnab A. Purkayastha, Jay Tharwani, Shobhit Aggarwal
Обзор сопоставляет FPGA и GPU в контексте ускорения высокопроизводительных вычислений, AI и компьютерного зрения. Анализ охватывает пропускную способность, задержку, энергоэффективность и удобство программирования. Выясняется, что FPGA лучше справляются с низкой задержкой и энергоэффективностью в специализированных конвейерных задачах (встроенное зрение, обработка сигналов), тогда как GPU превосходят по масштабируемости и простоте при параллельных нагрузках (обучение нейросетей, обход графов).
2511.10343 Omnidirectional type inference for ML: principality any way. Alistair O’Brien, Didier Rémy, Gabriel Scherer
OmniML предлагает всенаправленный вывод типов для языка ML, сохраняющий свойство главенства даже при сложных расширениях — GADT, полиморфизм высшего ранга и перегрузка. Вместо классического двунаправленного метода используется динамическая система решения ограничений с возможностью приостановки сопоставлений и поэтапной конкретизации обобщённых типов в let-выражениях, что позволяет формировать и уточнять частичные схемы типов на лету.
2511.10361 Lazy Linearity for a Core Functional Language. Rodrigo Mesquita, Bernardo Toninho
Рассмотрено внедрение линейных типов в ленивые функциональные языки, на примере Haskell. Линейные типы гарантируют единократное использование ресурса, но ленивый вывод нарушает синтаксическую линейность из-за оптимизаций компилятора. Предложен промежуточный язык Linear Core, который статически проверяет семантическую линейность — подтверждая, что в рантайме ресурс используется ровно один раз, и обеспечивает сохранение этого свойства при любых оптимизациях.
