28 artículos
Este artículo establece que las RNN lineales son altamente paralelizables porque equivalen a circuitos aritméticos de profundidad logarítmica, mientras que las RNN no lineales enfrentan barreras fundamentales de paralelización al poder resolver problemas completos en P, ofreciendo así una base teórica para equilibrar expresividad y eficiencia en arquitecturas de modelos de lenguaje.
Este trabajo presenta un algoritmo distribuido aleatorio de una ronda para colorear ciclos con dos colores que reduce la fracción esperada de aristas monocromáticas a menos de 0.24118, establece un límite inferior de 0.23879 para cualquier algoritmo de una ronda, y destaca que sus demostraciones fueron descubiertas principalmente por modelos de lenguaje grandes y formalizadas en Lean 4.
Este artículo establece la complejidad del problema de alcanzabilidad en las extensiones VASS con contadores enteros (VASS+Z), demostrando que es NP-completo para un solo contador no negativo, se sitúa en la clase para , y reduce significativamente la dimensión necesaria para alcanzar durezas PSPACE y TOWER en comparación con los VASS estándar.
Este artículo presenta un método algebraico que permite caracterizar y sintetizar en tiempo constante las reglas de los autómatas celulares de primer grado reversibles sobre para cualquier tamaño de red, verificando únicamente tres condiciones sobre sus parámetros.
Este artículo analiza la complejidad computacional del cálculo de alineaciones en minería de procesos, demostrando que el problema es PSPACE-completo en redes de Petri seguras, NP-completo en diversas subclases como árboles de procesos y T-sistemas, pero resoluble en tiempo polinómico en sistemas S-vivos y seguros.
Este artículo resuelve un problema abierto durante más de una década al demostrar la existencia de un autómatas de Büchi histórico-determinista de 65 estados que es estrictamente más conciso que cualquier autómata de Büchi determinista equivalente, utilizando una combinación de insights teóricos y asistencia computacional.
Este artículo presenta la formalización, verificación y pruebas del entorno de ejecución de autómatas de contratos (CARE) mediante el uso de autómatas temporales estocásticos y la herramienta Uppaal para mejorar la fiabilidad de esta aplicación distribuida de código abierto.
Este trabajo presenta SpotIt, un nuevo pipeline de evaluación para Text-to-SQL que utiliza verificación de equivalencia formal para identificar diferencias entre consultas generadas y de referencia que los métodos basados en pruebas tradicionales pasan por alto.