64 artículos
Este artículo estudia cómo las presentaciones como monadas de codensidad de varias monadas de medidas de probabilidad permiten derivar leyes de Kleisli hacia la monada de Giry, establecer propiedades universales y caracterizar condiciones para que sean laxas monoidales y afines, vinculando así estos conceptos con la teoría de categorías de Markov y la convolución de Day.
Este artículo introduce un operad de diagramas de cableado dirigidos dependientes para componer máquinas de Mealy y diagramas de stock y flow, permitiendo la conexión instantánea de sistemas sin ciclos al definir una semántica mediante un morfismo de álgebras hacia las máquinas de Mealy.
Este artículo presenta Preguss, un marco modular que combina análisis estático y modelos de lenguaje grandes para sintetizar especificaciones formales y verificar automáticamente la ausencia de errores en tiempo de ejecución en programas a gran escala, reduciendo significativamente el esfuerzo humano necesario.
El artículo presenta una metodología de verificación formal escalable basada en lógica de vectores de bits que permite verificar circuitos de estimación de fase cuántica con más de 1.000 qubits utilizando menos de 3,5 GB de memoria.
Este artículo establece explícitamente que el tamaño óptimo de un circuito cambia como máximo en ante una perturbación de un punto en su tabla de verdad, extendiendo el resultado a distancias de Hamming generales y verificando su optimalidad exhaustiva para mediante un análisis SAT en la base AIG.
El artículo presenta RoadLogic, una herramienta de código abierto que utiliza programación lógica y planificación de movimiento para convertir automáticamente especificaciones declarativas de escenarios de OpenSCENARIO en simulaciones ejecutables y verificadas, facilitando así la prueba sistemática de vehículos autónomos.
Este artículo presenta un marco general novedoso que extiende la compilación a d-DNNF al nivel de SMT mediante la combinación de fórmulas de entrada con lemas teóricos precalculados, permitiendo así realizar consultas SMT en tiempo polinomial utilizando razonadores proposicionales estándar.
Este artículo presenta BemaGANv2, un vocador basado en GAN optimizado para la generación de audio de larga duración que introduce innovaciones arquitectónicas como el módulo AMP y el Discriminador de Sobres Multi-Envolvente (MED), evaluando sistemáticamente diversas estrategias de combinación de discriminadores para mejorar la coherencia temporal y la fidelidad del audio.
El artículo presenta FATE, una nueva serie de benchmarks en álgebra formal que abarca desde ejercicios universitarios hasta problemas de investigación avanzada, revelando que los modelos de lenguaje actuales tienen un rendimiento muy limitado en esta área, especialmente en la formalización de su razonamiento natural.
Este artículo formaliza en la teoría de tipos homotópicos la correspondencia de Galois entre espacios de recubrimiento y subgrupos del grupo fundamental, generaliza este concepto a dimensiones superiores y aplica el marco desarrollado para clasificar los recubrimientos de espacios de lentes y construir la esfera de homología de Poincaré.
Este artículo presenta un enfoque que extiende la minería de especificaciones más allá de las abstracciones booleanas mediante la combinación de síntesis guiada por sintaxis y una interpretación de lógica temporal (TSL) para aprender transformaciones de datos y especificaciones temporales, demostrando una mayor eficiencia y robustez en la síntesis de programas reactivos en entornos de aprendizaje automático.
Este artículo compara tres semánticas de satisfacibilidad para la lógica cuántica en espacios de Hilbert de dimensión fija, demostrando que la semántica estándar es estrictamente más expresiva que las semánticas de proyectores conmutantes globales y parcial-booleanas, y proporcionando una fórmula explícita que separa estas clases.
El artículo presenta "Agent Hunt", un experimento que utiliza un mercado simulado basado en recompensas donde múltiples agentes de LLM colaboran de forma descentralizada para formalizar y demostrar teoremas de topología algebraica en un entorno de demostración interactiva, proponiendo lemas, compitiendo por recompensas y refinando iterativamente sus pruebas hasta que son verificadas por el asistente de demostración.
El artículo presenta Twitch, una herramienta que descubre automáticamente abstracciones (patrones de términos recurrentes) en demostraciones de teoremas para guiar al probador equacional Twee, logrando resolver problemas de igualdad unitaria previamente no resueltos y acelerando significativamente la demostración de otros.
Este artículo presenta LLM2SMT, un estudio de caso en el que un agente de codificación basado en modelos de lenguaje construye un solver SMT completo para QF_UF sin ninguna línea de código escrita por humanos, logrando un rendimiento competitivo en los benchmarks de SMT-LIB.
El artículo presenta Elenchus, un sistema de diálogo que utiliza un modelo de lenguaje como oponente para construir bases de conocimiento mediante la explicitación de compromisos inferenciales bajo una semántica inferencialista, demostrando su eficacia al generar y verificar formalmente la ontología de procedencia PROV-O.
Este artículo investiga el uso de redes neuronales gráficas para predecir órdenes de ramificación iniciales que aceleran significativamente a los solucionadores SAT CDCL en instancias aleatorias y pseudo-industriales, aunque su eficacia disminuye en problemas industriales complejos debido a que las heurísticas dinámicas del solucionador sobrescriben rápidamente la inicialización.
Este artículo presenta las bases de datos orientadas a bocetos, un marco categórico que codifica paradigmas de bases de datos como bocetos de límites finitos y sus modelos, demostrando su aplicabilidad en grafos, definiendo reglas de inferencia para rutas mediante localizadores y proponiendo bocetos de titubeo para facilitar la composición modular y el crecimiento escalable de modelos.
Este artículo presenta un método automatizado para generar ejercicios de demostración matemática con niveles de complejidad comparables, utilizando pruebas de tablaux basadas en reglas extraídas mecánicamente para controlar la dificultad en cursos de matemáticas discretas.
Este documento presenta las actas de la Octava Conferencia Internacional sobre Teoría de Categorías Aplicada, celebrada en la Universidad de Florida en junio de 2025, que reunió contribuciones teóricas y prácticas de diversas disciplinas como informática, química y computación cuántica.