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

cs.AIOct 26, 2026

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

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

Organizations: Department of Engineering, Niccolò Cusano University, Rome, Italy · SOMA Research Division, Rome, Italy

Abstract

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.

Figures & tables

Acronym	Meaning	Acronym	Meaning
AUROC	area under the receiver operating characteristic curve	MLP	multilayer perceptron
BCE	binary cross-entropy	MLP-SHAP	grouped SHAP attributions of the residual MLP
CAD	computer-aided design	MTOW	maximum take-off mass
CAM	class activation map	NeSy	neuro-symbolic artificial intelligence
CFD	computational fluid dynamics	OEW	operating empty mass
FAA	Federal Aviation Administration	PGD	projected gradient descent

Table 1: Acronyms.

Panel of Figure 1 — Figure 1: Overview of the NeSySpec pipeline.

Work	Violated constraint	Altered field	Repair proposal	Exact abstention	Learned tolerances	Part grounding	Record report
LTN and its applications [ 19 , 39 , 40 , 41 , 18 ]	( 3 )	( 3 )	7	( 3 )	( 3 )	( 3 )	7
DeepProbLog, Scallop, NeurASP, abductive learning b [ 42 , 43 , 44 , 45 ]	( 3 )	( 3 )	( 3 )	( 3 )	( 3 )	7	7
DL2 a , semantic loss, constraint layers a [ 20 , 46 , 47 ]	( 3 )	7	( 3 )	7	7	7	7
KENN, LEN, PSL b [ 48 , 49 , 50 ]	( 3 )	( 3 )	( 3 )	( 3 )	( 3 )	7	( 3 )
Statistical data editing and validation a [ 13 , 23 ]	3	3	3	3	( 3 )	7	3
SMT diagnosis a , language model with SMT [ 14 , 28 , 51 ]	3	3	3	( 3 )	7	7	( 3 )

Table 2: Comparison with the state of the art.

Panel of Figure 2 — Figure 2: Data and verification instances.

ID	Graded predicate and quantity	Fields read	Available ( $\alpha_{k}=1$ ) when	Learned parameters
Specification axioms $\mathcal{A}$ (records; 336 trainable scalars, 126 of them latents; $w_{k}=1$ )
A1	graded identity of $(\mathit{AR}-\hat{A})/\hat{A}$ , $\hat{A}=b^{2}/S$	$b$ , $S$ , $\mathit{AR}$	all declared	tolerance (8); $\kappa$ , $\beta$ (2)
A2	graded band of $C_{L}=2\mathit{MTOW}g/\big(\rho(h_{\mathrm{cr}})V_{\mathrm{cr}}^{2}S\big)$	$\mathit{MTOW}$ , $V_{\mathrm{cr}}$ , $h_{\mathrm{cr}}$ , $S$	all declared	band (16); $\kappa$ , $\beta$ (2)
A3	graded band of $\mathit{MTOW}/S$	$\mathit{MTOW}$ , $S$	all declared	band (16); $\kappa$ , $\beta$ (2)
A4	graded band of $F_{\mathrm{tot}}/(\mathit{MTOW}g)$	$F_{\mathrm{tot}}$ , $\mathit{MTOW}$	all declared; turbofan	band (16); $\kappa$ , $\beta$ (2)
A4P	graded band of $\mathit{MTOW}/P_{\mathrm{tot}}$	$P_{\mathrm{tot}}$ , $\mathit{MTOW}$	all declared; propeller	band (16); $\kappa$ , $\beta$ (2)

Table 3: Axiom catalog.

Panel of Figure 3 — Figure 3: Knowledge base and graded predicates.

Benchmark	Labels	Independent of the oracle	Sections	Size
Specification records	generator labels: corruptions kept when the oracle flags them, with per-constraint labels; noisy-but-coherent controls; fields hidden at random	no	4.2 to 4.5 , 4.8	107 aircraft of 71 families; test: 16 aircraft of 9 families, 204 rows with 32 controls
Intervention-labeled records	from the edit alone, with a tolerance fixed before generation	yes	4.2 to 4.4 , 4.8	2,582 rows, 1,810 altered; same aircraft and splits
Falsification	the attacker’s edits of genuine records	yes	4.7	736 attack problems on the 46 genuine held-out records
Satellite pairs (RarePlanes)	generator labels; image swaps	no	4.4 , 4.5	5,250 pairs; 10 test and 8 unseen sites
Photographic pairs (FGVC-Aircraft)	constructed mismatches, attribute labels, automatic pseudo-masks	yes	4.4 , 4.6	4,543 pairs; 800 test photographs
Human part masks	PASCAL-Part [ 84 ] , PartImageNet [ 85 ] and UDA-Part [ 86 ] annotations, for evaluation only	yes	4.6	535 aircraft in 506 PASCAL-Part images; 40 UDA-Part items

