Mistral이 대형 모델과 경쟁하기 어렵다는 비판은 타당하지만, 실제로는 작은 모델에서 특정 기능을 고품질로 제공하는 데 집중하고 있다고 봄
OCR이나 파일 분석 같은 작업에 Mistral을 쓰는데, 계정에 100달러를 넣어두면 요청량 걱정 없이 1년은 돌아감
비용이 극히 작아서, Opus 4.8과 경쟁하지 못하더라도 충분히 가치가 있음

OCR에서는 실제로 얼마나 경쟁력이 있는지 궁금함 저렴한 가격에 괜찮은 품질은, 나중에 실수를 줄이기 위해 10배 가격을 내고 최고 품질을 쓰는 것보다 더 틈새시장처럼 보임

유럽 바보들은 돈을 최대한 버는 최적화가 아니라 좋은 제품을 만드는 최적화를 하고 있네 /s

“연 100달러 이하로 1년치 문서 처리”가 생각만큼 훌륭한지는 잘 모르겠음. 적어도 유럽 경쟁력 관점에서는 Mistral이 매출 상한을 너무 낮게 잡는 셈임
OCR은 이미 범용재에 가깝고, 오픈소스 모델이나 AWS 같은 곳에서도 기본으로 제공함
게다가 연 100달러 가격표로는 충성도를 만들기 어렵고, 전환 비용도 없어서 더 낮은 가격이 나오면 고객은 바로 떠날 수 있음
쉽게 복제되는 저가 도구에 고객 락인이 없다면 사업이라기보다 기능에 가까움
구매자 입장에서는 좋겠지만, 유럽 기업이 장기적으로 세계 경쟁사와 제품 역량으로 경쟁하길 원한다면 나쁜 전략으로 보임

작업 자체는 좋지만, 버그 발견 예시가 이상하게 느껴졌음
zigzag 디코딩의 sign 함수에서 Std.U64.MAX 입력 시 (value + 1)이 오버플로되어 디버그 모드에서는 크래시, 릴리스 모드에서는 조용한 손상이 난다고 했는데, 이걸 테스트가 “보통 놓치는” 경계 조건이라고 부를 수 있는지 모르겠음
나쁜 테스트라면 놓치겠지만, 신중한 사람이나 기계학습 기반 코딩 시스템은 “극단값을 테스트해야겠다”를 꽤 잘함. 특히 사용자 입력을 파싱하는 코드라면 더 그렇다
더 흥미로운 버그도 찾았지만 빠르게 설명하기 어려워서 이 예시를 든 건지 궁금함

특히 “퍼징도 놓친다”는 부분이 이상함. 내가 본 퍼징은 일반적으로 경계값을 의도적으로 탐색함
이런 인코딩 라이브러리라면 괜찮은 코드의 기본 기대치가 퍼징이고, 거의 확실히 몇 초 안에 잡혔을 것 같음
실제로 proptest로 아주 간단한 왕복 테스트를 만들었더니 1초도 안 돼 수십 개 실패와 아래 결과가 나왔음: thread 'signed_round_trip' (50528) panicked at tests/test.rs:72:1: Test failed: attempt to multiply with overflow. minimal failing input: value = 4611686018427387904 successes: 2 local rejects: 0 global rejects: 0

“보통 놓친다”고 하긴 어렵겠지만, 실제로 존재했으니 가끔은 놓치는 버그이긴 함
Lean을 쓰면 어떤 예시를 테스트해야 할지 영리하게 고를 필요가 줄어든다는 장점은 드러남

이건 기본적인 품질 보증임. 테스트가 이런 걸 놓친다면 우리가 보통 기대하는 것보다 훨씬 쓸모가 제한적일 것임
저자들의 배경이 궁금해짐

이건 그냥 쓰레기 홍보임
1980년쯤 발명된 모든 속성 기반 테스트 시스템은 경계값을 탐색함
C와 C++의 의미론, 또는 그 부재 때문에 실제 테스트가 어려울 수는 있음. 컴파일러가 정의되지 않은 동작으로 이어지는 모든 입력에 대해 “테스트 통과”라고 해도 허용되기 때문임

글 중간에 여러 최전선급 LLM과 비교가 나오는데, 전부 반년 전 모델들임
“우리 새 모델이 3세대 전 중국 모델들보다 낫다”는 식이라 꽤 웃겼음

이건 60억 매개변수 모델이라 완전히 다른 급임. 오히려 “최전선급 소형 언어 모델”이 더 기대됨

동의하지만, 오픈 가중치이고 비교적 작다는 것만으로도 헤드라인감임. 이 모델은 꽤 잘 돌아감

