Los investigadores proponen SD-GPS, un framework impulsado por el solver para la resolución de problemas geométricos que aborda los cuellos de botella en la autoformalización y la predicción de teoremas tratando al solver simbólico como un oráculo de ejecución. Este enfoque unifica la adaptación supervisada del lenguaje formal con el aprendizaje por refuerzo guiado por la solvabilidad para garantizar la ejecutabilidad durante la formalización.
- El framework utiliza QwenVL3-2B para unificar la adaptación supervisada del lenguaje formal y el aprendizaje por refuerzo guiado por la solvabilidad en un único módulo.
- La Propuesta Verificada de Teoremas introduce un agente consciente de los puntos muertos que propone lemas auxiliares locales a partir de los estados de prueba actuales.
- Todos los teoremas propuestos se filtran mediante verificación simbólica para garantizar su corrección.
- Las evaluaciones empíricas en Geometry3K y PGPS9K muestran que SD-GPS supera a los métodos MLLM, neurales y neuro-simbólicos existentes en regímenes estándar de completado, opción múltiple y referencia multimodal.
Cerrar el bucle entre la percepción multimodal y la ejecución simbólica mejora significativamente el razonamiento geométrico, ofreciendo perspectivas sobre cómo los agentes neurales pueden estar fundamentados por sistemas formales para lograr capacidades de resolución de problemas verificables.