Table 4: Benchmarks and labels.

Figure 4: Constraint-level verdicts on test records.

Method	Verdicts macro-F1	Violated constraint	Altered field	Repair error	Exact, no image	Part pointing, PASCAL-Part	Records AUROC	Half fields hidden, unseen class	Satellite pairs
Learners on the physical residuals
Residual MLP	·	·	·	·	·	·	0.990	0.536	·
TabPFN v2 with native missing values	·	·	·	·	·	·	0.957	0.539	·
LightGBM trained with masks	·	·	·	·	·	·	-	0.566	·
MLP-SHAP	0.693/0.479 a	0.942	·	·	·	·	0.990	-	·
LightGBM-SHAP	0.595/0.418 a	0.871	·	·	·	·	0.957	-	·

Table 5: The audit at a glance: NeSySpec and its comparators on each output.

Panel of Figure 5 — Figure 5: Verification report of one declared record.

Figure 6: Constraint verdicts, diagnosis and field localization.

Figure 7: Verdicts under missing evidence.

Figure 9: Training dynamics of the axioms.

Figure 10: Detection and the knowledge encoded.

Regime	What NeSySpec provides	Strongest comparator
Workflow: run NeSySpec first and read its report; on a class without training aircraft, enable its optional rank-then-explain setting, in which a residual learner raises the alarm and NeSySpec explains it; cross-check a repair value against a statistical imputer such as MICE; against omission, enable the optional critical-field alert.
Constraint verdicts and diagnosis (Section 4.2 )
classical diagnosis and other encodings	the largest-violation key, from the verdict’s own degrees, above Fellegi-Holt, Z3 and the rules (also on intervention labels), the DL2-loss network’s key, the DL2 method on the declared fields and a language model; 0.812 where the crisp edits flag nothing	the crisp edits, on par where they flag the record (generator labels)
held or violated, test and unseen families	the constraint verdicts, macro-F1 0.795 on generator-label test, above the DL2-loss network, with the key, the field and a repair	crisp edits, on par in macro-F1; the DL2-loss network, with fewer false violations (0.020 against 0.074)
residual rankings	the key, above both on 81 single-violation records and above the residual on the unseen class, with a held or violated verdict, a repair and exact abstention	the class-standardized residual and MLP-SHAP, on par in distribution; MLP-SHAP on the unseen class
Field localization and repair (Section 4.3 )

Table 6: Deployment map.

Appendix figures & tables22 assets

Supplementary material from the paper’s appendix.

Appendix

Component	Content	Aircraft study
Supplied by the new system
Knowledge base	one exact, differentiable quantity per relation, each with a graded predicate, an availability condition and a scope; bounded latents for rarely declared quantities; initial bands fitted on clean training records; regulatory bands frozen	12 constraints on records and 10 on satellite annotations (Table ); 336 trainable parameters on records, 126 of them latents, and 57 on satellite annotations; no neural network
Visual predicates	one sigmoid head per class, with the parts where its evidence must lie; cross-modal axioms with the same form	25 heads per dataset (Table E.1 )
Generator and data	corruptions that break one relation or swap a block of fields; noisy-but-coherent controls; an oracle with per-constraint labels; an intervention tolerance fixed before generation; sourced records with units, split by family or site	five corruption families, controls and intervention labels; 107 records of 71 families (Appendix D )
Fitted again
Bands and visual modules	tolerances learned from the training fleet; visual heads specific to their sensor	45.7% of the learned bands with both edges inside the widened training fleet range (Appendix G.9 ); with a visual stratum trained on photographs, the fused verdict reaches an AUROC of 0.724 on satellite pairs, against 0.796 for the record verdict alone (Appendix G.5 )

Appendix

Table A.1: Porting to a new engineered system.

