El artículo presenta Lean4Agent, un marco que utiliza Lean4 para el modelado y la verificación formal del comportamiento de los agentes, especialmente en flujos de trabajo de múltiples pasos impulsados por LLM. Aborda la falta de métodos formales en los sistemas de agentes actuales, permitiendo verificaciones de consistencia semántica y la localización de fallos en tiempo de ejecución.
Esta investigación presenta un novedoso marco de aprendizaje para refinar que aborda el costo computacional prohibitivo de los Grandes Modelos de Lenguaje (LLM) en la demostración formal de teoremas. Al explotar las salidas del compilador que comprimen diversos intentos de prueba en modos de falla estructurados, el método permite una exploración eficiente de pruebas y una corrección local de errores, amplificando significativamente las capacidades de razonamiento de los demostradores base.
Se presenta un marco formalmente verificado para el análisis de patentes, utilizando una tubería híbrida de IA y Lean 4. Es la primera aplicación conocida de la demostración de teoremas interactiva a la propiedad intelectual, superando las limitaciones de los métodos existentes.
Este es un esquema v0.0 del artículo 'Rei as a Formal-Verification Compilation Pass for AI-Generated Mathematics', que detalla la propuesta de Rei como un paso de compilación para la verificación formal de hipótesis generadas por IA. La validación actual se encuentra en una etapa de prueba inicial, con una demostración completa pendiente para la promoción a v0.1.
Este artículo presenta una semántica algebraica para la ejecución gobernada, basada en árboles de interacción y coinducción parametrizada, con una implementación mecanizada en Rocq. El marco introduce una GovernanceAlgebra que induce una categoría monoidal simétrica y un sistema de efectos algebraicos que asegura manejadores que preservan la gobernanza.
Este artículo propone BODHI, un método de "prompting" de conocimiento de dominio para la inferencia de especificaciones del kernel del sistema operativo, con el objetivo de superar las limitaciones actuales de los LLM. Aumenta el "prompt" estándar de pocas muestras con una guía estructurada de traducción de C a Python, mejorando la automatización y la precisión de las especificaciones.
Esta investigación presenta los Transformers Verificables, un marco para convertir circuitos de Transformer localizados por tarea en afirmaciones acotadas y verificables por un solucionador. Permite la verificación de propiedades como la equivalencia funcional y la robustez mediante codificación SMT directa o mediada por sustituto.
NeuroNL2LTL es una arquitectura neurosimbólica que unifica la traducción aprendida con la verificación formal para convertir el lenguaje natural en Lógica Temporal Lineal. Utiliza un entrenamiento con verificador en el bucle, donde los resultados de la verificación sirven como señales de recompensa para el aprendizaje por refuerzo, optimizando la corrección formal.