PaperlayerView exact revision on arXiv

Source-linked AI summary

NeSySpec: Neuro-Symbolic Technical Intelligence for Auditing Engineering Specifications with an Application to Aircraft

Pier Mattia Basciano, Gianvito Antenori, Cristiano Andolfi, Giovanni Farina, Salvatore Monteleone

arXiv:2610.35403v1cs.AIcs.CVcs.SC

TL;DR

Auditors need to determine which physical constraints a declared specification violates and which fields may be wrong. NeSySpec uses fleet-trained neuro-symbolic axioms to audit specifications; its largest-violation key names the violated constraint in 0.942 of corrupted test records with generator labels.

  • Problem

    Auditors must determine which physical constraints a declared specification respects or violates and identify misreported records, whose errors can propagate into performance models.

    Source: §1 · p. 1

  • Method

    NeSySpec uses fleet-trained graded axioms in Logic Tensor Networks to assess constraints and derive altered fields, repair proposals, image evidence, and verification reports, abstaining on missing evidence.

    Source: §1 · p. 2, §5 · p. 25

  • Results

    The largest-violation key identifies the violated constraint in 0.942 of corrupted test records with generator labels, outperforming Fellegi–Holt, solver-based diagnosis, and rule-based diagnosis.

    Source: §5 · p. 26

  • Takeaways & Limitations

    The logical formulation helps interpret anomalies by exposing which relations fail and which fields are implicated.

    Source: §5 · p. 27

    Evaluation is on aircraft and constructed errors; generalization to unseen systems remains to be tested through independent replications.

    Source: §4.10 · p. 25, §5 · p. 27

Abstract

from arXiv · show

Engineers who audit a declared specification of an engineered system need to know which physical constraints it respects, which it violates, which field was altered and how to correct it. NeSySpec is an integrated and interpretable neuro-symbolic audit framework, built on Logic Tensor Networks, that answers these questions in one pipeline. Its axioms encode the physical relations of the domain as differentiable graded predicates whose tolerances are learned from a fleet of real records; from the same degrees, it diagnoses the violated constraint, identifies the altered field by abduction, proposes a minimum-change correction and ties image evidence to the parts it describes, abstaining exactly where evidence is missing, and returns all of it in one verification report. We validate NeSySpec on 107 aircraft types, with 16 test aircraft of 9 families held out of training, on specification records paired with ground photographs and satellite imagery and on synthetic errors: generated corruptions, edits labeled from the edit alone and deliberate falsifications. NeSySpec combines all the assessed audit outputs in one pipeline, which no learned, rule-based, solver-based, neuro-symbolic or language-model comparator does; on the test aircraft none is ahead of it in the macro-F1 of its constraint verdicts, in naming the violated constraint and the altered field or in the repair error, and it is competitive in record and image-pair detection. Its diagnosis names the violated constraint in 94.2% of corrupted test records, against 79.5% for classical Fellegi-Holt diagnosis, and on edits labeled from the edit alone, without retraining, abduction finds the altered field in 59.3% of records, against 30.6% for minimum-cardinality localization with random tie- breaking. Only the knowledge base, the visual predicates, the corruption generator and the data are specific to the domain.

1 Introduction

Specification audits must distinguish valid, inconsistent, incomplete, or misreported records, since erroneous values can propagate into performance models. NeSySpec combines constraint verdicts, diagnosis, repair, visual evidence, and reporting in one learned neuro-symbolic pipeline.

1 Introduction

  • NeSySpec learns graded physical-constraint tolerances from fleet records and derives verdicts, altered-field diagnoses, minimum-change repairs, and part-grounded image evidence in one report.Masked quantification excludes constraints whose required evidence is missing.Source: §1 · pp. 2–3
  • The evaluation covers 107 aircraft, including 16 test aircraft from 9 held-out families, with specification records, ground photographs, satellite imagery, and generated or independently labeled errors.The protocol also assesses deliberate falsifications and human part annotations.Source: §1 · pp. 2–4
  • The largest-violation key identified the violated constraint in 0.942 of generator-labeled test corruptions; abduction identified the altered field in 0.593 of independently labeled errors.Minimum-cardinality localization achieved 0.306 with random tie-breaking and 0.453 with oracle tie-breaking.Source: §1 · p. 3
  • No evaluated comparator returns all assessed audit outputs, and none leads NeSySpec on test-aircraft constraint-verdict macro-F1, violated-constraint naming, altered-field naming, or repair error.For record and image-pair detection, residual learners and late fusions are close and rank higher in some settings.Source: §1 · p. 3
  • The paper contributes a comparative study across rule-based, solver-based, learned, language, and vision-language methods, plus a deployment map linking audit questions to framework outputs.The study uses a shared physical knowledge base for its comparisons.Source: §1 · p. 4

