Resumen: Los avances recientes, como Deepseek-Prover-V2-671B y Kimina-Pres-Preview-72B, demuestran una tendencia predominante para aprovechar el entrenamiento a gran escala basado en el aprendizaje de refuerzo (RL) para la prueba del teorema automatizado. Sorprendentemente, descubrimos que incluso sin ningún entrenamiento, la coordinación neuroimbólica cuidadosa de los modelos de razonamiento existentes y tácticos de táctica puede lograr un rendimiento comparable. Este documento presenta TextBF {DSP+}, una versión mejorada del marco de borrador, bosquejo y prueba, con una mejora neuro-simbólica de grano fino e integrado para cada fase: (1) En la fase de draft, provocamos modelos de razonamiento para generar subgaals de lenguaje natural para beneficiar la fase de boceto, remover la fase de pensamiento de los pensamientos a los tokens a las pruebas de los humanos a las pruebas de los húmedos humanos; (2) En la fase de boceto, las subggoas se autoformalizan con hipótesis para beneficiar la fase de prueba, y las líneas de boceto que contienen errores sintácticos se enmascaran de acuerdo con las reglas predefinidas; (3) En la fase de prueba, integramos estrechamente métodos de búsqueda simbólicos como AESOP con medidores de pasos para establecer pruebas para los subgemes de boceto. Los resultados experimentales muestran que, sin ningún entrenamiento de modelo adicional o ajuste fino, DSP+ resuelve 80.7 %, 32.8 %y 24 de 644 problemas de MINIF2F, Prueba y Putnambench, respectivamente, al tiempo que requieren menos presupuestos en comparación con el estado de los artes. DSP+ prueba texttt {IMO _2019 _P1}, un problema de la OMI en minif2f que no se resuelve por ningún trabajo anterior. Además, DSP+ genera patrones de prueba comprensibles por expertos humanos, facilitando la identificación de errores de formalización; Por ejemplo, se descubren ocho declaraciones mal formalizadas en Minif2F. Nuestros resultados destacan el potencial de los patrones de razonamiento clásico además de la capacitación basada en RL. Todos los componentes serán de código abierto.
Publicado Originalme en rss.arxiv.org El 15 de junio de 2025.
Ver Fuente Original
