쌓인 기록에서 찾기
무엇을 찾으세요?
날짜를 몰라도 됩니다. 제목·Key Point·요약·태그를 한꺼번에 뒤집니다.
검색 범위부터 2026년 9월 24일 (목)까지932건
8건 · "Lean"조건 지우기 ×
OpenAI, 신흥 AI 모델 Jev를 빠르게 따라잡을 수 있을까
Key Point
OpenAI의 기술 역량과 기존 인프라가 Jev의 추격을 어렵게 만드는 요소가 무엇인지, 그리고 TypeSafe가 경쟁 우위를 지키려면 어디에 집중해야 하는지를 이해하는 데 필요하다.
핵심 요약
- TypeSafe의 Jev는 LLM의 토큰 확률 분포를 이용해 boolean, choice, score 같은 분류 작업을 수행하는 새로운 방식의 모델로 급속도로 채택되고 있다.
- OpenAI는 도구 호출과 응답 생성 같은 기능에서 이미 수년간 토큰 단위 마이크로 분류기를 암묵적으로 사용해왔으며, 이 기술을 Jev의 방식으로 명시적으로 학습하고 패키징할 수 있다.
- OpenAI가 같은 기술을 습득하면 Jev를 빠르게 복제할 수 있을 뿐 아니라, 기존 모델과 에이전트에 통합해 더 빠르고 저렴한 응답, 보안 강화, 모델 선택 최적화 같은 추가 가치를 제공할 수 있다.
- TypeSafe의 경쟁력은 학습 데이터와 학습 방식에 있으며, 이를 보호하지 못하면 OpenAI의 진입에 취약할 수 있다.
컴파일러 기법으로 Skia 그래픽 성능 최적화
Key Point
웹 브라우저와 그래픽 애플리케이션의 2D 렌더링 성능을 크게 개선할 수 있는 형식 검증 방법론이 제시되었으며, 실제 Chrome 데이터로 검증되었다.
핵심 요약
- Skia, CoreGraphics, Direct2D 같은 래스터화 라이브러리의 형식적 의미론을 정의한 μSkia를 개발했다.
- 복잡한 실행 모델 때문에 Google Chrome도 비효율적인 명령어를 생성하고 있다는 점을 발견했다.
- μSkia로 Chrome에서 찾은 4가지 부최적 코드 패턴을 분석하고 Lean으로 검증된 최적화 규칙을 만들었다.
- 상위 100개 웹사이트의 99개 Skia 프로그램에서 GPU 백엔드 대비 18.7% 성능 향상을 달성했다.
- 최적화는 최대 32μs 내에 완료되며, 다양한 웹사이트와 GPU에서 일관되게 효과를 보였다.
AI와 함께 50년 묵은 수학 난제 증명 성공
Key Point
AI가 인간과 협력해 순수 수학 난제를 해결할 수 있음을 보여주는 사례로, 형식 검증 시스템의 신뢰성이 수학 증명의 새로운 인정 방식이 될 수 있음을 시사한다.
핵심 요약
- 수학 비전공자가 Claude AI를 활용해 John Conway가 1976년에 제시한 초현실수 관련 미해결 난제를 Lean 증명으로 완성했다.
- 해당 난제는 omnific integers의 refinement property에 관한 Conway의 추측으로, 두 가지 인수분해가 공통 세분화를 가지는지를 묻는 문제다.
- 저자는 Claude에게 초현실수 분야의 흥미로운 문제를 골라달라 요청했고, Claude가 이 난제를 추천했다.
- 증명은 Palomar registry 기계 검증을 통과했으며 Lean과 해당 분야에 정통한 여러 사람이 정당성을 확인했다.
- 다만 독립적인 수학자 검증은 아직 이루어지지 않았으며, 저자는 반박을 공개적으로 초대하고 있다.
- 이 프로젝트에 1개월 이상의 자유 시간과 상당한 토큰을 투자했다.
Siri AI 탑재한 iOS·iPadOS·macOS 27 공개
Key Point
Apple의 차세대 운영체제에서 AI 에이스 어시스턴트의 구체적 기능과 한국어 지원 일정을 확인할 수 있다.
핵심 요약
- Apple Intelligence의 차세대 버전인 Siri AI가 iPhone, iPad, Mac, Apple Watch, Apple Vision Pro에 통합되어 개인 맥락 이해, 광범위한 세계 지식, 화면 인식 능력을 갖추고 롤아웃 시작했다.
- Siri AI는 영어로 베타 출시되며 프랑스어, 일본어, 한국어, 포르투갈어, 스페인어 지원은 10월 예정이다.
- 카메라 앱의 Siri 모드는 시각적 정보를 인식해 계산 분할, 지갑 추가 등 실시간 액션을 지원하고, Write with Siri는 음성 설명으로 문서 초안 작성을 돕는다.
- Safari의 탭 자동 정렬, 가격 변동 알림, Photos 앱의 공간 리프레이밍과 Clean Up 도구, 이미지 생성 기능이 추가되었다.
- 부모가 자녀의 앱 접근, 웹사이트 방문, 연락처를 단계적으로 승인하는 '나이 기반 보호 기능'이 강화되었으며, Communication Safety는 이제 폭력적 콘텐츠도 감지하고 차단한다.
AI가 나비에-스토크스 문제를 풀었다는 것의 의미
Key Point
형식적으로 증명되었다고 해서 수학의 진정한 진전이 이루어지는지, AI 시대 수학의 역할이 어떻게 재정의되어야 하는지를 다루는 근본적인 질문이기 때문이다.
핵심 요약
- OpenAI는 2026년 9월 밀레니엄 상금 문제 중 하나인 나비에-스토크스 존재성과 정칙성 문제의 해를 제시했다고 발표했다.
- AI가 제출한 것은 Lean 형식 증명과 비형식 증명 원고인데, 이는 논리적 증명(기계적 검증 가능)의 기준은 충족하지만 수학자가 원하는 이해 가능한 증명은 아닐 수 있다.
- 논리적 증명과 이해 가능한 증명은 역사적으로 함께 진행되었으나, AI로 인해 형식 증명만 남고 수학적 통찰력 없는 증명이 생겨날 수 있다.
- 수학은 문제 해결만이 아니라 새로운 개념 개발, 이론 구축, 질문 제기, 커뮤니티 형성, 아름다움 추구 등 훨씬 광범위한 활동이다.
- AI가 수학 문제를 '해결했다'는 서사는 수학이 단순히 문제 풀이이며 형식적 답만 중요하다는 두 가지 잘못된 가정에 기반한다.
OpenAI, Navier-Stokes 증명을 Lean 4 형식 증명으로 공개
Key Point
형식 검증 비용이 만 배 절감되면서 AI 증명 방식이 학문과 산업 전반의 검증 방식을 근본적으로 바꿀 수 있는 전환점이 되었다.
핵심 요약
- OpenAI가 유체역학의 오랜 난제인 Navier-Stokes 방정식을 증명하면서 동시에 Lean 4 형식 증명을 공개했다.
- 종전에는 수학 논문 한 페이지를 형식화하는 데 약 40시간이 소요되었으나, 이번 증명은 17시간 만에 Lean 형식으로 검증되었다.
- 166쪽 규모의 OpenAI 논문을 전통적 방식으로 형식화했다면 13만 2800인시가 필요했을 것으로 추정되어, 약 만 배의 비용 감소를 의미한다.
- 형식 증명의 비용이 급격히 낮아지면서 수학 연구뿐 아니라 보안 정책 검증, 스마트 계약 검증, 미션 크리티컬 알고리즘 검증 등이 현실화될 수 있다.
무료 오픈소스 시스템 클리너 Kudu 공개
Key Point
CCleaner 같은 폐쇄형 시스템 클리너 대신 투명하고 검증 가능한 오픈소스 대안을 찾는 사용자들이 신뢰할 수 있는 선택지가 생겼다.
핵심 요약
- Windows, macOS, Linux를 지원하는 무료 오픈소스 시스템 클리너 및 보안 스캐너 Kudu를 GitHub에서 공개했다.
- 임시 파일·캐시·레지스트리 정리, 악성코드 검사, 프라이버시 설정 제어, 성능 모니터링 등 30개 이상의 기능을 제공한다.
- 광고, 번들 소프트웨어, 과금 요구 없이 완전 무료이며 모든 코드가 공개되어 감시 가능하다.
- 스캔과 정리는 로컬에서만 처리되고, Kudu Cloud 기능은 사용자가 명시적으로 활성화할 때만 연결된다.
- TypeScript 기반으로 개발되었으며 30개 언어를 지원하고, 청소 규칙을 JSON으로 정의해 코딩 없이도 새 클리너를 추가할 수 있다.
- GitHub Releases에서 exe, dmg, AppImage, deb 포맷으로 다운로드할 수 있고 MIT 라이선스를 적용한다.
저장소 보기 ↗github.com