Reviewer has chosen to be Anonymous

Overall Impression: Weak

Content:
Technical Quality of the paper: Average
Originality of the paper: Yes, but limited
Adequacy of the bibliography: Yes

Presentation:
Adequacy of the abstract: No
Introduction: background and motivation: Good
Organization of the paper: Satisfactory
Level of English: Satisfactory
Overall presentation: Weak

Detailed Comments:

The paper proposes a three-stage pipeline (NL--> FOL grounding, trust-aware verification against a digitally signed Knowledge Graph, explanation generation) for verifying LLM-generated claims. The main declared contribution is a five-signal trust function (digital signature, reputation, freshness, provenance completeness, corroboration) that weights the KG triples during verification. The authors report preliminary results both on the grounding stage (FOLIO, LE=0.853; medical claims, LE=0.801) and on an end-to-end pipeline (30 Verified, 1 Falsified, 19 Indeterminate over 50 claims). The work has genuine system design merits and the related work section is solid, but it suffers from a significant misalignment between the theoretical apparatus presented (in particular the integration with Logic Tensor Networks) and what is actually implemented and evaluated. Strengths
- Extensive and well-organized related work and background.
- Clear illustrative examples
- Well-motivated evaluation metrics.
- Proven formal properties (Propositions 1-3) provide interpretable guarantees on the system's conservative behavior (default to Indeterminate in the absence of evidence).
- Partial honesty about limitations: the authors themselves note in several places (Sec. 5.2, Sec. 7) that the evaluation is preliminary and that some components (E1, E3, ablation) are deferred to future work.

Major concerns
Section 3.2 presents the integration with LTNs as the central innovation; Equation 6 defines a trust-weighted satisfiability loss, w_t \dot f_θ(φⱼ), where f_θ is the neural predicate grounding function proper to the LTN framework (Badreddine et al. 2022). But:
- in none of the reported examples does a value of f_θ appear. All calculations shown use exclusively w_t.
- Section 5.2 confirms that the actual implementation uses "rule-guided filters" and embedding similarity retrieval (sentence-transformers), not a differentiable neural component. The authors themselves acknowledge in Section 7 that the learned, differentiable LTN objective is not yet implemented and will be the subject of the "first follow-up paper," replacing the current "rule-based retrieval+verdict combination." Consequently, the title, abstract, and Eq. 6 promise a differentiable neuro-symbolic system, but the system actually built and evaluated is a rule-based system with semantic retrieval and trust thresholds.

The passage from a logical formula to KG evidence is described in an extremely vague manner. Algorithm 1 condenses it into a single line ("Retrieve supporting triples S⁺ ⊆ G for φⱼ"), and Section 3.2 mentions only generically "embedding-based similarity (TransE-style)... combined with rule-guided filters." It is not clear how an FOL predicate is transformed into a retrieval query, nor how the semantic misalignment between the closed-world assumption (FOL) and the open-world assumption (OWL/RDF) is concretely resolved — a problem the authors themselves acknowledge in Section 6.1 but for which they offer only a preventive mitigation (constraining the grounding vocabulary to the target ontology), not a mapping algorithm. An explicit formal description of this step is recommended, with pseudocode or at least an end-to-end example showing the predicate→query→retrieved triples transformation.

The dataset of 50 medical claims was curated by the authors themselves and not validated by independent clinical experts (explicitly admitted in Section 5.2). The KG of 98 triples is admittedly built ad hoc "to permit complete authorial control over signatures and provenance metadata," is not representative of a real KG, and does not allow for a meaningful computation of E1 nor an E3 (macro-F1) evaluation against ground-truth verdicts; and Tables 5-6 and Scenario 3 present trust coefficients (rep, fresh, comp, corr) manually assigned by the authors "using a public registry," without a description of the procedure or any inter-annotator reliability checks. These limitations are declared by the paper itself, which is commendable for transparency, but they make the numerical results (30/1/19 verdicts) demonstrative of architectural executability rather than of real accuracy a point that should be reflected more explicitly in the abstract and conclusion, where the numbers are instead presented with a weight that suggests broader validity.

Several components presented in the architectural flow are adopted from external works without always being clearly distinguished from the original contributions in the text (although correctly cited): - the grammar-masked decoding (Eq. 2) is from Li et al. (2024), not the authors. - the NL-->FOL translator (LogicLLaMA) is from Yang et al. (2024). - the differentiable logic framework (LTN) is from Badreddine et al. (2022).

