쌓인 기록에서 찾기
무엇을 찾으세요? 날짜를 몰라도 됩니다. 제목·Key Point·요약·태그를 한꺼번에 뒤집니다.
검색 범위 2026년 8월 13일 (목) 부터 2026년 11월 3일 (화)까지 3800건
7건 · "형식 증명"조건 지우기 ×
001 00:11 ▲ 106 · 댓글 25 AI 시대, 형식검증이 소프트웨어 엔지니어링을 바꾼다 Lean 개발자 Leo de Moura는 AI가 형식검증을 실용적으로 만들고 있으며, 코드 생성이 쉬워진 지금이 검증의 중요성이 높아진 순간이라고 주장한다. AI · 머신러닝 · AI, Lean, and the Future of Formal Verification, with Lean Creator Leo de Moura
Key Point AI가 자동으로 코드를 생성·최적화하는 시대에, 형식검증이 버그의 절대적 부재를 증명하는 유일한 수단이며, 소프트웨어 엔지니어의 역량과 커리큘럼을 근본적으로 바꿀 것이기 때문이다.
핵심 요약
Lean 개발자 Leo de Moura는 AI가 형식검증을 실용적으로 만들고 있으며, 코드 생성이 쉬워진 지금이 검증의 중요성이 높아진 순간이라고 주장한다. Lean은 프로그래밍 언어이자 정리증명기로, 코드의 성질을 명시하고 기계검증되는 증명을 작성할 수 있다. 신뢰하려면 Lean 커널만 믿으면 되고, 다중 커널이 존재한다. AI 기반 자동형식화(autoformalization)로 어떤 언어의 코드든 Lean 모델로 변환할 수 있게 됐다. 예로 Microsoft의 SymCrypt 암호화 라이브러리는 Aeneas 도구를 통해 Lean으로 검증된다. 전체 요약 12문장 읽기 → 002 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문장 읽기 → 003 18:11 ▲ 114 · 댓글 22 수학 증명의 형식화, AI 자동화 시대 열리다 형식 증명은 수학의 기초와 논리 규칙 수준에서 철저히 검증한 증명으로, 컴퓨터로 자동 검사하는 것이 일반적이며 페르마 최종 정리·구 채움 문제 등이 형식화됐다. AI · 머신러닝 · What mathematicians should know about the Lean Theorem Prover: reliability & AI
Key Point AI가 수학 증명을 자동 형식화하기 시작하면서 신뢰성·일관성 검증의 새로운 시대가 열렸지만, 커널 버그와 AI 자체에 대한 신뢰 문제가 수학의 기초를 위협할 수 있다.
핵심 요약
형식 증명은 수학의 기초와 논리 규칙 수준에서 철저히 검증한 증명으로, 컴퓨터로 자동 검사하는 것이 일반적이며 페르마 최종 정리·구 채움 문제 등이 형식화됐다. 증명 보조기(proof assistant) 중 Lean이 수학자들에게 가장 인기 있으며, 2013년 Leo de Moura가 개발했고 마이크로소프트에서 오픈소스로 공개됐다. Lean의 표준 수학 라이브러리인 mathlib은 약 30만 개 정리, 10만 개 이상 정의, 250만 줄 코드로 700명 이상이 기여했다. 전체 요약 13문장 읽기 → 004 15:11 ▲ 103 · 댓글 33 소프트웨어 엔지니어를 위한 Lean 형식 증명 완전 분석 소프트웨어 엔지니어 입장에서 형식 증명이 무엇인지 이해하기 위해 Lean을 이용해 결정적 유한 오토마타(DFA) 이론 문제를 증명한 과정을 설명한다. 오픈소스 · 도구 · Anatomy of a Lean proof for software engineers
Key Point 형식 증명은 프로그램처럼 작성되어 컴파일되므로, 이 사례는 소프트웨어 엔지니어가 타입 검사와 증명 보조기의 관계를 이해하고 실제 이론 문제에 어떻게 적용하는지 구체적으로 배울 수 있다.
핵심 요약
소프트웨어 엔지니어 입장에서 형식 증명이 무엇인지 이해하기 위해 Lean을 이용해 결정적 유한 오토마타(DFA) 이론 문제를 증명한 과정을 설명한다. 계산 이론 교재의 문제: 세 행의 비트 문자열(최상단 + 중간 = 최하단)에서 덧셈이 성립하는지 검증하는 언어 B가 정규언어임을 증명하는 것이었다. 정규언어의 폐쇄성을 이용해 B의 역순 B^R을 인식하는 DFA를 구성하면, B^R이 정규이므로 그 역순인 B도 정규임을 결론 낼 수 있다. 전체 요약 13문장 읽기 → 005 09:10 ▲ 227 · 댓글 123 AI 실수 원천 차단하는 프로그래밍 언어 'Bend' 공개 형식 증명(proof)으로 AI가 작성한 코드의 정확성을 검증하는 프로그래밍 언어 Bend를 발표했다. AI · 머신러닝 · Bend – A language that blocks AI mistakes via proof, on CPU and GPU
Key Point AI 에이전트가 코드를 자동 생성하는 시대에 형식 증명으로 보안 결함을 원천 차단할 수 있는 새로운 접근 방식을 제시하기 때문입니다.
핵심 요약
형식 증명(proof)으로 AI가 작성한 코드의 정확성을 검증하는 프로그래밍 언어 Bend를 발표했다. C 수준의 단일 코어 성능으로 컴파일되며, 동일 바이너리가 GPU에서 100배까지 빠르게 실행된다. 타입 체커가 증명 체커로 작동해 중간 규모 코드베이스에서 최대 1초 내에 검증을 완료한다. 전체 요약 5문장 읽기 → 006 21:11 ▲ 102 · 댓글 83 AI가 나비에-스토크스 문제를 풀었다는 것의 의미 OpenAI는 2026년 9월 밀레니엄 상금 문제 중 하나인 나비에-스토크스 존재성과 정칙성 문제의 해를 제시했다고 발표했다. AI · 머신러닝 · After Math
Key Point 형식적으로 증명되었다고 해서 수학의 진정한 진전이 이루어지는지, AI 시대 수학의 역할이 어떻게 재정의되어야 하는지를 다루는 근본적인 질문이기 때문이다.
핵심 요약
OpenAI는 2026년 9월 밀레니엄 상금 문제 중 하나인 나비에-스토크스 존재성과 정칙성 문제의 해를 제시했다고 발표했다. AI가 제출한 것은 Lean 형식 증명과 비형식 증명 원고인데, 이는 논리적 증명(기계적 검증 가능)의 기준은 충족하지만 수학자가 원하는 이해 가능한 증명은 아닐 수 있다. 논리적 증명과 이해 가능한 증명은 역사적으로 함께 진행되었으나, AI로 인해 형식 증명만 남고 수학적 통찰력 없는 증명이 생겨날 수 있다. 전체 요약 5문장 읽기 → 007 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문장 읽기 → 
