미스트랄, 리언4 증명 자동화 모델 ‘린스트랄 1.5’ 공개
미스트랄 문서에 리언4 형식 증명 공학에 최적화된 린스트랄 1.5 모델 카드가 올라왔다. 모델은 자동 정리 증명과 자동 형식화에 맞춰졌고, 전체 1190억 파라미터 중 65억 파라미터가 활성화되는 구조이며 25만6000 토큰 컨텍스트를 제공한다.
- 1
린스트랄 1.5는 리언4 형식 증명 공학용 모델
- 2
자동 정리 증명과 자동 형식화에 최적화
- 3
전체 1190억 파라미터, 활성 65억 파라미터, 컨텍스트 25만6000 토큰
본문은 짧지만 타깃은 꽤 선명하다. 일반 코딩 모델이 아니라 형식 검증과 증명 자동화 쪽으로 모델이 세분화되는 흐름이라, 안전성이 중요한 코드베이스를 다루는 팀은 눈여겨볼 만함.
관련 기사
메타가 남는 AI 컴퓨팅을 클라우드로 팔 수도 있다는 얘기에 시장이 뒤집힘
메타가 남는 AI 컴퓨팅 자원과 모델 접근권을 외부에 판매하는 클라우드 사업을 검토 중이라는 보도가 나왔다. 메타 주가는 장중 10% 가까이 뛰었지만, 마이크론과 코어위브 같은 AI 인프라 관련주는 공급 과잉 우려로 크게 밀렸다. 핵심은 빅테크의 AI 투자금 회수 전략이 GPU·HBM 수요를 더 키울지, 아니면 이미 사둔 자원을 시장에 다시 풀어 수요를 잠식할지다.
메타, 남는 AI 컴퓨팅으로 클라우드 장사까지 노린다
메타가 자사 데이터센터의 남는 AI 컴퓨팅 자원을 외부 고객에게 파는 클라우드 사업을 검토 중이다. 모델 API를 제공하는 방식과 GPU 같은 연산 자원만 빌려주는 방식이 함께 거론되고, 이 소식에 메타 주가는 9.48% 급등한 반면 코어위브와 반도체주는 크게 흔들렸다.
메타, 남는 AI 연산 자원 팔아서 클라우드 사업 뛰어드나
메타가 인공초지능 개발을 위해 쌓아둔 데이터센터와 GPU 인프라를 외부 고객에게 판매하는 클라우드 사업을 검토 중인 것으로 알려졌다. 자체 AI 모델 API를 제공하는 PaaS 방식과 순수 연산 자원을 임대하는 IaaS 방식이 모두 거론되며, 시장은 메타 주가 10% 상승과 네오클라우드 주가 급락으로 바로 반응했다.
피지컬 AI 시대, 한국 반도체는 메모리만으론 부족하다는 경고
성균관대 이우근 교수가 피지컬 AI 시대에는 한국 반도체 산업이 메모리 중심 구조를 넘어 아날로그·통신 설계자산과 팹리스 생태계를 키워야 한다고 주장했다. 생성형 AI 덕분에 고대역폭메모리의 전략적 가치는 커졌지만, 로봇·자율주행·산업용 기계처럼 기기 자체에서 판단하고 움직이는 환경에선 센서·통신·전력관리 반도체가 더 중요해진다는 내용이다.
미국 중앙정보국장 “AI는 디지털 핵무기”, 조직도 코드 중심으로 바꾼다
미국 중앙정보국장이 공개 행사에서 AI를 ‘디지털 핵무기’급 기술로 규정하며, 조직을 사이버·기술 중심으로 개편하겠다고 밝혔다. 베네수엘라 대통령 체포 작전과 이란 추락 전투기 조종사 위치 파악 사례까지 언급하며 AI가 정보전의 판을 바꾸고 있다고 강조했다.
댓글
댓글
댓글을 불러오는 중...