Standard atmosphere		Relations and graded degrees
$g$	9.80665 m s -2	units	SI, except $R$ (km), $F_{\mathrm{tot}}$ (kN) and $P_{\mathrm{tot}}$ (kW)
$R_{\mathrm{air}}$ ; $\gamma_{\mathrm{air}}$	287.05287 J kg -1 K -1 ; 1.4	A5	$W_{1}=\max\{\mathit{MTOW}-0.94\,m_{\mathrm{fuel}},\,0.05\,\mathit{MTOW}\}$ , a 6% fuel reserve; log residual clipped to $[-3,3]$ ; available only when $\mathit{AR}$ is also declared and, for propeller aircraft, $V_{\mathrm{cr}}$
$T_{0}$ ; $\rho_{0}$	288.15 K; 1.225 kg m -3	A6	log residual clipped to $[-2,2]$ ; wide $C_{L,\max}$ bounds, because published stall speeds mix clean and landing configurations
$\Gamma$	$6.5\times 10^{-3}$ K m -1 (troposphere)	A7	95 kg per passenger with baggage; $f_{u}\in[0.3,1]$
$h_{\mathrm{tr}}$ ; $T_{\mathrm{tr}}$	11,000 m; 216.65 K, isothermal above; density continuous	unused	an estimate of maximum $L/D$ from $\mathit{AR}$ (Oswald factor 0.80, zero-lift drag coefficient 0.020) is implemented but read by no axiom; A5 takes $L/D$ from its latent
$\bar{h}$	$h_{\mathrm{cr}}$ clamped to $[0,\,20{,}000]$ m	coordinates	$z=(\log_{10}q-m_{g})/\sigma_{g}$ for a band, $z=\xi/\sigma_{g}$ for the residual $\xi$ of A1, A5, A6 and A7; $m_{g}$ , $\sigma_{g}\geq 10^{-3}$ from the clean training rows of group $g$ ( $\sigma_{g}$ a root-mean-square around 0 for $\xi$ ), shrunk toward the fleet with weight $n_{g}/(n_{g}+5)$ , the scatter through its square; a group without rows takes the fleet values

Appendix

Table C.1: Constants of the physical relations.

Design group	Wingspan (m)
I	below 14.9352
II	14.9352-24.0792
III	24.0792-35.9664
IV	35.9664-52.1208
V	52.1208-65.2272
VI	65.2272-79.8576

Appendix

Table C.2: Constants of the remote-sensing axioms.

					Realized magnitude $\epsilon$
Operator	Fields altered	Kept if the oracle flags	Kept	Disc.	5%	10%	20%	40%	80%	160%	320%
Single value	one of $S$ , $F_{\mathrm{tot}}$ or $P_{\mathrm{tot}}$ , $\mathit{OEW}$ , $V_{\mathrm{cr}}$	the targeted envelope (A3, A4 or A4P, A8, A10)	212	2	0	0	53	105	46	8	0
Geometric	one of $b$ , $S$ , $\mathit{AR}$	A1	208	6	104	104	0	0	0	0	0
Performance	$R$ or $m_{\mathrm{fuel}}$	A5	189	25	1	2	13	35	55	66	17
Cruise	one of $V_{\mathrm{cr}}$ , $h_{\mathrm{cr}}$ , $S$	A2	206	8	0	8	59	85	46	7	1
Frankenstein	one block of a record of another class	any constraint	176	38	-

Appendix

Table D.1: Corruption types and magnitudes.

Specification records
Type	Label	Train	Val.	Test	Unseen fam.	Unseen class	Total
Clean	coherent	44	17	16	11	19	107
Single value	incoherent	86	34	32	22	38	212
Geometric	incoherent	88	32	32	22	34	208
Performance	incoherent	81	29	28	22	29	189
Cruise	incoherent	86	32	32	22	34	206

Appendix

Table D.2: Benchmarks.

Predicate	Classes (one sigmoid head each)	Part region	Read by
Photographs (8 predicates, 25 heads; regions from the pseudo-masks)
EngineCount	1, 2, 3, 4	engine	AX1
EnginePlacement	underwing, rear, overwing	engine	AX4
Propulsion	jet, turboprop, piston	propeller and engine	AX2
WingPosition	high, mid, low	wing	AX5 (not implemented)
TailConfig	conventional, T-tail, cruciform, V-tail	tail	AX4

