Pace system supports flexible math conjecture proof exploration
PACE: Research Proving Agent for Adaptive Conjecture Exploration
Artificial Intelligence
Summary
Traditional math-solving programs try to solve fixed problems, but real research often changes the questions as new insights arise. The authors designed PACE, a system that helps mathematicians explore and revise their conjectures while building proofs, tracking all assumptions and evidence carefully. They tested PACE on a set of known and open math challenges related to optimization, showing it can reconstruct proofs and create conditional results that experts evaluated positively.
What this means in practice
- •For software developers: Integrate PACE to assist in developing mathematical proofs for optimization algorithms requiring dynamic conjecture refinement.
- •For financial modelers: Employ PACE to explore and validate evolving mathematical models underpinning optimization in finance under changing market assumptions.
Authors
Shu Miao, Feiming Wang, Wentao Long, Chenyi Li, Kun Yuan, Zaiwen Wen
Abstract
Many mathematical research agents focus on solving problems with fixed statements. However, conjecture research, especially in applied mathematics, may require revising candidate questions or conclusions as investigation proceeds, coupling problem formulation with proof development. We present PACE, a research-proof agent that supports this process through a structured research loop that selects mathematical objectives and develops or challenges candidate mechanisms. The whole prover constructs proofs from these mechanisms, and an independent verifier checks them against the original target. Evidence-tracking memory stores assumptions and dependencies arising during research and marks evidence for revalidation when a candidate or condition changes. This memory supports task-specific context composition that keeps checked premises, exploratory material and unresolved obligations distinct. To evaluate proof construction and conjecture research, we introduce ResearchProofBench, an applied-mathematics benchmark focused on optimization, comprising 51 known-proof tasks with 331 hidden checkpoints under historical abstract access and six open-problem cases. The known-proof tasks assess reconstruction of published results, while the open-problem cases assess mathematical investigation and proof development. On the 51 known-proof tasks, PACE achieves an aggregate Proof Score of 75.16 and completes 20 proofs. In conjecture research, PACE develops conditional results, with its submissions receiving higher review scores than the compared baselines.