Resumen: IC3, también conocido como accesibilidad dirigida a propiedades (PDR), es un algoritmo comúnmente utilizado para la verificación de modelos de seguridad de hardware. Comprueba si un sistema de transición estatal cumple con una propiedad de seguridad determinada. IC3 devuelve INSEGURO (lo que indica una violación de propiedad) con un rastro de contraejemplo, o SEGURO con un invariante inductivo verificable como prueba de seguridad. En la práctica, el rendimiento de IC3 está dominado por una gran red de heurísticas interactivas y opciones de implementación, lo que hace que el ajuste manual sea costoso, frágil y difícil de reproducir. Este artículo presenta IC3-Evolve, un marco automatizado de evolución de código fuera de línea que utiliza un LLM para proponer parches pequeños, auditables y con ranuras restringidas para una implementación de IC3. Fundamentalmente, cada parche candidato se admite solo a través de una validación controlada por pruebas/testigos: las ejecuciones SEGURAS deben emitir un certificado que se verifica de forma independiente, y las ejecuciones NO SEGURAS deben emitir un rastro de contraejemplo reproducible, evitando que se implementen ediciones incorrectas. Dado que el LLM se usa solo fuera de línea, el artefacto implementado es un verificador evolucionado independiente sin sobrecarga de inferencia ML/LLM y sin dependencia del modelo de tiempo de ejecución. Evolucionamos en el punto de referencia de la competencia de verificación de modelos de hardware público (HWMCC) y evaluamos la generalización en puntos de referencia de verificación de modelos públicos e industriales invisibles, lo que demuestra que IC3-Evolve puede descubrir de manera confiable mejoras heurísticas prácticas bajo estrictas puertas de corrección.
Publicado originalmente en export.arxiv.org el 6 de abril de 2026.
Ver fuente original
