Pith. sign in

REVIEW 3 major objections 5 minor 36 references

A neuro-symbolic pipeline lets an LLM propose requirement selections but hands all structural checks to a deterministic validator, reducing structural errors to 0.39% of decisions and revealing that about a quarter of the model's choices ar

Reviewed by Pith at T0; open to challenge. T0 means a machine referee read the full paper against a public rubric. the ladder, T0–T4 →

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗

T0 review · deepseek-v4-flash

2026-08-01 00:27 UTC pith:2OVLMMVH

load-bearing objection A concrete and reproducible proof-of-concept that a deterministic validator in an LLM loop reduces structural errors in a narrow feature-selection task, but the 'guarantee' language exceeds what the formalization actually supports. the 3 major comments →

arxiv 2607.26220 v1 pith:2OVLMMVH submitted 2026-07-28 cs.SE cs.AI

Model-Driven Requirements Configuration with Three-Valued Uncertainty Scoring

Ahmed Ibrahim This is my paper
classification cs.SE cs.AI
keywords requirements engineeringneuro-symbolic systemslarge language modelsstructural conformanceOOMRAMthree-valued logicuncertainty quantificationproduct-line elicitation
verification ladder T0 review T1 audit T2 compute T3 formal T4 reserved

The pith

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper sets out to prove that a deterministic symbolic checker, not the language model, should be the source of structural correctness in LLM-driven requirements elicitation. It instantiates this idea on the OOMRAM requirement lattice, where a selection is valid exactly when it satisfies four invariants: core nodes are mandatory, single-adaptor nodes select exactly one child, multiple-adaptor nodes select at least one child, and no node is orphaned. The LLM proposes selections from a natural-language project vision; the validator rejects any proposal that violates an invariant and feeds the error back until convergence. On 37 project visions across eleven application families, 35 of 37 runs converge to zero structural falsity with a lightweight model, leaving 0.39% residual errors due to iteration limits, and a frontier model reaches zero falsity on all 37. The three-valued T/I/F scoring then separates mandated choices (T), valid-but-discretionary choices (I, 24.7% of decisions), and structural violations (F).

Core claim

The central claim is that any run that converges is structurally sound by construction: the four invariants Ψ(S) (Eqs. 4–7) are enforced by a deterministic validator that sits between the LLM proposer and the final specification, so logically inconsistent requirement combinations cannot pass. The paper reports that this eliminates structural falsity in 35/37 visions under a lightweight model, with the two non-convergent runs leaving six residual errors (0.39% of all decisions), and that replacing the proposer with a frontier instruction-following model yields 100% convergence with zero falsity. It also claims that a binary correct/incorrect label hides a real distinction: 24.7% of decisions

What carries the argument

The load-bearing object is the OOMRAM requirement lattice, a directed acyclic graph whose nodes are typed as Core, single-adaptor (exactly one child), multiple-adaptor (at least one child), or Option. Structural validity is defined by the global predicate Ψ(S): the conjunction of four invariants — mandatory core selection when a parent is active, exactly-one SA selection, at-least-one MA selection, and orphan prevention. The symbolic validator is a deterministic Python check of Ψ(S) run after each LLM proposal; it returns error messages that the LLM must resolve, and the loop is bounded by a call budget. A frontier-based navigation strategy keeps the LLM's context window O(1) in lattice size

Load-bearing premise

The load-bearing premise is that structural validity for OOMRAM is fully captured by the four invariants in Eq. (8): core mandatory, SA exactly one, MA at least one, orphan prevention; if the real metamodel has additional structural rules, the validator does not enforce them and the reported falsity figures measure only these four checks.

What would settle it

Construct a lattice that includes a constraint outside the four invariants — for example, a rule that two sibling SA choices are mutually exclusive across different parent paths, or that a node's version must match its parent's version — run the pipeline on a vision that triggers that rule, and check whether the final specification violates it. A positive result would refute the claimed 'if and only if' completeness. A cheaper check: audit the six residual errors from the two non-converging eRecord Keeping visions; if any of them involve rules beyond Eqs. (4)–(7), the completeness claim is in

