Publications
- A. Kozyrev, G. Solovev, N. Khramov, A. Podkopaev (2024). CoqPilot, a plugin for LLM-based generation of proofs. ASE’24, doi
10.1145/3691620.3695357 pdf video (5 min) - A. Kozyrev, N. Khramov, G. Solovev, A. Podkopaev (2025). RocqStar: Leveraging Similarity-driven Retrieval and Agentic Systems for Rocq generation. arXiv preprint pdf
Talks
- CoqPilot benchmarking framework. EuroProofNet workshop’25, dedicated to Theorem Proving and Machine Learning in the age of LLMs: SoA and Future Perspectives. abstract recording
Education
- 2023 — 2025, M.S., Computer Science, Constructor University Bremen
Thesis: A. Kozyrev, A. Podkopaev. Similarity-driven Retrieval Mechanism for Rocq theorems. pdf - 2022 — 2023, B.S., Computer Science, Constructor University Bremen
Thesis: A. Kozyrev, A. Podkopaev. Equality saturation for solving equalities of relational expressions. pdf code - 2020 — 2022, Undergrad student, Mathematics and Computer Science, St. Petersburg State University
Professional Experience
- December 2022 – present: Research Scientist, JetBrains Research, Germany
- January 2022 – May 2022: IOS Software Developer, Russia