RMA: an Agentic System for Research-Level Mathematical Problems¶

🕒 Published (v1): 2026-05-20 04:54 UTC · Source: Arxiv · link

Why this paper was selected

RMA: agentic framework targeting research-level mathematics beyond competition benchmarks

Ask a follow-up

Open an assistant pre-loaded with this paper's context.

TL;DR¶

RMA (Research Math Agents) is a modular multi-agent agentic framework targeting research-level mathematical proof construction — a qualitatively harder regime than competition math or formal theorem proving. It coordinates three role-specialized agent types (Initializer, Proposer, Verifier) via a shared disk-based structured memory across multiple iterative rounds. On the First Proof benchmark (ten expert-contributed research problems), RMA solves 8/10 problems, outperforming GPT-5.2R and Aletheia from DeepMind.

Problem¶

Existing AI math systems target competition-style problems (MATH, IMO) or formal theorem proving in fixed formal contexts (Lean). Research-level mathematics requires: interpreting specialized definitions, retrieving and grounding in prior literature, constructing novel intermediate lemmas, and carrying out long chains of reasoning across many steps — none of which fit single-pass generation, competition-benchmark approaches, or formal proof assistants that assume fully-specified contexts. Generic auto-research agents also lack the structured reasoning and rigorous proof-gap detection needed for mathematical proofs.

Method¶

RMA is built on top of CLI-based coding agents (models issuing shell commands, reading/writing files, calling tools) and decomposes proof solving into six specialized modules:

Problem Analysis Module — applies formalization, decomposition, and constraint extraction operators to convert raw problem statements into structured subgoals.
Literature Search Module — uses the structured problem representation (not keyword matching) to retrieve relevant prior work from arXiv/MathSciNet/zbMATH, with query expansion for notation variants; critically, candidate paper lists are generated before retrieval to prevent solution leakage.
Fair Comparison Module — enforces (1) literature filtering to exclude known solutions, (2) context isolation (history reset per run), (3) sandboxed CLI execution, and (4) temporal control (model training cutoff August 2025 predates First Proof release February 2026).
Literature Understanding Module — extracts lemmas/techniques from retrieved papers, filters for compatibility with the current problem, and organizes them by role (e.g., which subgoal they support).
Knowledge Bank Module — a curated cheat-sheet of canonical inequalities, spectral bounds, and combinatorial identities (from standard textbooks), structured with explicit applicability conditions for direct reuse.
Proof Commandment Module — enforces grounding, faithfulness, gap-free reasoning, constructiveness, and LaTeX format correctness via structured prompts and rejection-based regeneration.

These modules are composed into role-specific workflows executed by three agent types: a single Initializer (produces initial draft, populates shared memory), \(K_p\) Proposers (identify proof gaps, invoke modules, write updated proof state), and \(K_v\) Verifiers (evaluate proof under Proof Commandment, write structured critiques to feedback state). All agents share a disk-based structured memory with five append-only partitions (Problem State, Literature Context, Knowledge Entries, Proof State, Feedback State), with role-specific read/write permissions enforced. Rounds alternate Proposer→Verifier for \(N\) total rounds, with feedback appended and used in the subsequent Proposer round.

Key Contributions¶

A modular agentic framework (RMA) decomposing research-level proof solving into six domain-specific modules, each implemented as a structured CLI-agent routine.
A multi-agent, multi-round instantiation with role-differentiated workflows (Initializer/Proposer/Verifier) and an append-only shared structured memory with enforced read/write permissions.
The Fair Comparison Module — a contamination-prevention protocol covering literature filtering, context isolation, sandboxing, and temporal controls, enabling controlled evaluation.
Comprehensive expert evaluation (ten mathematicians) on the First Proof benchmark; ablation studies showing that gains arise from interaction of all components rather than any single module.

Results¶

RMA solves 8/10 research-level problems on First Proof (expert-verified correct).
GPT-5.2R (OpenAI): solves fewer problems, produces looser bounds (e.g., constant \(1/256\) vs. RMA's tight \(1/42\) on Q6), and exhibits hallucinated references.
Aletheia (DeepMind): produces no successful output on at least one problem (Q6) within the time limit; overall solves fewer problems than RMA.
Agentic Researcher and Gemini Deep Research: underperform RMA in both problem-solving count and proof quality.
Ablation studies confirm that structured modules, multi-agent/multi-round interaction, shared memory, and role-specific workflows each contribute; no single component accounts for the full gain.
RMA's proofs are rated by mathematicians as more logically sound and readable than baselines.

(Table 1 with full per-problem counts is in the paper but truncated in the provided text.)

Limitations¶

Evaluated on only 10 problems (First Proof benchmark), a small set; generalization to broader research math domains is unknown.
Expert evaluation is inherently costly and not fully reproducible at scale; inter-rater agreement details are deferred to appendix.
The Fair Comparison Module's temporal control relies on the model training cutoff (August 2025); any model with later cutoff would require additional filtering.
Number of rounds \(N\) and agent counts \(K_p\), \(K_v\) are fixed hyperparameters; no adaptive termination criterion is described.
The system does not produce machine-checkable formal proofs (Lean/Coq), so correctness guarantees rest entirely on human expert review.
No cost/compute analysis provided; multi-agent multi-round runs over large literature retrievals are likely expensive.

Relevance to Harnesses / Meta-Harnesses¶

RMA is a textbook example of a domain-specialized meta-harness: it wraps CLI-based coding agents inside a layered orchestration shell that enforces module sequencing, memory partitioning with read/write ACLs, role-specific workflows, and multi-round feedback loops — the same structural concerns (state management, contamination control, role specialization, iterative refinement) that recur in general-purpose agent harnesses. The Fair Comparison Module is particularly notable as an explicit harness-level concern (sandboxing, context isolation, temporal gating) that is decoupled from reasoning logic. The append-only, agent-ID-stamped shared disk memory architecture is a concrete implementation pattern for multi-agent harnesses where write conflicts must be avoided without a centralized lock manager. For researchers building harnesses, RMA demonstrates how domain-specific invariants (gap-free proofs, grounded citations) can be encoded as module-level contracts enforced by the harness rather than left to individual agent prompts.