쌓인 기록에서 찾기
무엇을 찾으세요?
날짜를 몰라도 됩니다. 제목·Key Point·요약·태그를 한꺼번에 뒤집니다.
검색 범위부터 2026년 9월 19일 (토)까지674건
2건 · "SPARK"조건 지우기 ×
001▲ 255 · 댓글 176Bend 2가 빠진 형식 검증의 표준 방식Bend 2는 AI가 코드를 작성하고 증명을 통해 검증하는 언어로 소개되지만, 간단한 게임 규칙 검증에 442줄의 증명 코드를 필요로 한다.오픈소스 · 도구 · Bend 2 and the Vibe-Coding Trap
Bend 2가 빠진 형식 검증의 표준 방식
Key Point기존 형식 검증 분야의 성숙한 도구와 방식을 모르고 같은 문제를 더 복잡하게 재구성하는 것이 가능한 이유를 설명하며, 신생 언어/도구를 평가할 때 학문 기초의 중요성을 보여준다.
핵심 요약
- Bend 2는 AI가 코드를 작성하고 증명을 통해 검증하는 언어로 소개되지만, 간단한 게임 규칙 검증에 442줄의 증명 코드를 필요로 한다.
- 저자는 이를 '비브 코딩의 함정'으로 지칭하며, 개발자가 충분한 분야 지식 없이 대규모 솔루션을 완성해 더 나은 방식을 놓친다고 비판한다.
- Bend의 웹페이지와 코드베이스에는 형식 검증(formal verification) 용어가 나타나지 않으며, 저자는 이 분야의 표준 언어인 SPARK로 동일한 프로그램을 작성해 12개 검사만으로 증명할 수 있음을 보인다.
- 저자의 핵심 주장은 Bend가 형식 검증이라는 기존 학문 분야의 표준 방식을 모르거나 간과한 채 복잡한 시스템을 새로 만들었다는 것이다.
AI · 머신러닝 · Speculative Decoding in vLLM on AMD GPUs
vLLM이 AMD GPU에서 추측 디코딩 지원
Key PointLLM 추론 성능 최적화를 위한 주요 기법이 AMD GPU에서 실제 구현되어, 장기 생성 작업의 처리량 개선 가능성을 보여준다.
핵심 요약
- vLLM이 추측 디코딩(speculative decoding) 기능을 AMD Instinct MI300X·MI355X GPU와 ROCm에서 구현했다.
- 추측 디코딩은 경량 드래프트 모듈이 여러 토큰을 먼저 제안하고 타겟 모델이 한 번에 검증하는 방식으로, 기존 자동회귀 디코딩보다 모델 통과 횟수를 줄인다.
- 표준 방식은 토큰 하나당 모델 실행 1회가 필요하지만, 추측 디코딩은 여러 드래프트 토큰이 검증을 통과하면 단일 모델 실행으로 여러 토큰을 커밋할 수 있다.
- Native MTP, Gemma 4 MTP, EAGLE-3, DFlash, DSpark 등 5가지 드래프팅 방식을 검토했으며, 방식·제안 길이·모델 종류·수용 동작 등에 따라 처리량 개선 효과가 달라진다.
- 드래프트 토큰이 거부되면 거부 지점 이후의 토큰들은 폐기되고 타겟 모델의 결과로 생성을 계속한다.