2 Background and Related Works

The background connects differentiable first-order logic to specification auditing, while related work spans data editing, learned detection, neuro-symbolic reasoning, explanation supervision, and multimodal verification. The review identifies a gap in jointly providing and evaluating the outputs needed for a complete audit.

2.1 Background

  • LTNs interpret predicates as differentiable functions and aggregate formula truth so knowledge-base parameters can be learned from data.In NeSySpec, records, availability masks, and optional images are grounded as individuals and predicates.Source: §2.1 · p. 4
  • NeSySpec uses learned graded predicates, availability-guarded quantification, a shared truth scale for physical and visual predicates, and a grounding axiom whose localization pressure scales with visual-predicate truth.Its specification stratum preserves each axiom’s truth value, enabling constraint-level verdicts; crisp rule validation also supports exact abstention.Source: §2.1 · p. 5

2.2 Related Works

  • Prior editing and diagnosis methods use minimum-weight edits, integrity constraints, solver conflict sets, or crisp rules, whereas NeSySpec grades constraints against fleet-learned bands and uses abduction to localize altered fields.The review also contrasts learned record scorers and multimodal methods with NeSySpec’s per-constraint verdicts and audit outputs.Source: §2.2 · p. 5
  • NeSySpec represents part-level explanation supervision as an axiom on each visual head’s class-activation map, gated by assertion and part visibility.The review also notes that encoding its knowledge base in DeepProbLog, Scallop, or PSL would change its axiomatic and logical structure, leaving that comparison for future work.Source: §2.2 · p. 6
  • Table 2 compares seven audit outputs, and none of the reviewed works provides and evaluates all seven together.Statistical editing and validation come closest, but use crisp bounds and provide no image evidence.Source: Table 2 · p. 6, §2.2 · p. 7

3 Proposed Methodology

NeSySpec audits declared engineering records through graded physical and visual axioms, deriving constraint verdicts, diagnoses, repairs, and evidence reports. Its method combines fleet-based learning, guarded aggregation, and image grounding across aircraft data and synthetic error benchmarks.

3 Proposed Methodology

  • The seven-module framework derives constraint verdicts, altered fields, repair proposals, missing-evidence accounting, part-grounded visual evidence, and a verification report from logical axioms.Masked aggregation, graded predicates, and grounding connect the outputs while keeping separate evidence-source verdicts.Source: §3 · p. 7

3.1 Data and Verification Instances

  • Records cover 107 aircraft types, while the family-based specification split holds out business-jet families and six randomly selected families for evaluation.Records use 16 numeric fields; satellite records use nine, and the corruption benchmark includes generator-certified errors and edits labeled from the edit alone.Source: §3.1 · p. 8

3.2 Knowledge Base and Graded Predicates

  • Fleet-trained graded predicates score physical relations, with learned bands and slopes defining constraint tolerances.Bands start from a prior widened to [0.88 min, 1.12 max]; after training, 45.7% remain within the similarly widened fleet range.Source: §3.2 · pp. 10–11

3.3 Vision Module and Grounding Axiom

  • A grounding axiom encourages each visual head to concentrate evidence on the image part it describes, and the report displays its activation map.Photographic part regions use automatically generated pseudo-masks; satellite regions use the annotated diamond.Source: §3.3 · pp. 11–12

3.4 Cross-Modal Axioms

  • Cross-modal axioms compare declared attributes with image-predicted posteriors and are available only when the declared value is covered and relevant parts are visible.Their truths are computed from posteriors and logical implications without additional trainable parameters.Source: §3.4 · p. 12

3.5 Masked Stratified Aggregation

  • Masked stratified aggregation excludes unavailable axioms, so each verdict reduces exactly to available evidence and preserves a separate verdict for each evidence source.A masked axiom receives zero gradient; when no cross-modal axioms are available, that stratum drops out.Source: §3.5 · p. 13

3.6 Verdict and Diagnosis Keys

  • For a flagged record, the largest-violation key names the constraint with the greatest violation degree, while a learned second head provides a secondary ranking.The second head is a logistic regression on degrees of available axioms.Source: §3.6 · p. 13

3.7 Verification Report and Optional Checks

  • The verification report states which available constraints are held or violated and treats masked constraints as unevaluated; abduction searches single-field changes, and repair minimizes change over top-ranked fields.A constraint is violated when its truth is below 0.5; repair targets a stricter validation-selected threshold and retains its best-effort change if the threshold is not reached.Source: §3.7 · p. 14