Watch this falsifier — get emailed when new claim-graph text bears on it.

If this is right

  • Any run that converges is guaranteed to satisfy all four invariants; no invalid combination can survive the loop, regardless of the underlying LLM.
  • The residual failure mode of the lightweight model is model-specific: stronger instruction-following models satisfy the 'at least one' constraint and converge on all 37 visions.
  • The validator raises the structural fidelity metric from 0.9635 (unvalidated baseline) to 0.9954 with the lightweight model, cutting the vision-level violation rate from 51.4% to 5.4%.
  • Three-valued scores give analysts a signal of vision underspecification: high indeterminacy marks choices the stakeholder did not pin down, so those nodes are candidates for clarification.
  • Because the LLM is only a heuristic, the same pattern transfers to any requirements meta-model with well-defined constraints without changing the correctness argument.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • The 0.39% figure is an upper bound on conformance only if the four invariants are complete; a deployed OOMRAM repository may carry extra rules (versioning, cross-discriminant dependencies, cardinality bounds) that the validator never checks. A useful next experiment is to instantiate the validator for a richer constraint language and measure how many 'structurally valid' outputs violate those exte
  • The validator doubles as a capability probe: retry counts per node type (12.4% for SA, 28.7% for MA) tell you which constraint shapes the proposer model struggles with; one could use these per-node retry rates to compare models or to fine-tune a small model specifically on the error messages.
  • The indeterminacy metric conflates two distinct things: freedom in the lattice and vagueness in the vision. A testable extension would compare the same lattice against deliberately underspecified versus over-specified visions; if indeterminacy tracks vision specificity, the score becomes a practical ambiguity detector, whereas if it tracks only lattice shape, it is a property of the domain rather

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit.

Referee Report

3 major / 5 minor

Summary. The paper presents a neuro-symbolic multi-agent system for feature-selection from a pre-engineered OOMRAM requirements lattice. An LLM Navigator/Interpreter proposes child-node selections from a natural-language project vision; a deterministic symbolic Validator checks four structural invariants (core mandatory, SA exactly-one, MA at-least-one, orphan prevention) and feeds rejected proposals back for revision. A three-valued ⟨T,I,F⟩ scoring scheme labels each accepted decision as mandated, indeterminate, or invalid. The system is evaluated on 37 project visions across 11 application families, reporting zero structural falsity in 35/37 runs with Llama 3.1 8B and 37/37 with Nemotron 3 Ultra. The paper claims that the symbolic layer guarantees structural conformance for converging runs and that traversal scales linearly in the number of nodes.

Significance. The core mechanism is simple, deterministic, and plausibly useful: it converts an unreliable neural proposer into a bounded configurator for a fixed lattice. The empirical benchmark is broad (37 visions, 11 families), and the claim of public source code and logs supports reproducibility. The three-valued T/I/F scoring is a genuinely useful way to separate stakeholder-mandated choices from legitimate free variability. However, the paper's headline guarantee is stronger than the evidence: the completeness of the four invariants is asserted but not established, the promised convergence proof is absent, and the abstract's unconditional guarantee is contradicted by the two non-converged Llama runs. The contribution is therefore an empirically strong and architecturally clean system with a partial formal core, not a verified formal guarantee.

