LongTails: Automated Research in Optimization

이 논문은 최적화 이론의 복잡도 상한을 에이전트가 찾고 Lean 4로 형식 검증하게 만든 자동 연구 틀을 만들었다.

이 논문은 한마디로 최적화 알고리즘의 이론 보장을 에이전트가 찾고 형식 검증까지 하게 만든 자동 연구 프레임워크다. 저자들은 문제 설정과 복잡도 목표를 분리해 정의했다. 에이전트는 더 나은 복잡도를 증명하는 알고리즘을 찾고 틀이 증명을 검사한다. 이렇게 이미 100개 넘는 새 결과를 얻었다.

핵심 요약

• 저자들은 최적화 문제의 복잡도 상한을 찾고 개선하는 자동 연구 프레임워크 LongTails를 만들었다.
• 틀은 문제 설정을 정의하는 Setup과 목표 예산을 정의하는 Complexity로 나눠 명세를 분리했다.
• 에이전트가 알고리즘을 설계하고 수렴을 증명하면 틀이 증명을 검사해 인정된 복잡도가 실제로 도달 가능함을 보장했다.
• 모든 검증은 Lean 4 형식 증명 도구로 수행되었다.
• 저자들은 이미 100개 넘는 새 결과를 얻었다고 밝혔다.
• 에이전트가 더 나은 복잡도를 얻는 단일 실행은 약 2–7 hours 걸렸다.

논문 링크

외부 연구를 정리한 자료입니다. HDATF가 발표한 논문이나 제품 성능을 측정한 결과는 아닙니다.