4 Evaluation and Results

The evaluation uses synthetic edits and constructed record–image mismatches on 16 test aircraft from 9 held-out families to assess NeSySpec’s audit pipeline, including physical verdicts, diagnosis, field localization and repair. It examines the contribution of logic and learned axioms to detection, alongside the scope and limitations of the aircraft validation.

4.1 Experimental Setup

  • NeSySpec alone returns every audit output; on test aircraft no comparator leads its constraint-verdict macro-F1, diagnosis of violated constraints or altered fields, or repair error, while detection is competitive.Residual learners and late fusions are close in record and pair detection, and some rank higher in specified settings.Source: §4.1 · p. 16, Table 5 · p. 17

4.2 Constraint Verdicts and Diagnosis

  • 0.942 of corrupted test records are correctly diagnosed by NeSySpec’s largest-violation key, above Fellegi-Holt, Z3 and rule diagnosis at 0.795 to 0.857.Constraint-verdict macro-F1 is 0.795 on generator-label test and 0.575 on intervention-label test, above the DL2 network’s 0.661 and 0.426, respectively.Source: §4.2 · pp. 18–19, Figure 6 · p. 19

4.3 Field Localization and Repair

  • 0.593 of intervention-labeled test records have their altered field found by abduction without retraining, versus 0.306 for minimum-cardinality localization with random tie-breaking.On altered fields, repair reduces log-space error from 0.366 to 0.133; the solver reaches its stricter target on 0.555 of single-field test records and otherwise returns a best-effort value.Source: §4.3 · p. 20

4.4 Record Coherence

  • 0.979 ± 0.002 test AUROC distinguishes coherent from incoherent records, above raw-field learners at 0.748 to 0.792; residual learners are close in distribution.On the unseen business-jet class, detection AUROC is 0.934, while five residual learners rank higher; NeSySpec’s optional rank-then-explain setting lets the residual MLP raise the alarm and NeSySpec explain it.Source: §4.4 · p. 20

Records with images.

  • 0.994 ± 0.002 AUROC detects mismatches across satellite pair types, versus 0.748 for Qwen3-VL-8B; on photographs, NeSySpec is on par on test but trails on unseen families.With ResNet-50, the verifier outperforms end-to-end fusions on test and unseen satellite sites, though some fusions score higher on image swaps and unseen-site pairs.Source: Records with images · p. 21

4.5 Missing Evidence and Absent Images

  • With half the fields hidden on the unseen class, NeSySpec reaches 0.577 AUROC, above residual MLP at 0.536 and TabPFN v2 at 0.539, and on par with masked LightGBM at 0.566.Masked verdicts depend only on available evidence, and without an image the fused verdict matches the tabular verdict in all 9 satellite cells; with 30% of satellite images hidden, pair AUROC is 0.947, below CatBoost at 0.978.Source: §4.5 · pp. 21–22

4.6 Grounding of the Visual Axioms

  • 0.780 ± 0.017 of test pseudo-mask maps point to the annotated part, versus 0.360 ± 0.066 with permuted masks and 0.103 ± 0.017 without localization.The grounding axiom also points to annotated parts in 0.737 ± 0.015 of PASCAL-Part human masks; localization depends on anatomically correct masks.Source: §4.6 · p. 22

4.7 Robustness to Deliberate Falsification

  • 0.936 of cover-ups pass when up to five fields are edited, while 0.247 of NeSySpec-flagged bare lies cannot be covered; the residual MLP has rates of 1.000 and 0.000, respectively.With the optional critical-field alert, 0.729 of lies pass against an attacker who knows the alert and withholds up to two fields; false alarms on 32 test controls are 0.148, below Mahalanobis distance at 0.656.Source: §4.7 · pp. 22–23

4.8 What the Logic Adds: Other Encodings of the Same Knowledge

  • On test detection, NeSySpec’s record verdict scores 0.979 versus 0.965 for the DL2-loss network and 0.966 for the per-constraint monotone model.Training the knowledge base through Real Logic raises AUROC from 0.907 to 0.979 on test and from 0.845 to 0.934 on the unseen class.Source: §4.8 · p. 23
  • Against alternative encodings, the DL2 method on declared fields reaches 0.703 ± 0.030 and Qwen3-8B reaches 0.620, both below NeSySpec’s record verdict.The binary record-label-only ablation equals generator labels in 0.081 of test records, while the full model outperforms the flat-bank ablation on every split.Source: §4.8 · pp. 23–24
  • Figure 9 tracks axiom training: validation feasibility rises from 0.734 to 0.930 on clean-labeled records and falls from 0.335 to 0.151 on corrupted records.The verdict’s validation AUROC rises from 0.901 to 0.997; grounding-axiom satisfaction also rises during training for photographs and satellite crops.Source: §4.8 · p. 24, Figure 9 · p. 24
  • The learned knowledge base strengthens detection: intervention-label AUROC rises from 0.535 with one specification constraint to 0.723 with all twelve.Across three held-out splits, AUROC rises with diminishing returns as constraints are added; removing any one constraint lowers abduction for 7 constraints and slightly lowers it for 3 more.Source: §4.8 · p. 24, Figure 10 · p. 25