Appendix

Table E.1: Axiom catalog: visual predicates and cross-modal axioms.

Panel of Figure 23 — Figure E.1: Verification report and optional settings.

Panel of Figure 24 — Figure E.2: Vision module and grounding axiom.

Knowledge	Comparators	Input	Output	Data
None	Isolation Forest, Mahalanobis, MLP on normalized fields	declared fields	error score	records
	LightGBM, XGBoost, CatBoost, TabPFN v2 on raw fields	declared fields, availability mask, one-hot categories	error score	records
Crisp rules	train-fitted rule checker; rules with hierarchical pooling	band exceedances of the residuals	score, violated rules	records
Classical diagnosis	Fellegi-Holt, first unsatisfiable core of Z3, MaxSMT	crisp constraints	violated set, minimum-cardinality localization	records
Sizing statistics	Class I sizing regressions on maximum take-off mass, fitted on the training aircraft	declared fields	largest class-I residual, its field	records
Residual learners	MLP, LightGBM, XGBoost, CatBoost, logistic regression, TabPFN v2, TabICL with its v2 checkpoint, local outlier factor, one-class SVM, autoencoder; class-standardized residual and its Ochiai ranking; SHAP attributions	physical residuals with availability	score, attribution	records

Appendix

Table F.1: Comparators.

Setting	Value
Specification stratum	graded degrees in standard units of the clean training rows of each group, shrunk toward the fleet with weight $n_{g}/(n_{g}+5)$ ; in-band grading; hierarchical banks; truth $\exp(-v_{k})$ , degrees capped at $10^{4}$ ; masked mean verdict ( $p=1$ ), $V=\ln 2$ without available axioms; 336 trainable parameters, 126 of them bounded latents; chosen on validation among eight candidates with eight seeds each
Remote-sensing stratum	six graded slots (R1, R2 for civil and military roles, R3, R4, R10) in standard units of the clean training rows; R5 to R9 as the negative logarithm of their truth; masked weighted mean verdict ( $p=1$ ); in-band grading; flat banks; 57 trained parameters; chosen on validation among eight candidates
Training of the strata	AdamW [ 72 ] , learning rate $5\times 10^{-3}$ multiplied by 5, that is $2.5\times 10^{-2}$ , for every trained parameter of a stratum (bands, tolerances, slopes, in-band weights, latents and the parameters of R5 and R6), weight decay 0, batch 256; at most 100 epochs, early stopping on validation AUROC with patience 15, best state restored; $\lambda_{\mathrm{aux}}=0.5$ ; seeds 0-7
Fusion of the strata	weighted mean between strata with $\lambda_{\mathcal{R}}=\lambda_{\mathcal{AX}}=1$ ; masked $p$ -mean error with $p=4$ inside the cross-modal stratum; Reichenbach implication (R7-R9, grounding axiom, photographic AX4, satellite AX5); axiom weight 1, except R9 and satellite AX5 (0.5)
Second head	monotone logistic regression on the degrees, the availabilities and the verdict (on satellite pairs $V_{\mathcal{R}}$ , the cross-modal truths and $1-\mathrm{feas}_{\mathcal{AX}}$ ), inverse regularization in $\{10^{-4},\dots,10^{3}\}$ and, on specification records, the inclusion of the verdict selected on validation AUROC; operating thresholds: maximum of Youden’s $J$ [ 78 ] on validation
Abduction and repair	single-field log changes on a grid from $-3$ to 3 in steps of 0.005; smallest-change rule; feasibility threshold 0.9 ( $V\leq-\ln 0.9\approx 0.1054$ ) for both; repair on the $k_{r}=1$ top-ranked field by an augmented-Lagrangian method with Adam steps

Appendix

Table F.2: Configuration.

Comparator	Difference and intervals
Constraint diagnosis (top-1); NeSySpec returns the violated constraint from its own degrees, by the largest-violation key
Test
NeSySpec’s second head	+0.002	[−0.010, +0.018]·[−0.013, +0.011]
Fellegi-Holt	+0.147	[+0.068, +0.234]·[+0.079, +0.298]
Z3	+0.117	[+0.040, +0.209]·[+0.045, +0.256]
Rule diagnosis	+0.085	[+0.027, +0.146]·[+0.023, +0.150]

