5 papers
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…
MADD: Multi-Agent Drug Discovery Orchestra
Gleb V. Solovev, Alina B. Zhidkovskaya, Anastasia Orlova +18
Hit identification is a central challenge in early drug discovery, traditionally requiring substantial experimental resources. Recent advances in artificial intelligence, particula…
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.,…
Hybrid Generative AI for De Novo Design of Co-Crystals with Enhanced Tabletability
Nina Gubina, Andrei Dmitrenko, Gleb Solovev +7
Co-crystallization is an accessible way to control physicochemical characteristics of organic crystals, which finds many biomedical applications. In this work, we present Generativ…