arXiv subjects

Akond Ashfaque Ur Rahman

Publications and source records attributed to Akond Ashfaque Ur Rahman.

3 recordsLinked to original sources

arXiv2026

Can Open-Weight LLMs Produce Kernel-Verified Coq Proofs? A Pilot Study

Large language models (LLMs) can generate text that resembles a mathematical proof, but resemblance does not establish correctness. A formal proof checker verifies whether each proof step follows established logical rules. Coq bases its rules on the Calculus of Inductive Constructions, a logical framework that defines which proof steps the system may accept. This pilot study evaluated six open-weight LLMs on the same 100 theorems from CoqStoq, a benchmark derived from real Coq projects. Each LLM received one attempt per theorem with the temperature set to 0, and Coq checked every proposed proof in the theorem's original project environment. We counted a proof as successful only if the Coq kernel accepted it. Gemma 4 verified 12 of 100 theorems, Llama 3.3 verified 8, and DeepSeek Coder V2 Lite verified 1. Qwen 3.5, Mistral Small 3.1, and GPT-OSS verified none. The 21 successful model-theorem results covered 15 distinct theorems, 11 of which were not solved by a baseline of standard Coq tactics. All verified theorems had short or medium human-written reference proofs; no model verified a theorem with a long reference proof. Because the proof-length analysis was exploratory, this pattern does not establish that proof length caused the difference. For the three models with at least one success, the total generation cost per verified proof ranged from 741 to 36,193 output tokens, 14.9 to 178.0 seconds, and 0.0167 to 0.2000 aggregate GPU hours. We could not calculate these ratios for models with no verified proofs. Across 600 attempts, the models produced 21 kernel-verified proofs, giving an overall success rate of 3.5%. The study reports descriptive differences among the models but does not statistically test whether one model outperforms another. Therefore, the results do not establish a universal ranking of the six models.

cs.LO↗

arXiv2026

An Evaluation of Large Language Models for Detection of Malicious Python Packages

Modern software development relies on open-source package repositories. Attackers use these to distribute malicious packages. Large Language Models (LLMs) can automatically detect these packages, but their ability to pinpoint specific malicious behaviors remains unclear. We evaluate 13 LLMs on two tasks using a dataset of 4,070 PyPI packages (370 malicious, 3,700 benign). The first task detects whether a package is malicious. The second identifies specific malicious indicators (lines of code). We evaluate each LLM across five prompt strategies and three temperatures. For the first task, LLMs achieve mean F1 scores from 0.40 to 0.99, detecting most malicious packages but frequently flagging safe ones. For the second task, LLMs achieve a weighted F1 score of 0.69 for recognizing behavior types, dropping to 0.48 when identifying specific indicators. LLMs recognize standard code patterns but miss indicators requiring broader context or the author's intent. LLMs also report absent indicators. Evaluating the association between performance and model size, context width, prompt strategy, temperature, and code complexity reveals only code complexity has a meaningful impact: longer packages are harder to analyze. We recommend using LLMs for initial triage to flag suspicious packages for human review, rather than identifying specific malicious mechanisms.

cs.CR↗

arXiv2025

Unveiling Malicious Logic: Towards a Statement-Level Taxonomy and Dataset for Securing Python Packages

The widespread adoption of open-source ecosystems enables developers to integrate third-party packages, but also exposes them to malicious packages crafted to execute harmful behavior via public repositories such as PyPI. Existing datasets (e.g., pypi-malregistry, DataDog, OpenSSF, MalwareBench) label packages as malicious or benign at the package level, but do not specify which statements implement malicious behavior. This coarse granularity limits research and practice: models cannot be trained to localize malicious code, detectors cannot justify alerts with code-level evidence, and analysts cannot systematically study recurring malicious indicators or attack chains. To address this gap, we construct a statement-level dataset of 370 malicious Python packages (833 files, 90,527 lines) with 2,962 labeled occurrences of malicious indicators. From these annotations, we derive a fine-grained taxonomy of 47 malicious indicators across 7 types that capture how adversarial behavior is implemented in code, and we apply sequential pattern mining to uncover recurring indicator sequences that characterize common attack workflows. Our contribution enables explainable, behavior-centric detection and supports both semantic-aware model training and practical heuristics for strengthening software supply-chain defenses.

cs.CR↗