major comments (3)
  1. [§3.2, Eq. (8); §5.3; Abstract] The central claim that Ψ(S) characterizes OOMRAM structural validity is not established. Ψ is the conjunction of Eqs. (4)–(7), and S=∅ satisfies all four vacuously: every invariant is an implication with a false precondition on the empty set. Thus the validator would certify the empty specification as structurally valid under Eq. (8), which is not a plausible OOMRAM conformance notion. Section 3.2 defers full OOMRAM details (versioning, repository design) to [3,4], and §5.3 concedes the validator is only as strong as the lattice constraints. Consequently, the reported 0.39% / 0% falsity figures measure conformance to Ψ, not to the full OOMRAM metamodel. The Abstract's "guarantees structural conformance" overreaches. Either prove the completeness of Ψ relative to OOMRAM (including root/core inclusion and any additional structural rules), or explicitly redefine the guarantee as conditional
  2. [§1 (contributions); §3.5; Abstract] The introduction lists as a contribution 'a formal proof of validator convergence,' but no such proof appears in the manuscript. Section 3.5 gives only empirical convergence rates and a pragmatic 150-call budget. Moreover, the Abstract's unconditional 'guarantees structural conformance' is contradicted by §3.5's own report that two Llama 3.1 8B runs hit the iteration cap with six residual structural errors. The guarantee is explicitly conditional ("whenever the search converges"), so the formal-proof claim and the unconditional abstract statement should be removed or the missing convergence theorem should be supplied.
  3. [§4.5, Table 5; Eq. (10)] The ablation in §4.5 is reconstructed from logs rather than re-run without the Validator. The baseline row 'Residual violations (final spec) ≥56' appears to equate every one of the 56 validator rejections with a distinct final-specification violation. Multiple rejections can refer to the same node or the same underlying proposal across correction cycles, so 56 is not a justified lower bound on the number of distinct violations. The conservative and defensible number is the 19 visions with at least one rejection. Please either re-run the no-validator condition or clearly label the 56 as 'total rejected proposals,' not 'residual violations in the final spec.'
minor comments (5)
  1. [§3.6 and Table 4] The 24.7% indeterminacy headline is threshold-dependent: Table 4 shows the proportion varies from 18.0% to 31.0% as the keyword-overlap threshold ranges from 1 to 3. The paper does acknowledge this, but the abstract and RQ2 answer state 24.7% without the sensitivity caveat. Please qualify the headline number.
  2. [§4.8] Structural Fidelity Σ uses F=7 in Eq. (9), but §4.2 explains that one of the seven falsity labels was recorded during a correction cycle and is not part of any final specification. The final-output F is 6. Please clarify which F is used in Σ and why.
  3. [References [3,4]] Reference [4] is a Master's thesis with an appended note that the 'foundational OOMRAM ... defined in Appendix B,' but no appendix is provided in the current paper. Please add a precise citation to the published/available specification of OOMRAM so readers can check the completeness of the invariant set.
  4. [Eq. (8)] Eq. (8) uses the symbol '⇐ ⇒'; this should be a single biconditional '⇔'.
  5. [§3.5] The phrase 'guarantees that the execution halts deterministically' is misleading even with the call budget: the budget guarantees termination, but the final output is not guaranteed to satisfy Ψ when the budget is exhausted (as the two non-converged runs show). Please rephrase to say termination is guaranteed, not structural soundness.

Circularity Check

2 steps flagged

The headline indeterminacy rate and the structural-conformance guarantee both reduce to the paper's own definitions, while the empirical benchmark retains independent content.

