LLM Hacker News Mar 17, 2026 1 min read
2026년 3월 16일 Hacker News에서는 Mistral의 Leanstral 공개가 277 points와 49 comments를 기록했다. Lean 4 proof engineering에 맞춘 Apache 2.0 open model과 FLTEval benchmark 결과가 커뮤니티의 관심을 끌었다.
#formal-verification
RSS 피드AI Reddit Mar 5, 2026 1 min read
r/MachineLearning에서 주목받은 TorchLean은 PyTorch 스타일 실행 경로와 정형 검증 경로를 Lean 4 안에서 같은 의미 체계로 통합하려는 시도다. Float32 의미론, SSA/DAG IR, IBP·CROWN 계열 검증을 결합해 안전성 검증 파이프라인의 의미 불일치 문제를 줄이는 데 초점을 둔다.