Au-delà de la démonstration de théorèmes : formulation, cadre et benchmark pour la résolution formelle de problèmes

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

Résumé

En tant que tâche apparemment évidente, la résolution de problèmes constitue un élément fondamental des sciences et de l'ingénierie. Cependant, une formulation générale et concrète de la résolution de problèmes elle-même fait défaut. Avec le développement récent d'agents de résolution de problèmes basés sur l'IA, la demande de vérifiabilité au niveau des processus augmente rapidement, tout en restant insuffisamment explorée. Pour combler ces lacunes, nous proposons une formulation rigoureuse de la résolution de problèmes en tant que processus de décision markovien déterministe ; un nouveau cadre, FPS (Formal Problem-Solving), qui utilise des environnements existants de preuve formelle (FTP) pour réaliser une résolution de problèmes vérifiée au niveau des processus ; et D-FPS (Deductive FPS), qui découple la résolution et la vérification des réponses pour une meilleure alignement avec les humains. L'expressivité, la solidité et la complétude de ces cadres sont démontrées. Nous construisons trois benchmarks pour la résolution de problèmes : FormalMath500, une formalisation d'un sous-ensemble du benchmark MATH500 ; MiniF2F-Solving et PutnamBench-Solving, des adaptations des benchmarks FTP MiniF2F et PutnamBench. Pour une évaluation fidèle, interprétable et alignée avec les humains, nous proposons RPE (Restricted Propositional Equivalence), une approche symbolique pour déterminer la correction des réponses par vérification formelle. Nous évaluons quatre modèles FTP répandus et deux méthodes d'incitation comme références, résolvant au plus 23,77 % de FormalMath500, 27,47 % de MiniF2F-Solving et 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.