AI-Assisted Discovery of Convex Relaxations via Dual Agents

Motivation

• Known: 기존 연구(Georgiev et al., 2025 등)는 LLM/evolutionary 탐색으로 극단 함수(extremal construction)를 찾아 sharp-constant inequality의 upper bound를 개선하는 데 성공했으며, autocorrelation inequality와 Erdős minimum overlap 문제의 lower bound는 수작업 analytic/duality 논증(Cloninger & Steinerberger, White 2022)으로 얻어져 있었다.
• Gap: Lower bound는 모든 admissible function에 대해 성립해야 하는 전칭 명제로, convex relaxation을 통해서만 증명 가능하며 더 tight한 relaxation을 찾는 것은 반복적이고 open-ended한 작업임에도, 이를 AI 에이전트가 자동으로 발견하고 엄밀하게 검증하는 방법은 아직 다루어지지 않았다.
• Why: Lower bound는 수학적 정리의 형태로 증명되어야 하며 잘못된 constraint 하나가 전체 결과를 무효화할 수 있기 때문에, 단순히 값을 최적화하는 upper bound 탐색과 달리 correctness 검증이 핵심 난제이다. 이를 해결하면 AI가 단순 탐색 도구를 넘어 실제 수학적 증명 발견에 기여할 수 있음을 보여준다.
• Approach: coding agent가 기존 convex relaxation에 tightening constraint를 반복적으로 제안하고, theory agent가 각 constraint의 유효성을 rigorous하게 검증하며 반례를 탐색하는 dual-agent 루프를 autoresearch paradigm으로 구성하고, 최종 bound는 interval arithmetic으로 검증된 explicit dual-feasible point로 certify한다.

Achievement

1. Lower bound 개선: Georgiev et al. (2025)의 두 상수, first autocorrelation inequality (C6.2)의 lower bound를 1.28에서 1.2937로, Erdős minimum-overlap constant (C6.5)의 lower bound를 0.379005에서 0.37912로 개선했다.
2. Dual-agent 프레임워크 제안: coding agent와 theory agent를 분리하여 relaxation 제안과 rigorous 검증(반례 탐색 포함)을 분업시키는 구조를 설계했다.
3. 엄밀한 certification 체계 확립: 모든 보고된 bound가 explicit dual-feasible point와 interval arithmetic 검증을 통해 solver-independent하게 검증 가능하도록 했다.
4. autoresearch paradigm의 새로운 적용 사례 제시: 기존에 upper bound(구성적 예시) 탐색에만 쓰이던 agentic 접근을 lower bound(증명 기반) 발견에 최초로 적용했다.

How

• 문제를 White (2022)의 방식을 따라 무한차원 min-max nonconvex 문제를 유한 개 변수(cell integral, Fourier coefficient, truncation slack 등)로 구성된 convex program으로 reduction한다.
• 각 admissible f가 induce하는 변수들이 만족해야 하는 제약 중 convex한 것만 남겨 feasible set K를 구성하고, 이 relaxation의 최적값 r이 항상 실제 상수 p보다 작거나 같음(r ≤ p)을 보장한다.
• coding agent가 relaxation에 새로운 tightening constraint를 반복적으로 제안(edit-benchmark-improve 루프)한다.
• theory agent가 제안된 각 constraint가 실제로 모든 admissible f에 대해 성립하는지 rigorous하게 검증하고, 위반하는 counterexample을 탐색한다.
• 최종적으로 얻어진 relaxation에 대해 weak duality를 이용, dual-feasible point λ를 explicit하게 구성하고 dual objective d(λ)를 interval arithmetic으로 rigorous하게 계산하여 인증된 lower bound d(λ) ≤ r ≤ p를 제공한다.

Originality

• 기존 AI-보조 수학 연구가 주로 extremal construction 탐색을 통한 upper bound 개선에 집중되었던 것과 달리, 본 논문은 convex relaxation 발견을 통한 lower bound 개선이라는 상보적 방향을 최초로 자동화했다.
• 단일 에이전트가 아닌 coding agent와 theory agent로 역할을 분리하여, 제안(생성)과 검증(증명)을 독립적으로 수행하게 함으로써 잘못된 relaxation이 결과에 반영되는 위험을 구조적으로 완화했다.
• 수치적으로 보고된 optimal value가 아니라 explicit dual-feasible point와 interval arithmetic을 통한 rigorous certification을 결합하여, agent가 생성한 결과의 수학적 신뢰성을 담보하는 방법론을 제시했다.

Limitation & Further Study

• 검증된 사례가 C6.2, C6.5 두 개의 특정 autocorrelation/minimum-overlap 상수에 국한되어 있어, 다른 유형의 sharp-constant inequality나 더 일반적인 nonconvex 최적화 문제에 대한 일반화 가능성은 추가 검증이 필요하다.
• theory agent의 검증이 여전히 특정 constraint 형태(대칭성, even function 등 제한적 구조)에 의존할 가능성이 있으며(Figure 5의 even function limitation 사례 언급), 완전히 임의의 relaxation 제안에 대한 rigorous 검증의 확장성은 불분명하다.
• 개선폭(1.28→1.2937, 0.379005→0.37912)이 크지 않아, 이 방법이 upper bound(construction) 탐색만큼 극적인 성능 향상을 가져오는지, 그리고 사람 연구자 대비 시간/비용 효율성이 어느 정도인지에 대한 정량적 비교가 부족하다.
• 후속 연구로는 더 다양한 sharp-constant inequality 클래스에 대한 일반화, agent 루프의 실패/반례 발견 실패 확률에 대한 통계적 분석, 그리고 완전 자동화된 end-to-end 증명 검증 파이프라인(Lean 등 formal verification과의 결합) 등이 필요하다.

Evaluation

총평: AI 보조 수학 연구에서 기존에 다뤄지지 않았던 lower bound/convex relaxation 발견이라는 방향을 dual-agent 구조와 rigorous certification으로 구현하여 실질적인 상수 개선을 이뤄낸, 방법론적으로 신선하고 실용적 기여가 있는 논문이다.