Resumen: Como una tarea aparentemente autoexplicativa, la resolución de problemas ha sido un componente significativo de la ciencia y la ingeniería. Sin embargo, falta una formulación general pero concreta de la resolución de problemas en sí. Con el reciente desarrollo de agentes de resolución de problemas basados en IA, la demanda de verificabilidad del nivel de proceso está aumentando rápidamente pero subexplorada. Para llenar estos vacíos, presentamos una formulación de principios de resolución de problemas como un proceso determinista de decisión de Markov; Un marco novedoso, FPS (resolución de problemas formal), que utiliza entornos FTP existentes (prueba de teorema formal) para realizar la resolución de problemas verificados por procesos; y D-FP (FPS deductivos), resolución de desacoplamiento y verificación de respuestas para una mejor alineación humana. La expresividad, la solidez y la integridad de los marcos están probados. Construimos tres puntos de referencia sobre la resolución de problemas: formalmath500, una formalización de un subconjunto del punto de referencia Math500; Solución de minif2f y resolución de Putnambench, adaptaciones de puntos de referencia FTP Minif2f y Putnambench. Para la evaluación fiel, interpretable y alineada por los humanos, proponemos RPE (equivalencia proposicional restringida), un enfoque simbólico para determinar la corrección de las respuestas mediante verificación formal. Evaluamos cuatro modelos FTP prevalentes y dos métodos de incrustación como líneas de base, resolviendo como máximo el 23.77% de formalmath500, 27.47% de la resolución de minif2f y el 0.31% de la resolución de putnambench.
Publicado Originalme en rss.arxiv.org El 7 de mayo de 2025.
Ver Fuente Original