4.9 Deployment Map

  • Table 6 maps each audit regime to the NeSySpec output serving it and the strongest comparator for that regime.The deployment map follows the audit workflow.Source: §4.9 · p. 24

4.10 Limitations

  • Validation is limited to aircraft and generated or edited errors; naturally occurring errors, expert red teams, larger fleets, and replication on a new fleet remain future work.The 107-aircraft evaluation holds out every test family and satellite site; classes without training aircraft favor residual learners for record-level detection, while an optional rank-then-explain setting lets them raise alarms and NeSySpec explain them.Source: §4.10 · p. 25

5 Conclusion and Future Works

NeSySpec combines specification verdicts, diagnosis, localization, repair, image grounding and reporting in one audit, and no evaluated comparator returns all outputs together. The study is an aircraft-based first approach with constructed errors; future work proposes broader data, evidence and domains.

Conclusion

  • NeSySpec derives constraint verdicts, altered-field diagnosis, repair, exact abstention, part-grounded image evidence and a verification report from graded Logic Tensor Network axioms.The framework was validated on 107 aircraft with generated, intervention-labeled and falsified errors.Source: §5 · p. 25
  • 0.942 of generator-labeled corrupted test records had the violated constraint named; abduction found altered fields in 0.593 of independently labeled errors without retraining.Minimum-cardinality localization reached 0.306 with random tie-breaking and 0.453 with oracle tie-breaking.Source: §5 · p. 26
  • No comparator returns all audit outputs, and none leads NeSySpec on test constraint macro-F1, violated-constraint and altered-field naming, or altered-field repair error.Record-level detection is closer: residual learners are competitive and sometimes rank records higher.Source: §5 · p. 27
  • The study is a first approach to specification auditing, evaluated on aircraft and constructed errors.The authors identify broader physical knowledge, richer evidence and larger, more diverse datasets as possible routes to improving generalization to unseen systems.Source: §5 · p. 27

Future Works

  • Planned technical work includes comparing alternative neuro-symbolic encodings, refining aircraft relations and thresholds, and measuring hyperparameter sensitivity and inference cost.The authors also propose profiling batching, caching and adaptive search budgets against latency, diagnostic accuracy and repair quality.Source: §5 · pp. 27–28
  • Proposed applications include other engineered systems, uncertain observations and CAD models assessed with FEM or CFD simulations.Other systems would require adapted knowledge bases, visual predicates and corruption generators.Source: §5 · p. 27
  • Future work proposes testing naturally occurring errors, including cross-source discrepancies, variant mix-ups and uncorroborated fields, alongside expanded falsification protocols.The authors also propose block abduction for variant mix-ups.Source: §5 · p. 28
  • Planned evidence extensions include imputation channels, hand-annotated aircraft part masks, visual strata for new sensors and class-level axioms for critical-field omissions.These are proposed extensions, not evaluated capabilities in the described study.Source: §5 · p. 28

Data Licenses

The paper distinguishes the licensing and redistribution conditions for the two image datasets and the derived materials.

Data Licenses

  • FGVC-Aircraft is provided for non-commercial research, and its photographs are not redistributed except for four credited Figure 8 images.The four reproduced photographs are credited to their photographers at airliners.net.Source: Data Licenses · p. 28
  • RarePlanes is distributed under the Creative Commons Attribution-ShareAlike 4.0 International license.The two Figure 8 satellite crops are adapted from RarePlanes.Source: Data Licenses · p. 28
  • The adapted satellite crops, tables and crop indices derived from RarePlanes will be shared under the same license; human part masks are not redistributed.Source: Data Licenses · p. 28

A Porting to Other Engineered Systems

The porting checklist frames NeSySpec for systems whose declared fields are linked by physical, definitional or regulatory relations with statable tolerances. It identifies what must be specified, fitted or evaluated anew.

