쌓인 기록에서 찾기
무엇을 찾으세요?
날짜를 몰라도 됩니다. 제목·Key Point·요약·태그를 한꺼번에 뒤집니다.
검색 범위부터 2026년 9월 19일 (토)까지674건
3건 · "형식화"조건 지우기 ×
001▲ 133 · 댓글 90ML 에이전트는 왜 벤치마크에 오버피팅되지 않을까반복적인 벤치마크 평가에도 불구하고 ML 모델이 오버피팅되지 않는 현상을 Amazon Science 연구진이 설명했다.AI · 머신러닝 · Why don't machine learning research agents overfit?
ML 에이전트는 왜 벤치마크에 오버피팅되지 않을까
Key Point벤치마크 기반 ML 연구가 실제로 진전을 이루는 이유를 처음으로 실험적으로 검증한 연구로, 정보 압축성이 오버피팅을 방지하는 메커니즘을 밝혔다.
핵심 요약
- 반복적인 벤치마크 평가에도 불구하고 ML 모델이 오버피팅되지 않는 현상을 Amazon Science 연구진이 설명했다.
- 성공적인 ML 에이전트의 전략은 매우 압축 가능하며, 16개 토큰 수준으로 축약해도 새 에이전트가 원래 성능을 재현할 수 있다는 점에서 데이터 암기가 아닌 실제 구조를 학습함을 보여준다.
- 진정한 오버피팅 전략은 정보 병목을 통과하면 벤치마크 성과가 사라진다는 압축 테스트로 진단할 수 있다.
- LLM은 강력한 압축 디코더로서 전문가 단축 프롬프트로부터 전체 ML 파이프라인을 재구성할 수 있으며, 이는 이들의 뛰어난 성능을 설명하는 구체적 방식이다.
- 오캄의 면도날을 수학적으로 형식화하면, 데이터 암기보다 훨씬 적은 비트로 표현 가능한 가설은 새 데이터에서도 잘 작동해야 한다.
AI · 머신러닝 · After Math
AI가 나비에-스토크스 문제를 풀었다는 것의 의미
Key Point형식적으로 증명되었다고 해서 수학의 진정한 진전이 이루어지는지, AI 시대 수학의 역할이 어떻게 재정의되어야 하는지를 다루는 근본적인 질문이기 때문이다.
핵심 요약
- OpenAI는 2026년 9월 밀레니엄 상금 문제 중 하나인 나비에-스토크스 존재성과 정칙성 문제의 해를 제시했다고 발표했다.
- AI가 제출한 것은 Lean 형식 증명과 비형식 증명 원고인데, 이는 논리적 증명(기계적 검증 가능)의 기준은 충족하지만 수학자가 원하는 이해 가능한 증명은 아닐 수 있다.
- 논리적 증명과 이해 가능한 증명은 역사적으로 함께 진행되었으나, AI로 인해 형식 증명만 남고 수학적 통찰력 없는 증명이 생겨날 수 있다.
- 수학은 문제 해결만이 아니라 새로운 개념 개발, 이론 구축, 질문 제기, 커뮤니티 형성, 아름다움 추구 등 훨씬 광범위한 활동이다.
- AI가 수학 문제를 '해결했다'는 서사는 수학이 단순히 문제 풀이이며 형식적 답만 중요하다는 두 가지 잘못된 가정에 기반한다.
AI · 머신러닝 · OpenAI’s Navier-Stokes release included a Lean 4 formal proof
OpenAI, Navier-Stokes 증명을 Lean 4 형식 증명으로 공개
Key Point형식 검증 비용이 만 배 절감되면서 AI 증명 방식이 학문과 산업 전반의 검증 방식을 근본적으로 바꿀 수 있는 전환점이 되었다.
핵심 요약
- OpenAI가 유체역학의 오랜 난제인 Navier-Stokes 방정식을 증명하면서 동시에 Lean 4 형식 증명을 공개했다.
- 종전에는 수학 논문 한 페이지를 형식화하는 데 약 40시간이 소요되었으나, 이번 증명은 17시간 만에 Lean 형식으로 검증되었다.
- 166쪽 규모의 OpenAI 논문을 전통적 방식으로 형식화했다면 13만 2800인시가 필요했을 것으로 추정되어, 약 만 배의 비용 감소를 의미한다.
- 형식 증명의 비용이 급격히 낮아지면서 수학 연구뿐 아니라 보안 정책 검증, 스마트 계약 검증, 미션 크리티컬 알고리즘 검증 등이 현실화될 수 있다.