Section 4.3 defines five ablation variants explicitly designed to isolate the contribution of each architectural component; however, none of these ablations is executed or reported. Thus, the implicit claim that trust weighting is responsible for the quality of the reported verdicts (Section 5.2, "Interpretation") remains empirically unverified

Minor
- The ⟨s,p,o⟩ notation for triples (Table 4, p. 14) is never made explicit as the standard RDF convention (subject-predicate-object), making the paper less accessible to readers who are not Semantic Web specialists.
- f_θ appears in Table 4 and in Eq. 6 without an explicit reference to where/how it is defined in the originating LTN framework, leaving the reader to infer the connection.
- The manual assignment of the α_i coefficients (Section 3.5, "Sensitivity to α Coefficients") shows only one example of sensitivity analysis; systematic criteria or data for calibrating these hyperparameters are missing, despite Section 6.2 recommending a three-step calibration protocol.
- Table 7 (comparison with neural-only and standard RAG) is useful but remains a qualitative/analytical comparison, not an empirical comparative evaluation on the same data.

The paper presents a potentially relevant system design idea, supported by a solid literature review and clear formal properties. However, the set of identified concerns cannot be attributed to incremental corrections: it concerns the very coherence between what the paper claims to have built and what has actually been implemented and evaluated.
In particular, the gap between the central architectural promise (differentiable integration with Logic Tensor Networks, presented in Eq. 6 as the technical core of the contribution) and the system actually evaluated (embedding similarity retrieval and fixed thresholds, with no differentiable neural component whatsoever) is not a missing implementation detail, but fully affects the contribution declared in the title and abstract, reducing the neuro-symbolic impact of the work. Similarly, the absence of concrete ablation studies leaves without empirical verification precisely the thesis the paper sets out to demonstrate, namely that trust weighting improves verification quality compared to a uniform treatment of evidence. Added to this are an evaluation dataset and KG both built by the authors themselves, too small to support generalizable conclusions, and an FOL-->KG mapping that is never made explicit.
For these reasons, it is considered that the paper in its current form is not suitable for a simple minor or major revision within the same review cycle, since the concerns require substantial re-implementation work (primarily of the LTN objective, or alternatively an honest rescoping of the contribution) and empirical validation (ablation studies, adequately sized dataset/KG, independent clinical validation). Reject and resubmit is therefore recommended: the authors are encouraged to resubmit the work in a future version that:
- explicitly aligns the theoretical apparatus with what is actually implemented, either completing the LTN integration or consistently rescaling the architectural claims
- formally specifies the FOL-->KG mapping
- executes and reports the ablation studies already defined in the protocol
- extends the evaluation dataset and KG to a scale and level of independent validation adequate to support the conclusions presented.

Reviewer has chosen not to be Anonymous

Overall Impression: Good

Content:
Technical Quality of the paper: Good
Originality of the paper: Yes, but limited
Adequacy of the bibliography: Yes, but see detailed comments

Presentation:
Adequacy of the abstract: Yes
Introduction: background and motivation: Good
Organization of the paper: Satisfactory
Level of English: Satisfactory
Overall presentation: Excellent

Detailed Comments:

- Summary -

The paper proposes a trust-centric neuro-symbolic architecture for verifying LLM-generated claims. The pipeline translates natural language into FOL, verifies claims against a provenance-rich knowledge graph using trust scores, and produces explanations linked to the supporting evidence. The main contribution is the incorporation of provenance signals such as signatures, reputation, freshness, completeness, and corroboration into the verification process.

I find the problem important and the overall architecture interesting, particularly the explicit treatment of conflicting or insufficient evidence through an Indeterminate verdict. However, several central claims are stronger than what is currently implemented and evaluated.

- Reasons to accept -

The paper addresses an important problem for trustworthy LLM systems and fits the scope of the journal well.

The integration of provenance and source credibility into neuro-symbolic verification is promising. The five-component trust score is interpretable, and the conflict-aware verdict mechanism provides a useful way of avoiding forced decisions under weak or contradictory evidence.

The architecture is clearly structured, and the illustrative walkthrough in Section 3.5 is particularly helpful for understanding the intended behavior of the system.