A Porting to Other Engineered Systems

  • Porting applies to engineered systems with declared fields linked by physical, definitional or regulatory relations with statable tolerances.The appendix distinguishes what a new system supplies, what is fitted again and what is reused.Source: A Porting to Other Engineered Systems · p. 32
  • List field units and one relation per constraint, and let constraints that read undeclared fields abstain.On aircraft records, filling undeclared fields at scoring lowered detection in several evaluated settings.Source: A Porting to Other Engineered Systems · p. 32
  • Fit initial bands on clean training records and fix an intervention tolerance before error generation.On aircraft, the generator oracle flagged no constraint on 613 of 1,810 intervention-labeled altered rows (33.9%).Source: A Porting to Other Engineered Systems · p. 32
  • Measure automatic part masks against public human masks and train visual heads on images from the sensor in use.Source: A Porting to Other Engineered Systems · p. 33
  • Include learners on the same physical residuals among comparators; on aircraft, a multilayer perceptron serves as the optional rank-then-explain alarm.Source: A Porting to Other Engineered Systems · p. 33
  • NeSySpec abstains on constraints that read undeclared fields; its optional critical-field alert brings withholding-field evasion back to the level of bare lies on aircraft.Source: A Porting to Other Engineered Systems · p. 33

B Implementation and Verification Report

The appendix describes a shared prediction-file format and gives an example verification report, aircraft relation constants and benchmark construction details. The example illustrates how constraint degrees inform the report's verdict and diagnosis.

B Implementation and Verification Report

  • A common prediction-file format lets one evaluation script score NeSySpec and every comparator.Files include an instance identifier, split and score, with per-constraint outputs where the method provides them.Source: B Implementation and Verification Report · p. 33

B.1 Example of a Verification Report

  • In the illustrated test corruption, the verdict flags the record and the largest-violation key names A4, which the generator oracle also flags.The report lists degrees for available constraints; A4 and A5 exceed ln 2 and are marked violated, while A8 and A9 are held. A5 is also violated on the clean record.Source: §B.1 · pp. 33–34

C Physical Relations and Constants

  • Specification axioms use closed-form conceptual aircraft-design relations; learned bands act as fleet-derived tolerances.Initial per-class ranges are widened to [0.88 min, 1.12 max] over 44 clean training aircraft, then learned with their slopes.Source: C Physical Relations and Constants · p. 34

D Data and Benchmark Details

  • The 107 aircraft records span seven classes and were compiled from aviation-authority type certificates and manufacturer documents.The records passed loose screening with the verifier's physics module; intervention labels set from the edit alone bypass that dependence.Source: D Data and Benchmark Details · p. 34

D.1 Benchmarks

The appendix specifies the aircraft benchmarks, their splits and corruption types, and details the associated physical and remote-sensing constants. It also describes cross-dataset scoring and examples used to illustrate visual grounding.

D.1 Benchmarks

  • The benchmarks pair aircraft specification records with photographs and satellite imagery, using held-out aircraft and family splits.The appendix reports 107 aircraft overall and describes the realized instances and partitions for the photographic and satellite datasets.Source: §D.1 · p. 34, Table D.2 · p. 37

E Method Details

  • The appendices catalog physical-relation and remote-sensing constants and describe the verification report, vision module and cross-modal axioms.The implementation details include learned bands and residual scaling based on clean training rows.Source: Table C.1 · p. 35, Table C.2 · p. 35, §D.1 · p. 35

D.1 Benchmarks

  • Cross-dataset runs use only axioms R2–R4 on a unified 23-field frame, while records are associated with their nearest clean training record.The nearest-record output also assigns business jets to a nearest training class, although business jets are absent from training.Source: §D.1 · p. 35
  • Corruption candidates are generated by operators, with discarded cases reflecting unavailable inputs or conditions unmet after six attempts.Each operator draws two candidates per clean record; 38 discarded Frankenstein swaps come from the unseen class.Source: §D.1 · p. 36, Table D.1 · p. 36
  • Figure 8 examples are selected by a fixed rule, and the grounding-axiom network has higher pointing than its no-localization-term counterpart in every seed pair.The displayed pseudo-masks can include background or off-part regions.Source: §D.1 · p. 36
  • Photographic pairs vary record matching, aircraft class or family, selected attributes, occlusion and image degradation; satellite pairs include tabular, image-swap and geometric corruptions.Satellite pairs also include clean annotation–crop matches.Source: §D.1 · p. 37

E.1 Proof of the Exact Reduction

The proof establishes that masked axioms do not affect a stratum’s verdict or gradients, and that missing images reduce the combined feasibility score to the tabular score. Numerical checks confirm these reductions.