Appendix

Table G.1: Contrasts behind the body results: constraint diagnosis.

Comparator	Difference and intervals
Field localization (exact top-1); NeSySpec returns the altered field by abduction, the single-field change that restores consistency
Test
Minimum cardinality	+0.375	[+0.286, +0.470]·[+0.293, +0.529]
Ochiai ranking	+0.339	[+0.234, +0.450]·[+0.246, +0.413]
Largest class-I residual	+0.145	[+0.065, +0.232]·[+0.071, +0.203]
Same comparator, NeSySpec with the largest-feasibility rule a	+0.095	[−0.006, +0.192]·[−0.020, +0.176]

Appendix

Table G.2: Contrasts behind the body results: field localization, repair and missing evidence.

Comparator	Difference and intervals
Record coherence (AUROC); NeSySpec returns its verdict, each flag with the violated constraint, field and repair
Test, learners on the raw fields
CatBoost	+0.187	[+0.114, +0.259]·[+0.094, +0.335]
TabPFN v2	+0.197	[+0.118, +0.266]·[+0.105, +0.320]
XGBoost	+0.205	[+0.119, +0.280]·[+0.109, +0.334]
LightGBM	+0.231	[+0.136, +0.315]·[+0.119, +0.395]

Appendix

Table G.3: Contrasts behind the body results: record coherence.

Comparator	Difference and intervals
Black-box attacks (evasion); NeSySpec returns its verdict, each flag with the field found by abduction and a repair proposal
Cover-ups, up to five further edits
Residual MLP	−0.064	[−0.073, −0.055]·[−0.075, −0.053]
Residual TabPFN v2	−0.059	[−0.071, −0.046]·[−0.072, −0.043]
Residual one-class SVM	−0.062	[−0.077, −0.048]·[−0.081, −0.043]
Raw-field LightGBM	−0.065	[−0.075, −0.055]·[−0.076, −0.055]

Appendix

Table G.4: Contrasts behind the body results: deliberate falsification.

Differentiable logic: a probability per constraint
Reading	Generator-oracle labels	Intervention labels
Network with the DL2 loss on the same residuals	0.474/0.661/0.020	0.222/0.426/0.019
same network, thresholds tuned on validation	0.436/0.746/0.056	0.218/0.541/0.056
DL2 method on the declared fields	0.106/0.425/0.140	0.048/0.259/0.141
same method, thresholds tuned on validation	0.053/0.484/0.216	0.015/0.319/0.214
Crisp rules and edits: a crisp violated set

Appendix

Table G.5: Constraint verdicts against per-constraint labels on test.

Constraint diagnosis, top-1 on corrupted records	Test	Unseen families	Unseen class
MLP-SHAP on residuals	0.942	0.895	0.970
Class-standardized residual	0.929	0.955	0.667
LightGBM-SHAP on residuals	0.871	0.856	0.930
Rule diagnosis, rules ranked by exceedance	0.857	0.863	0.815
Z3, first unsatisfiable core	0.825	0.799	0.778
Fellegi-Holt, complete violated set	0.795	0.799	0.670

Appendix

Table G.6: Diagnosis, localization and repair.

	AUROC
Detector	Test	Unseen families	Unseen class	FPR, controls
Learners on the physical residuals: score; the network with the DL2 loss also a probability per constraint
MLP	$0.990\pm 0.003$	$0.999\pm 0.001$	$0.978\pm 0.011$	0.008
TabPFN v2	$0.958\pm 0.006$	$0.999\pm 0.001$	$0.983\pm 0.006$	-
TabPFN v2, native missing values	$0.957\pm 0.009$	$0.999\pm 0.001$	$0.984\pm 0.006$	-
TabPFN v2, raw fields and residuals a	$0.965\pm 0.007$	$1.000\pm 0.000$	$0.978\pm 0.006$	-

Appendix

Table G.7: Detection.

	Test	Unseen families	Unseen class