- Reasons for major revision -

1. The role and contribution of differentiability are unclear
Equation 6 introduces a trust-weighted differentiable satisfiability objective and states that gradient updates to θ prioritise high-trust evidence. However, it is not clear what f_θ is trained to represent, how it is trained, or how its learned satisfaction values influence the final verdict.

The verdict in Equations 7 and 8 appears to depend directly on provenance-derived trust weights through max aggregation and fixed thresholds, without an obvious role for the differentiable component. The authors should clarify the connection between the differentiable objective, the learned neural predicates, and the final verification decision, and explain what differentiability contributes beyond a symbolic verifier with provenance-weighted evidence.

2. The differentiable verifier does not appear to be part of the evaluated system

Relatedly, the conclusion states that a future version will implement the trust-weighted LTN objective in LTNtorch, replacing the current rule-based retrieval and verdict mechanism with a learned differentiable verification function.
This makes the status of the central technical contribution unclear and Table 1 is not really transparent on this. Ideally, the differentiable verifier should be implemented and evaluated in this paper rather than deferred to follow-up work.

3. The reported "end-to-end" experiment bypasses Stage A

Section 5.2 states that all three stages are executed in sequence, but the pipeline configuration subsequently states that Stage A is bypassed and gold-standard FOL representations are used in order to isolate Stage B and Stage C.

I therefore do not think the resulting experiment should be described as a full end-to-end evaluation of the proposed architecture. One of the central challenges motivating the paper is precisely the possibility that natural-language claims are grounded incorrectly. These errors cannot propagate into the reported system-level results because gold FOL is supplied directly.

The authors should either run the complete pipeline using predicted Stage A outputs or consistently describe the current experiment as an evaluation of Stages B and C conditioned on gold-standard logical forms.

4. No end-to-end accuracy result is currently reported

Section 4 identifies end-to-end verdict accuracy and E3 macro-F1 as important evaluation criteria. However, the current experiment only reports the distribution of outputs: 30 Verified, 1 Falsified, and 19 Indeterminate.
The authors explicitly acknowledge that the current dataset does not contain independently expert-validated ground-truth verdicts sufficient to compute E3.

A verdict distribution does not establish verification accuracy. For example, producing Indeterminate frequently may reflect desirable conservatism, but without an independent ground truth it is not possible to determine whether these abstentions are appropriate.
This substantially limits claims about factual verification performance, "behavioural correctness," or reduction in hallucination. At minimum, these claims should be narrowed. Preferably, the authors should provide independently validated verdict labels and report accuracy, macro-F1, and error analysis.

5. The proposed ablations and relevant baselines are not evaluated

Section 4.3 defines Neural-Only, Standard RAG, Unweighted Verifier, Verdict-Only, and Citations-Only baselines. However, these comparisons are not reported in Section 5 and are explicitly deferred to future work.
Without the Unweighted Verifier baseline in particular, the current experiments do not establish that provenance weighting improves verification outcomes relative to the same symbolic verifier with uniform evidence weights.
The related-work section also discusses strong existing approaches such as CoVe and KG-CRAFT. KG-CRAFT is described as achieving state-of-the-art results on two real-world fact-checking datasets, yet there is no empirical comparison to it or another competitive KG-based verification approach.

I do not necessarily expect all of these systems to be directly comparable on the authors' medical dataset, but the paper should contain at least one meaningful empirical baseline that isolates the contribution of the proposed trust mechanism.

6. The novelty claim should be narrowed and the related-work discussion expanded.

The statement that "no existing differentiable logic framework incorporates source credibility into the reasoning objective" appears too broad. In particular, ClaimEval (Samadi et al., AAAI 2016) jointly estimates source credibility and claim correctness using Probabilistic Soft Logic, representing credibility relations as first-order rules with continuous truth values and Łukasiewicz soft logic. This appears closely related to the proposed use of trust within a soft logical reasoning objective and should be discussed explicitly. The authors should position their contribution more precisely, perhaps around the particular combination of provenance signals, cryptographic signatures, and LTN-style reasoning rather than source credibility in soft reasoning more generally.

7. The trust scores require more methodological detail