E.1 Proof of the Exact Reduction

  • A masked axiom contributes neither a value nor a gradient, so a field read only by masked axioms does not affect the stratum verdict.The proof establishes this by selection before summation; if no tabular axioms are available, the stratum value is ln 2.Source: §E.1 · p. 37
  • The masked-verdict reduction matched the knowledge base restricted to available constraints bit for bit in 16 of 16 runs.The check used two tolerance priors and agreed with float64 recomputation within 2.2 × 10^-7 relative.Source: §E.1 · p. 38
  • Without an image, the combined feasibility reduces exactly to exp(−V_T), and the implementation returns that value bit for bit.The reduction also held in all 180 runs with newly drawn masks hiding a nominal 30% of satellite images.Source: §E.1 · p. 38

E.2 Method Components

This appendix zooms into the verification-report and vision modules and details a matched study of the grounding axiom’s gate. It also states which visual axioms are available for the two image types.

E.2 Method Components

  • Figure E.1 expands the module that assembles the verification report and its optional settings.Figure E.2 focuses on the vision module and grounding axiom.Source: §E.2 · p. 38, Figure E.1 · p. 39, Figure E.2 · p. 39
  • The matched grounding study varies the grounding-term gate while holding its loss weights at 0.3, 1 and 3.Variants use the predicted gate, a supervised-label gate, no gate, or a label gate with a changed normalizer; an auxiliary-loss reference is also trained.Source: §E.2 · pp. 38–39
  • On photographs, AX1 and AX2 carry instance-specific signals, while AX5 is available on 95.2% of satellite pairs.The gear heads read by AX3 have no attribute label, AX4 reads no declared field, and a pair without an available axiom scores 0.Source: §E.2 · p. 39
  • Algorithm E.1 transcribes the forward pass for one declared record.The appendix identifies it as the forward pass shown in Figure 1.Source: §E.2 · p. 39

F Protocol Details

The protocol describes comparator selection, configuration choices and evaluation scope, including a vision-threshold sensitivity analysis. Additional results report constraint-verdict performance and diagnosis, localization and repair outcomes across the specified splits and label settings.

F Protocol Details

  • The configuration was selected on validation data and held-out training classes, but earlier configurations were also evaluated on test splits during development.The visibility threshold used in the paper, 0.20, was selected informally on a 240-image subset that included test and out-of-distribution images.Source: F Protocol Details · pp. 39–40
  • On validation alone, a predeclared criterion selects visibility threshold 0.25 in 197 of 200 resampled subsets, while equal weighting of visibility and false propeller detections keeps 0.20.At 0.25 without retraining, 12.1% of part flags become not visible.Source: F Protocol Details · p. 40

G Additional Results and Figures

  • The evaluation covers 14 comparator groups and six benchmarks, with specification-record intervals generally based on 5,000 cluster-bootstrap resamples at each of two cluster levels.A planned language-model arm has no result because too few pilot answers could be parsed.Source: F Protocol Details · p. 39, G Additional Results and Figures · p. 41

G.1 Constraint Verdicts

  • NeSySpec’s constraint-verdict macro-F1 is 0.795 on generator-label test and 0.575 on intervention-label test, without retraining.Against the network trained with the DL2 loss on the same residuals, its macro-F1 is higher in all six split and label-family cells.Source: §G.1 · pp. 41–42

G.2 Diagnosis, Localization and Repair

  • NeSySpec names the violated constraint in 0.942 of corrupted test records, localizes single-field test corruptions at 0.742 ± 0.011, and lowers repair log-space error from 0.366 to 0.133.On the unseen class, the largest-violation key identifies the constraint in 0.897 ± 0.007 of records.Source: §G.2 · p. 43
  • Strict abstention withdraws 3 to 5 diagnoses per seed when no available degree exceeds ln 2, and none of those records is correctly diagnosed.With the same alarm, rank-then-explain remains above Fellegi–Holt and Z3 on test but below NeSySpec’s verdict using its own alarm and the same key.Source: §G.2 · p. 44

G.3 Missing Evidence

With hidden fields, NeSySpec bases its verdict on available evidence and reports which constraints remain checkable. Its abduction-based field localization is compared with minimum-cardinality and other localization methods.

G.3 Missing Evidence

  • With 10% of fields hidden in distribution, the masked verdict reads only declared evidence, while MLPs trained with masks read every field.On unseen families with hidden fields, MICE ranks higher; with no additional hidden fields, the masked verdict is ahead of MICE imputation on test and unseen families.Source: §G.3 · pp. 44–45
  • +0.375 is NeSySpec’s test difference from minimum-cardinality localization on exact top-1 field localization.The comparisons also include Ochiai ranking and largest class-I residual; the table reports results for test, unseen families, unseen class, and intervention labels.Source: §G.3 · p. 45
  • The masked verdict reports which constraints remain checkable rather than filling in the values of hidden fields.With MICE imputation enabled, an optional setting, the verdict is on par with the MLP trained with masks given the same imputer on test records with 10% hidden fields.Source: §G.3 · pp. 44–45

