TL;DR

  • 오픈소스 Rust 애플리케이션의 보안 관련 로직을 i5h로 포팅하고 Lean 4로 추출한 뒤, 코딩 에이전트가 명세의 속성을 증명할 수 있는지 평가하는 벤치마크임.
  • 각 과제는 접근 제어, 입력 검증, 파싱 중 하나의 속성을 다루며 에이전트는 포팅된 Rust 코드, 추출된 Lean 코드, 명세를 바탕으로 증명을 시도함.
  • 포팅 코드와 업스트림 코드는 같은 무작위 입력에서 결과가 일치해야 하며, 의도적으로 변형한 포팅 코드는 차등 테스트에서 실패해야 함.
  • 에이전트에는 네트워크 접근 없이 i5h Lean 라이브러리와 스킬이 제공되며, 과제당 40분 동안 증명을 시도하고 조기 중단 시 한 번 재개할 수 있음.
  • 벤치마크 결과는 아직 측정 중인 중간 스냅샷으로, 모든 모델이 모든 과제를 실행한 상태가 아니며 수치가 달라질 수 있음.

i5h 벤치마크

  • 각 과제는 보안 관련 로직이 i5h로 포팅되고 Lean 4로 추출된 오픈소스 Rust 애플리케이션의 속성 하나를 대상으로 함.
  • 에이전트는 포팅된 Rust 코드, 추출된 Lean 코드, 명세를 받아 해당 속성을 증명해야 함.
  • 각 과제를 선택하면 업스트림 Rust 코드, 포팅 코드, 두 코드의 동등성 검사 방식, Lean 코드, 모델이 작성한 증명을 확인할 수 있음.

진행 중

  • 벤치마크는 아직 측정 중임.
  • 아래 결과는 중간 스냅샷이며, 모든 모델이 모든 과제를 실행한 상태가 아니므로 수치가 달라질 수 있음.

i5h란

  • i5h는 애플리케이션 로직의 정확성을 Lean 4에서 증명할 수 있는 Rust 웹 프레임워크임.
  • 빌드 핸들러와 상태 변경 로직은 Rust의 부분집합으로 작성되며, axum과 PostgreSQL 트랜잭션을 사용함.
  • Aeneas는 해당 Rust를 Lean 4 정의로 변환하며, 이 Lean 코드는 실제 실행되는 코드이지 실행 코드를 모사한 모델이 아님.
  • 권한 부여, 테넌트 격리와 그 밖의 불변 조건은 해당 정의에 관한 정리로 표현됨.
  • 이 벤치마크는 기존 오픈소스 애플리케이션의 로직을 i5h로 포팅했을 때 코딩 에이전트가 마지막 증명 단계를 수행할 수 있는지 평가함.

방법

  • 과제 구성과 해결로 인정되는 기준을 설명함.
  • 업스트림 코드(Rust): 고정된 커밋에서 가져온 오픈소스 애플리케이션의 접근 제어, 입력 검증, 파싱 코드임.
  • i5h 포팅(Rust): 함수를 하나씩 포팅함. 문자열은 바이트 슬라이스가 되고 반복자는 루프로 바뀌며, 각 변경 사항은 포팅의 편차 파일에 기록됨.
  • 추출 모델(Lean 4): Aeneas가 포팅된 코드를 추출함. 직접 작성한 명세는 속성을 정리로 표현함.
  • 에이전트의 증명 시도: 네트워크 접근은 제공되지 않으며 i5h Lean 라이브러리와 스킬이 제공됨. 시간 제한은 40분이며, 에이전트가 일찍 멈추면 한 번 재개함.
  • 채점 기준: 증명이 빌드되고, 정리의 명제가 변경되지 않으며, propext, Classical.choice, Quot.sound만 사용해야 함.
  • 차등 테스트: 업스트림 코드와 i5h 포팅 코드를 동일한 무작위 입력으로 실행해 같은 결과를 반환하는지 확인함. 의도적으로 변형한 포팅 코드는 테스트에서 실패해야 함.
  • 차등 테스트는 에이전트에게 제공되지 않음. 벤치마크 자체의 참조 증명도 에이전트에게 제공되지 않으며, 모델이 작성하고 채점기가 승인한 증명은 각 과제 아래에 표시됨.

애플리케이션

  • 업스트림 코드 줄 수는 빈 줄, 주석, 속성을 제외해 계산함.
  • 표의 항목은 애플리케이션, 업스트림 코드 줄 수, 포팅 코드 줄 수, 속성 수, 적어도 한 모델이 증명한 속성 수임.

모델

  • 막대별로 시도한 과제 중 해결한 비율을 표시하며, 모델마다 실행한 과제가 같지는 않음. 과제 수는 각 막대 옆에 표시됨.
  • 해결까지 걸린 시간과 비용은 각 모델이 해결한 과제만 집계함.
  • Rust 코드 줄당 비용은 해당 속성이 다루는 연산의 업스트림 코드 줄 수로 나눈, 해결 과제의 정가 기준 지출임.
  • 표의 항목은 모델, 하네스, 해결 과제 수, 해결당 소요 시간, Rust 코드 줄당 비용임.

과제

  • 과제마다 한 행을 표시함. ✓는 해결, ✗는 미해결, ·는 미실행을 뜻함.
  • 애플리케이션 필터는 전체 과제를 표시하는 옵션을 제공함.
  • 과제 필터는 전체 과제, 모든 모델이 실행한 과제, 일부 모델이 해결한 과제, 어느 모델도 해결하지 못한 과제로 구성됨.
  • 검색 기능을 제공함.