The reputation values used in the experiment are manually assigned by the authors using a "public registry." The paper should explain how these values are derived and how the other trust signals would be obtained in practice.
It should also clarify whether the RSA signatures attributed to sources such as WHO and EMA are genuine source-issued signatures or simulated signatures created for the experiment. This distinction seems important for assessing the practical applicability of the method.

8. Stage A's consistency check appears to conflate incorrect grounding with factual contradiction

After translation, the paper checks whether Φ ∪ KB entails a contradiction. If so, it triggers reparsing or manual review. Algorithm 1 instead returns an Indeterminate verdict before Stage B.

This raises a conceptual concern. If a claim is correctly parsed but is contradicted by the knowledge base, this seems like precisely the type of evidence that should be handled by Stage B as negative evidence and potentially produce a Falsified verdict.
For example, if the claim is P(a) and the KB contains ¬P(a), the contradiction does not necessarily imply a parsing error. Did the authors consider this case, or did I misunderstand something there?

9. The claim-level aggregation rule requires additional justification

Equation 9 states that an overall claim is Falsified only if at least one constituent formula is Falsified and none is Indeterminate.
If one constituent is Falsified and all others are Verified, the resulting Falsified verdict is straightforward. However, if one constituent is clearly Falsified while another is Indeterminate, the overall claim becomes Indeterminate.

For a conjunctive claim, this differs from classical logic, where one false conjunct is sufficient to falsify the conjunction regardless of whether another conjunct is unknown. I understand that this may be an intentional safety-oriented or epistemic policy, but the rationale for allowing Indeterminate to dominate Falsified should be explained more clearly.

- Further comments -

The selection procedure for the 254 FOLIO examples should be reported, including whether they overlap with LogicLLaMA's fine-tuning data. The paper also states that tree-edit distance is reported as a soft grounding metric, but I could not find this result in Section 5.

Finally, there is some inconsistency between the abstract's description of the medical claims as "expert-annotated" and the later statement that they were author-annotated and not independently clinically validated.

- Overall assessment -

I see merit in the central idea of incorporating provenance and source quality into neuro-symbolic claim verification, and I believe the architecture could make a useful contribution. However, the current manuscript presents a stronger empirical and technical contribution than the reported experiments presently support.

In particular, the role of differentiability is not sufficiently clear, the differentiable trust-weighted verifier does not appear to be part of the evaluated proof of concept, the reported system-level experiment bypasses semantic grounding, ground-truth verdict accuracy is not yet available, the proposed ablations are not executed, and important trust metadata is manually constructed.

I therefore recommend major revisions. A revised paper should either implement and evaluate the complete proposed architecture, including the differentiable trust-weighted reasoning objective and meaningful baselines, or reposition the manuscript more clearly as an architectural framework and preliminary proof of concept, with corresponding claims of novelty, implementation maturity, and empirical validation narrowed accordingly.

Reviewer has chosen to be Anonymous

Overall Impression: Average

Content:
Technical Quality of the paper: Average
Originality of the paper: Yes, but limited
Adequacy of the bibliography: Yes

Presentation:
Adequacy of the abstract: Yes
Introduction: background and motivation: Good
Organization of the paper: Satisfactory
Level of English: Satisfactory
Overall presentation: Good

Detailed Comments:

The paper lays out a three-stage pipeline for checking what an LLM says: turn the claim into first-order logic, test it against a signed knowledge graph that carries provenance, then hand back a verdict with an explanation trace. The interesting move is putting digital signatures and source reputation directly into the differentiable satisfiability objective, so the proof search actually cares where a fact came from instead of treating every triple alike. The authors ship a working implementation, a signed 98-triple pharmacology KG, and two experiments.

I'll start with credit where it's due. This paper does not oversell itself, which is rarer than it should be. Table 1 grades every component by how far along it is, the evaluation protocol is labeled partially executed, and Section 5.2 comes right out and says the results show the thing runs end to end, not that it verifies accurately. That honesty made my job easier, and everything below should be read in that light.

There's real substance here too. The problem is worth solving, and the complaint that most pipelines treat all retrieved evidence as equally trustworthy is fair. Building provenance into the reasoning objective rather than stapling it on afterward is the right instinct. Two choices in particular caught my eye. Using max in Equation 7 is defended on the grounds that one authoritative signed source ought to be enough, and that max won't buckle under padding attacks. That's a security argument, not a shortcut. And in Equation 9, letting Indeterminate outrank Falsified is the right safety ordering for this setting. Releasing the code and the signed KG is a real contribution to a corner of the field where almost nobody does.