G.4 Record Coherence

NeSySpec scores record coherence from constraint violations and is evaluated against generator labels and labels derived independently from edits. Its detection performance depends on what counts as an error: edits that violate no constraint remain difficult to detect.

G.4 Record Coherence

  • 0.979 ± 0.002 is NeSySpec’s test AUROC on generator labels, with scores ranging from 0.937 on cruise corruptions to 1.000 on geometric corruptions.Each flag also names the violated constraint, altered field, and a repair proposal.Source: §G.4 · p. 45, Table G.3 · p. 46
  • Intervention labels are set from the edit alone and independently of the generator’s per-constraint training targets.They mark available constraints whose scope contains a field moved beyond tolerance; edits within tolerance can still break a constraint.Source: §G.4 · p. 47
  • Against intervention labels, NeSySpec’s record verdict reaches 0.701 on test, 0.750 on unseen families, and 0.719 on the unseen class without retraining.The generator oracle reaches 0.676, 0.709, and 0.714 on those same splits, respectively.Source: §G.4 · p. 47
  • On altered rows that break no constraint, NeSySpec’s detection stays below chance: 0.394, 0.449, and 0.439 across test, unseen families, and the unseen class.The passage reports that comparators using physics also perform below chance on these rows across pooled held-out splits.Source: §G.4 · p. 47

G.5 Records with Images

Across records with images, visual grounding, deliberate falsification, and knowledge-base ablations, NeSySpec evaluates how its axioms behave across evidence sources and settings. Its results include exact reduction under missing images, improved pointing from a grounding axiom, and different evasion rates under black-box cover-ups.

G.5 Records with Images

  • Without an image, NeSySpec’s fused verdict equals its record verdict bit for bit in 9 of 9 satellite cells, against 0 of 207 learned method and cell rows.With 30% of satellite images hidden, the fused verdict is 0.947 and keeps the exact reduction; a read-out trained with modality dropout ranks pairs at 0.973 without keeping it.Source: §G.5 · p. 47, Table G.6 · p. 48, Table G.7 · p. 49
  • The knowledge base fitted on specification records reaches 0.767 ± 0.007 on satellite test annotations and 0.764 ± 0.008 on unseen sites without satellite training.The satellite-trained remote-sensing record verdict reaches 0.796 and 0.812 on those sets, respectively.Source: §G.5 · pp. 48–49

G.6 Grounding

  • On FGVC pseudo-masks, the grounding axiom raises test pointing over a network without a localization term on every backbone.The gains range from +0.615 to +0.699, and the axiom points to the part in 0.790 of test pseudo-masks.Source: §G.6 · pp. 50–51, Figure G.1 · p. 51
  • On satellite crops, the grounding axiom keeps attribute and head AUROC on par with the network without a localization term.The comparison uses ConvNeXt-T and seed intervals over 8 paired seeds.Source: §G.6 · p. 51

G.7 Deliberate Falsification

  • Under black-box falsification, 0.936 of cover-ups of lies flagged by NeSySpec’s verdict pass, compared with 1.000 for the residual MLP.For flagged bare lies, 0.247 cannot be covered, compared with 0.000 for the residual MLP; the smallest cover takes 2.69 further edited fields on average.Source: §G.7 · p. 51
  • Withheld fields mask the axioms that read them, while the optional critical-field alert names the undeclared field and constraints left unchecked.On unseen families, NeSySpec with the alert is evaded less than the residual MLP with the same alert; on the unseen class, it is evaded more.Source: §G.7 · p. 51

G.8 Ablation and Other Forms of the Same Knowledge

  • Training the knowledge base through Real Logic is ahead of its initial values on every split, by +0.073, +0.061, and +0.088.The full model is also ahead of the saturating-envelope and flat-bank ablations on every split.Source: Table G.8 · p. 50, §G.8 · p. 52
  • Across constraint-subset ablations, intervention-label AUROC rises from 0.535 with one constraint to 0.723 with all twelve.The reported gain follows the share of edits that alter a field read by an active constraint, which grows from 0.22 to all edits.Source: §G.8 · p. 52

G.9 Selected Components and Sensitivity Analyses

The selected diagnosis and abduction rules are compared with alternatives, followed by sensitivity analyses that vary learned bands and the oracle used to generate labels. Performance changes when the oracle is fitted without test or out-of-distribution aircraft, making that benchmark boundary consequential.

