Voorbij Theoriebewijzen: Formulering, Kader en Benchmark voor Formeel Probleemoplossen

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

May 7, 2025

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

cs.AI

Samenvatting

Als een ogenschijnlijk vanzelfsprekende taak is probleemoplossing een belangrijk onderdeel geweest van wetenschap en techniek. Een algemene maar concrete formulering van probleemoplossing zelf ontbreekt echter. Met de recente ontwikkeling van AI-gebaseerde probleemoplossingsagenten neemt de vraag naar verifieerbaarheid op procesniveau snel toe, maar dit gebied blijft onderbelicht. Om deze lacunes op te vullen, presenteren we een principiële formulering van probleemoplossing als een deterministisch Markov-beslissingsproces; een nieuw raamwerk, FPS (Formal Problem-Solving), dat bestaande FTP (formal theorem proving) omgevingen gebruikt om procesgeverifieerde probleemoplossing uit te voeren; en D-FPS (Deductive FPS), dat het oplossen en antwoordverificatie ontkoppelt voor betere afstemming op mensen. De expressiviteit, correctheid en volledigheid van de raamwerken worden bewezen. We construeren drie benchmarks voor probleemoplossing: FormalMath500, een formalisering van een subset van de MATH500 benchmark; MiniF2F-Solving en PutnamBench-Solving, aanpassingen van de FTP benchmarks MiniF2F en PutnamBench. Voor een betrouwbare, interpreteerbare en op mensen afgestemde evaluatie stellen we RPE (Restricted Propositional Equivalence) voor, een symbolische benadering om de juistheid van antwoorden te bepalen door formele verificatie. We evalueren vier veelvoorkomende FTP-modellen en twee prompting-methoden als basislijnen, waarbij maximaal 23,77% van FormalMath500, 27,47% van MiniF2F-Solving en 0,31% van PutnamBench-Solving wordt opgelost.

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.