Oli Ataeva, Khalov A., Tuchkova N.
We investigate whether structured knowledge retrieval from a mathematical library's dependency graph can improve neural theorem proving at inference time while maintaining explainability of the retrieved context. Through a controlled ablation study on the miniF2F-Test benchmark (197~tasks, 8~non-chain-of-thought modes, $K{=}8$ attempts per mode), we find that graph-based retrieval augmentation significantly improves proof generation on hard problems -- those where the base model's parametric knowledge is insufficient -- while having no measurable effect on problems the model already solves reliably. On 109~hard tasks, the best graph-augmented mode nearly triples the baseline success rate (pass@1: $3.56\% \to 10.42\%$, $+6.8$~percentage points, $p{=}0.001$, Wilcoxon signed-rank test). Deterministic pattern-based graph entry points outperform LLM-generated ones ($11\times$ faster, higher accuracy). The retrieved graph context is fully traceable: each hint maps to a specific edge in the Mathlib dependency graph, enabling the user to verify \emph{why} particular lemmas were suggested. The approach is training-free, composable with any base prover, and adds negligible computational overhead.
Natalia Agapova, Rustam A. Lukmanov
Modern automated resume screening systems are typically based on neural text classification models that encode a resume as a feature representation and predict a discrete label corresponding to candidate category, suitability level, or job role. Such models commonly produce class logits parameterized by model weights, which are converted into class probabilities via the softmax function over the target classes. These models are typically trained using cross-entropy loss and deployed as the first stage of automated candidate filtering.
Despite their effectiveness, resume classifiers may encode implicit bias through correlations between predictions and non-job-related or proxy textual features. To study this effect, we analyze feature influence using Integrated Gradients, which assign an attribution score to each input feature based on the path integral of partial derivatives between a baseline representation and the actual input. This analysis reveals systematic dependencies on features that should be irrelevant to candidate evaluation.
Building on these observations, we evaluate multiple debiasing techniques and propose an interpretability-guided framework for bias mitigation. We compare six methods spanning in-processing approaches (GroupDRO, Focal Loss, Label Smoothing, Adversarial debiasing) and attribution-based approaches (Data Scrubbing, Attention Regularization) that leverage the interpretability findings directly. This allows explainable analysis to guide the development of fairer resume screening models.