Search arXiv⌕ Search

arXiv · 2610.33690

PACE: Research Proving Agent for Adaptive Conjecture Exploration

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.

Explore related subjects

Keep this discovery

Explore connections, maps & timelines

BibTeXRIS

Shu Miao, Feiming Wang, Wentao Long, Chenyi Li, Kun Yuan, Zaiwen Wen. 2026-10-24. PACE: Research Proving Agent for Adaptive Conjecture Exploration. https://arxiv.org/abs/2610.33690

Cite the original work for its findings. Save a collection to share your selection of sources.

KEEP EXPLORING

Related papers

Evaluating Harmful Memorization in LLM Code Generation

Assessing memorization in LLM code generation is challenging because code reuse is not inherently harmful. Correct programs often share APIs, templates, and algorithmic idioms, so code similarity alone may reflect benign reuse rather than problematic memorization. We focus on the harmful case: a model fails to adapt when task semantics change and instead produces code that remains highly similar to the original solution. We propose \emph{code rewriting}, an automated semantic perturbation pipeline that constructs superficially similar but semantically different variants of existing coding tasks by modifying a core logic element of the reference solution and regenerating the corresponding prompt. To summarize this behavior, we introduce the \emph{Harmful Memorization Index} (HMI), an operational diagnostic that combines similarity to the original solution with performance degradation on rewritten tasks. We use harmful memorization as an operational behavioral term for this specific failure mode; HMI does not establish whether an original task or solution appeared in a model's training data. HMI is intended to complement standard accuracy metrics by capturing brittleness under small semantic changes. Across MBPP+ and BigCodeBench, we find that: (1) HMI does not monotonically increase with model scale and often decreases on simpler tasks; (2) high-HMI failures are concentrated in specific logic-edit types, especially constraint changes and data transformations; (3) supervised fine-tuning improves original-task accuracy but can substantially increase HMI on held-out tasks; and (4) across the evaluated post-training settings, PPO yields a more favorable accuracy--HMI trade-off than SFT.

cs.AI↗

Efficient Generation of Diverse Cooperative Agents with World Models

A major bottleneck in the training process for Zero-Shot Coordination (ZSC) agents is the generation of diverse partner agents via Population-based Training (PBT). Prominent PBT methods, such as Cross-play Minimization (XPM), can be very computationally expensive and sample inefficient, as the training objective requires sampling multiple types of trajectories, in particular the need of Mixed-Play (MP) trajectories to mitigate self-sabotage in cross-play. Each partner agent in the population is also trained from scratch, despite all of the partners in the population learning policies of the same coordination task. In this work, we propose that simulated trajectories from the dynamics model of an environment can drastically speed up the training process for XPM methods. We introduce XPM-WM, a framework for generating simulated trajectories for XPM via a learned World Model (WM). We show XPM with simulated trajectories removes the need to sample Mixed-Play trajectories while still mitigating any self-sabotage. The learned WM also bootstraps the training of subsequent agents in the population. We show that these two factors combined gives XPM-WM significantly better sample efficiency as compared to other XPM methods and scales linearly to the size of the population. We show our proposed method can effectively generate partners with diverse conventions that match the performance of previous methods. Finally, we show that our proposed training paradigm of using learned world models to generate diverse population can be extended to other PBT methods beyond XPM.

cs.AI↗

Agentic AI Empowered Intent-Based Networking for 6G

The transition towards sixth-generation (6G) wireless networks necessitates autonomous orchestration mechanisms capable of translating high-level operational intents into executable network configurations. Existing approaches to Intent-Based Networking (IBN) rely upon either rule-based systems that struggle with linguistic variation or end-to-end neural models that lack interpretability and fail to enforce operational constraints. This paper presents a hierarchical multi-agent framework where Large Language Model (LLM) based agents autonomously decompose natural language intents, consult domain-specific specialists, and synthesise technically feasible network slice configurations through iterative reasoning-acting (ReAct) cycles. The proposed architecture employs an orchestrator agent coordinating two specialist agents, namely Radio Access Network (RAN) and Core Network agents, via ReAct-style reasoning, grounded in structured network state representations. Experimental evaluation across diverse benchmark scenarios demonstrates that the proposed system outperforms monolithic agents, rule-based systems, and direct LLM prompting, with architectural principles applicable to Open RAN (O-RAN) deployments. The results also demonstrate that whilst contemporary LLMs possess substantial general telecommunications knowledge, structured prompt engineering encoding domain-specific decision thresholds and operational policies is essential for reliable network automation performance.

cs.AI↗