Sharp small-deviation inequalities for sums of independent nonnegative random variables

20년 묵은 확률 부등식 난제를 대형 언어모델이 증명하고 Lean으로 검증한 사례.

음이 아닌 독립 확률변수 합의 하한에 대한 날카로운 부등식을 증명한 확률론 논문이다. 델타가 1 이상인 구간에서 Feige 추측을 참으로 확정하고 모든 n에 대해 최적임을 보였다. 증명은 ChatGPT 5.6 Pro가 찾았고 Vlassis-Thomas 정리와 볼록기하 정리를 결합했다. Codex로 만든 Lean 형식증명으로 종단 간 검증까지 마쳤다.

핵심 요약

• Vlassis와 Thomas의 정확한 디리클레 보정 정리를 Grünbaum 무게중심 정리 등 볼록기하 결과와 결합했다.
• 0<δ<1과 δ≥1을 나누어 음이 아닌 독립 확률변수 합의 작은 편차 확률에 대한 명시적 하한을 증명했다.
• δ≥1에서는 모든 n에 대해 하한이 최적이며 1/e 이상이어서 Feige 추측을 확정한다.
• 이 결과는 독립적인 음이 아닌 확률변수 합의 하위 꼬리를 분석할 때 사용할 수 있는 날카로운 기준을 제공한다.
• 다만 모든 n에 대한 최적성은 δ≥1에서만 확립됐고 0<δ<1 구간의 하한은 같은 수준의 날카로움이 증명되지 않았다.

논문 링크

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