Ablation or model	AUROC Difference	AUROC Difference	AUROC Difference
Ablations of NeSySpec on specification records, generator-oracle labels, train prior; intervals [aircraft]·[family]
Saturating envelopes (bounded envelope truths)	0.821 +0.158 [+0.073, +0.223] · [+0.022, +0.196]	0.883 +0.108 [+0.031, +0.163] · [+0.014, +0.123]	0.898 +0.035 [+0.0031, +0.062] · [+0.005, +0.067]
Generalized mean, p = 4, instead of the mean degree	0.983 −0.004 [−0.020, +0.013] · [−0.008, +0.004]	0.980 +0.011 [−0.004, +0.041] · [−0.004, +0.065]	0.940 −0.006 [−0.016, +0.006] · [−0.015, +0.006]
Without in-band grading	0.970 +0.009 [+0.002, +0.017] · [+0.0003, +0.015]	0.977 +0.014 [+0.0012, +0.039] · [+0.0010, +0.052]	0.908 +0.025 [+0.014, +0.036] · [+0.014, +0.036]
Flat banks instead of hierarchical banks	0.965 +0.015 [+0.004, +0.026] · [+0.0031, +0.023]	0.960 +0.031 [+0.006, +0.065] · [+0.009, +0.090]	0.915 +0.019 [+0.008, +0.030] · [+0.008, +0.031]

Appendix

Table G.8: Ablation study.

Figure G.1: Grounding of visual parts.

Removed	Drop	Intervals	Drop	Intervals	Drop	Intervals
	Detection AUROC, intervention labels		Detection AUROC, generator labels		Abduction top-1, intervention labels
None (level)	0.723		0.968		0.542
A5	+0.033	[+0.016, +0.053] [+0.017, +0.060]	+0.059	[+0.042, +0.079] [+0.043, +0.078]	+0.077	[+0.054, +0.100] [+0.049, +0.098]
A2	+0.022	[+0.011, +0.034] [+0.003, +0.035]	+0.041	[+0.031, +0.053] [+0.032, +0.056]	+0.035	[−0.000, +0.071] [+0.006, +0.075]
A1	+0.017	[−0.004, +0.039] [−0.006, +0.038]	+0.136	[+0.120, +0.150] [+0.119, +0.153]	+0.187	[+0.161, +0.214] [+0.164, +0.212]
A4 and A4P	+0.014	[+0.003, +0.026] [+0.001, +0.029]	+0.032	[+0.021, +0.044] [+0.022, +0.049]	+0.052	[+0.024, +0.078] [+0.023, +0.081]

Appendix

Table G.9: Specification constraints removed from the knowledge base.

	Oracle fitted on
Reading	107 aircraft	44 aircraft	61 aircraft
Benchmark
Instances	1,312	1,239	1,260
Test controls	32	4	10
Clean test aircraft flagged by the oracle, of 16	0	15	11
Intervention labels, same records: NeSySpec

Appendix

Table G.10: Generator oracles: levels of NeSySpec and its comparators.

	Oracle on 44 aircraft		Oracle on 61 aircraft
Reading	Value	Intervals	Value	Intervals
Intervention labels, same records: NeSySpec, change from the oracle on 107 aircraft
Constraint verdicts, macro-F1, test	−0.087	[−0.173, −0.022]·[−0.146, −0.029]	−0.039	[−0.109, −0.007]·[−0.098, −0.0034]
unseen families	−0.028	[−0.054, +0.017]·[−0.061, +0.003]	−0.058	[−0.105, −0.022]·[−0.116, −0.026]
unseen class	+0.013	[−0.010, +0.041]·[−0.011, +0.039]	−0.032	[−0.059, +0.003]·[−0.060, +0.002]
Constraint verdicts, exact-set, test	−0.213	[−0.309, −0.125]·[−0.279, −0.117]	−0.060	[−0.164, +0.032]·[−0.187, +0.043]

Appendix

Table G.11: Generator oracles fitted without test or out-of-distribution aircraft: paired changes and differences with their intervals.

Neuro-Symbolic Reasoning

Neuro-symbolic reasoning combines learned neural models with explicit logic, rules, knowledge structures, or executable tools to solve structured tasks.

See all 279 papers

Sep 4, 2026

Think-Verify-Revise: Neuro-Symbolic Visual Reasoning with Vision-Language Models and Dynamic Logic Tensor Networks

