Jenseits des Theorembeweises: Formulierung, Rahmenwerk und Benchmark für formales Problemlösen

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

May 7, 2025

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

cs.AI

Zusammenfassung

Als eine scheinbar selbsterklärende Aufgabe ist Problemlösen ein wesentlicher Bestandteil von Wissenschaft und Technik. Dennoch fehlt eine allgemeine, aber konkrete Formulierung des Problemlösens selbst. Mit der jüngsten Entwicklung von KI-basierten Problemlösungsagenten steigt die Nachfrage nach Prozessverifizierbarkeit rapide an, bleibt jedoch untererforscht. Um diese Lücken zu schließen, präsentieren wir eine prinzipielle Formulierung des Problemlösens als deterministischen Markov-Entscheidungsprozess; ein neuartiges Framework, FPS (Formal Problem-Solving), das bestehende FTP-Umgebungen (Formal Theorem Proving) nutzt, um prozessverifiziertes Problemlösen durchzuführen; und D-FPS (Deductive FPS), das Lösen und Antwortverifizierung entkoppelt, um eine bessere menschliche Ausrichtung zu erreichen. Die Ausdrucksstärke, Korrektheit und Vollständigkeit der Frameworks werden nachgewiesen. Wir konstruieren drei Benchmarks für Problemlösen: FormalMath500, eine Formalisierung einer Teilmenge des MATH500-Benchmarks; MiniF2F-Solving und PutnamBench-Solving, Anpassungen der FTP-Benchmarks MiniF2F und PutnamBench. Für eine treue, interpretierbare und menschlich ausgerichtete Bewertung schlagen wir RPE (Restricted Propositional Equivalence) vor, einen symbolischen Ansatz zur Bestimmung der Korrektheit von Antworten durch formale Verifizierung. Wir evaluieren vier verbreitete FTP-Modelle und zwei Prompting-Methoden als Baselines, die höchstens 23,77 % von FormalMath500, 27,47 % von MiniF2F-Solving und 0,31 % von PutnamBench-Solving lösen.

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.