specific steps
  1. self definitional [§3.2 Lattice Model (Eq. 8); Abstract/Conclusion]
    "A selection set S is structurally valid if and only if it satisfies the global consistency predicate Ψ(S) ... Ψ(S) ⇔ Eqs.(4)∧(5)∧(6)∧(7)"

    Structural validity is defined as Ψ, and the Validator is defined as checking Ψ. Hence the claim that the symbolic validator 'guarantees structural conformance' restates the definition rather than proving conformance to an independent OOMRAM metamodel. The paper does not establish that Eqs. 4-7 are complete for the OOMRAM rules cited from the author's own [3,4]; S=∅ satisfies all four invariants vacuously (Eqs. 4-6 have false antecedents, Eq. 7 quantifies over no selected non-root nodes), so the 'guarantee' is exactly the paper's own predicate, not an external derivation. This is a definitional equivalence, not an independent result.

  2. self definitional [§3.6 Three-Valued Discretion Scoring; §4.2 RQ1 & RQ2 (Table 2)]
    "i d = 1 (Indeterminacy) iff the proposal was accepted by the validator but, the selection is not mandated. This includes any option node, SA or MA choices that differ from the gold standard, and for visions without a gold standard, a child whose keyword overlap is less than two. ... Optional nodes are entirely Indeterminate by definition."

    The Indeterminacy category is defined to include every option node, every SA/MA choice differing from the gold standard, and every below-threshold keyword match (threshold 2). Therefore RQ2's headline finding that 24.7% of decisions are indeterminate and concentrated in 'multiple-adaptor and optional nodes' is a restatement of the scoring rule, not an empirical discovery. Table 4's sensitivity analysis (18%-31% as the threshold varies) confirms the number is an artifact of the hand-set definition.

full rationale

The empirical core of the paper is self-contained and not circular: the four-agent architecture, the deterministic Validator, the 37-vision benchmark, the rejection counts, the ablation reconstruction, and the scalability regression are all concrete and reproducible. The Validator is an external Python function checking the stated invariants, and the RQ1/RQ3/RQ4 claims are grounded in logged runs rather than in the definitions themselves. However, two headline results reduce to definitions. First, 'structural conformance' is defined as Ψ in Eq. 8, so the Validator's guarantee is a tautology with respect to Ψ; the step from Ψ-conformance to OOMRAM conformance is an asserted completeness assumption (the paper itself concedes in §5.3 that 'the symbolic validator is only as strong as the lattice constraints'). Second, the three-valued uncertainty result is constructed by the paper's own labeling rules: every option node is Indeterminate by definition, and the 24.7% figure is directly sensitive to the chosen keyword threshold (§4.4, Table 4). These are self-definitional reductions rather than fitted predictions, so the central uncertainty claim and the overbroad conformance claim are partially circular; the underlying benchmark data provide independent content and keep the score below 8.

Axiom & Free-Parameter Ledger

3 free parameters · 3 axioms · 0 invented entities

The central claims rest on the completeness of the four invariants, the assumption that parsed JSON IDs are real lattice children, a self-created benchmark, a hand-set keyword threshold, and a call budget. The structural-conformance claim is independent of the threshold; the uncertainty claim (24.7% indeterminacy) is threshold-dependent.

free parameters (3)
  • keyword_overlap_threshold = 2 (baseline; 1 and 3 in sensitivity)
    Hand-set threshold defining 'mandated' (T) vs 'indeterminate' (I) for the 34 non-gold-standard visions. The aggregate indeterminacy headline shifts from 18.0% (threshold 1) to 31.0% (threshold 3), so the reported 24.7% depends directly on this choice.
  • call_budget = 150 LLM calls / 250 recursion steps
    Halting cap that defines the convergence rate (94.6% vs 100% under a stronger model). Two runs hit the cap and left residual falsities; a higher cap would likely reduce the 0.39% figure.
  • gold_standard_visions = 3 of 37 visions
    Manual gold standard IDs created by the authors for er_small_biz, er_gov_agency, sh_elderly. These directly determine T/I labels for those runs; all other runs use the keyword heuristic, so the T/I split is partly an author-annotation choice.
axioms (3)
  • domain assumption OOMRAM structural conformance is completely captured by the four invariants Ψ(S) (Eqs. 4–7): core mandatory, SA exactly one, MA at least one, and orphan prevention.
    Section 3.2 states a selection is structurally valid iff Ψ(S) holds. If OOMRAM's full metamodel includes additional rules (cross-discriminant dependencies, versioning, cardinalities beyond these), the validator's 'guarantee' is incomplete.
  • domain assumption The Interpreter LLM always emits existing lattice child IDs in valid JSON; the validator does not verify that an ID exists or matches vision semantics.
    Section 3.3/3.7: only structural checks are applied; a parseable JSON list of plausible-looking IDs passes if the four invariants hold, regardless of whether the IDs correspond to the stakeholder's intent.
  • domain assumption The 37 project visions and 11 family lattices are representative, correctly pre-engineered inputs for the benchmark.
    Section 4.1 describes a self-constructed dataset; no external standard corpus is used, and gold standards exist for only 3 visions, limiting external validity.