G.9 Selected Components and Sensitivity Analyses

  • On held-out training classes, the selected largest-violation diagnosis key ranks a violated constraint first in 0.802 of corrupted records, versus 0.630 for the second head.The abduction rule and its feasibility threshold were selected on validation; with threshold 0.8, abduction reaches 0.750 on single-field test corruptions.Source: §G.9 · pp. 52–53
  • Band alternatives that place more learned bands inside the training-fleet range lower validation detection by more than 0.005 on generator labels.The validation-selected penalty alternative reaches test detection AUROC 0.977, on par with 0.979 for NeSySpec, while localization top-1 is 0.728 against 0.742.Source: §G.9 · pp. 53–54
  • With oracle bands fitted on 44 clean training aircraft, 38 of 63 clean held-out aircraft are flagged, including 15 of 16 test aircraft.The benchmark consequently has four test controls instead of 32, and the crisp edits lead NeSySpec on generator labels in key and macro-F1 on every split.Source: §G.9 · p. 54, Table G.10 · p. 56, Table G.11 · p. 57
  • Under the 44-aircraft oracle, NeSySpec’s test intervention-label macro-F1 is 0.488 against 0.575, while detection is on par at 0.695 against 0.701.It remains ahead of Fellegi-Holt and Z3 in diagnosis and minimum-cardinality localization with random tie-break on every split.Source: §G.9 · pp. 54, 56
  • Under the 44-aircraft oracle, the learned bands have median width ratio 0.903 relative to those learned under the paper’s oracle, and 64% narrow.The repair reaches its target on 0.036 of single-field test records, compared with 0.555 under the paper’s oracle.Source: §G.9 · pp. 54–55
  • With tolerances selected by leaving one family out, 14 of 46 clean test and out-of-distribution aircraft are flagged, including 11 of 16 test aircraft.On intervention labels, NeSySpec’s test false-violation rate is on par with the paper’s level, while macro-F1 and abduction are lower.Source: §G.9 · pp. 55–56

G.10 Training Checkpoints

At the frozen best-validation checkpoint, every specification constraint had lower mean truth on corrupted than clean-labeled records where evidence was available; three of eight train-prior seeds reached the 100-epoch cap.

G.10 Training Checkpoints

  • 46 of 46 split-and-constraint pairs with available evidence had lower mean constraint truth on corrupted than clean-labeled records.The smallest difference was 1.0 × 10−5 on the unseen class.Source: §G.10 · p. 57
  • At the frozen checkpoint restored from the best validation epoch, the truth comparison favored clean-labeled records across all available pairs.Figure 9 shows the training curves of the axioms.Source: §G.10 · p. 57
  • With the train prior across eight seeds, early stopping selected the 100-epoch cap in three seeds.The best epoch was selected by validation AUROC (Table F.2).Source: §G.10 · p. 57

H Explanation-Supervision Comparison

Under the stated comparison protocol, the grounding axiom localized annotated parts more than the tested explanation-supervision baselines across the evaluated mask datasets. It also retained an out-of-distribution accuracy lead over the auxiliary loss, while test accuracy was degenerate.

H Explanation-Supervision Comparison

  • All 27 differences across nine mask configurations and three baselines favored the grounding axiom, with intervals above zero on an independent bootstrap seed as well.Its pointing exceeded RRR by +0.725 on FGVC test pseudo-masks, +0.594 on PASCAL-Part, +0.523 on PartImageNet, and +0.483 on UDA-Part.Source: H Explanation-Supervision Comparison · p. 58
  • Across weights 0.3, 1, and 3, the axiom kept at most one collapsed head, versus up to 5.7 on average for the auxiliary loss.At weight 1, its out-of-distribution accuracy lead over the auxiliary loss at validation weight 0.3 was +0.016 [+0.012, +0.020]; test accuracy was degenerate, with a constant predictor scoring 0.926.Source: H Explanation-Supervision Comparison · p. 58
  • The comparison retrained RRR, GradMask, and Pukdee et al. using per-example penalties, fixed normalization constants, and validation-selected λ values.RES-L was not retrained because its adapted objective did not reward localization on these masks.Source: H Explanation-Supervision Comparison · p. 58
  • With calibration measured at Pukdee et al.’s first projection step, it pointed to the part in 0.179 of PASCAL-Part masks; the axiom’s lead was +0.558 [+0.524, +0.591].The axiom’s differences also had intervals above zero on FGVC pseudo-masks and every other human-mask set.Source: H Explanation-Supervision Comparison · p. 58

Related papers

Loading 2610.35403v1…