쌓인 기록에서 찾기
무엇을 찾으세요? 날짜를 몰라도 됩니다. 제목·Key Point·요약·태그를 한꺼번에 뒤집니다.
검색 범위 2026년 8월 13일 (목) 부터 2026년 11월 3일 (화)까지 3800건
18건 · "형식 검증"조건 지우기 ×
001 00:11 ▲ 18 · 댓글 2 자동 정리 증명, 복잡한 워크플로우보다 단순 반복 루프가 더 효과적 형식 정리 증명(formal theorem proving) 분야는 계획, 분해, 전문 도구 연계 등 인간이 설계한 복잡한 워크플로우에 의존해왔으나, 비형식 수학은 대규모 언어 모델의 연쇄 추론으로 진전을 이뤄왔다. AI · 머신러닝 · h1: A Taste of the Bitter Lesson in Automated Theorem Proving
Key Point 자동화된 정리 증명에서 복잡한 설계 워크플로우 대신 단순한 에이전트 루프가 더 효과적일 수 있다는 발견은, 향후 형식 검증 시스템을 어떻게 구축할 것인지에 대한 근본적인 접근 방향을 바꿀 수 있다.
핵심 요약
형식 정리 증명(formal theorem proving) 분야는 계획, 분해, 전문 도구 연계 등 인간이 설계한 복잡한 워크플로우에 의존해왔으나, 비형식 수학은 대규모 언어 모델의 연쇄 추론으로 진전을 이뤄왔다. 이 논문은 '비터 레슨' 질문을 제기한다: 테스트 타임 계산을 확장하는 단순한 에이전트 루프가 이런 복잡한 워크플로우와 경쟁할 수 있는가? h1이라는 단순한 도구를 개발했는데, 이는 모델에게 Lean 4의 효율적인 인터페이스를 제공하고 검증자 피드백과 자기 성찰로 작동하며, 명시적 분해나 탐색 구조를 강요하지 않는다. 전체 요약 7문장 읽기 → 002 15:11 ▲ 113 · 댓글 37 클라우드플레어 AI 모델서 사용자 데이터 노출, 155건 영향 클라우드플레어의 Workers AI에서 제공하는 GLM-5.3 모델에서 한 사용자의 응답이 다른 사용자의 요청 데이터를 포함하는 테넌트 격리 문제가 발생했다. 보안 · Cross-request KV cache exposure in the GLM-5.3 Workers AI model (155 responses)
Key Point 컨텍스트 윈도우와 실제 메모리 풀 크기의 불일치가 추론 엔진의 버그와 결합되어 사용자 간 데이터 유출을 초래한 사례로, disaggregated 구조의 AI 추론 서비스를 운영하는 회사들이 참고해야 할 설정·배포 체크리스트와 업스트림 수정 사항을 제시한다.
핵심 요약
클라우드플레어의 Workers AI에서 제공하는 GLM-5.3 모델에서 한 사용자의 응답이 다른 사용자의 요청 데이터를 포함하는 테넌트 격리 문제가 발생했다. 8월 27일부터 9월 9일까지 681,280토큰을 초과하는 긴 프롬프트에 대한 응답 155건이 영향을 받았으며, 의도적인 악용 흔적은 없었다. 근본 원인은 두 가지였다: 첫째, GLM-5.3의 KV 캐시 풀 크기(681,280토큰)가 선언된 컨텍스트 윈도우(1,048,576토큰)보다 작았고, 둘째, 오픈소스 추론 엔진 SGLang에서 초과 길이 요청을 disaggregated prefill/decode 모드로 처리할 때 거부된 요청을 제대로 중단하지 않는 버그가 있었다. 전체 요약 9문장 읽기 → 003 21:12 ▲ 503 · 댓글 218 엔비디아, AI 에이전트 샌드박스 OpenShell 0.1.0 공개 엔비디아가 자율 AI 에이전트 플릿을 위한 안전한 런타임 'OpenShell'의 0.1.0 안정화 버전을 출시했으며, 새로운 격리 기법과 확장 API를 포함하고 있다. AI · 머신러닝 · OpenShell – A safe, private runtime for fleets of autonomous AI agents
Key Point AI 에이전트에게 능력을 주면서도 데이터·자격증·네트워크 접근을 제한하는 커널 수준의 격리 방식이 자율 에이전트 배포의 보안 문제를 어떻게 풀고 있는지 보여준다.
핵심 요약
엔비디아가 자율 AI 에이전트 플릿을 위한 안전한 런타임 'OpenShell'의 0.1.0 안정화 버전을 출시했으며, 새로운 격리 기법과 확장 API를 포함하고 있다. OpenShell은 AI 에이전트가 파일 읽기, 패키지 설치, API 호출, 자격증 사용이 필요할 때 정책 선언을 통해 무제한 접근을 제한하면서 이를 가능하게 한다. 커널 수준에서 각 에이전트를 격리된 샌드박스에서 실행하고, 모든 파일 접근, 시스템 콜, 네트워크 연결을 런타임에 정책으로 제어한다. 전체 요약 12문장 읽기 → 004 12:11 ▲ 162 · 댓글 75 LLM으로 대규모 소프트웨어 형식 검증이 현실화되다 Anthropic과 Theorem이 협력해 Claude로 100개 이상의 실제 오픈소스 라이브러리 어셈블리 코드(RISC-V)에 대한 형식 증명을 생성했으며, 이는 AI를 활용한 프로덕션 소프트웨어의 대규모 형식 검증 최초 사례다. AI · 머신러닝 · LLMs are making formal software verification feasible at a much larger scale
Key Point 형식 검증이 역사적으로 수십 년의 전문 인력을 요구했으나, LLM이 이 비용을 획기적으로 낮추면서 일반 소프트웨어 개발에도 적용 가능해졌고, 향후 소프트웨어 보안 수준을 크게 변화시킬 기술이기 때문이다.
핵심 요약
Anthropic과 Theorem이 협력해 Claude로 100개 이상의 실제 오픈소스 라이브러리 어셈블리 코드(RISC-V)에 대한 형식 증명을 생성했으며, 이는 AI를 활용한 프로덕션 소프트웨어의 대규모 형식 검증 최초 사례다. 개발자의 퍼지 테스트(fuzz test)를 자동으로 형식 사양으로 변환해 증명했으며, 239개 엔트리포인트에서 64MB 이하 모든 입력에 대해 크래시가 없음을 증명했다. 총 약 1억 8천만 줄의 Rocq 증명을 작성했고, 전형적인 증명은 약 60만 줄의 코드로 18,000개 RISC-V 명령어에 대한 보안 보장을 제공한다. 전체 요약 13문장 읽기 → 005 09:11 ▲ 13 · 댓글 2 형식검증으로 강화한 LLM 에이전트 학습, Lean4AgenticRL LLM의 에이전트 능력을 강화하기 위해 복잡한 소프트웨어 엔지니어링과 터미널 작업 문제를 풀어야 하는 상황에서, 기존 모델들은 고수준의 결과 보상에만 의존해 학습 효율이 낮았다. AI · 머신러닝 · Lean4AgenticRL: Advancing Agentic RL with Verifiable Multi-level Process Rewards
Key Point 기존 LLM 에이전트 학습에서 다단계 보상 검증을 도입해 실제 성능 향상을 입증한 사례로, 형식 검증이 강화학습 효과성을 높일 수 있음을 보여준다.
핵심 요약
LLM의 에이전트 능력을 강화하기 위해 복잡한 소프트웨어 엔지니어링과 터미널 작업 문제를 풀어야 하는 상황에서, 기존 모델들은 고수준의 결과 보상에만 의존해 학습 효율이 낮았다. Lean4AgenticRL은 Lean4 형식화 체계에 다단계 프로세스 보상을 통합한 첫 번째 프레임워크로, 에이전트의 능력과 제어성 사이 균형을 맞추는 문제별 워크플로우 시스템을 구축한다. 워크플로우 형식화와 다단계 보상 주석 방식을 통해 일반 하니스 시스템 내에서 에이전트 동작을 검증하며, 저수준 도구 호출 보상과 중수준 워크플로우 단계 보상을 포함한다. 전체 요약 7문장 읽기 → 006 00:11 ▲ 118 · 댓글 53 형식 검증으로 코드 최적화하는 AI 'Maxwell' 공개 doubleAI가 프로그램 실행 중 코드를 동적으로 최적화하는 '코드 실행 모델(CEM)' Maxwell을 공개했다. AI · 머신러닝 · Maxwell: A new kind of model that sits between code and hardware
Key Point 기존 AI는 코드 작성만 지원했지만, Maxwell은 형식 검증을 통해 프로그램 실행 중 동적으로 코드를 재작성·최적화하는 새로운 영역을 열었기 때문에, 소프트웨어 성능과 자원 효율성에 미칠 파급 효과가 크다.
핵심 요약
doubleAI가 프로그램 실행 중 코드를 동적으로 최적화하는 '코드 실행 모델(CEM)' Maxwell을 공개했다. Maxwell은 실행 중인 프로그램의 병목을 감지하고 알고리즘 전체를 재작성해 더 빠른 바이너리를 생성하며, 생성된 코드는 원본과 의미적으로 완전히 동등함을 형식 검증으로 증명한다. 기존 JIT 컴파일러나 최적화 도구와 달리 Maxwell은 실제 하드웨어와 데이터 흐름에 맞춰 함수와 알고리즘 수준의 전체 변환을 수행하고 조건에 따라 보호 조항을 둔다. 전체 요약 13문장 읽기 → 007 12:11 ▲ 107 · 댓글 20 클로드, 양자 회로 설계를 대폭 개선하다 앤스로픽은 Claude Mythos 5에게 화학, 최적화, 물리 시뮬레이션, 정수론의 8가지 양자 회로 설계 과제를 평문으로 제시하고, 자동 평가기가 정확성을 검증하고 큐빗·게이트 수로 채점하도록 했다. AI · 머신러닝 · Designing more efficient quantum circuits with Claude
Key Point 양자 컴퓨터의 실용화는 회로 설계 최적화에 달렸는데, Claude가 연구 그룹이 8년에 걸쳐 이룬 성과(FeMoco 게이트 150,000배 감소)를 53시간에 달성했다는 점이 양자 알고리즘 개발의 속도를 근본적으로 바꿀 수 있음을 보여준다.
핵심 요약
앤스로픽은 Claude Mythos 5에게 화학, 최적화, 물리 시뮬레이션, 정수론의 8가지 양자 회로 설계 과제를 평문으로 제시하고, 자동 평가기가 정확성을 검증하고 큐빗·게이트 수로 채점하도록 했다. Claude는 피드백 루프를 통해 폐쇄형으로 회로를 반복 설계했으며, 8가지 모두에서 이전의 최고 성능 회로보다 큐빗과 게이트 수를 줄인 새로운 설계를 발견했다. 첫 번째 사례는 타원곡선 암호 계산의 핵심인 모듈러 역수 문제로, Claude는 divsteps 알고리즘의 가지 정보(branch information)를 저장하지 않고 수치 쌍에서 직접 복원할 수 있음을 발견했다. 전체 요약 12문장 읽기 → 008 00:11 ▲ 106 · 댓글 32 Rust를 가독성 높은 C 코드로 변환하는 Eurydice Rust 컴파일러의 다양화 추세 속에서 Eurydice는 Rust 코드를 깔끔한 C 코드로 변환하는 야심찬 목표를 지닌 최신 프로젝트다. 인프라 · 데브옵스 · Compiling Rust to readable C with Eurydice
Key Point Rust에서 C로의 자동 변환이 고보증 소프트웨어나 C 기반 환경으로의 이식 시 검증 도구 호환성을 유지하면서 코드 동기화를 가능하게 한다.
핵심 요약
Rust 컴파일러의 다양화 추세 속에서 Eurydice는 Rust 코드를 깔끔한 C 코드로 변환하는 야심찬 목표를 지닌 최신 프로젝트다. 고보증 소프트웨어(high-assurance software) 분야에서 기존 검증·규정준수 도구들이 C를 기대하므로, Eurydice는 이러한 프로젝트들의 부드러운 전환을 가능하게 한다. 2023년 시작된 Eurydice는 Inria(프랑스 국립 컴퓨터과학연구원)와 Microsoft 직원들이 유지보수하는 Aeneas 프로젝트의 일부이며, MIT와 Apache-2.0 라이선스 코드를 포함한다. 전체 요약 13문장 읽기 → 009 18:11 ▲ 111 · 댓글 96 C 언어의 미정의 동작 감소, 메모리 안전성 강화 논의 C 언어는 여전히 이식성과 안정성, 빠른 컴파일 속도를 갖춘 우수한 언어로, 추상 머신 모델을 통해 다양한 하드웨어를 지원한다. 인프라 · 데브옵스 · Reducing undefined behavior in the C language
Key Point C 언어는 여전히 주요 임베디드·시스템 소프트웨어의 핵심이며, 표준위원회가 메모리 안전성 개선에 적극 나서면서 앞으로 C의 보안과 안정성이 크게 달라질 가능성을 보여준다.
핵심 요약
C 언어는 여전히 이식성과 안정성, 빠른 컴파일 속도를 갖춘 우수한 언어로, 추상 머신 모델을 통해 다양한 하드웨어를 지원한다. C 표준에는 약 100개의 미정의 동작(undefined behavior)이 존재하는데, 이는 컴파일러 최적화와 하드웨어 제어를 가능하게 하지만 개발자 간 의견 충돌을 초래한다. 구조체 패딩 읽기, 0으로 나누기 후 실행 흐름 등의 경우 컴파일러가 예상 밖으로 코드를 최적화하여 버그를 야기하는 사례들이 있다. 전체 요약 8문장 읽기 → 010 18:30 ▲ 115 · 댓글 53 11개 정사각형 최적 배치 증명, AI 보조로 완성 Lean 형식 검증을 통해 11개 정사각형의 최적 배치 문제에 대한 완전한 증명을 완성했다. AI · 머신러닝 · AI-assisted proof of optimal packing for 11 squares
Key Point 최적화 문제의 엄밀한 증명에 AI 보조 도구와 형식 검증이 어떻게 결합되는지 보여주는 사례로, 수학적 추측을 기계 검증 가능한 형태로 변환하는 최신 방법론을 시연한다.
핵심 요약
Lean 형식 검증을 통해 11개 정사각형의 최적 배치 문제에 대한 완전한 증명을 완성했다. 7,920개 지역 Lean 모듈을 EvolvingPrograms 검증 시스템으로 검증했으며 모든 감사에서 오류가 0건이다. 최적 한 변의 길이는 T = (6u+4)/(1+2u-u²) 형태이며, u는 방정식 5u⁸-10u⁷-2u⁶+14u⁵+12u⁴-6u³+2u²+2u-1=0의 (9/25, 37/100) 범위 내 유일한 근이다. 전체 요약 8문장 읽기 → 011 21:11 당일 +600 NVIDIA가 공개한 AI 에이전트 실행 환경 OpenShell NVIDIA가 OpenShell을 공개했으며, 이는 자율 AI 에이전트가 안전하고 격리된 환경에서 파일 접근, 패키지 설치, API 호출, 자격증명 사용이 가능하도록 지원하는 런타임이다. 인프라 · 데브옵스 · NVIDIA/OpenShell · Rust
Key Point AI 에이전트에게 파일 접근·API 호출 등의 능력을 주면서도 커널 수준의 정책으로 데이터와 자격증명을 보호하는 새로운 접근 방식으로, 자율 에이전트를 프로덕션 환경에 배포하려는 개발자들이 주목할 만한 인프라 솔루션이다.
핵심 요약
NVIDIA가 OpenShell을 공개했으며, 이는 자율 AI 에이전트가 안전하고 격리된 환경에서 파일 접근, 패키지 설치, API 호출, 자격증명 사용이 가능하도록 지원하는 런타임이다. OpenShell은 커널 수준의 정책 강제와 형식 검증 두 가지 방식으로 에이전트의 행동을 관리하며, 정책 변경 전 형식 검증을 통해 위험한 접근 권한을 사전에 적발한다. 각 에이전트는 격리된 샌드박스에서 실행되며, 커널이 파일 접근과 시스템 콜을 제한하고 모든 네트워크 연결이 정책 검사를 거친다. 전체 요약 12문장 읽기 → 012 06:11 ▲ 106 · 댓글 60 형식 검증의 새로운 시대, TLA+와 AI가 만나다 보리스 체르니의 바이럴 트윗 이후 TLA+에 관심이 몰리고 있으며, 이 글은 TLA+의 실용성과 한계, 그리고 미래 방향을 설명한다. AI · 머신러닝 · The internet discovers TLA+. Now what?
Key Point TLA+가 30년 된 도구이지만 AI 에이전트를 활용한 자동화로 형식 검증을 실용적으로 확장하는 방식을 보여주며, 안전성이 중요한 분산 시스템 개발에 영향을 미칠 수 있는 기술 전환점이다.
핵심 요약
보리스 체르니의 바이럴 트윗 이후 TLA+에 관심이 몰리고 있으며, 이 글은 TLA+의 실용성과 한계, 그리고 미래 방향을 설명한다. TLA+(Temporal Logic of Actions)는 시스템의 가능한 동작과 만족해야 할 성질을 기술하는 형식 언어로, 상태와 행동으로 이루어진 전이 시스템을 모델링한다. TLA+의 모델 체커인 TLC는 유한 모델의 모든 가능한 실행을 탐색해 안전성(bad thing이 일어나지 않음)과 생존성(good thing이 결국 일어남) 같은 시간적 성질을 검증한다. 전체 요약 8문장 읽기 → 013 21:11 ▲ 108 · 댓글 66 AI 시대 프로그래밍 언어는 어떻게 진화해야 할까 Elixir 창시자 José Valim이 AI 코딩 에이전트가 대부분의 코드를 작성하는 미래에 프로그래밍 언어가 어떻게 변할지 분석했다. AI · 머신러닝 · Evolving programming languages in the AI era
Key Point 에이전트가 코드의 대부분을 작성하는 시대가 도래했을 때, 언어 설계자들이 무엇을 다시 생각해야 하는지 구체적으로 제시한다: 기존 프로그래밍 언어의 인간 친화적 기능은 덜 중요해지고, 대신 더 강한 보증과 에이전트 친화적 개발 도구(프로그램 데이터베이스, 런타임 관찰성)가 새로운 경쟁력이 된다.
핵심 요약
Elixir 창시자 José Valim이 AI 코딩 에이전트가 대부분의 코드를 작성하는 미래에 프로그래밍 언어가 어떻게 변할지 분석했다. AI 에이전트가 코드 작성을 주도하면 프로그래밍 언어 커뮤니티의 정체성이 흔들릴 수 있다: Python의 '명백한 방법'이나 Ruby의 '프로그래머 행복'은 에이전트에게 의미가 없어질 수 있다. 생태계는 모순적인 영향을 받는다: 에이전트가 알려진 알고리즘 구현과 언어 간 이식을 빠르게 처리해 작은 커뮤니티가 따라잡을 수 있게 하지만, 동시에 라이브러리가 저렴해지면 협력할 필요성이 줄어든다. 전체 요약 11문장 읽기 → 014 18:10 ▲ 113 · 댓글 22 컴파일러 기법으로 Skia 그래픽 성능 최적화 Skia, CoreGraphics, Direct2D 같은 래스터화 라이브러리의 형식적 의미론을 정의한 μSkia를 개발했다. 웹 · 프론트엔드 · Compiler-style optimization for drawing via Skia
Key Point 웹 브라우저와 그래픽 애플리케이션의 2D 렌더링 성능을 크게 개선할 수 있는 형식 검증 방법론이 제시되었으며, 실제 Chrome 데이터로 검증되었다.
핵심 요약
Skia, CoreGraphics, Direct2D 같은 래스터화 라이브러리의 형식적 의미론을 정의한 μSkia를 개발했다. 복잡한 실행 모델 때문에 Google Chrome도 비효율적인 명령어를 생성하고 있다는 점을 발견했다. μSkia로 Chrome에서 찾은 4가지 부최적 코드 패턴을 분석하고 Lean으로 검증된 최적화 규칙을 만들었다. 전체 요약 5문장 읽기 → 015 03:10 ▲ 123 · 댓글 114 AI와 함께 50년 묵은 수학 난제 증명 성공 수학 비전공자가 Claude AI를 활용해 John Conway가 1976년에 제시한 초현실수 관련 미해결 난제를 Lean 증명으로 완성했다. AI · 머신러닝 · I vibed a proof of Conway's conjecture
Key Point AI가 인간과 협력해 순수 수학 난제를 해결할 수 있음을 보여주는 사례로, 형식 검증 시스템의 신뢰성이 수학 증명의 새로운 인정 방식이 될 수 있음을 시사한다.
핵심 요약
수학 비전공자가 Claude AI를 활용해 John Conway가 1976년에 제시한 초현실수 관련 미해결 난제를 Lean 증명으로 완성했다. 해당 난제는 omnific integers의 refinement property에 관한 Conway의 추측으로, 두 가지 인수분해가 공통 세분화를 가지는지를 묻는 문제다. 저자는 Claude에게 초현실수 분야의 흥미로운 문제를 골라달라 요청했고, Claude가 이 난제를 추천했다. 전체 요약 6문장 읽기 → 016 00:10 ▲ 255 · 댓글 176 Bend 2가 빠진 형식 검증의 표준 방식 Bend 2는 AI가 코드를 작성하고 증명을 통해 검증하는 언어로 소개되지만, 간단한 게임 규칙 검증에 442줄의 증명 코드를 필요로 한다. 오픈소스 · 도구 · Bend 2 and the Vibe-Coding Trap
Key Point 기존 형식 검증 분야의 성숙한 도구와 방식을 모르고 같은 문제를 더 복잡하게 재구성하는 것이 가능한 이유를 설명하며, 신생 언어/도구를 평가할 때 학문 기초의 중요성을 보여준다.
핵심 요약
Bend 2는 AI가 코드를 작성하고 증명을 통해 검증하는 언어로 소개되지만, 간단한 게임 규칙 검증에 442줄의 증명 코드를 필요로 한다. 저자는 이를 '비브 코딩의 함정'으로 지칭하며, 개발자가 충분한 분야 지식 없이 대규모 솔루션을 완성해 더 나은 방식을 놓친다고 비판한다. Bend의 웹페이지와 코드베이스에는 형식 검증(formal verification) 용어가 나타나지 않으며, 저자는 이 분야의 표준 언어인 SPARK로 동일한 프로그램을 작성해 12개 검사만으로 증명할 수 있음을 보인다. 전체 요약 4문장 읽기 → 017 09:10 ▲ 125 · 댓글 121 OpenAI, Navier-Stokes 증명을 Lean 4 형식 증명으로 공개 OpenAI가 유체역학의 오랜 난제인 Navier-Stokes 방정식을 증명하면서 동시에 Lean 4 형식 증명을 공개했다. AI · 머신러닝 · OpenAI’s Navier-Stokes release included a Lean 4 formal proof
Key Point 형식 검증 비용이 만 배 절감되면서 AI 증명 방식이 학문과 산업 전반의 검증 방식을 근본적으로 바꿀 수 있는 전환점이 되었다.
핵심 요약
OpenAI가 유체역학의 오랜 난제인 Navier-Stokes 방정식을 증명하면서 동시에 Lean 4 형식 증명을 공개했다. 종전에는 수학 논문 한 페이지를 형식화하는 데 약 40시간이 소요되었으나, 이번 증명은 17시간 만에 Lean 형식으로 검증되었다. 166쪽 규모의 OpenAI 논문을 전통적 방식으로 형식화했다면 13만 2800인시가 필요했을 것으로 추정되어, 약 만 배의 비용 감소를 의미한다. 전체 요약 4문장 읽기 → 018 08:12 ▲ 174 · 댓글 64 AI 에이전트, 테스트 기법 지시로는 코드 품질 개선 못해 연구자는 Zstd 구현 평가를 통해 AI 에이전트에게 TDD·퍼지 테스트·형식 검증 등 26가지 테스트 기법을 지시해 효과를 비교했다. AI · 머신러닝 · How well do agents use test/verification techniques?
Key Point 개발자들이 AI 에이전트에게 테스트 기법을 지시해도 코드 품질이 개선되지 않는 현실을 체계적으로 보여주며, AI 코딩 도구의 신뢰성 문제의 근본 원인을 지목합니다.
핵심 요약
연구자는 Zstd 구현 평가를 통해 AI 에이전트에게 TDD·퍼지 테스트·형식 검증 등 26가지 테스트 기법을 지시해 효과를 비교했다. 특정 테스트 기법이나 라이브러리 사용 지시, 큰 스킬 프롬프트, 유명 오픈소스 스킬 등을 시도했지만 대부분 지시 없는 기본 방식보다 나은 결과를 주지 못했다. 높은 비용 설정에서는 퍼지 테스트와 속성 기반 테스트가 평균적으로 형식 검증보다 조금 나았으나, 전반적으로 어느 기법도 압도적 성능 향상을 보이지 않았다. 전체 요약 5문장 읽기 → 
