Pith Number

pith:QGCGJZ3F

pith:2026:QGCGJZ3FX5B3XBBFBQTYOWTZFR

not attested not anchored not stored refs resolved

Neurosymbolic Auditing of Natural-Language Software Requirements

Bethel Hall, William Eiers

Large language models with an SMT solver can translate and audit natural-language software requirements for ambiguity and defects.

arxiv:2605.13817 v1 · 2026-05-13 · cs.SE · cs.AI

Open paper page JSON Open Graph Bundle Merged state Verified badge What is a Pith Number?

Add to your LaTeX paper

\usepackage{pith}
\pithnumber{QGCGJZ3FX5B3XBBFBQTYOWTZFR}

Prints a linked badge after your title and injects PDF metadata. Compiles on arXiv. Learn more · Embed verified badge

Record completeness

1 Bitcoin timestamp

2 Internet Archive

3 Author claim open · sign in to claim

4 Citations open

5 Replications open

✓ Portable graph bundle live · download bundle · merged state

The bundle contains the canonical record plus signed events. A mirror can host it anywhere and recompute the same current state with the deterministic merge algorithm.

Claims

C1strongest claim

large language models, equipped with an SMT solver, can audit such requirements: translating them into formal logic, detecting ambiguity through stochastic variation in the generated formalization, and exposing inconsistency, vacuousness, and safety violations through solver queries on the resulting specification.

C2weakest assumption

that stochastic variation in LLM-generated formalizations reliably signals genuine ambiguity in the original natural-language requirement rather than LLM inconsistency or hallucination.

C3one line summary

VERIMED translates natural-language requirements to formal logic via LLMs, detects ambiguity from stochastic formalization differences, and audits for inconsistency and safety violations using SMT queries.

References

29 extracted · 29 resolved · 1 Pith anchors

[1] A. Akinfaderin and S. Subramanian. Verafi: Verified agentic financial intelligence through neurosymbolic policy generation.arXiv preprint arXiv:2512.14744, 2025. 9 2025

[2] M. Allamanis, S. Panthaplackel, and P. Yin. Unsupervised evaluation of code llms with round-trip correctness.arXiv preprint arXiv:2402.08699, 2024 2024

[3] Faithful Autoformalization via Roundtrip Verification and Repair 2026 · arXiv:2604.25031

[4] P. Arcaini, S. Bonfanti, A. Gargantini, and E. Riccobene. How to assure correctness and safety of medical software: the hemodialysis machine case study. InInternational Conference on Abstract State Ma 2016

[5] C. Barrett, P. Fontaine, and C. Tinelli. The satisfiability modulo theories library (smt-lib). www. SMT-LIB. org, 2:68, 2016 2016

Formal links

1 machine-checked theorem link

Receipt and verification

First computed	2026-05-18T02:44:15.312948Z
Builder	pith-number-builder-2026-05-17-v1
Signature	Pith Ed25519 (`pith-v1-2026-05`) · public key
Schema	pith-number/v1.0

Canonical hash

818464e765bf43bb84250c27875a792c754c0bd1fd6e2fe3350400fb14148aec

Aliases

arxiv: 2605.13817 · arxiv_version: 2605.13817v1 · doi: 10.48550/arxiv.2605.13817 · pith_short_12: QGCGJZ3FX5B3 · pith_short_16: QGCGJZ3FX5B3XBBF · pith_short_8: QGCGJZ3F

Agent API

Resolver JSON Graph JSON Events JSON Schema Signing key

Verify this Pith Number yourself

curl -sH 'Accept: application/ld+json' https://pith.science/pith/QGCGJZ3FX5B3XBBFBQTYOWTZFR \
  | jq -c '.canonical_record' \
  | python3 -c "import sys,json,hashlib; b=json.dumps(json.loads(sys.stdin.read()), sort_keys=True, separators=(',',':'), ensure_ascii=False).encode(); print(hashlib.sha256(b).hexdigest())"
# expect: 818464e765bf43bb84250c27875a792c754c0bd1fd6e2fe3350400fb14148aec

Canonical record JSON

{
  "metadata": {
    "abstract_canon_sha256": "a1c4b7fe399eb389cce542ca3b1fbfa06caece94be51760c5b7bb82f8eb2e6c8",
    "cross_cats_sorted": [
      "cs.AI"
    ],
    "license": "http://creativecommons.org/licenses/by/4.0/",
    "primary_cat": "cs.SE",
    "submitted_at": "2026-05-13T17:43:13Z",
    "title_canon_sha256": "f0d61d0272c1d967335b581877d07dc6caa75a70e94f9aaed34390edd5d12856"
  },
  "schema_version": "1.0",
  "source": {
    "id": "2605.13817",
    "kind": "arxiv",
    "version": 1
  }
}