쌓인 기록에서 찾기
무엇을 찾으세요? 날짜를 몰라도 됩니다. 제목·Key Point·요약·태그를 한꺼번에 뒤집니다.
검색 범위 2026년 8월 13일 (목) 부터 2026년 10월 30일 (금)까지 3636건
9건 · "형식검증"조건 지우기 ×
001 06:11 ▲ 12 · 댓글 2 LLM으로 안정성 증명서 합성하고 형식검증기로 검증 Lyapunov 함수와 barrier certificate는 비선형 고차원 시스템의 안정성과 안전성을 보장하지만, 이들을 합성하고 검증하는 것은 여전히 난제이다. AI · 머신러닝 · LLM2Cert: LLM Synthesis of Certificates with SMT/Lean Verification
Key Point 동적 시스템의 안정성 증명이 형식검증기와 LLM으로 자동화되는 방식이 바뀌고 있으며, 기존 솔버 중심 접근을 넘는 실질적 성과를 보여준다.
핵심 요약
Lyapunov 함수와 barrier certificate는 비선형 고차원 시스템의 안정성과 안전성을 보장하지만, 이들을 합성하고 검증하는 것은 여전히 난제이다. 기존 방식은 수치해석 솔버, 구간 방법, SMT 솔버 등을 사용하는데, 완화(relaxation)가 필요하거나 보수적이거나 차원과 비선형성에 따라 확장성이 나빠진다. 표준 벤치마크는 솔버가 다룰 수 있는 저차원 다항식 시스템으로 지배되어 실제 공학 응용과 거리가 있다. 전체 요약 8문장 읽기 → 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 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문장 읽기 → 004 18:11 ▲ 129 · 댓글 44 Lean, 검증된 증명 커널 네 개 추가 Lean v4.35.0부터 lake check 명령으로 개발 환경을 leanchecker(공식 커널)로 재검증할 수 있으며, 프로세스는 샌드박스에서 실행된다. AI · 머신러닝 · Lean now ships with verified kernels
Key Point Lean 증명 보조기의 핵심인 커널에 버그가 증명을 검증하지 못하는 치명적 문제를 여러 커널로 재검증해 해결하는 방식이 도입되었고, 특히 형식적으로 증명된 Lean 기반 커널의 등장으로 신뢰성이 크게 강화되는 시점이다.
핵심 요약
Lean v4.35.0부터 lake check 명령으로 개발 환경을 leanchecker(공식 커널)로 재검증할 수 있으며, 프로세스는 샌드박스에서 실행된다. nanoda, lean4lean, con-leche, con-ron 네 개의 추가 커널을 탑재했고, lake check --paranoid로 모든 커널로 증명을 재검증할 수 있다. con-leche는 Lean으로 작성되고 일관성이 증명된 첫 번째 커널이며, Claude(Fable과 Opus)가 구현하고 Joachim Breitner가 감독했다. 전체 요약 11문장 읽기 → 005 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문장 읽기 → 006 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문장 읽기 → 007 06:11 ▲ 107 · 댓글 23 TLA+로 검증할 수 있는 것과 없는 것 AI 안전을 TLA+ 형식검증으로 완전히 해결할 수 있다는 기대가 커지고 있지만, 실제 한계가 크다. AI · 머신러닝 · What TLA+ can and can't check
Key Point TLA+로 AI 시스템 검증을 완벽히 해결할 수 있다는 기대가 커지고 있는데, 형식화 불가능한 성질, 다중 단계 속성, 행동 수열 비교 같은 근본적 한계를 알아야 현실적 기대를 조정할 수 있다.
핵심 요약
AI 안전을 TLA+ 형식검증으로 완전히 해결할 수 있다는 기대가 커지고 있지만, 실제 한계가 크다. TLA+는 시스템을 상태 수열로 나누고, 각 상태에서 불린 식을 표현하며 항상(always), 다음(prime), 결국(eventually) 같은 시간논리 연산자로 성질을 정의한다. 불변식(invariants)과 안전 성질(safety properties)은 TLA+의 가장 기본적인 검증 대상이며, 생생성 성질(liveness properties)은 좋은 일이 언젠가 일어남을 보장한다. 전체 요약 11문장 읽기 → 008 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문장 읽기 → 009 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문장 읽기 → 
