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

要約

一見自明のタスクとして、問題解決は科学と工学の重要な要素でした。
ただし、問題解決自体の一般的な具体的な定式化は欠落しています。
AIベースの問題解決エージェントの最近の開発により、プロセスレベルの検証可能性の需要は急速に増加しているが、露出度が低い。
これらのギャップを埋めるために、決定論的なマルコフ決定プロセスとしての問題解決の原則的な定式化を提示します。
新しいフレームワーク、FPS（正式な問題解決）。これは、既存のFTP（正式な定理証明）環境を利用して、プロセス検証の問題解決を実行します。
およびD-FPS（演ductive的なFPS）、解決のデカップリング、およびより良い人間の整列のための検証に応答します。
フレームワークの表現力、健全性、完全性が証明されています。
問題解決に3つのベンチマークを構築します。Math500ベンチマークのサブセットの形式化であるFormalMath500。
MINIF2Fソルビングおよびパトナムベンチソービング、FTPベンチマークの適応MINIF2FおよびPUTNAMBENCH。
忠実で解釈可能な、人間に合った評価のために、正式な検証による回答の正確性を判断するための象徴的なアプローチであるRPE（制限された命題の等価性）を提案します。
4つの一般的なFTPモデルと2つのプロンプトメソッドをベースラインとして評価し、Minif2F解決の27.47％、Putnambench-Solvingの0.31％をFormalMath500の最大23.77％、27.47％で解きます。

要約(オリジナル)

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.

arxiv情報

提供元, 利用サービス

arxiv.jp, Google