쌓인 기록에서 찾기
무엇을 찾으세요?
날짜를 몰라도 됩니다. 제목·Key Point·요약·태그를 한꺼번에 뒤집니다.
검색 범위부터 2026년 9월 19일 (토)까지674건
3건 · "형식 검증"조건 지우기 ×
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 · 머신러닝 · OpenAI’s Navier-Stokes release included a Lean 4 formal proof
OpenAI, Navier-Stokes 증명을 Lean 4 형식 증명으로 공개
Key Point형식 검증 비용이 만 배 절감되면서 AI 증명 방식이 학문과 산업 전반의 검증 방식을 근본적으로 바꿀 수 있는 전환점이 되었다.
핵심 요약
- OpenAI가 유체역학의 오랜 난제인 Navier-Stokes 방정식을 증명하면서 동시에 Lean 4 형식 증명을 공개했다.
- 종전에는 수학 논문 한 페이지를 형식화하는 데 약 40시간이 소요되었으나, 이번 증명은 17시간 만에 Lean 형식으로 검증되었다.
- 166쪽 규모의 OpenAI 논문을 전통적 방식으로 형식화했다면 13만 2800인시가 필요했을 것으로 추정되어, 약 만 배의 비용 감소를 의미한다.
- 형식 증명의 비용이 급격히 낮아지면서 수학 연구뿐 아니라 보안 정책 검증, 스마트 계약 검증, 미션 크리티컬 알고리즘 검증 등이 현실화될 수 있다.
AI · 머신러닝 · How well do agents use test/verification techniques?
AI 에이전트, 테스트 기법 지시로는 코드 품질 개선 못해
Key Point개발자들이 AI 에이전트에게 테스트 기법을 지시해도 코드 품질이 개선되지 않는 현실을 체계적으로 보여주며, AI 코딩 도구의 신뢰성 문제의 근본 원인을 지목합니다.
핵심 요약
- 연구자는 Zstd 구현 평가를 통해 AI 에이전트에게 TDD·퍼지 테스트·형식 검증 등 26가지 테스트 기법을 지시해 효과를 비교했다.
- 특정 테스트 기법이나 라이브러리 사용 지시, 큰 스킬 프롬프트, 유명 오픈소스 스킬 등을 시도했지만 대부분 지시 없는 기본 방식보다 나은 결과를 주지 못했다.
- 높은 비용 설정에서는 퍼지 테스트와 속성 기반 테스트가 평균적으로 형식 검증보다 조금 나았으나, 전반적으로 어느 기법도 압도적 성능 향상을 보이지 않았다.
- TDD 지시는 기본 방식보다 성능이 저하되는 경향을 보였고, 형식 검증 도구 프롬프트는 예상보다 우수하지 않았다.
- 연구자는 에이전트가 지시받은 테스트 기법을 실제로 제대로 수행하지 않거나, 개발자의 입력 없이 기본 설정된 효과적인 테스트 방법이 활용되지 않고 있다고 지적했다.