Aprendizaje automático para la resolución automatizada de teoremas: Aprender a resolver SAT y QSAT

Título original:

Machine Learning for Automated Theorem Proving: Learning to Solve SAT and QSAT

Contenido del libro:

La demostración automática de teoremas es un campo de investigación importante y antiguo en informática, con numerosas aplicaciones. Una gran parte de los métodos desarrollados hasta la fecha para la implementación de demostradores automatizados de teoremas (ATP) han sido algorítmicos, compartiendo mucho en común con el estudio más amplio de los algoritmos de búsqueda heurística. Sin embargo, en los últimos años los investigadores han comenzado a incorporar métodos de aprendizaje automático (AM) a los ATP en un esfuerzo por obtener un mejor rendimiento. La resolución de la satisfacibilidad proposicional (SAT) y el aprendizaje automático son dos áreas de investigación amplias y antiguas, y cada una de ellas cuenta con una bibliografía correspondientemente extensa.

En este libro, el autor presenta los resultados de su revisión exhaustiva y sistemática de la investigación en la intersección de estos dos campos aparentemente no relacionados. Se centra en la investigación que ha aparecido hasta la fecha sobre la incorporación de métodos de ML en los solucionadores de problemas SAT de satisfactores proposicionales, y también en los solucionadores de sus variantes inmediatas, como SAT cuantificado (QSAT). La amplitud de la cobertura significa que los investigadores de ML adquieren una comprensión de los solucionadores SAT y QSAT más avanzados que es suficiente para hacer claramente visibles las nuevas oportunidades de aplicar su propia investigación de ML a este dominio, mientras que los investigadores de ATP adquieren una clara apreciación de cómo el aprendizaje automático más avanzado podría ayudarles a diseñar mejores solucionadores.

Al presentar el material, el autor se centra en los métodos de aprendizaje utilizados y en la forma en que se han incorporado a los solucionadores. Esto permite a los investigadores y estudiantes, tanto en el campo de la Prueba de Teoremas Automatizada como en el del Aprendizaje Automático, a) conocer lo que se ha probado y b) comprender la a menudo compleja interacción entre ATP y ML, necesaria para el éxito en estas aplicaciones innegablemente desafiantes.