64 artículos
Este artículo presenta un nuevo enfoque que combina estrategias de saturación y reducción de objetivos mediante codificaciones SAT con ruptura de simetría para los cálculos de conexión en lógica de primer orden, implementado en el solver upCoP para impulsar la automatización de demostraciones.
Este artículo introduce las "grupos de conmutación" y los "palabras contextuales" como herramientas algebraicas para estudiar y caracterizar la contextualidad independiente del estado, un tipo fundamental de no-clasicidad cuántica.
Este artículo presenta un marco de monitoreo en línea eficiente y escalable para la Lógica Temporal Métrica (MTL) en sistemas ciberfísicos, basado en la construcción unificada de redes secuenciales mediante una técnica de marcado temporal futuro que utiliza representaciones simbólicas basadas en intervalos para comportamientos en tiempo discreto y denso.
Este artículo establece que la verificación de módulos en sistemas multiagente de pila (PMS) es 2EXPTIME-completa para especificaciones ATL y 4EXPTIME-completa para ATL*, demostrando que este último caso es exponencialmente más difícil que la verificación de modelos y constituye un problema natural elemental con una complejidad superior al tiempo triplemente exponencial.
Este artículo demuestra mediante verificación formal en Lean 4 la imposibilidad de probar la terminación de recursores duplicadores de pasos mediante medidas composicionales globales, identificando que los métodos basados en proyección superan esta barrera y validando un certificado completo de normalización fuerte y confluencia para un fragmento seguro del sistema.
Este artículo presenta MPBMC, un enfoque híbrido que utiliza redes neuronales gráficas y estadísticas de diseño para agrupar propiedades de manera funcional y acelerar la verificación formal mediante comprobación de modelos acotada.
Este artículo demuestra que la fusión independiente de lógicas modales de primer orden de una variable preserva la completitud de Kripke y la decidibilidad sin igualdad, pero no con igualdad ni constantes no rígidas, mientras que la propiedad del modelo finito solo se conserva en el caso local.
Este trabajo presenta axiomatizaciones completas de la divergencia de Kullback-Leibler y de las divergencias de Rényi de orden arbitrario para dos estructuras monoidales naturales de matrices estocásticas, formuladas desde una perspectiva categórica mediante diagramas de cadenas enriquecidos con ecuaciones cuantitativas.
Este artículo presenta una encuesta sobre enfoques sistemáticos para fragmentos restringidos de la lógica proposicional y modal, analizando cómo su poder expresivo y complejidad computacional dependen de los operadores permitidos, integrando marcos históricos y resultados sobre aprendibilidad para clasificar estos fragmentos y proponer problemas abiertos.
El artículo introduce las lógicas modales constructivas y , demuestra que ambas son completas en tiempo exponencial (EXPTIME) y poseen la propiedad de modelo finito de tamaño exponencial, resolviendo así la conjetura de Afshari et al. sobre su fragmento sin diamantes y estableciendo que los problemas de validez de y también se encuentran en EXPTIME mediante su incrustación en estas lógicas.
Este artículo presenta un enfoque de aprendizaje de restricciones para el cálculo de conexiones de primer orden que reduce significativamente el retroceso en la búsqueda de pruebas sin comprometer la completitud, ofreciendo una solución prometedora para otros cálculos de tablas no confluentes.
Este artículo presenta un nuevo enfoque para resolver ecuaciones de cadenas mediante la extensión de las transformaciones de Nielsen, combinando un operador de potencia, generalizaciones de las imágenes de Parikh y la descomposición de igualdades para abordar entradas complejas de SMT.
El artículo presenta NL2GDS, un marco innovador que utiliza modelos de lenguaje grandes para convertir descripciones de hardware en lenguaje natural directamente en diseños RTL y layouts GDSII optimizados mediante el flujo de código abierto OpenLane, logrando reducciones significativas en área, retardo y consumo de energía.
Este trabajo presenta SCORE, un lenguaje diseñado para manipular variables y pilas, y demuestra mediante un asistente de prueba que sus operaciones pueden interpretarse como biyecciones totales, superando así las limitaciones de las estrategias de reversibilización convencionales que generan funciones parciales.
Este artículo introduce los "árboles Ohana" como una nueva noción de aproximación para el cálculo I que preserva las variables ocultas o infinitas, estableciendo un teorema de conmutación con la expansión de Taylor y presentando un modelo denotacional basado en un sistema de tipos no idempotente modificado para caracterizar su teoría de igualdad.
Este artículo presenta LeanTutor, un prototipo de tutor de demostraciones matemáticas basado en IA que combina las capacidades de los modelos de lenguaje grandes con la corrección verificable de los demostradores de teoremas Lean, y lo evalúa mediante el nuevo conjunto de datos PeanoBench.
Este artículo propone un marco geométrico que modela el razonamiento de los modelos de lenguaje como flujos suaves en el espacio de representaciones, demostrando que estos modelos internalizan invariancias lógicas como geometría de alto orden y sugiriendo la existencia de una ley representacional universal independiente de la arquitectura o el entrenamiento.
El artículo presenta Strat2Rocq, un enfoque que extrae y formaliza estrategias de prueba de modelos de lenguaje grandes para enriquecer el contexto de demostración de provadores simbólicos como CoqHammer, logrando así mejorar significativamente sus tasas de éxito en la verificación de software.
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.
Este artículo presenta una metodología escalable para la verificación formal de la aritmética de punto flotante que, mediante un enfoque modular de comprobación de modelos RTL-a-RTL, estrategias de refinamiento guiadas por contraejemplos y la integración de inteligencia artificial generativa con supervisión humana, logra una mayor eficiencia de cobertura y reduce la dependencia de modelos de alto nivel.