Resumen:Presentamos CodeLogician, un agente neurosimbólico para el análisis preciso de la lógica del software, integrado con ImandraX, un motor de razonamiento automatizado industrial implementado en mercados financieros y sistemas críticos para la seguridad. A diferencia de los enfoques anteriores que utilizan métodos formales principalmente para validar los resultados de los LLM, CodeLogician utiliza los LLM para construir modelos formales explícitos de sistemas de software, lo que permite que el razonamiento automatizado responda preguntas semánticas ricas más allá de los resultados de la verificación binaria.
Para evaluar rigurosamente el razonamiento matemático sobre la lógica del software, presentamos code-logic-bench, un punto de referencia que apunta al término medio entre la demostración de teoremas y los puntos de referencia de ingeniería de software. Mide la corrección del razonamiento sobre los espacios de estado del programa, el flujo de control, las restricciones de cobertura y los casos extremos, con la verdad fundamental definida mediante modelado formal y descomposición de regiones.
Al comparar el razonamiento exclusivo de LLM con los LLM aumentados con CodeLogician, el aumento formal produce mejoras sustanciales, cerrando una brecha de 41 a 47 puntos porcentuales en la precisión del razonamiento. Estos resultados demuestran que la integración neurosimbólica es esencial para escalar el análisis de programas hacia una comprensión del software rigurosa y autónoma.
Publicado originalmente en export.arxiv.org el 20 de enero de 2026.
Ver fuente original
