HW 0-4: VeriQuick

[bongjunj]

안녕하세요. 조교 장봉준입니다.

이번 공지에서는 참여형 과제 VeriQuick에 대해서 다룹니다.
VeriQuick은 알고리즘의 올바름과 빠름에 대해 Lean으로 구현하고 증명한 것을 모아둔 벤치마크입니다.
보통 프로그램의 올바름만 증명하는 것과는 다르게 VeriQuick에서는 프로그램이 얼마나 빠르게 동작하는지도 검증합니다.
이번 과제에서는 알고리즘의 올바름 명세를 정의하고, 주어진 시간 복잡도 검증 방법에 따라 시간 복잡도를 보여 벤치마크 확장에 기여하는 것을 목표로 합니다.

절차

1. VeriQuick 저장소를 포크(fork)합니다.
2. CONTRIBUTING.md 가이드에 따라 (1) 새로운 알고리즘 구현/검증 또는 (2) 시간 복잡도 검증 방법(Instrumentation.lean)에 기여합니다.
3. 본 저장소 Discussion > Social Contribution 에 본인이 기여한 점을 설명합니다.
4. 조교의 검토를 거쳐 승인된 PR에 따라 보너스 포인트가 제공됩니다.

정책

1. 보너스 포인트는 제출된 PR의 품질과 난이도에 따라 결정됩니다. 승인된 PR에 따라 최대 3 Grade Up을 받을 수 있습니다. (e.g. B+ -> A+)
2. 동일한 알고리즘에 대해 여러 PR이 올라온 경우 선착순으로 인정되며, 먼저 올라온 PR의 품질이 낮거나 더 낮은 시간복잡도를 증명한 경우 차순위 PR에 점수가 제공됩니다.
3. 여러 PR을 제출한 경우 보너스 점수는 누적됩니다.
4. AI 사용은 자유롭게 할 수 있지만, 사용한 경우 명시해주시기 바라며 AI 사용으로 코드 품질이 낮은 경우 PR이 받아들여지지 않을 수 있습니다.

PR 품질 기준

1. 구현이 간결한가?
2. 명세가 올바르고 빠트림이 없는가? (빠트림 예시: 정렬 알고리즘의 올바름을 보이는데 출력이 정렬됨만 보이고 입출력 원소가 서로 순열 관계임을 보이지 않음)
3. 알려진 이상적인 시간 복잡도를 증명하였는가? (이상적이지 않은 예시: O(log n) 알고리즘을 O(n)으로 구현)

기간

• 11월 30일까지 올라온 PR에 대해서는 보너스 점수가 제공됩니다.
• 11월 30일 이전에 PR을 연 경우, 11월 30일 후에 추가 커밋을 올리면 해당 PR은 인정되지 않습니다.

그 외 질문은 자유롭게 댓글 달아 주시기 바랍니다.

---

Hi, this is your TA, Bongjun Jang

This announcement covers the participatory assignment, RealQuick.
VeriQuick is a benchmark that collects algorithm's implementation, correctness, and time complexity in Lean.
Unlike conventional program verification, VeriQuick requires time complexity proofs of programs.
In this assignment, you will define the correctness and the time complexity of an algorithm, implement the algorithm, and prove the correctness and the time complexity.

Procedure

1. Fork the VeriQuick repository.
2. Following the CONTRIBUTING.md guidelines, contribute to (1) implementing and verifying a new algorithm and (2) the time complexity verification framework (Instrumentation.lean).
3. Upload your work and explanation at Discussion > Social Contribution at this repository.
4. Students will be awarded with bonus points, once the PRs are approved.

Policy

1. Bonus points will be determined based on the quality of the submitted PR. Each approved PR can raise your final grade by up to three grade steps. (e.g. B+ -> A+)
2. PRs will be approved in the first-come-first-served manner. However, if the first PR is of insufficient quality or do not prove the desired time complexity, next PRs can be approved.
3. Bonus points accumulate with multiple PRs.
4. You may freely use AI. However, you must specify how you used it, and, if the quality is low, the PR can be rejected.

Quality Criteria

1. The implementation must be succinct
2. The specification must be sound and complete. (e.g. only specifying the sortedness of the output and not specifying the permutation of the input and output lists).
3. Does it prove the desired time complexity? (e.g. O(n) is implemented when O(log n) is possible)

Due Date

1. Bonus points will only be awarded for PRs submitted by November 30. PRs submitted after the deadline will not be accepted for bonus credit.
2. If you open a PR before November 30 but add additional commits after November 30, the PR will also be ineligible for bonus credit.

If you have any other questions, please feel free to leave a comment.

[bongjunj]

안녕하세요 조교 장봉준입니다.

VeriQuick 프로젝트에 참여해주셔서 감사합니다.
LLM이 코드와 증명을 모두 잘 생성하는 시대입니다.
그러나 LLM을 돌려서 코드 및 증명을 찍어내는 것이 이 과제의 핵심은 아닐 것입니다.
LLM이 빠르고 정확해지는 만큼, 그 결과를 다른 사람에게 효과적으로 전달하는 일은 더 중요해지기 마련입니다.

이를 위해 PR 제출 전에 다음 사항을 지켜주시길 부탁드립니다.

1. 다음 글을 읽어보세요: Mathematics in the Age of AI(Terrence Tao, https://arxiv.org/pdf/2608.16753)
2. 기계적인 출력 결과보다, 리뷰어(교수님, 조교 및 외부인 누구나)가 쉽게 이해할 수 있도록 설명해주세요. 설명은 Discussion > Social Contribution에 제출하시면 됩니다. 다음 사항을 먼저 생각해보시길 바랍니다.

• 풀고자 하는 문제는 한 마디로 요약하면 무엇인가?
• 이 문제를 풀면서 가장 어려웠던 점은 무엇인가? (예: 어떠한 불변식을 떠올리기 힘들었던 과정, 계산이나 증명이 어쩔 수 없이 길어졌던 과정, 더 깔끔하고 쉬운 방법을 생각해봤으나 실패한 이유)
• 설명은 두괄식으로 구성해주세요. 문단을 작성한 뒤 다시 읽어보시고, 가장 중요한 내용이 첫 문장인지 확인해보시기 바랍니다.

3. 문제를 푸는 것보다 중요한 것은 다른 사람에게 진심을 전달하는 일입니다.

감사합니다.

---

Hi, this is your TA Bongjun Jang.

Thank you for participating in the VeriQuick project.
LLMs can now effectively generate both code and proofs.
However, mechanically generating code and proofs is not the core objective of this assignment.
The faster and more accurate LLMs become, the more important communicating your work to others becomes.

To this end, please keep the following in mind before submitting your PR:

1. Read this article: Mathematics in the Age of AI(Terrence Tao, https://arxiv.org/pdf/2608.16753)
2. Explain your work clearly for your reviewers (the professor, TAs, and others). Submit your explanation at Discussion > Social Contribution. Consider the following points:

• What is the problem you are solving, summarized in a single clear sentence?
• What was the most challenging part of solving it? (e.g. identifying the key invariant, unavoidably lengthy calculations, or struggling to find a more succinct solution)
• Put the bottom line up front (lead with the conclusion). Review each paragraph and verify that the main point appears in the first sentence.

3. Keep in mind that what matters the most is demonstrating your genuine thought and interest to others.

Thank you