Records · kv:2610.00040v1

Reproduction of dynaroars/neuralsat: VNN-COMP 2023 ACAS Xu benchmark

K-Veritas Team

Submitted by K-Veritas Team

Published 2026-10-13

Independent reproduction · Benchmark or leaderboard entry · Security and cryptography

PaperReproduction of: original code

Abstract

Ran NeuralSAT (src/main.py, default settings, as vnncomp_scripts/run_instance.sh calls it) at the pinned commit on all 186 instances of the VNN-COMP 2023 acasxu benchmark (45 ACAS Xu networks, properties 1 to 10, per-instance timeout from instances.csv, 116 s for most), one instance at a time, counting unsat, sat, timeout and error verdicts and the wall-clock time per instance. Benchmark files come from the ChristopherBrix/vnncomp2023_benchmarks repository; their SHA-256 hashes are printed at the start of the run. One instance (network 1_9, property 7) did not honour its 116 s timeout: the process ran for about 17.7 hours without writing a result and is counted as error, which accounts for most of the run's duration. The src/example folder (109 MB of sample networks) was moved out since the run does not use it. Newer packages than requirements.txt pins (PyTorch 2.11 with CUDA 12.8, gurobipy 13 with its restricted license). One NVIDIA RTX 5060 Ti.

Sealed report

Cite this record

@misc{kveritas261000040v1,
  title={Reproduction of dynaroars/neuralsat: VNN-COMP 2023 ACAS Xu benchmark},
  author={K-Veritas Team},
  year={2026},
  howpublished={K-Veritas Records},
  note={kv:2610.00040v1},
  url={https://kveritas.org/records/2610.00040v1},
}

References

1. [1] Mamadou K. Keita and Christopher Homan. Computer Science Conferences Should Require Nonrepudiable Experimental Results. NeurIPS 2026 Position Paper Track. arXiv:2605.08586.

Sealed with K-Veritas [1]. Listed, not endorsed. A record shows these results came from the sealed code, unchanged. Whether the work is sound is for the reader to judge.