Além da Demonstração de Teoremas: Formulação, Estrutura e Benchmark para Resolução 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

Resumo

Como uma tarefa aparentemente autoexplicativa, a resolução de problemas tem sido um componente significativo da ciência e da engenharia. No entanto, uma formulação geral e concreta da própria resolução de problemas está ausente. Com o recente desenvolvimento de agentes de resolução de problemas baseados em IA, a demanda por verificabilidade em nível de processo está aumentando rapidamente, mas ainda é pouco explorada. Para preencher essas lacunas, apresentamos uma formulação fundamentada da resolução de problemas como um processo de decisão de Markov determinístico; um novo framework, FPS (Formal Problem-Solving), que utiliza ambientes existentes de FTP (prova de teoremas formais) para realizar a resolução de problemas verificada em nível de processo; e D-FPS (Deductive FPS), que desacopla a resolução e a verificação de respostas para melhor alinhamento humano. A expressividade, solidez e completude dos frameworks são comprovadas. Construímos três benchmarks de resolução de problemas: FormalMath500, uma formalização de um subconjunto do benchmark MATH500; MiniF2F-Solving e PutnamBench-Solving, adaptações dos benchmarks de FTP MiniF2F e PutnamBench. Para uma avaliação fiel, interpretável e alinhada com humanos, propomos RPE (Restricted Propositional Equivalence), uma abordagem simbólica para determinar a correção das respostas por meio de verificação formal. Avaliamos quatro modelos prevalentes de FTP e dois métodos de prompting como baselines, resolvendo no máximo 23,77% do FormalMath500, 27,47% do MiniF2F-Solving e 0,31% do 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.