pith-pipeline@v1.3.0-alltime-deepseek · 16722 in / 20504 out tokens · 168579 ms · 2026-08-01T00:27:22.950870+00:00 · methodology

0 comments
read the original abstract

Context: Large Language Models (LLMs) offer natural-language flexibility for automated requirements elicitation but frequently generate structurally invalid requirements and logical inconsistencies, lacking formal correctness guarantees. Objectives: This study aims to eliminate logical inconsistencies and enforce structural conformance in LLM-generated requirements while quantifying the LLM's pre-validation decision uncertainty within a formal domain model. Methods: We present a neuro-symbolic multi-agent architecture that operationalizes the Object-Oriented Method for Requirements Authoring and Management (OOMRAM) lattice. The LLM acts as a non-deterministic heuristic for lattice traversal, while a deterministic symbolic validator enforces all structural constraints. We introduce a three-valued (T, I, F) -- Truth, Indeterminacy, Falsity -- framework to classify and score the LLM's requirement decisions before and after validation. Results: Evaluated across 37 natural-language project visions in eleven application families, the system completely eliminated structural inconsistencies in 35 out of 37 cases (94.6%), with the remaining two containing only 6 unresolved structural errors (0.39% of decisions) due to iteration limits. Three-valued analysis revealed that 24.7% of all decisions are indeterminate -- structurally valid but discretionary choices not explicitly mandated by the stakeholder. Conclusion: Offloading structural integrity to a deterministic symbolic layer successfully guarantees structural conformance, while the three-valued classification provides a formal way to measure neural uncertainty, facilitating safe LLM deployment in formal requirements engineering.

Figures

Figures reproduced from arXiv: 2607.26220 by Ahmed Ibrahim.