증명의 문제는 가치를 전달하기가 가끔 어렵다는 데 있음
핵심은 버그를 찾는 게 아니라, 특정 종류의 버그가 특정 가정 아래 없다는 것을 증명하는 것임
하지만 이 이야기는 팔기 어려워서 마케팅은 자주 “이 버그를 찾았다” 쪽으로 흘러감

Lean을 전혀 모르는 사람에게도 유용할 수 있을까? 작업 중인 소프트웨어를 검증하고 싶은데 형식 검증 경험이 없음
명세, 코드, 그리고 제한된 학습 시간만으로도 쓸 만한 결과를 얻을 수 있을지 궁금함

증명하려는 부분 자체는 이해해야 하지만, 전체 증명 과정을 다 이해할 필요는 없음
수학이라기보다 Haskell 타입을 읽는 것에 더 가깝고, 어휘만 수학에서 많이 빌려온 느낌임

글의 “Bug Discovery: Finding Hidden Flaws” 절을 읽어보면, Rust 코드만 가지고 시작해서 오픈소스 Rust에서 문제를 찾는 데 모델을 쓴 것으로 보임
애플리케이션 검증을 위한 Lean 코드를 작성하도록 대화하며 도움받을 수도 있겠지만, 확실하진 않음

최소한 코드에 대해 어떤 정리를 증명하고 싶은지, 그리고 그걸 Lean에서 어떻게 표현할지는 이해해야 함
그렇지 않으면 출력을 검증할 수 없음
기계적으로는 올바르다고 검사된 어떤 명제를 증명했을 수 있지만, 그 명제가 무슨 뜻인지, 실제로 검증하려는 내용을 포괄하는지 모르면 의미가 없음

Lean4를 전혀 모르는 상태에서 약 6개월 만에 대부분의 코딩을 Lean4로 하는 수준까지 왔고, 이 과정은 AI 보조 덕분에 크게 빨라졌음
모델들이 Lean4에 얼마나 일관되게 유창한지 놀라울 정도임. 최전선급 모델뿐 아니라 작은 로컬 모델도 마찬가지였고, LLM이 Lean4를 그냥 잘 이해하는 것 같음
아직 Lean4 전문가라고 부르기엔 갈 길이 남았지만, 이제 유용한 프로그램을 만드는 데 보조가 꼭 필요하진 않음
지식이 거의 없는 상태에서도 완전히 이해하지 못한 부분을 신뢰할 수 있다는 점은 학습 속도를 크게 끌어올림. 불완전한 지식으로도 의존 가능한 프로그램을 얻는 게 실용적이고 동기부여도 됨
중간 증명 단계 전체가 아니라, 자신의 공리와 명제 표면을 설명하는 언어 부분에 의해 한계가 정해지는 느낌임. 시간이 지나 더 많은 것을 하려면 더 많이 이해해야 하지만, 어떤 의미에서는 N+1 수준에서 안전하게 작업할 수 있음
Lean4는 정리 증명 역할과 별개로도 즐거운 프로그래밍 언어이고, 속도도 놀랍게 빠름 io_uring에 붙여서 쓰고 있는데, 많은 경우 C++/libuv나 Rust/Tokio보다 훨씬 빠름
가끔 p99.99 지연 시간 같은 데서 큰 꼬리가 보이면 숫자를 고정 폭으로 바꾸는 식의 튜닝이 필요하지만, C++와 Rust도 튜닝은 해야 함

Lean 4를 형식 검증용으로 밀고 있는 점이 흥미로움
이 영역은 Isabelle/HOL과 TLA+ 쪽이라고 생각했음
적어도 세 가지 모두를 쓰도록 학습한 모델을 기대했을 것 같음. 선형대수의 전방향 유도에는 Isabelle/Isar도 더 나아 보이는데, 누가 설명해줄 수 있을까?

Lean은 Isabelle이나 예전 Coq인 Rocq에 비해 소프트웨어 검증에서 채택이 적었던 게 맞음
이 분야에서는 Agda조차 더 많이 쓰인 편임
다만 Lean은 현재 대안으로 상당한 추진력을 얻고 있고, 특히 범용 함수형 프로그래밍 언어로서의 능력이 큼
개인적으로는 요구사항과 명세를 맞추기 쉬운 Hoare 논리나 분리 논리 기반 접근이 더 실용적이라고 봄. Dafny와 F*가 마음에 듦

Twitter 발표에서 개발자들이 Le Chaton Fat을 슬쩍 언급하는 게 재미있었음
그들이 실제로 Le Chaton Fat에 관여했는지와 무관하게, 진짜 “새로운 대형 범용” 모델이 곧 나올 것 같음
미디어 소동 이후에도 직접 언급했으니 기대됨. 이름은 “Large 4”보다 더 창의적이면 좋겠음