Resumen:La resolución de problemas de geometría ha adoptado cada vez más el paradigma neurosimbólico, combinando la intuición neuronal con el rigor simbólico. Sin embargo, los marcos actuales sufren de graves obstáculos en dos etapas centrales: la autoformalización, que trata la traducción multimodal como una tarea estática desacoplada de la compatibilidad del solucionador posterior, y la predicción de teoremas, donde los solucionadores frecuentemente llegan a un callejón sin salida deductivo debido a bibliotecas de reglas fijas. Para abordar estos problemas, proponemos SD-GPS, un marco basado en solucionador que trata al solucionador simbólico como un oráculo de ejecución tanto en la formalización como en la deducción. En primer lugar, la autoformalización impulsada por Solver unifica la adaptación supervisada del lenguaje formal y el aprendizaje por refuerzo guiado por la solvabilidad en un único módulo construido en QwenVL3-2B, lo que convierte la ejecutabilidad en la señal de entrenamiento central. En segundo lugar, Verified Theorem Proposing introduce un agente consciente del impasse que propone lemas auxiliares locales a partir de estados de prueba actuales, asegurando solidez al filtrar todas las propuestas a través de verificación simbólica. Las evaluaciones empíricas en Geometry3K y PGPS9K demuestran que SD-GPS supera consistentemente los métodos MLLM, neuronales y neurosimbólicos existentes en los regímenes de referencia de finalización estándar, de opción múltiple y multimodal, lo que demuestra que cerrar el círculo entre la percepción multimodal y la ejecución simbólica mejora significativamente el razonamiento geométrico, ofreciendo conocimientos profundos sobre cómo los agentes neuronales pueden basarse en sistemas formales para lograr capacidades verificables de resolución de problemas.
Publicado originalmente en export.arxiv.org el 28 de junio de 2026.
Ver fuente original
