AI Briefing#formal-verification
#formal-verification와 관련된 AI·개발 뉴스를 최신순으로 모았습니다. 원문 출처와 한국어 요약을 함께 확인할 수 있습니다.
#formal-verification와 관련된 AI·개발 뉴스를 최신순으로 모았습니다. 원문 출처와 한국어 요약을 함께 확인할 수 있습니다.
Anthropic이 Claude로 페르마의 마지막 정리의 첫 완전 기계 검증 증명을 공개했다.
LLM의 산술적 약점을 보완하기 위해 수학적 증거와 검증 수준을 명시하는 멀티엔진 수학 커널 'MathKernel'이 공개됐다.
Claude가 Lean 언어로 페르마의 마지막 정리를 11일 만에 자율적으로 형식화하며 1,300만 줄의 코드를 생성했다.
Anthropic이 AI 에이전트를 활용해 리만 제타 함수의 임계선 위 영점 비율 하한을 67.25%로 높이는 연구 결과를 발표했다.
Amazon의 Automated Reasoning Group이 지난 10년의 연구와 성과를 돌아봤다.
OpenAI의 미공개 모델 Astra가 미해결 수학 문제 10개에서 새 결과를 제시했다.
Microsoft가 Rust, Aeneas, Lean을 활용해 SymCrypt 암호화 알고리즘의 수학적 무결성을 검증하는 기술을 공개했다.
Lean 4 기반의 정식 검증에 특화된 오픈 소스 모델 Leanstral 1.5가 출시되었습니다.
AWS가 수학적 증명을 통해 가상 머신 간 격리를 보장하는 Nitro Isolation Engine을 상용 클라우드에 최초로 도입했다.
AWS는 Isabelle/HOL로 Nitro Isolation Engine의 보안과 정당성을 형식 검증했다.
105M회 fuzzing으로 Lean runtime heap overflow와 lean-zip DoS를 발견했다.
Arm64 AES-256-XTS를 HOL Light로 검증해 s2n-bignum에 넣었다.
Lean 4용 첫 오픈소스 코드 에이전트 Leanstral이 형식 증명까지 겨냥해 공개됐다.