Figure 1
Figure 1. Figure 1: A fragment of an OOMRAM lattice showing core (blue), single-adaptor (SA, [PITH_FULL_IMAGE:figures/full_fig_p007_1.png] view at source ↗
Figure 2
Figure 2. Figure 2: Neuro-symbolic agent workflow. The Navigator selects the next discriminant [PITH_FULL_IMAGE:figures/full_fig_p010_2.png] view at source ↗

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Reference graph

Works this paper leans on

36 extracted references · 7 canonical work pages

  1. [1]

    Mannion, O

    M. Mannion, O. Lewis, H. Kaindl, G. Montroni, J. Wheadon, Repre- senting requirements of generic software in an application family model, in: W. Frakes (Ed.), Software Reuse: Advances in Software Reusabil- ity, Proceedings of the 6th International Conference on Software Reuse (ICSR-6), Vol. 1844 of Lecture Notes in Computer Science, Springer, Vienna, Aust...

    arXiv 2000

  2. [2]

    Clements, L

    P. Clements, L. Northrop, Software Product Lines: Practices and Pat- terns, Addison-Wesley Software Engineering Series, Addison-Wesley Professional, Boston, MA, USA, 2001

    2001

  3. [3]

    Ibrahim, M

    A. Ibrahim, M. Fakhry, Building requirements repository to enable re- quirements reuse, in: Proceedings of the 14th Annual International Con- ference on Computer Theory & Applications (ICCTA), Egypt, 2004

    2004

  4. [4]

    A. F. Ibrahim, Building Requirements Repository to Enable Require- ments Reuse, Master’s thesis, Arab Academy for Science, Technology and Maritime Transport, the foundational OOMRAM object-oriented requirement lattice and discriminant types are defined in Appendix B. (2005). URLhttps://www.researchgate.net/publication/257936401

    arXiv 2005

  5. [5]

    X. Hou, Y. Zhao, Y. Liu, Z. Yang, K. Wang, L. Li, X. Luo, D. Lo, J. Grundy, H. Wang, Large language models for software engineering: A systematic literature review, ACM Trans. Softw. Eng. Methodol. 33 (8) (Dec. 2024).doi:10.1145/3695988. URLhttps://doi.org/10.1145/3695988 28

    doi:10.1145/3695988 2024

  6. [6]

    J. Lang, M. Fischer, Generative artificial intelligence for requirements engineering in software development – analysis of the state-of-the-art, HCI International 2025 – Late Breaking Papers: 27th International Conference on Human-Computer Interaction, HCII 2025, Gothenburg, Sweden, June 22–27, 2025, Proceedings, Part XVI (2025) 175–185doi: 10.1007/978-3-...

    work page doi:10.1007/978-3-032-13187-4 2025

  7. [7]

    M. A. Zadenoori, J. Dąbrowski, W. Alhoshan, L. Zhao, A. Ferrari, Large language models (llms) for requirements engineering (re): A systematic literature review, preliminary study; cross-checking not yet performed (2025).arXiv:2509.11446

    arXiv 2025

  8. [8]

    Puchleitner, S

    T. Puchleitner, S. Lubos, A. Felfernig, D. Garber, Evaluating large lan- guage models for the automated generation of software requirements, in: Advances and Trends in Artificial Intelligence. Theory and Applications: 38th International Conference on Industrial, Engineering and Other Ap- plications of Applied Intelligent Systems, IEA/AIE 2025, Kitakyushu,...

    work page doi:10.1007/978-981-96-8892-0 2025

  9. [9]

    Masoudifard, M

    A. Masoudifard, M. M. Sorond, M. Madadi, M. Sabokrou, E. Habibi, Leveraging graph-rag and prompt engineering to enhance llm-based au- tomated requirement traceability and compliance checks, arXiv preprint arXiv:2412.08593 (2024). URLhttps://arxiv.org/abs/2412.08593

    Pith/arXiv arXiv 2024

  10. [10]

    J. A. Khan, S. Qayyum, H. S. Dar, Large language model for require- ments engineering: A systematic literature review, Research Square (Preprint)Posted December 2024. Not yet peer reviewed. (2024). doi:10.21203/rs.3.rs-5589929/v1. URLhttps://sciety.org/articles/activity/10.21203/rs.3. rs-5589929/v1

    doi:10.21203/rs.3.rs-5589929/v1 2024

  11. [11]

    Z. Ji, N. Lee, R. Frieske, T. Yu, D. Su, Y. Xu, E. Ishii, Y. J. Bang, A. Madotto, P. Fung, Survey of hallucination in natural language gener- ation, ACMComput.Surv.55(12)(Mar.2023).doi:10.1145/3571730. URLhttps://doi.org/10.1145/3571730 29

    doi:10.1145/3571730 2023

  12. [12]

    Zhang, C

    Z. Zhang, C. Wang, Y. Wang, E. Shi, Y. Ma, W. Zhong, J. Chen, M. Mao, Z. Zheng, Llm hallucinations in practical code generation: Phenomena, mechanism, and mitigation, Proceedings of the ACM on Software Engineering 2 (2024) 481–503.doi:10.1145/3728894

    doi:10.1145/3728894 2024

  13. [13]

    J. J. Norheim, E. Rebentisch, D. Xiao, L. Draeger, A. Kerbrat, O. L. de Weck, Challenges in applying large language models to requirements engineering tasks, Design Science 10 (2024) e16.doi:10.1017/dsj. 2024.8

    work page doi:10.1017/dsj 2024

  14. [14]

    K. C. Kang, S. G. Cohen, J. A. Hess, W. E. Novak, A. S. Peterson, Feature-oriented domain analysis (foda) feasibility study, Tech. Rep. CMU/SEI-90-TR-021, Software Engineering Institute, Carnegie Mellon University (1990)

    1990

  15. [15]

    Alturayeif, I

    N. Alturayeif, I. Ahmad, J. Hassine, TraceLLM: Leveraging large lan- guage models with prompt engineering for enhanced requirements trace- ability (2026).arXiv:2602.01253. URLhttps://arxiv.org/abs/2602.01253

    Pith/arXiv arXiv 2026

  16. [16]

    Ayala, P

    O. Ayala, P. Bechard, Reducing hallucination in structured outputs via retrieval-augmented generation, in: Proceedings of the 2024 Conference of the North American Chapter of the Association for Computational Linguistics: Human Language Technologies (Volume 6: Industry Track), Association for Computational Linguistics, Mexico City, Mexico, 2024, pp. 228–2...

    doi:10.18653/v1/2024.naacl-industry.19 2024

  17. [17]

    Eghbali, M

    A. Eghbali, M. Pradel, De-hallucinator: Mitigating LLM hallucina- tions in code generation tasks via iterative grounding, arXiv preprint arXiv:2401.01701 (2024). URLhttps://arxiv.org/abs/2401.01701

    Pith/arXiv arXiv 2024

  18. [18]

    Hiriyanna, W

    S. Hiriyanna, W. Zhao, Multi-layered framework for llm hallucination mitigation in high-stakes applications: A tutorial, Computers 14 (2025) 332.doi:10.3390/computers14080332

    work page doi:10.3390/computers14080332 2025

  19. [19]

    Chaudhuri, K

    S. Chaudhuri, K. Ellis, O. Polozov, R. Singh, A. Solar-Lezama, Y. Yue, Neurosymbolic programming, Found. Trends Program. Lang. 7 (3) (2021) 158–243.doi:10.1561/2500000049. 30

    doi:10.1561/2500000049 2021

  20. [20]

    A. d. Garcez, L. C. Lamb, Neurosymbolic AI: The 3rd wave, arXiv preprint arXiv:2012.05876 (2020).doi:10.48550/arXiv.2012.05876

    Pith/arXiv arXiv doi:10.48550/arxiv.2012.05876 2012

  21. [21]

    Bayat, A

    A. Bayat, A. Abate, N. Ozay, R. M. Jungers, Llm-enhanced symbolic control for safety-critical applications (2025).arXiv:2505.11077. URLhttps://arxiv.org/abs/2505.11077

    Pith/arXiv arXiv 2025

  22. [22]

    Councilman, D

    A. Councilman, D. J. Fu, A. Gupta, C. Wang, D. Grove, Y.-X. Wang, V. Adve, Towards formal verification of llm-generated code from natural language prompts (2025).arXiv:2507.13290. URLhttps://doi.org/10.48550/arXiv.2507.13290

    doi:10.48550/arxiv.2507.13290 2025

  23. [23]

    R.Yang, X.Liu, Y.Xu, H.Zhao, Haven: Hallucination-mitigatedllmfor verilog code generation aligned with hdl specifications, in: Proceedings ofthe2025Design, AutomationandTestinEuropeConference(DATE), IEEE, 2025.doi:10.23919/date64628.2025.10993072

    arXiv 2025

  24. [24]

    Z. Wang, C. Feng, L. Liu, G. Jiao, P. Ye, The application of llms in the analysis and modeling of software requirements, in: 2024 IEEE 24th International Conference on Software Quality, Reliability, and Security Companion (QRS-C), 2024, pp. 1143–1153.doi:10.1109/QRS-C63300. 2024.00151

    arXiv 2024

  25. [25]

    Ataei, H

    M. Ataei, H. Cheong, D. Grandi, Y. Wang, N. Morris, A. Tessier, Elicitron: A framework for simulating design requirements elicitation using large language model agents, in: Proceedings of the ASME In- ternational Design Engineering Technical Conferences and Comput- ers and Information in Engineering Conference (IDETC-CIE), 2024. doi:10.1115/DETC2024-143598

    work page doi:10.1115/detc2024-143598 2024

  26. [26]

    Oriol, Q

    M. Oriol, Q. Motger, J. Marco, X. Franch, Multi-agent debate strategies to enhance requirements engineering with large language models (2025). arXiv:2507.05981. URLhttps://arxiv.org/abs/2507.05981

    arXiv 2025

  27. [27]

    Bissoli, M

    A. Bissoli, M. Mollaeefar, D. Van Landuyt, S. Ranise, Benchmarking the effectiveness of multi-agent llms in collaborative privacy threat modeling with linddun go, Journal of Information Security and Applications 100 (2026) 104489.doi:10.1016/j.jisa.2026.104489. 31

    arXiv 2026

  28. [28]

    Stoica, L

    F. Stoica, L. F. Stoica, Formal verification of business constraints in workflow-based applications, Information 15 (2024) 778.doi:10.3390/ info15120778

    2024

  29. [29]

    Somogyi, G

    N. Somogyi, G. Mezei, Verifying static constraints on models using gen- eral formal verification methods, in: Proceedings of the International Conference on Model-Driven Engineering and Software Development (MODELSWARD), 2023, pp. 85–93.doi:10.5220/0011796500003402

    work page doi:10.5220/0011796500003402 2023

  30. [30]

    Blikle, Three-valued predicates for software specification and valida- tion, Fundamenta Informaticae 14 (4) (1991) 379–400.doi:10.3233/ fi-1991-14402

    A. Blikle, Three-valued predicates for software specification and valida- tion, Fundamenta Informaticae 14 (4) (1991) 379–400.doi:10.3233/ fi-1991-14402

    1991

  31. [31]

    Konikowska, A

    B. Konikowska, A. Tarlecki, A. Blikle, A three-valued logic for software specification and verification, Fundamenta Informaticae 14 (4) (1991) 401–426.doi:10.3233/fi-1991-14403

    work page doi:10.3233/fi-1991-14403 1991

  32. [32]

    Baharloo, M

    M. Baharloo, M. Amini, A. Bohlooli, Verifying trust over iot-ad hoc networks under uncertainty, Ad Hoc Networks 151 (2023) 103380.doi: 10.1016/j.adhoc.2023.103380

    arXiv 2023

  33. [33]

    Khushal, K

    A. Khushal, K. Fatima, Fuzzy three-valued logic-based machine learning for medical decision support under uncertainty, Computers in Biology and Medicine (2025).doi:10.1016/j.compbiomed.2024.109636

    arXiv 2025

  34. [34]

    Vogelsang, J

    A. Vogelsang, J. Fischbach, Using large language models for nlp tasks in requirements engineering: A systematic guideline (2024).arXiv: 2402.13823. URLhttps://doi.org/10.48550/arXiv.2402.13823

    Pith/arXiv arXiv doi:10.48550/arxiv.2402.13823 2024

  35. [35]

    F. Yang, X. Ma, S. Wang, X. Xu, Q. Cao, N. Zhan, X. Li, B. Gu, Integrating symbolic execution with llms for automated generation of program specifications, accepted by ACM TOSEM (2025).arXiv:2506. 09550. URLhttps://arxiv.org/abs/2506.09550

    arXiv 2025

  36. [36]

    Mannion, B

    M. Mannion, B. Keepence, H. Kaindl, J. Wheadon, Reusing single sys- tem requirements from application family requirements, in: Proceedings of the 1999 International Conference on Software Engineering (IEEE Cat.No.99CB37002), 1999, pp.453–462.doi:10.1145/302405.302677. 32

    arXiv 1999