Más allá de la demostración de teoremas: formulación, marco de trabajo y referencia para la resolución formal de problemas

Beyond Theorem Proving: Formulation, Framework and Benchmark for Formal Problem-Solving

May 7, 2025

Autores: Qi Liu, Xinhao Zheng, Renqiu Xia, Xingzhi Qi, Qinxiang Cao, Junchi Yan

cs.AI

Resumen

Como una tarea aparentemente autoexplicativa, la resolución de problemas ha sido un componente significativo en 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 a nivel de proceso está aumentando rápidamente, aunque aún está poco explorada. Para llenar estos vacíos, presentamos una formulación fundamentada de la resolución de problemas como un proceso de decisión de Markov determinista; un marco novedoso, FPS (Resolución Formal de Problemas), que utiliza entornos existentes de FTP (demostración formal de teoremas) para realizar una resolución de problemas verificada a nivel de proceso; y D-FPS (FPS Deductivo), que desacopla la resolución y la verificación de respuestas para una mejor alineación con los humanos. Se demuestra la expresividad, solidez y completitud de los marcos. Construimos tres puntos de referencia en la resolución de problemas: FormalMath500, una formalización de un subconjunto del punto de referencia MATH500; MiniF2F-Solving y PutnamBench-Solving, adaptaciones de los puntos de referencia FTP MiniF2F y PutnamBench. Para una evaluación fiel, interpretable y alineada con 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 prompting como líneas base, resolviendo como máximo el 23.77% de FormalMath500, el 27.47% de MiniF2F-Solving y el 0.31% de PutnamBench-Solving.

English

As a seemingly self-explanatory task, problem-solving has been a significant component of science and engineering. However, a general yet concrete formulation of problem-solving itself is missing. With the recent development of AI-based problem-solving agents, the demand for process-level verifiability is rapidly increasing yet underexplored. To fill these gaps, we present a principled formulation of problem-solving as a deterministic Markov decision process; a novel framework, FPS (Formal Problem-Solving), which utilizes existing FTP (formal theorem proving) environments to perform process-verified problem-solving; and D-FPS (Deductive FPS), decoupling solving and answer verification for better human-alignment. The expressiveness, soundness and completeness of the frameworks are proven. We construct three benchmarks on problem-solving: FormalMath500, a formalization of a subset of the MATH500 benchmark; MiniF2F-Solving and PutnamBench-Solving, adaptations of FTP benchmarks MiniF2F and PutnamBench. For faithful, interpretable, and human-aligned evaluation, we propose RPE (Restricted Propositional Equivalence), a symbolic approach to determine the correctness of answers by formal verification. We evaluate four prevalent FTP models and two prompting methods as baselines, solving at most 23.77% of FormalMath500, 27.47% of MiniF2F-Solving, and 0.31% of PutnamBench-Solving.