Technical Summary: AI-Assisted Discovery of Convex Relaxations via Dual Agents

1. Problem Statement

The paper addresses the challenge of improving certified lower bounds for sharp-constant inequalities in functional analysis, specifically focusing on nonconvex optimization problems where the goal is to find the infimum of a score over an infinite-dimensional space of admissible functions.

The authors target two specific constants studied by Georgiev et al. (2025):

1. The First Autocorrelation Inequality (C6.2): A constant arising in additive combinatorics related to Sidon sets, defined by the inequality:
   $$\max_{-1/2 \le t \le 1/2} \int_{\mathbb{R}} f(t-x)f(x) \, dx \ge C_{6.2} \left( \int_{-1/4}^{1/4} f(x) \, dx \right)^2$$
   for all non-negative $f: \mathbb{R} \to \mathbb{R}$.
2. The Erdős Minimum Overlap Constant (C6.5): A constant governing the asymptotics of the minimum overlap problem, defined as:
   $$\sup_{x \in [-2, 2]} \int_{-1}^{1} f(t)g(x+t) \, dt \ge C_{6.5}$$
   for non-negative $f, g: [-1, 1] \to [0, 1]$ with $f+g=1$ and $\int f = 1$.

While recent AI-driven work has successfully improved upper bounds by searching for extremal constructions (specific functions that violate a bound), improving lower bounds is distinct. A lower bound must hold for every admissible function, requiring a proof that no function can drive the score below a certain value. This is typically achieved by solving a convex relaxation of the original nonconvex problem. The tighter the relaxation (i.e., the more valid constraints added), the stronger the lower bound.

2. Methodology: The Dual-Agent Loop

The authors instantiate an autoresearch paradigm using a human-in-the-loop framework driven by two specialized Large Language Model (LLM) agents. The system is designed to iteratively discover and verify valid constraints that tighten a convex relaxation.

The Agents

1. Coding Agent:

   • Role: Proposes new constraints or strengthens existing ones for the convex program.
   • Output: Generates a modified convex optimization program and a "rigorous proof" (a mathematical argument) justifying why the new constraint holds for all admissible functions.
   • Action: Implements the constraint in code (using CVXPY) and solves the program to produce a candidate lower bound.

2. Theory Agent:

   • Role: Acts as a verifier and counterexample searcher.
   • Action: Reads the proposed constraint and its proof. It critically analyzes the logic to ensure the constraint is a necessary consequence of the admissibility conditions (e.g., $f \ge 0$). Crucially, it actively searches for counterexamples—specific admissible functions whose coefficients violate the proposed constraint.
   • Decision: If the proof is sound and no counterexample is found, the constraint is accepted. If a flaw or counterexample is found, the proposal is rejected, and the Coding Agent is directed to try a different approach.

The Verification Pipeline

To ensure the final result is a certified bound (mathematically proven, not just numerically estimated), the system employs a rigorous dual-certification process:

• Dual Feasibility: The system constructs the dual of the convex program.
• Interval Arithmetic: It finds a dual-feasible point $\lambda$ and verifies its feasibility and the dual objective value using rigorous interval arithmetic. This accounts for floating-point rounding errors and irrational problem data (e.g., trigonometric moments).
• Certification: By weak duality, a valid dual point $\lambda$ with objective value $\beta$ proves that the primal optimum (and thus the true constant) is at least $\beta$. The final reported bound is the lower endpoint of a verified enclosure.

Human Role

A human researcher performs a final review and compactification. The agent loop often accumulates redundant constraints. The human reviews the final program, removes unnecessary constraints to create a minimal, readable formulation, and verifies the mathematical arguments before the final certification.

3. Key Contributions

• Paradigm Shift: The paper demonstrates a novel application of AI agents to the discovery of convex relaxations rather than just searching for extremal examples. It addresses the "lower bound" side of inequalities, which requires proving universal quantification (validity for all functions) rather than existential quantification (finding one function).
• Dual-Agent Framework: It introduces a specific loop where a coding agent proposes constraints and a theory agent verifies validity and hunts for counterexamples, effectively automating the iterative refinement of mathematical relaxations.
• Rigorous Certification: The integration of interval arithmetic and dual-feasibility checks ensures that the improved bounds are mathematically certified, independent of the numerical solver's floating-point precision.

4. Results

The framework was applied to the two constants mentioned above, improving the certified lower bounds:

• C6.2 (First Autocorrelation Inequality):

  • Previous Best Lower Bound: 1.28 (Cloninger & Steinerberger, 2017).
  • New Certified Lower Bound: 1.2937.
  • Note: No prior convex program existed for this problem; the agents constructed one from scratch.

• C6.5 (Erdős Minimum Overlap Constant):

  • Previous Best Lower Bound: 0.379005 (White, 2022).
  • New Certified Lower Bound: 0.37912.
  • Note: The agents started from White's existing convex program and discovered two new valid constraints based on Bochner's theorem (enforcing that the moment sequences of both $f$ and its complement $g=1-f$ are realizable by non-negative measures).

The paper notes that the upper bounds for these problems have been improved by search-based methods (e.g., Together AI, 2026), but the lower bounds had remained stagnant since 2022. This work successfully moves the lower bounds forward.

5. Significance and Claims

The authors claim this is the first use of an autoresearch-style agentic loop to improve certified lower bounds on these specific inequalities. The significance lies in:

1. Complementarity: It complements existing AI research that focuses on finding extremal examples (upper bounds) by tackling the harder problem of proving lower bounds via relaxation.
2. Autonomy in Discovery: The agents successfully identified mathematical properties (such as the Bochner conditions for $f$ and $1-f$) that previous human-designed formulations had overlooked or failed to impose explicitly.
3. Generality: While demonstrated on autocorrelation inequalities, the authors state the framework is not specific to these problems. It applies to any nonconvex optimization where a lower bound can be expressed as a convex relaxation tightened by valid constraints and certified by duality (e.g., in optimization, combinatorics, and control).

The paper concludes modestly, acknowledging that the validity of the constraints currently relies on human review of the mathematical arguments rather than formal proof assistants (like Lean), though it suggests that future integration with formal verification tools could make the loop fully autonomous.