기술 요약: Dual Agent를 통한 볼록 완화(Convex Relaxation)의 AI 보조 발견

1. 문제 정의

본 논문은 함수 해석학에서의 날카로운 상수(sharp-constant) 부등식을 위한 **인증된 하한(certified lower bounds)**을 개선하는 과제를 다룹니다. 구체적으로는, 가용한 함수들의 무한 차원 공간에서 점수(score)의 하한(infimum)을 찾는 비볼록 최적화(nonconvex optimization) 문제에 초점을 맞춥니다.

저자들은 Georgiev 등(2025)이 연구한 두 가지 특정 상수를 목표로 합니다:

1. 제1 자기상관 부등식 (C6.2): Sidon 집합과 관련된 조합론에서의 상수로, 다음 부등식에 의해 정의됩니다:
   $$\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$$
   여기서 모든 비음수 함수 $f: \mathbb{R} \to \mathbb{R}$에 대해 성립합니다.
2. Erdős 최소 중첩 상수 (C6.5): 최소 중첩 문제의 점근적 거동을 결정하는 상수로, 다음과 같이 정의됩니다:
   $$\sup_{x \in [-2, 2]} \int_{-1}^{1} f(t)g(x+t) \, dt \ge C_{6.5}$$
   여기서 $f, g: [-1, 1] \to [0, 1]$은 비음수이며 $f+g=1$ 및 $\int f = 1$을 만족합니다.

최근의 AI 기반 연구들은 극한 구성(extremal constructions, 즉 부등식을 위반하는 특정 함수)을 탐색함으로써 **상한(upper bounds)**을 개선하는 데 성공했지만, **하한(lower bounds)**을 개선하는 것은 이와 다릅니다. 하한은 모든 가용한 함수에 대해 성립해야 하므로, 어떤 함수도 점수를 특정 값 아래로 떨어뜨릴 수 없음을 증명하는 과정이 필요합니다. 이는 일반적으로 원래의 비볼록 문제를 해결하기 위한 **볼록 완화(convex relaxation)**를 푸는 방식으로 이루어집니다. 완화가 더 정교할수록(즉, 더 많은 유효한 제약 조건이 추가될수록), 하한은 더 강력해집니다.

2. 방법론: Dual-Agent 루프

저자들은 두 개의 특화된 대규모 언어 모델(LLM) 에이전트에 의해 구동되는 인간 참여형(human-in-the-loop) 프레임워크를 사용하여 **자기 연구 패러다임(autoresearch paradigm)**을 구현했습니다. 이 시스템은 유효한 제약 조건을 반복적으로 발견하고 검증하여 볼록 완화를 강화하도록 설계되었습니다.

에이전트 구성

1. 코딩 에이전트 (Coding Agent):

   • 역할: 볼록 프로그램에 대한 새로운 제약 조건을 제안하거나 기존 제약 조건을 강화합니다.
   • 출력: 수정된 볼록 최적화 프로그램을 생성하고, 해당 새로운 제약 조건이 모든 가용한 함수에 대해 왜 성립하는지에 대한 "엄밀한 증명"(수학적 논거)을 생성합니다.
   • 동작: 코드로 제약 조건을 구현하고(CVXPY 사용), 프로그램을 풀어 후보 하한을 산출합니다.

2. 이론 에이전트 (Theory Agent):

   • 역할: 검증자 및 반례 탐색자 역할을 수행합니다.
   • 동작: 제안된 제약 조건과 그 증명을 읽습니다. 제안된 제약 조건이 가용성 조건(예: $f \ge 0$)의 필연적 결과인지 확인하기 위해 논리를 비판적으로 분석합니다. 결정적으로, 제안된 제약 조건을 위반하는 계수를 가진 특정 가용 함수(반례)를 적극적으로 찾습니다.
   • 결정: 증명이 타당하고 반례가 발견되지 않으면 제약 조건을 수락합니다. 만약 결함이나 반례가 발견되면 제안을 거부하고, 코딩 에이전트에게 다른 접근 방식을 시도하도록 지시합니다.

검증 파이프라인

최종 결과가 (단순한 수치적 추정이 아닌) 수학적으로 증명된(certified) 하한임을 보장하기 위해, 시스템은 엄격한 이중 인증(dual-certification) 과정을 사용합니다:

