За пределами доказательства теорем: формулировка, структура и эталон для формального решения задач

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

Аннотация

Решение задач, казалось бы, является интуитивно понятным процессом и играет важную роль в науке и технике. Однако общая, но конкретная формулировка самого процесса решения задач отсутствует. С недавним развитием агентов на основе ИИ, способных решать задачи, спрос на проверяемость на уровне процесса стремительно растет, но остается недостаточно изученным. Чтобы восполнить эти пробелы, мы предлагаем принципиальную формулировку решения задач как детерминированного марковского процесса принятия решений; новую структуру FPS (Formal Problem-Solving), которая использует существующие среды FTP (формального доказательства теорем) для выполнения проверяемого на уровне процесса решения задач; и D-FPS (Deductive FPS), разделяющую решение и проверку ответа для лучшего согласования с человеческим мышлением. Доказаны выразительность, корректность и полнота предложенных структур. Мы создаем три эталона для оценки решения задач: FormalMath500, формализацию подмножества эталона MATH500; MiniF2F-Solving и PutnamBench-Solving, адаптации эталонов FTP MiniF2F и PutnamBench. Для достоверной, интерпретируемой и согласованной с человеческим мышлением оценки мы предлагаем RPE (Restricted Propositional Equivalence), символический подход для определения правильности ответов с помощью формальной проверки. Мы оцениваем четыре популярные модели FTP и два метода подсказок в качестве базовых, решая максимум 23,77% задач FormalMath500, 27,47% задач MiniF2F-Solving и 0,31% задач 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.