Resumen:Resolver restricciones que involucran definiciones inductivas (también conocidas como recursivas) es un desafío. Los solucionadores SMT/CHC de última generación y los probadores de lógica de primer orden solo brindan un soporte limitado para resolver tales restricciones, especialmente cuando involucran, por ejemplo, tipos de datos abstractos. En este trabajo, aprovechamos indicaciones estructuradas para generar modelos de lenguaje grandes (LLM) para generar lemas auxiliares que son necesarios para razonar sobre estas definiciones inductivas. Además, proponemos un enfoque neurosimbólico, que integra sinérgicamente los LLM con los solucionadores de restricciones: el LLM genera conjeturas de forma iterativa, mientras que el solucionador verifica su validez y utilidad para probar el objetivo. Evaluamos nuestro enfoque en un conjunto diverso de puntos de referencia que comprende restricciones que se originan en tipos de datos algebraicos y relaciones de recurrencia. Los resultados experimentales muestran que nuestro enfoque puede mejorar los solucionadores SMT y CHC de última generación, resolviendo considerablemente más (alrededor del 25%) tareas de prueba que involucran definiciones inductivas, lo que demuestra su eficacia.
Publicado originalmente en export.arxiv.org el 8 de marzo de 2026.
Ver fuente original
