定理証明を超えて：形式的問題解決のための定式化、フレームワーク、ベンチマーク

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

May 7, 2025

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

cs.AI

要旨

一見自明なタスクとして、問題解決は科学と工学において重要な要素となってきた。しかし、問題解決そのものに対する一般的かつ具体的な定式化は未だ存在しない。近年のAIベースの問題解決エージェントの発展に伴い、プロセスレベルでの検証可能性に対する需要が急速に高まっているが、これはまだ十分に探求されていない。これらのギャップを埋めるため、我々は問題解決を決定論的マルコフ決定過程として原理的に定式化し、既存のFTP（形式的定理証明）環境を活用してプロセス検証済みの問題解決を行う新たなフレームワークFPS（Formal Problem-Solving）、および解決と回答検証を分離することで人間との整合性を高めたD-FPS（Deductive FPS）を提案する。これらのフレームワークの表現力、健全性、完全性を証明する。我々は問題解決に関する3つのベンチマークを構築した：MATH500ベンチマークの一部を形式化したFormalMath500、FTPベンチマークMiniF2FとPutnamBenchを適応させたMiniF2F-SolvingとPutnamBench-Solvingである。忠実で解釈可能かつ人間との整合性を重視した評価のために、形式的検証によって回答の正しさを判定する記号的手法RPE（Restricted Propositional Equivalence）を提案する。我々は4つの主要なFTPモデルと2つのプロンプト手法をベースラインとして評価し、FormalMath500の最大23.77%、MiniF2F-Solvingの27.47%、PutnamBench-Solvingの0.31%を解決した。

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.