Here's my main problem: the experiments don't test the paper's central claim. The whole argument is that trust-weighted verification beats the alternatives, but not one of the five ablation baselines from Section 4.3 was ever run. The Unweighted Verifier is the one that counts, since it's the only comparison that isolates what the trust weights buy you. Without it, the core claim rests on the design argument alone. Same story with E1, E3, and E4: defined, never computed. What's left is a verdict distribution over 50 claims against 98 triples, which tells me the pipeline executes, not that it verifies well.

The headline number is also close to unfalsifiable as reported. Nineteen of fifty claims come back Indeterminate, and the paper reads that as an intended safety property. Maybe so, but without ground-truth verdicts, which the authors put in future work, "appropriately cautious" and "couldn't figure it out" look exactly the same in the data. Table 11 makes this sharper. Every conditional universal comes back Indeterminate, 7 out of 7. Every conditional negation, 5 out of 5. Meanwhile the 30 Verified cases sit almost entirely in atomic predicates (7 of 7) and conjunctions (9 of 9). So on the evidence here, the verdict function has been shown to work on the easy logical forms and nowhere else, with exactly one Falsified case in the entire batch. Annotating ground-truth verdicts for these same 50 claims and reporting E3, even at this small scale, would turn a distribution into a result. If the authors do only one thing from this review, it should be that.

The staged evaluation also makes the system look better than it is. Stage A gets measured on FOLIO (LE 0.853) and the medical set (LE 0.801), but then the end-to-end run bypasses Stage A entirely and feeds in gold-standard FOL. Given that Stage A scores 0.479 on drug interactions and 0.688 on treatments, a pipeline that actually strings the stages together will do noticeably worse than that verdict distribution suggests. Push the same 50 claims through Stage A's own output and you get a number for error propagation, which to my mind is the most interesting question this architecture raises.

One inconsistency needs fixing. The abstract says "50 expert-annotated medical claims." Section 5.2 says the set was curated by the authors and has not been independently validated by clinical experts. Section 5.2 is the accurate version and the abstract needs to match it. That matters more than usual when the claims are clinical.

On originality I land somewhere in the middle. The parts are all off the shelf: LogicLLaMA for grounding, LTN-style differentiable satisfiability, PROV-O and signed named graphs for provenance. What's new is the composition, plus dropping trust weights into the satisfiability loss. That's a sensible piece of integration, but it's integration, not a new mechanism. I'd also soften Table 3, where the authors pick the comparison dimensions and, unsurprisingly, only their own system checks every box. Those tables tend to convince the people who made them more than anyone else.

Two smaller technical notes. Propositions 1 and 2 fall straight out of the definitions, no evidence gives you Indeterminate, a zero signature gives you zero weight, and they'd sit better as stated design properties than as propositions with proofs. As written they promise a depth the statements don't deliver. Second, the trust score is a hand-tuned convex combination, uniform coefficients at alpha 0.2, tau 0.5, delta 0.3, with reputations assigned by hand. Since the entire architecture hinges on this one quantity, it needs a sensitivity analysis. How much do the verdicts move when you vary the coefficients and thresholds, and what happens when a reputation score is simply wrong? That's cheap to run with what's already built.

The bibliography is broad and the related work section is one of the stronger parts of the paper. The writing is clean and easy to follow. Two small things: the caption on Table 10 already interprets the result as an intended property, which tells the reader what to think before they've looked, and would read better as plain description. And the open-world versus closed-world gap between FOL and OWL, noted in Section 6.1, deserves more than a paragraph, since it goes to whether Stage A's output can be checked against the KG at all.

To sum up: a clearly written, honest architectural contribution to a problem that deserves attention, with released artifacts other people can build on, but not yet backed by enough evidence to support its central claim. I'm recommending major revisions. Four things would win me over: run the Unweighted Verifier ablation, annotate ground-truth verdicts and report E3, do a cascaded run without bypassing Stage A, and add a sensitivity analysis over the trust coefficients and thresholds. None of it needs new infrastructure, and together they'd turn a well-argued blueprint into a substantiated one.