Claude, 123개 오픈소스 라이브러리에서 수년간 숨어 있던 버그를 찾아내고 형식 검증까지 해냈다
LLMs are making formal software verification feasible at a much larger scale
Anthropic이 Theorem과 협력해 Claude로 123개 오픈소스 라이브러리의 RISC-V 어셈블리 코드 수준에서 보안 속성을 증명했다. 기존 퍼즈 테스트를 명세로 변환해 64MB 이하 모든 입력에서 크래시가 없음을 증명했고, 그 과정에서 수년간 수조 회의 테스트에도 잡히지 않던 버그들을 발견해 수정했다. 약 1억 8천만 줄의 Rocq 증명이 생성됐으며, 신뢰해야 할 구성 요소는 RISC-V·Linux 시맨틱, 정리 명세, Rocq 검사기뿐이다.
seL4 운영체제 커널을 구현하는 데는 2인년이 걸렸지만, 이를 형식 검증하는 데는 20인년이 걸렸다.
HN 토론
238- yazaddaruvala
오히려 어느 정도 반대의 일이 벌어질 거라고 생각한다. LLM은 LLM이 생성한 명령형 스타일 코드를 형식 검증하지 않을 것이다. 우리(에이전트 개발 포함)는 명령형 언어에서 벗어나 함수형을 건너뛰고 결정론적 선언형 언어로 이동할 것이다.
아마도 SQL을 위한 Typescript와 다소 유사하지만, 명령형 언어와 동일한 결과를 간결하게 포착하기 위해 훨씬 더 미묘한 연산자를 갖춘 실험적 언어들이 확산될 것이다.
이들은 게임 개발이나 심지어 Linux 커널(리누스가 동의할 리 없겠지만 ㅋㅋ)에서도 성능 좋게 실행될 수 있도록 컴파일되지만, 동시에 사실상 공유 메모리 공간을 가진 분산 실행 엔진에서도 실행될 수 있을 것이다.
훨씬 더 간결한 아티팩트를 가능하게 한다. 환각 가능성이 낮아지고, 출력 토큰이 줄어들며, 사고 루프 반복이 줄어들고, (필요한 영역에서는) 인간이 검토하기에 충분히 간결하다.
게다가 함수의 능력 등을 대폭 제한하는 추가적인 정리(theorem) 같은 구문, 아마도 검증을 위한 일종의 고수준 효과 시스템이 있을 것이다. 이는 "암호 함수를 위한 상수 시간 컴파일", 로컬 컨텍스트에서 쓰기와 읽기에 대한 "ACID 준수 보장", 분산 실행 엔진의 함수에 대한 "정확히 한 번 전달 보장" 등 많은 것에 사용된다.
그 시점에는 모든 프로그램이 기본적으로 형식 검증될 것이다. AdaErlangSQL+++라고 생각하면 된다.
- jaykru
부록 [0]에서: "에이전트가 작성한 증명은 동일한 정리의 다른 어떤 증명만큼이나 '좋다'. 즉, 동등성 정리를 증명한다. 그러나 에이전트가 이 장황한 증명 스타일을 더 복잡한 프로그램으로 직접 확장할 수 있을지는 아직 지켜봐야 한다. MachCSL과 같은 다른 에이전트 기반 검증 프로젝트의 경험은 답이 '아니오'일 수 있음을 시사한다. 에이전트는 장황한 증명 스타일로 인해 복잡성 장벽에 부딪혔고, 확장하려면 증명이 더 나은 모듈식 추상화와 추론 원칙을 중심으로 구조화되어야 한다. 만약 그렇다면, 에이전트가 이 복잡성을 줄이기 위해 올바른 추상화를 발견하고 도입하도록 어떻게 도울 수 있을까? 전문 증명 엔지니어의 입력이 필요한가, 아니면 확장 가능한 증명을 가능하게 하는 좋은 추상화를 발견하도록 에이전트를 안내할 수 있는 공통 원칙을 추출할 수 있을까?"
일부 수학자들은 최근 LLM 증명 배포에서 유사한 패턴을 관찰했고, 이로 인해 LLM이 인간 수학의 볼록 껍질(convex hull)을 넘어서는 수학적 능력에서 장벽에 부딪힐 것이라고 제안했다. 형식 검증에서 수행되는 증명은 LLM 추론에 대한 꽤 흥미로운 리트머스 테스트인데, 고려되는 시스템이 반드시 분포 내에 있지는 않기 때문이다(수학에서는 다루는 '시스템'과 구조, 그리고 그에 대한 증명이 수천 권의 개별 책에 등장하는 것과 비교된다). 따라서 사전 훈련된 LLM이 인간보다 갖는 광범위한 도메인 지식의 이점은 별로 도움이 되지 않는다. 내 생각에 이 관찰은 […]
- malisper
회의적인 사람들을 위해, 나는 Postgres를 Rust로 다시 작성하면서 형식 검증을 사용해 꽤 성공을 거두었다. Rust와 C 코드를 모두 Lean으로 변환하는 컴파일러를 작성했다. 두 함수가 Lean에 들어가면, LLM이 두 함수가 동일하게 동작한다는 Lean 증명을 작성한다.
지금까지 약 12%의 코드가 단일 스레드로 실행될 때 동일하게 동작함을 증명했다. 이는 대략 70k 줄의 C 코드에 해당한다. 이 과정에서 플랫폼 간 부동 소수점 연산이 다른 결과를 낼 수 있는 방식 등 아주 사소한 동작 차이를 발견했다.
이를 확장하는 방법을 찾고 있지만, 더 확장하는 것을 막을 근본적인 한계는 보이지 않는다.
- fedupnow
나는 35살이고, 그들이 원하는 대로 되면 망했다. 나는 기술직으로 가지 않을 것이다. 27살에 건설업을 그만두었는데, 프로그래밍을 너무 사랑했기 때문이다. 건설업에서 일할 때는 거의 매일 자살하고 싶었다. 너무 싫어서 20대를 술로 날렸다. 지금은 프로그래밍 덕분에, 그리고 내가 하는 일을 정말 사랑하기 때문에 몇 년째 금주 중이다. 그런데 이 회사가 여러모로 내 일을 빼앗고 있다.
나는 인생의 상당 부분과 전 재산을 이 전환에 투자했다. 이제는 Anthropic이 어떻게든 정지 문제를 해결하겠다고 주장하기 때문에 매일 전기기사가 되라고 소리치는 말을 듣고 있다. 그들은 주장하는 것을 실제로 해낼 필요도 없다. 업계의 20%만 설득하면 되고, 나 같은 사람들은 은퇴할 만큼 오래 일할 기회를 절대 얻지 못할 것이다.
나는 그들이 성공할 거라고 정말 생각하지 않지만, 만약 성공한다면 나는 공공 도서관에서 코딩하며 노숙자가 될 것이다. 다시 처음부터 시작하지는 않을 테니까.
- sestep
지난 몇 주 동안 직장에서 이걸 해왔다. 에이전트가 SIMD나 CUDA를 사용해 어떤 함수를 더 빠르게 만든다는 실험을 보여주는 PR을 열고, 그 PR에 원래 구현과 동작적으로 동등하다는 Rocq 증명이 있기 때문에 자신 있게 병합할 수 있다는 것은 엄청나게 강력하다.
- pinevale
무엇에 대한 형식 검증인가?
의도된 모든 입력과 의도되지 않은 입력, 모든 이해관계자의 이익, 가능한 모든 사용자 행동을 포괄하는 100% 커버리지의 형식 명세? 바이브코딩 시대에? 아니다, 그 페이지는 이게 존재하지 않는다는 것을 인정할 정도로 양심은 있다.
결국 그들은 기존 퍼저로 크래시를 찾고, 크래시를 고치고, 그런 다음... 크래시가 고쳐졌다는 형식 증명을 작성하는 것으로 귀결된다? 그건... 꽤 무의미해 보이는데? 내가 뭔가 놓치고 있는 건가?
- Olscore
집을 짓는 데는 세 가지 층이 있다:
1. 비전: 우리가 원하는 것 (우리의 의도)
2. 청사진: 우리가 작성한 명세 (우리의 설계)
3. 검사: 우리가 지은 것을 청사진과 대조하는 것 (증명)
이 연구는 검사를 거의 완벽하게 만든다. 하지만 검사는 청사진만 확인할 뿐 우리의 비전은 확인하지 않으므로, 잘못된 청사진으로 지은 집도 완벽한 검사를 통과할 수 있다. 나머지 절반은 청사진이 우리의 의도와 일치하고 에이전트가 짓는 동안에도 그렇게 유지되도록 하는 것이다. 나는 그 부분을 작업 중이므로, 이것은 상호 보완적이라고 생각한다:
- passive
가능성이 높아 보였지만, 지금까지 소프트웨어에 LLM을 도입한 것이 대부분 모범 사례를 버리는 것이었기 때문에, 이것이 우리를 확장된 검증으로 이끌 것이라고는 회의적이다.
Bezos가 직원들에게 병에 오줌을 싸게 하면서 우리가 주 3일 근무를 하게 될 것이라고 말하는 것과 같다.