Visual reasoning tasks require a system to jointly perceive visual content and apply formal relational constraints---a combination that neither pure neural nor purely symbolic approaches handle well in isolation. This paper proposes a Neuro-Symbolic (NeSy) framework that closes this gap by tightly coupling a Vision-Language Model (VLM) for automatic First-Order Logic (FOL) rule induction with a Dynamic Logic Tensor Network (D-LTN) for differentiable rule verification, in a closed iterative feedback loop. The VLM receives a small set of labelled visual examples and proposes candidate FOL rules conforming to a strict grammar (Think); the D-LTN is automatically assembled from these rules at runtime and evaluates them grounding on CNN-produced visual embeddings (Verify); and verification failures are fed back to guide the VLM's next hypothesis (Revise). Evaluated on the ViSudo-PC benchmark across four visual domains (MNIST, EMNIST, KMNIST, FMNIST), the system induces valid Sudoku constraint rules using only three training examples as visual context. The proposed method achieves AUC scores matching or outperforming previous methods (NeuPSL, LTN), showing the potential for automatic rule discovery through VLM. Code is available at https://github.com/homayoun-afshari/nesy.

Homayoun Afshari, Pietro Basci, Alessandro Russo +1

Politecnico di Torino Department of Control and Computer Engineering Turin, Italy

Logic Tensor Networks Visual Reasoning Neuro-Symbolic Reasoning Visually Grounded Reasoning VLM Reasoning

Ask PDF

Oct 1, 2026

Auto-Formalizing Neuro-Symbolic Predictors

Neuro-Symbolic (NeSy) predictors incorporate prior knowledge into the prediction process of neural networks, ensuring that outputs satisfy specified constraints, making them particularly suitable for high-stakes applications where compliance with domain knowledge is essential. A key bottleneck in this paradigm is the acquisition of symbolic constraints: encoding domain knowledge into logical formulas remains a manual and expert-intensive process. In this work, we investigate the extent to which auto-formalization via LLMs can systematically translate textual knowledge into symbolic knowledge that can be plugged into NeSy predictors. To this end, we introduce auto-nesy-bench, a new benchmark for evaluating constraint formalization and its impact on downstream accuracy of NeSy predictors. Through an extensive evaluation across several domains, we find that LLMs can formalize constraints to a meaningful extent, generating formulas that are often similar to those provided by human experts. Moreover, when the generated formulas are syntactically valid, they can lead to high-quality downstream predictions. The code and benchmark are available at https://unitn-sml.github.io/auto-nesy-bench/.

Samuele Bortolotti, Weixin Chen, Han Zhao +3

University of Trento, Italy · University of Illinois Urbana-Champaign, USA · University of Edinburgh, UK

Neuro-Symbolic Reasoning

Ask PDF

May 13, 2026

Neurosymbolic Auditing of Natural-Language Software Requirements

Natural-language software requirements are often ambiguous, inconsistent, and underspecified; in safety-critical domains, these defects propagate into formal models that verify the wrong specification and into implementations that ship unsafe behavior. We show that large language models, equipped with an SMT solver, can audit such requirements: translating them into formal logic, detecting ambiguity through stochastic variation in the generated formalization, and exposing inconsistency, vacuousness, and safety violations through solver queries on the resulting specification. We present VERIMED, a neurosymbolic pipeline that operationalizes this idea for medical-device software requirements, and report two findings. First, stochastic variation across independent formalizations is a signal of ambiguity: requirements that admit multiple plausible interpretations produce SMT-inequivalent formalizations, and bidirectional SMT equivalence checking turns this disagreement into a solver-checkable test. Second, the usefulness of symbolic feedback depends on its granularity: in counterexample-guided repair on a hemodialysis question-answering benchmark, concrete SMT counterexamples raise verified accuracy from 55.4% to 98.5%. Over an extensive experimental evaluation on open-source hemodialysis safety requirements, we show that the LLM-based approach in VERIMED successfully reduces ambiguity-sensitive requirements and enables rigorous auditing of software requirements through SMT-based queries.

Bethel Hall, William Eiers

Stevens Institute of Technology

Requirements Engineering Formal Verification Satisfiability Modulo Theories Neuro-Symbolic Reasoning

Ask PDF

Abstract

Neuro-Symbolic Reasoning

Explore similar work

Think-Verify-Revise: Neuro-Symbolic Visual Reasoning with Vision-Language Models and Dynamic Logic Tensor Networks

Auto-Formalizing Neuro-Symbolic Predictors

Neurosymbolic Auditing of Natural-Language Software Requirements