사람들이 이제 에이전트가 원하는 동작을 명세하고, 그 명세에 맞춰 코드를 작성할 수 있다는 패턴을 인식하기 시작한 게 흥미로움
TDD나 검증 도구 등 어떤 방식을 쓰든, 시간이 지나면 이런 검증 스위트가 “어떻게 동작해야 하는가”를 보여주는 실행 가능한 문서 저장소로 쌓이게 됨
이런 접근은 단순한 마크다운 스펙보다 훨씬 강력함. 의도가 아니라 세부 동작을 코드로 담기 때문임
소프트웨어가 복잡해질수록 “그건 Jim한테 물어봐” 식의 구두 전승은 한계가 있음
차이가 크지 않다고 느낌. 코드도 결국 .md 파일에 적을 정보의 다른 표현일 뿐임
세밀함과 맥락이 해상도 변화 속에서 사라짐
TDD나 검증 중심 개발엔 동의하지만, 그걸 코드로 쓰는 게 최종 목표는 아님
이미 수백만 줄의 테스트가 존재하니, 그걸 기반으로 발전시키는 게 현실적임
AI가 등장하면서 비로소 TDD가 꿈꾸던 현실이 가능해졌다고 생각함
이런 접근이 흥미롭지만, 블로그 글이 헷갈렸음
Lean이 실제로 어떤 도움을 주는지 궁금함.
예를 들어 Lean으로 상태 머신을 증명하고, 그걸 Dart로 옮기는 식인가?
Lean을 잘 몰라서 이게 현실적인 접근인지 감이 안 옴
최근 Jack Clark(Anthropic 공동창업자)과 Ezra Klein의 팟캐스트에서도 언급됐듯, 모델 정렬(alignment) 은 상대적이며 다양성이 중요하다는 논의가 많음
Mistral의 모델이 다른 최전선 모델에 비해 뒤처진다는 의견도 있지만, 다양한 정렬 기법과 회사를 실험하는 게 생태계에 중요함
결국 시간이 해결해줄 것이라 생각함
실제 성공 사례가 Simon Willison의 Red Green TDD를 떠올리게 함
Leanstral이 실패 환경을 재현하는 테스트 코드를 만들고, 정의적 동등성(definitional equality) 문제를 찾아낸 과정이 인상적이었음
에이전트가 스스로 테스트를 작성한다면, 코드와 테스트를 따로 작성할 때보다 정확성 보장이 더 높아질까 궁금함
TDD는 결국 프롬프트 엔지니어링과 같다고 생각함. 에이전트에게 명확한 목표를 주는 과정이니까
이 모델이 특정 작업에 맞게 훈련되었지만 Opus보다 성능이 낮음
Opus는 6배 비싸지만, 그만한 가치가 있어 보임
아이디어는 좋지만, 결국 품질이 신뢰보다 우선임
자본이 적은 유럽 스타트업이 이런 틈새를 노리는 건 이해되지만, 큰 수익으로 이어지긴 어려울 듯함
벤치마크 신뢰도는 애매하지만, pass@2나 pass@3 결과를 보면 인상이 달라짐
Codex 같은 모델과 비교하는 게 더 흥미로울 것 같음
모델이 오픈소스라서 로컬에서 실행 가능함. 그게 꽤 중요한 포인트 아닌가?
“신뢰할 수 있는 코드”라는 컨셉이 마음에 듦
하지만 비교 기준이 헷갈림. Haiku보다 싸다고 강조하지만, Haiku 자체가 이 작업에 약하고 Leanstral은 그보다 더 약함
정확성이 목표라면 “싸지만 별로”가 왜 중요한지 모르겠음
그래도 Opus도 완벽하지 않으니, 규모를 키우면 더 나은 결과를 낼 수도 있을 듯함
그래프를 보면 pass 수를 늘릴수록 성능이 좋아짐
2회에서는 Haiku와 Sonnet보다 낫고, 16회에서는 Opus에 근접하면서도 비용 효율이 높음
사실 간단함 — 프롬프트에 “신뢰할 수 있는 출력만” 요청하면 됨
Lean을 모르는 입장에서, 이게 직접적인 가치가 있는지 궁금함
Go 같은 언어 코드에 자동으로 증명을 붙여주는 건가, 아니면 단순히 오픈 모델의 다양성을 응원하면 되는 건가?
아마도 에이전트가 Lean4 명세를 생성하고, 그 명세를 기준으로 소프트웨어를 평가하는 구조일 것임
하지만 결국 Lean4 명세 자체가 소프트웨어 아티팩트가 됨
그렇다면 그 명세가 올바른지 검증하는 문제로 다시 돌아감 — 결국 인간 검토가 필요함
몇 주 전부터 이런 흐름을 예상했는데, 실제로 맞아 기쁨임
LLM 시대에는 코드의 인간 친화성보다 증명 가능성과 토큰 효율성이 더 중요해질 것 같음
Lean과 Rust를 결합해, “증명된 코드만 컴파일되는” 세상이 올 수도 있음
관련 논의는 이전 댓글에 정리했음
다만 어떤 증명 시스템도 “옳은 증명”을 보장하지는 않음
단지 논리적으로 유효(valid) 함을 보장할 뿐임
증명이 무엇을 증명하는지 완전히 이해하는 건, 프로그램을 이해하는 것만큼 어렵지만, 그 과정에서 사고가 깊어지는 이점이 있음
“오픈소스”를 말만이 아니라 실제로 Apache-2.0 라이선스 가중치로 공개한 점이 반가움
하지만 커뮤니티 기준으로 보면, 모델을 재현할 수 없으면 “open weights”일 뿐 “open source”는 아님
Mistral 공식 뉴스에 따르면
Claude Opus는 비용 1,650달러에 점수 39.6,
Leanstral pass@8은 145달러에 31.0, pass@16은 290달러에 31.9로, 비용 대비 성능 효율이 꽤 높음
Hacker News 의견들
사람들이 이제 에이전트가 원하는 동작을 명세하고, 그 명세에 맞춰 코드를 작성할 수 있다는 패턴을 인식하기 시작한 게 흥미로움
TDD나 검증 도구 등 어떤 방식을 쓰든, 시간이 지나면 이런 검증 스위트가 “어떻게 동작해야 하는가”를 보여주는 실행 가능한 문서 저장소로 쌓이게 됨
이런 접근은 단순한 마크다운 스펙보다 훨씬 강력함. 의도가 아니라 세부 동작을 코드로 담기 때문임
소프트웨어가 복잡해질수록 “그건 Jim한테 물어봐” 식의 구두 전승은 한계가 있음
세밀함과 맥락이 해상도 변화 속에서 사라짐
TDD나 검증 중심 개발엔 동의하지만, 그걸 코드로 쓰는 게 최종 목표는 아님
이미 수백만 줄의 테스트가 존재하니, 그걸 기반으로 발전시키는 게 현실적임
Lean이 실제로 어떤 도움을 주는지 궁금함.
예를 들어 Lean으로 상태 머신을 증명하고, 그걸 Dart로 옮기는 식인가?
Lean을 잘 몰라서 이게 현실적인 접근인지 감이 안 옴
최근 Jack Clark(Anthropic 공동창업자)과 Ezra Klein의 팟캐스트에서도 언급됐듯, 모델 정렬(alignment) 은 상대적이며 다양성이 중요하다는 논의가 많음
Mistral의 모델이 다른 최전선 모델에 비해 뒤처진다는 의견도 있지만, 다양한 정렬 기법과 회사를 실험하는 게 생태계에 중요함
실제 성공 사례가 Simon Willison의 Red Green TDD를 떠올리게 함
Leanstral이 실패 환경을 재현하는 테스트 코드를 만들고, 정의적 동등성(definitional equality) 문제를 찾아낸 과정이 인상적이었음
이 모델이 특정 작업에 맞게 훈련되었지만 Opus보다 성능이 낮음
Opus는 6배 비싸지만, 그만한 가치가 있어 보임
자본이 적은 유럽 스타트업이 이런 틈새를 노리는 건 이해되지만, 큰 수익으로 이어지긴 어려울 듯함
Codex 같은 모델과 비교하는 게 더 흥미로울 것 같음
“신뢰할 수 있는 코드”라는 컨셉이 마음에 듦
하지만 비교 기준이 헷갈림. Haiku보다 싸다고 강조하지만, Haiku 자체가 이 작업에 약하고 Leanstral은 그보다 더 약함
정확성이 목표라면 “싸지만 별로”가 왜 중요한지 모르겠음
그래도 Opus도 완벽하지 않으니, 규모를 키우면 더 나은 결과를 낼 수도 있을 듯함
2회에서는 Haiku와 Sonnet보다 낫고, 16회에서는 Opus에 근접하면서도 비용 효율이 높음
Lean을 모르는 입장에서, 이게 직접적인 가치가 있는지 궁금함
Go 같은 언어 코드에 자동으로 증명을 붙여주는 건가, 아니면 단순히 오픈 모델의 다양성을 응원하면 되는 건가?
하지만 결국 Lean4 명세 자체가 소프트웨어 아티팩트가 됨
그렇다면 그 명세가 올바른지 검증하는 문제로 다시 돌아감 — 결국 인간 검토가 필요함
몇 주 전부터 이런 흐름을 예상했는데, 실제로 맞아 기쁨임
LLM 시대에는 코드의 인간 친화성보다 증명 가능성과 토큰 효율성이 더 중요해질 것 같음
Lean과 Rust를 결합해, “증명된 코드만 컴파일되는” 세상이 올 수도 있음
관련 논의는 이전 댓글에 정리했음
단지 논리적으로 유효(valid) 함을 보장할 뿐임
증명이 무엇을 증명하는지 완전히 이해하는 건, 프로그램을 이해하는 것만큼 어렵지만, 그 과정에서 사고가 깊어지는 이점이 있음
“오픈소스”를 말만이 아니라 실제로 Apache-2.0 라이선스 가중치로 공개한 점이 반가움
Mistral 공식 뉴스에 따르면
Claude Opus는 비용 1,650달러에 점수 39.6,
Leanstral pass@8은 145달러에 31.0, pass@16은 290달러에 31.9로,
비용 대비 성능 효율이 꽤 높음