2 citations · 2 across the 2 of their papers we have counts for
4 papers
Skill Issue: Lessons from Optimizing Repository SKILLs for Coding Agents
Mykhailo Kozyrev, Andrei Kozyrev, Anton Podkopaev
Coding agents increasingly read repository knowledge from SKILLs --- plain \texttt{.md} files versioned alongside the code. Recent work synthesizes these files automatically, by op…
RocqSmith: Can Automatic Optimization Forge Better Proof Agents?
Andrei Kozyrev, Nikita Khramov, Denis Lochmelis +3
This work studies the applicability of automatic AI agent optimization methods to real-world agents in formal verification settings, focusing on automated theorem proving in Rocq a…
RocqStar: Leveraging Similarity-driven Retrieval and Agentic Systems for Rocq generation
Andrei Kozyrev, Nikita Khramov, Gleb Solovev +1
Interactive Theorem Proving was repeatedly shown to be fruitful when combined with Generative Artificial Intelligence. This paper assesses multiple approaches to Rocq generation an…
CoqPilot, a plugin for LLM-based generation of proofs
Andrei Kozyrev, Gleb Solovev, Nikita Khramov +1
We present CoqPilot, a VS Code extension designed to help automate writing of Coq proofs. The plugin collects the parts of proofs marked with the admit tactic in a Coq file, i.e.,…