Oltre il Teorema Dimostrativo: Formulazione, Struttura e Benchmark per la Risoluzione Formale di Problemi

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

May 7, 2025

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

cs.AI

Abstract

Come compito apparentemente autoesplicativo, il problem-solving è stato una componente significativa della scienza e dell'ingegneria. Tuttavia, manca una formulazione generale ma concreta del problem-solving stesso. Con il recente sviluppo di agenti di problem-solving basati sull'IA, la richiesta di verificabilità a livello di processo sta crescendo rapidamente, ma rimane ancora poco esplorata. Per colmare queste lacune, presentiamo una formulazione rigorosa del problem-solving come processo decisionale di Markov deterministico; un nuovo framework, FPS (Formal Problem-Solving), che utilizza ambienti esistenti di FTP (formal theorem proving) per eseguire problem-solving verificato a livello di processo; e D-FPS (Deductive FPS), che separa la risoluzione dalla verifica delle risposte per una migliore allineamento con l'umano. L'espressività, la correttezza e la completezza dei framework sono dimostrate. Costruiamo tre benchmark sul problem-solving: FormalMath500, una formalizzazione di un sottoinsieme del benchmark MATH500; MiniF2F-Solving e PutnamBench-Solving, adattamenti dei benchmark FTP MiniF2F e PutnamBench. Per una valutazione fedele, interpretabile e allineata con l'umano, proponiamo RPE (Restricted Propositional Equivalence), un approccio simbolico per determinare la correttezza delle risposte mediante verifica formale. Valutiamo quattro modelli FTP prevalenti e due metodi di prompting come baseline, risolvendo al massimo il 23,77% di FormalMath500, il 27,47% di MiniF2F-Solving e lo 0,31% di 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.