• 쌍대 타당성 (Dual Feasibility): 시스템은 볼록 프로그램의 쌍대(dual) 문제를 구성합니다.
• 구간 산술 (Interval Arithmetic): 쌍대 실행 가능한 점 $\lambda$를 찾고, 엄격한 구간 산술을 사용하여 그 타당성과 쌍대 목적 함수 값을 검증합니다. 이는 부동 소수점 반올림 오차와 무리수 데이터(예: 삼각 모멘트)를 처리합니다.
• 인증 (Certification): 약쌍성(weak duality)에 의해, 목적 함수 값이 $\beta$인 유효한 쌍대 점 $\lambda$는 원형 문제의 최적값(따라서 진정한 상수)이 적어도 $\beta$임을 증명합니다. 최종 보고된 하한은 검증된 포위 영역(enclosure)의 하한값입니다.

인간의 역할

인간 연구자는 최종 검토 및 **압축(compactification)**을 수행합니다. 에이전트 루프는 종종 중복된 제약 조건을 축적합니다. 인간은 최종 프로그램을 검토하여 불필요한 제약 조건을 제거함으로써 최소한의 읽기 쉬운 공식을 만들고, 최종 인증 전 수학적 논거를 검증합니다.

3. 주요 기여

• 패러다임의 전환: 본 논문은 단순히 극한의 예를 찾는 것을 넘어, 볼록 완화의 발견에 AI 에이전트를 적용한 새로운 사례를 보여줍니다. 이는 존재적 양화(특정 함수 찾기)가 아닌 보편적 양화(모든 함수에 대한 유효성 증명)를 요구하는 부등식의 "하한" 측면을 다룹니다.
• Dual-Agent 프레임워크: 코딩 에이전트가 제약 조건을 제안하고 이론 에이전트가 유효성을 검증하며 반례를 추적하는 특정 루프를 도입하여, 수학적 완화의 반복적인 정교화 과정을 자동화했습니다.
• 엄격한 인증: 구간 산술과 쌍대 실행성 체크의 통합은 개선된 하한이 부동 소수점 정밀도와 무관하게 수학적으로 인증되었음을 보장합니다.

4. 결과

이 프레임워크는 위에서 언급한 두 가지 상수에 적용되어 인증된 하한을 개선했습니다:

• C6.2 (제1 자기상관 부등식):

  • 이전 최적 하한: 1.28 (Cloninger & Steinerberger, 2017).
  • 새로운 인증된 하한: 1.2937.
  • 참고: 이 문제에 대한 기존의 볼록 프로그램은 존재하지 않았으며, 에이전트들이 처음부터 이를 구축했습니다.

• C6.5 (Erdős 최소 중복 상수):

  • 이전 최적 하한: 0.379005 (White, 2022).
  • 새로운 인증된 하한: 0.37912.
  • 참고: 에이전트들은 White의 기존 볼록 프로그램에서 시작하여, **보흐너 정리(Bochner's theorem)**에 기반한 두 가지 새로운 유효 제약 조건($f$와 그 여집합 $g=1-f$의 모멘트 수열이 비음수 측도에 의해 실현 가능하다는 조건)을 발견했습니다.

본 논문은 상한의 경우 탐색 기반 방법(예: Together AI, 2026)에 의해 개선되었으나, 하한은 2022년 이후 정체되어 있었다고 언급합니다. 본 연구는 이러한 하한을 성공적으로 전진시켰습니다.

5. 의의 및 주장

저자들은 이 특정 부등식들에 대해 인증된 하한을 개선하기 위해 오토리서치 스타일의 에이전트 루프를 사용한 첫 번째 사례라고 주장합니다. 그 의의는 다음과 같습니다:

1. 상호 보완성: 극한의 예(상한)를 찾는 데 집중하는 기존 AI 연구를 보완하여, 완화를 통해 하한을 증명하는 더 어려운 문제를 다룹니다.
2. 발견의 자율성: 에이전트들은 이전의 인간 설계 공식들이 간과했거나 명시적으로 부과하지 못했던 수학적 성질(예: $f$와 $1-f$에 대한 보흐너 조건)을 성공적으로 식별했습니다.
3. 일반성: 자기상관 부등식에 대해 시연되었으나, 저자들은 이 프레임워크가 특정 문제에 국한되지 않는다고 밝힙니다. 이는 하한이 볼록 완화와 제약 조건의 강화 및 쌍대성을 통한 인증으로 표현될 수 있는 모든 최적화, 조합론, 제어 이론 등의 분야에 적용 가능합니다.

논문은 현재 제약 조건의 유효성이 형식 증명 도구(예: Lean)가 아닌 인간의 검토에 의존하고 있음을 인정하며, 향후 형식 검증 도구와의 통합을 통해 루프를 완전히 자율화할 수 있을 것이라고 제언하며 겸허히 마무리합니다.