Auto-Formalizing Neuro-Symbolic Predictors

Samuele Bortolotti; Weixin Chen; Han Zhao; Andrea Passerini; Stefano Teso; Antonio Vergari

cs.LGOct 1, 2026

Auto-Formalizing Neuro-Symbolic Predictors

Authors: Samuele Bortolotti, Weixin Chen, Han Zhao, Andrea Passerini, Stefano Teso, Antonio Vergari

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

Abstract

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/.

Figures & tables

Panel of Figure 1 — Figure 1: Illustration of our auto-nesy-bench auto-formalization framework : given a natural language description of a constraint and the corresponding variables, an LLM generates DIMACS , PySAT , CPMpy , SymPy , or natural language ( NAT ) formalizations. Non- DIMACS outputs are converted to DIMACS and later compiled, via knowledge compilation, into circuits that can be used in NeSy predictors ( SPL ), thus ensuring that the output satisfies the specified constraints by design, following Eq. 1 . The five boxes show equivalent encodings of $(\texttt{green}\land\texttt{clear})\Rightarrow\texttt{forward}$ .

Dataset	Model	F1 ( $\uparrow$ )	Precision ( $\uparrow$ )	Recall ( $\uparrow$ )	Syntax ER ( $\downarrow$ )
auto-nesy-bench	qwen3-8b	$0.372\pm 0.202$	$0.402\pm 0.192$	$0.423\pm 0.200$	$30.6\%\pm 25.5\%$
	mistral-nemo	$0.053\pm 0.074$	$0.051\pm 0.073$	$0.154\pm 0.093$	$62.8\%\pm 22.9\%$
	phi4-reasoning-plus	$0.423\pm 0.177$	$0.438\pm 0.167$	$0.440\pm 0.191$	$49.4\%\pm 16.9\%$
	gpt-oss-20b	$0.505\pm 0.163$	$0.564\pm 0.124$	$0.556\pm 0.149$	$30.0\%\pm 10.9\%$
	gemma3-27b	$0.040\pm 0.040$	$0.048\pm 0.053$	$0.164\pm 0.134$	$55.6\%\pm 29.7\%$
	gemma4-31b	$\underline{0.706\pm 0.233}$	$\underline{0.732\pm 0.203}$	$\underline{0.782\pm 0.197}$	$\mathbf{3.9\%\pm 2.5\%}$

Table 1: Model choice substantially affects auto-formalization performance across benchmarks. We compare various models on all benchmarks, reporting F1, precision, recall, and syntax error rate (mean

\pm

standard deviation). LLM coverage varies slightly due to resource constraints (see Appendix I for the full results). Best results are in bold, and second-best results are underlined. Ordered by size.

Dataset	Variant	Config.	F1 ( $\uparrow$ )	Precision ( $\uparrow$ )	Recall ( $\uparrow$ )	Syntax ER ( $\downarrow$ )
auto-nesy-bench	Description	Non-Detailed	$0.330\pm 0.206$	$0.357\pm 0.218$	$0.464\pm 0.221$	$\mathbf{25.3\%\pm 24.9\%}$
	Description	Detailed	$\mathbf{0.455\pm 0.277}$	$\mathbf{0.478\pm 0.279}$	$\mathbf{0.532\pm 0.263}$	$28.9\%\pm 25.7\%$
	Prompting	ZS	$0.437\pm 0.262$	$0.463\pm 0.268$	$0.515\pm 0.243$	$\mathbf{28.2\%\pm 24.7\%}$
	Prompting	ZS-CoT	$\mathbf{0.472\pm 0.290}$	$\mathbf{0.494\pm 0.289}$	$\mathbf{0.548\pm 0.281}$	$29.6\%\pm 26.6\%$
dcpbench	Prompting	ZS	$0.176\pm 0.119$	$0.181\pm 0.124$	$\mathbf{0.285\pm 0.132}$	$\mathbf{33.7\%\pm 20.6\%}$
dcpbench	Prompting	ZS-CoT	$\mathbf{0.191\pm 0.113}$	$\mathbf{0.197\pm 0.118}$	$0.272\pm 0.113$	$35.0\%\pm 20.3\%$

Table 2: Detailed descriptions and CoT prompts improve auto-formalization performance across all benchmarks. We compare detailed and natural descriptions on auto-nesy-bench and zero-shot (ZS) and zero-shot-chain-of-thought (ZS-CoT) prompts on auto-nesy-bench , dcpbench , and satbench , reporting F1, precision, recall, and syntax error rate, with mean

\pm

standard deviation. Best results are highlighted in bold. See Appendix I for the complete results.

Dataset	Format	F1 ( $\uparrow$ )	Precision ( $\uparrow$ )	Recall ( $\uparrow$ )	Syntax ER ( $\downarrow$ )
auto-nesy-bench	DIMACS	$0.364\pm 0.223$	$0.394\pm 0.231$	$0.467\pm 0.227$	$\mathbf{20.5\%\pm 18.8\%}$
	NAT	$0.331\pm 0.173$	$0.361\pm 0.178$	$0.457\pm 0.199$	$31.8\%\pm 22.5\%$
	PySAT	$0.453\pm 0.300$	$0.500\pm 0.310$	$0.498\pm 0.284$	$31.1\%\pm 26.3\%$
	CPMpy	$\mathbf{0.575\pm 0.299}$	$\mathbf{0.586\pm 0.303}$	$\mathbf{0.622\pm 0.280}$	$\underline{30.3\%\pm 28.2\%}$
	SymPy	$\underline{0.549\pm 0.280}$	$\underline{0.550\pm 0.281}$	$\underline{0.614\pm 0.265}$	$30.8\%\pm 29.4\%$
dcpbench	DIMACS	$0.147\pm 0.094$	$0.157\pm 0.106$	$\mathbf{0.358\pm 0.114}$	$\mathbf{21.3\%\pm 16.6\%}$

Table 3: Code-based output formats generally achieve higher auto-formalization performance on auto-nesy-bench and dcpbench , whereas the NAT performs best on satbench . We compare five output formats reporting F1, precision, recall, and syntax error, with mean

\pm

standard deviation. Best results are in bold, and second-best results are underlined (see Appendix I for full results).

	G-T		gpt-oss-120b				olmo3-32b-think				qwen3-8b
Task	F1 $(\uparrow)$	Rec $(\uparrow)$	$\Delta$ F1	$\Delta$ Rec	Rel	MC-R	$\Delta$ F1	$\Delta$ Rec	Rel	MC-R	$\Delta$ F1	$\Delta$ Rec	Rel	MC-R
bdd-oia	$0.58$	$0.57$	$+0.01$	$+0.01$	$=$	$1.00$	$\dagger$	$\dagger$	$\dagger$	$\dagger$	$+0.00$	$+0.01$	$=$	$1.00$
bdd-oia-2	$0.74$	$0.74$	$+0.01$	$+0.01$	$=$	$1.00$	$+0.01$	$+0.01$	$=$	$1.00$	$\star$	$\star$	$\star$	$\star$
cebab	$0.47$	$0.46$	$+0.00$	$+0.01$	$=$	$1.00$	$-0.01$	$-0.01$	$=$	$1.00$	$\star$	$\star$	$\star$	$\star$
chx	$0.54$	$0.52$	$-0.06$	$-0.04$	$=$	$1.00$	$\lx@sectionsign$	$\lx@sectionsign$	$\lx@sectionsign$	$\lx@sectionsign$	$\dagger$	$\dagger$	$\dagger$	$\dagger$
cifar10	$0.87$	$0.87$	$-0.07$	$-0.07$	$=$	$1.00$	$-0.06$	$-0.06$	$=$	$1.00$	$-0.06$	$-0.06$	$=$	$1.00$

Table 4: Generated formulas, when available, achieve comparable downstream SPL performance to expert-provided formulas on auto-nesy-bench . We report mean

\Delta

F1 /

\Delta

Recall ( Rec ) relative to the ground-truth; standard deviations across

5

seeds are omitted (see Appendix I ). Rel denotes the relation between predicted and ground-truth formulas: equal (

=

), strict (

\Rightarrow

), permissive (

\Leftarrow

), or incomparable (

\parallel

), indicating whether the predicted formula satisfying assignments are equal to, a subset of, a superset of, or neither. MC-R measures the ratio of satisfying assignments of the predicted formula to that of the ground-truth formula. Missing cells indicate:

\dagger

degenerate formula (e.g., UNSAT),

\star

no formula generated (no CNF), or

\lx@sectionsign

run failure (crash) (see Table 24 ).

Appendix figures & tables48 assets

Supplementary material from the paper’s appendix.

Appendix

mistral-nemo	mistralai/Mistral-Nemo-Instruct-2407
Model	Link	CUDA	vLLM	GPUs
qwen3-32b	Qwen/Qwen3-32B	12.5.0	0.23.0	2 $\times$ A100 80 GB
phi4-reasoning-plus	microsoft/Phi-4-reasoning-plus
gemma3-27b	google/gemma-3-27b-it	12.6	0.23.0	1–2 $\times$ RTX PRO 6000 Blackwell 96 GB (sm_120)
gemma4-31b	google/gemma-4-31B-it	12.6	0.23.0	1–2 $\times$ RTX PRO 6000 Blackwell 96 GB (sm_120)
olmo3-32b-think	allenai/Olmo-3-32B-Think	12.6	0.23.0	4 $\times$ A100

Appendix

Table 5: LLM evaluation with the vLLM backend across the clusters used in our experiments.

Dataset	Problems	Variables			Clauses			NeSy-Ready
Dataset	Problems	Min	Max	Mean	Min	Max	Mean	NeSy-Ready
satbench ( Wei et al., 2025 )	$1{,}041$	$5$	$90$	$36$	$4$	$50$	$20$	✗
dcpbench ( Michailidis et al., 2025b )	$85$	$8$	$1{,}102{,}080$	$58{,}673$	$20$	$7{,}095{,}776$	$394{,}204$	✗
auto-nesy-bench (ours)	$18$	$9$	$102$	$32$	$17$	$129{,}648$	$7{,}966$	✓

Appendix

Table 6: auto-nesy-bench is NeSy-ready, while existing benchmarks are not . satbench contains many small problems, whereas dcpbench contains fewer but substantially larger problems. auto-nesy-bench offers a balanced mix and, importantly, includes input-output annotations for use with NeSy predictors. Variables and clauses are reported as min / max / mean .

Natural-language constraint	CNF clause	DIMACS encoding
Ana signs up for watering duty.	$x_{0}$	1 0
Either Ben does not sign up, or Ana does not sign up.	$\neg x_{1}\lor\neg x_{0}$	-2 -1 0
Either Ana does not sign up, or Emma signs up.	$\neg x_{0}\lor x_{4}$	-1 5 0
Either Carla does not sign up, or Ben signs up.	$\neg x_{2}\lor x_{1}$	-3 2 0

Appendix

Table 7: Example from satbench . Each satbench instance pairs a natural language scenario and variable descriptions with a reference Boolean formula. Here, five community-garden volunteers, Ana, Ben, Carla, Dave, and Emma, decide whether to sign up for weekend watering duty, where

x_{i}

indicates whether volunteer

i

signs up, in the order just given. Each row shows one natural-language constraint and its corresponding CNF clause and DIMACS encoding. The reference formula is the conjunction of all clauses. In our auto-formalization setting, the natural language scenario and constraints serve as input, and the conjunction of all constraints serves as the reference formalization.

Task	Variables	Clauses
chx ( Cohen et al., 2022 )	9	27
fashion ( Xiao et al., 2017 )	10	46
bdd-oia-2 ( Xu et al., 2020 )	11	17
cle4evr ( Johnson et al., 2017 )	12	28
cifar10 ( Krizhevsky et al., 2009 )	15	157
mn-add-bin ( Manhaeve et al., 2018 )	13	512

Appendix

Table 8: NeSy tasks and their ground-truth DIMACS sizes.

Figure 2: A sample from the chx dataset.

Panel of Figure 3 — Figure 3: Samples from fashion and cifar100 datasets.

Figure 4: A sample from the cifar10 dataset.

Figure 5: A sample from the mn-add / mn-mul dataset.

Panel of Figure 6 — Figure 6: Samples from kand-logic-2 / kand-logic datasets.

Figure 7: A sample from the sudoku dataset.

Figure 8: A sample from the warcraft dataset.

Figure 9: A sample from the cle4evr dataset.

Dataset	Task(s)	License	Redistributed
MNIST ( LeCun, 1998 )	mn-add(mul)(-bin)	Unrestricted (NIST-derived)	✓
Fashion-MNIST ( Xiao et al., 2017 )	fashion	MIT	✓
CIFAR-based ( Krizhevsky et al., 2009 )	cifar10(100)	No explicit license	✗
BDD-OIA ( Xu et al., 2020 )	bdd-oia(-2)	See ( Bortolotti et al., 2024 )	✓
ROAD-R ( Giunchiglia et al., 2023 )	road-r	CC BY-NC-SA 4.0	✓
SUSHI3 ( Kamishima, 2003 )	sushi	Research use permitted; redistribution forbidden.	✗

Appendix

Table 9: License and redistribution status of every auto-nesy-bench datasets . “Redistributed” indicates whether the data itself can be shipped in a new benchmark, as opposed to being fetched from the original source.

Model	sample	$\tau$	$\rho$	$\kappa$	rep. pen.	think	precision
qwen3-32b	✓	0.6	0.95	20	–	✓	bf16
qwen3-8b	✓	0.6	0.95	20	–	✓	bf16
qwen3-coder-next	✓	1.0	0.95	40	–	–	bf16
mistral-nemo	–	–	–	–	–	–	bf16
phi4-reasoning-plus	✓	0.8	0.95	50	–	✓	bf16
gemma3-27b-it	✓	0.7	0.95	64	1.3	–	bf16

Appendix

Table 10: Decoding hyperparameters for the evaluated LLMs . “sample” is do_sample ; a dash means the parameter is unset (provider default); “think” marks models whose reasoning trace is always active. All values are the model-card / generation_config.json defaults unless noted.

$\times\,3$ more identical $(\text{Conv2d}+\text{BN}+\text{ReLU}+\text{MaxPool2d})$ blocks, depth $64\!\to\!64$
Input	Layer Type	Parameter	Activation
$(C_{\text{in}},H,W)$	Conv2d + BatchNorm2d	depth $=64$ , kernel $=3$ , stride $=1$ , padding $=1$	ReLU
$(64,H,W)$	MaxPool2d	kernel $=2$ , stride $=2$
$(64,H^{\prime},W^{\prime})$	AdaptiveAvgPool2d	output $=(1,1)$
$(64,1,1)$	Flatten	dim $=64$
$(64)$	Linear	$64\to\mathtt{output\_size}$

Appendix

Table 11: Conv4 architecture ( MNIST -based tasks, sudoku , fashion and warcraft ).

C_{\text{in}}

1

for grayscale and

3

for RGB inputs.

Input	Layer Type	Parameter	Activation
$(C_{\text{in}},H,W)$	Conv2d + BatchNorm2d	depth $=64$ , kernel $=7$ , stride $=2$ , padding $=3$	ReLU
$(64,H/2,W/2)$	MaxPool2d	kernel $=3$ , stride $=2$ , padding $=1$
$(64,H/4,W/4)$	BasicBlock $\times\,2$ ( layer1 )	depth $64\!\to\!64$ , stride $=1$	ReLU
$(64,H/4,W/4)$	BasicBlock $\times\,2$ ( layer2 )	depth $64\!\to\!128$ , stride $=2$ (block 1)	ReLU
$(128,H/8,W/8)$	BasicBlock $\times\,2$ ( layer3 )	depth $128\!\to\!256$ , stride $=2$ (block 1)	ReLU
$(256,H/16,W/16)$	BasicBlock $\times\,2$ ( layer4 )	depth $256\!\to\!512$ , stride $=2$ (block 1)	ReLU

Appendix

Table 12: ResNet-18 architecture ( cifar10 , cifar100 , chx ).

C_{\text{in}}

3

for all three tasks;

(H,W)

32\!\times\!32

for cifar10 , cifar100 and

224\!\times\!224

for chx .

Input	Layer Type	Parameter	Activation
$(d_{\text{in}})$	Linear	$d_{\text{in}}\to h$	ReLU
$(h)$	Linear	$h\to h$ ( $\times\,(L-1)$ )	ReLU
$(h)$	Linear	$h\to\mathtt{output\_size}$

Appendix

Table 13: MLP backbone ( bdd-oia , sushi ).

d_{\text{in}}

2048

for BDD-OIA and

36

for sushi .

Input	Layer Type	Parameter	Activation
$(n_{\text{tok}},2)$	tokenized input ( input_ids , attention_mask )	max length $n_{\text{tok}}=128$
$(n_{\text{tok}},2)$	BertModel ( bert-base-uncased , frozen)	$12$ Transformer encoder layers,
		hidden $=768$ , heads $=12$ ,
		FFN $=3072$	GELU (internal)
$(768)$	[CLS] pooled token	—
$(768)$	Linear	$768\to h$	ReLU

Appendix

Table 14: BERT backbone ( cebab ).

n_{\text{tok}}=128

is the fixed max token length;

L\in\{2,3\}

and

h

configure the trainable projection (same search parameters as Table 13 ). BERT itself is frozen; only the projection and SPL head receive gradients.

Stage	Slow pathway	Fast pathway	Output (slow / fast ch.)
data	sample $4$ frames ( $\alpha=2$ )	all $8$ frames	$3$ / $3$
conv1	Conv3d $k{=}(1,7,7)$ , $s{=}(1,2,2)$	Conv3d $k{=}(5,7,7)$ , $s{=}(1,2,2)$	$64$ / $8$
pool1	MaxPool3d $k{=}(1,3,3)$ , $s{=}(1,2,2)$	MaxPool3d $k{=}(1,3,3)$ , $s{=}(1,2,2)$	$64$ / $8$
res2	$3\times$ bottleneck	$3\times$ bottleneck	$256$ / $32$
res3	$4\times$ bottleneck, stride $2$	$4\times$ bottleneck, stride $2$	$512$ / $64$
res4	$6\times$ bottleneck, stride $2$	$6\times$ bottleneck, stride $2$	$1024$ / $128$

Appendix

Table 15: Slowfast-50 backbone used for road-r , for an

8

-frame

(3,8,96,96)

clip. Channel counts are given as slow / fast; the slow pathway runs at

T/\alpha=4

frames, the fast pathway at

T=8

Figure 10: Larger formulas are generally more difficult to formalize, although the magnitude of this effect is dataset-dependent. We report mean F1 against the number of variables or clauses on a log scale for auto-nesy-bench (top), dcpbench (middle), and satbench (bottom). Each point represents the mean F1 for a specific benchmark instance. The red line and shaded region indicate the ordinary least-squares fit and its

95\%

confidence interval.

Dataset	Model	Prompt	Format	F1 ( $\uparrow$ )	Precision ( $\uparrow$ )	Recall ( $\uparrow$ )	Syn. ER ( $\downarrow$ )
auto-nesy-bench	deepseek-r1-llama-70b	ZS	SymPy	$0.676$	$0.640$	$0.810$	$\underline{11.1\%}$
	gemma3-27b	ZS-CoT	NAT	$0.135$	$0.192$	$0.449$	$22.2\%$
	gemma4-31b	ZS-CoT	CPMpy	$\mathbf{0.991}$	$\mathbf{0.986}$	$\underline{0.997}$	$\mathbf{0.0\%}$
	gpt-oss-120b	ZS-CoT	CPMpy	$\underline{0.984}$	$\underline{0.974}$	$\mathbf{1.000}$	$\mathbf{0.0\%}$
	gpt-oss-20b	ZS-CoT	SymPy	$0.769$	$0.756$	$0.833$	$16.7\%$
	mistral-nemo	ZS-CoT	CPMpy	$0.259$	$0.256$	$0.325$	$50.0\%$

Appendix

Table 16: Selecting an appropriate prompting strategy and output format substantially improves best-case formalization performance. Best formalization performance of each model on auto-nesy-bench , dcpbench , and satbench . For each model, we select the best of ten configurations formed by two prompting strategies and five output formats according to F1 score, breaking ties by accuracy and then by fixed prompt and format order, and report the corresponding precision, recall, and syntax error rate. Average rows give each model equal weight. Within each dataset, best results are bolded, and second-best results are underlined; averages are excluded from the ranking.

Model	Prompt	Format	F1 ( $\uparrow$ )	Precision ( $\uparrow$ )	Recall ( $\uparrow$ )	Syntax ER ( $\downarrow$ )
deepseek-r1-llama-70b	ZS	CPMpy	$0.503$	$0.532$	$0.551$	$33.3\%$
deepseek-r1-llama-70b	ZS	DIMACS	$0.523$	$0.522$	$0.587$	$16.7\%$
deepseek-r1-llama-70b	ZS	NAT	$0.363$	$0.409$	$0.619$	$5.6\%$
deepseek-r1-llama-70b	ZS	PySAT	$0.541$	$0.695$	$0.604$	$16.7\%$
deepseek-r1-llama-70b	ZS	SymPy	$0.676$	$0.640$	$0.810$	$11.1\%$
deepseek-r1-llama-70b	ZS-CoT	CPMpy	$0.111$	$0.111$	$0.167$	$83.3\%$

Appendix

Table 17: Complete per-configuration formalization results on auto-nesy-bench . ZS and ZS-CoT denote zero-shot and zero-shot chain-of-thought prompting. Missing task scores are assigned zero. Syntax ER is taken directly from the selected results JSON.

Model	Prompt	Format	F1 ( $\uparrow$ )	Precision ( $\uparrow$ )	Recall ( $\uparrow$ )	Syntax ER ( $\downarrow$ )
deepseek-r1-llama-70b	ZS	CPMpy	$0.121$	$0.119$	$0.200$	$40.0\%$
deepseek-r1-llama-70b	ZS	DIMACS	$0.078$	$0.075$	$0.319$	$25.9\%$
deepseek-r1-llama-70b	ZS	NAT	$0.061$	$0.063$	$0.210$	$29.4\%$
deepseek-r1-llama-70b	ZS	PySAT	$0.085$	$0.088$	$0.174$	$30.6\%$
deepseek-r1-llama-70b	ZS	SymPy	$0.165$	$0.162$	$0.271$	$37.6\%$
deepseek-r1-llama-70b	ZS-CoT	CPMpy	$0.067$	$0.071$	$0.124$	$44.7\%$

Appendix

Table 18: Complete per-configuration formalization results on dcpbench . ZS and ZS-CoT denote zero-shot and zero-shot chain-of-thought prompting. Missing task scores are assigned zero. Syntax ER is taken directly from the selected results JSON.

Model	Prompt	Format	F1 ( $\uparrow$ )	Precision ( $\uparrow$ )	Recall ( $\uparrow$ )	Syntax ER ( $\downarrow$ )
gemma4-31b	ZS	CPMpy	$0.988$	$0.987$	$0.991$	$0.1\%$
gemma4-31b	ZS	DIMACS	$0.530$	$0.520$	$0.568$	$0.0\%$
gemma4-31b	ZS	NAT	$0.965$	$0.962$	$0.980$	$0.0\%$
gemma4-31b	ZS	PySAT	$0.982$	$0.981$	$0.986$	$0.0\%$
gemma4-31b	ZS	SymPy	$0.970$	$0.970$	$0.976$	$1.0\%$
gemma4-31b	ZS-CoT	CPMpy	$0.991$	$0.990$	$0.995$	$0.0\%$

Appendix

Table 19: Complete per-configuration formalization results on satbench . ZS and ZS-CoT denote zero-shot and zero-shot chain-of-thought prompting. Missing task scores are assigned zero. Syntax ER is taken directly from the selected results JSON.

Figure 11: The relationship between model size and auto-formalization performance varies across datasets. Larger models tend to perform better on auto-nesy-bench and dcpbench , but this trend does not extend to satbench . We report mean F1 as a function of total model parameter count on auto-nesy-bench (top), dcpbench (middle), and satbench (bottom). Each point represents a model mean F1 across matched runs. Circles denote non-reasoning models, while triangles denote reasoning models. The red line and shaded region show the ordinary least-squares fit and its 95% confidence interval, respectively. Parameter count is shown on a base-10 logarithmic scale. None of the fitted associations is statistically significant.

Panel of Figure 12 — Figure 12: Code representations, particularly CPMpy and SymPy , are generally effective on auto-nesy-bench and dcpbench , while NAT performs best on satbench . We report mean F1 by model and output format on auto-nesy-bench (top), dcpbench (middle), and satbench (bottom). Each cell reports F1 averaged across the two prompting strategies for a given model-format pair. The rightmost column shows the mean across formats for each model, while the bottom row shows the mean across models for each format. Missing F1 scores are treated as zero.

Panel of Figure 13 — Figure 13: Syntactic errors are concentrated in a small number of categories and models. Occurrences of each error code in the final model outputs on auto-nesy-bench (top), dcpbench (middle), and satbench (bottom), aggregated across output formats and prompting strategies. A single output can contribute to multiple error codes. The rightmost column reports the mean across error types, and the bottom row reports the mean across models.

Panel of Figure 14 — Figure 14: Output formats exhibit distinct syntactic errors. Occurrences of each error code in the final model outputs on auto-nesy-bench (top), dcpbench (middle), and satbench (bottom), aggregated over models and prompting strategies. A single output can contribute to multiple error codes. The rightmost column averages over error types, and the bottom row averages over formats.

Task	Consistency $(\uparrow)$	Accuracy $(\uparrow)$	Precision $(\uparrow)$	Recall $(\uparrow)$	F1 $(\uparrow)$	Rel	MC-R
bdd-oia-2	$1.00\pm 0.00$	$0.76\pm 0.00$	$0.75\pm 0.00$	$0.75\pm 0.00$	$0.75\pm 0.00$	$=$	$1.00$
cebab	$1.00\pm 0.00$	$0.63\pm 0.01$	$0.48\pm 0.01$	$0.45\pm 0.01$	$0.46\pm 0.01$	$=$	$1.00$
cifar10	$1.00\pm 0.00$	$0.94\pm 0.00$	$0.81\pm 0.01$	$0.81\pm 0.01$	$0.81\pm 0.01$	$=$	$1.00$
cifar100	$1.00\pm 0.00$	$0.99\pm 0.00$	$0.25\pm 0.01$	$0.31\pm 0.01$	$0.26\pm 0.01$	$=$	$1.00$
cle4evr	$1.00\pm 0.00$	$1.00\pm 0.00$	$0.99\pm 0.01$	$0.99\pm 0.01$	$0.99\pm 0.01$	$=$	$1.00$
fashion	$1.00\pm 0.00$	$0.98\pm 0.00$	$0.92\pm 0.00$	$0.92\pm 0.01$	$0.91\pm 0.01$	$=$	$1.00$

Appendix

Table 20: SPL full results with olmo3-32b-think formulas using CPMpy , CoT and detailed prompt . The table reports consistency, accuracy, precision, F1, Rel , and MC-R . Mean

\pm

std over 5 seeds.

Task	Consistency $(\uparrow)$	Accuracy $(\uparrow)$	Precision $(\uparrow)$	Recall $(\uparrow)$	F1 $(\uparrow)$	Rel	MC-R
bdd-oia	$1.00\pm 0.00$	$0.78\pm 0.00$	$0.58\pm 0.01$	$0.58\pm 0.01$	$0.58\pm 0.01$	$=$	$1.00$
cifar10	$1.00\pm 0.00$	$0.94\pm 0.00$	$0.82\pm 0.01$	$0.81\pm 0.01$	$0.81\pm 0.01$	$=$	$1.00$
cifar100	$1.00\pm 0.00$	$0.99\pm 0.00$	$0.25\pm 0.00$	$0.32\pm 0.00$	$0.27\pm 0.00$	$=$	$1.00$
cle4evr	$1.00\pm 0.00$	$1.00\pm 0.00$	$1.00\pm 0.00$	$1.00\pm 0.00$	$1.00\pm 0.00$	$=$	$1.00$
fashion	$1.00\pm 0.00$	$0.98\pm 0.00$	$0.92\pm 0.00$	$0.92\pm 0.00$	$0.92\pm 0.01$	$=$	$1.00$
kand-logic-2	$1.00\pm 0.00$	$0.80\pm 0.00$	$0.71\pm 0.00$	$0.70\pm 0.00$	$0.70\pm 0.00$	$\Rightarrow$	$0.02$

Appendix

Table 21: SPL full results with qwen3-8b formulas using CPMpy , CoT and detailed prompt . The table reports consistency, accuracy, precision, F1, Rel , and MC-R . Mean

\pm

std over 5 seeds.

Task	Consistency $(\uparrow)$	Accuracy $(\uparrow)$	Precision $(\uparrow)$	Recall $(\uparrow)$	F1 $(\uparrow)$	Rel	MC-R
bdd-oia	$1.00\pm 0.00$	$0.78\pm 0.00$	$0.60\pm 0.01$	$0.58\pm 0.01$	$0.59\pm 0.01$	$=$	$1.00$
bdd-oia-2	$1.00\pm 0.00$	$0.76\pm 0.00$	$0.75\pm 0.00$	$0.75\pm 0.01$	$0.75\pm 0.00$	$=$	$1.00$
cebab	$1.00\pm 0.00$	$0.64\pm 0.01$	$0.48\pm 0.01$	$0.47\pm 0.02$	$0.47\pm 0.01$	$=$	$1.00$
chx	$1.00\pm 0.00$	$0.64\pm 0.02$	$0.59\pm 0.07$	$0.47\pm 0.02$	$0.48\pm 0.02$	$=$	$1.00$
cifar10	$1.00\pm 0.00$	$0.94\pm 0.00$	$0.81\pm 0.01$	$0.80\pm 0.01$	$0.80\pm 0.01$	$=$	$1.00$
cifar100	$1.00\pm 0.00$	$0.99\pm 0.00$	$0.25\pm 0.00$	$0.32\pm 0.01$	$0.27\pm 0.00$	$=$	$1.00$

Appendix

Table 22: SPL full results with gpt-oss-120b formulas using CPMpy , CoT and detailed prompt . The table reports consistency, accuracy, precision, F1, Rel , and MC-R . Mean

\pm

std over 5 seeds.

Task	Consistency $(\uparrow)$	Accuracy $(\uparrow)$	Precision $(\uparrow)$	Recall $(\uparrow)$	F1 $(\uparrow)$	Rel	MC-R
bdd-oia	$-$	$0.78\pm 0.00$	$0.59\pm 0.00$	$0.57\pm 0.01$	$0.58\pm 0.00$	$-$	$-$
bdd-oia-2	$-$	$0.75\pm 0.00$	$0.75\pm 0.00$	$0.74\pm 0.00$	$0.74\pm 0.00$	$-$	$-$
cebab	$-$	$0.64\pm 0.00$	$0.48\pm 0.02$	$0.46\pm 0.02$	$0.47\pm 0.01$	$-$	$-$
chx	$-$	$0.68\pm 0.01$	$0.61\pm 0.10$	$0.52\pm 0.04$	$0.54\pm 0.05$	$-$	$-$
cifar10	$-$	$0.96\pm 0.00$	$0.88\pm 0.00$	$0.87\pm 0.01$	$0.87\pm 0.01$	$-$	$-$
cifar100	$-$	$0.99\pm 0.00$	$0.32\pm 0.00$	$0.41\pm 0.00$	$0.35\pm 0.00$	$-$	$-$

Appendix

Table 23: SPL full results with ground-truth formulas using CPMpy , CoT and detailed prompt . The table reports consistency, accuracy, precision, F1, Rel , and MC-R . Mean

\pm

std over 5 seeds. As Con and MC-R are defined against ground-truth formulas, they are left empty.

Model	Task	Category	Reason ( CPMpy + CoT )
olmo3-32b-think	bdd-oia	formula degenerate	UNSAT (0 models)
olmo3-32b-think	kand-logic	no formula produced	no CNF generated
olmo3-32b-think	sudoku	no formula produced	no CNF generated
olmo3-32b-think	chx	run failure	CUDA device-side assert
olmo3-32b-think	road-r	run failure	process stalled
olmo3-32b-think	mn-add-bin	formula degenerate	4 of 13 declared variables are missing

Appendix

Table 24: Reasons behind the missing results in Table 4 , CPMpy + CoT.

	G-T			gpt-oss-120b					olmo3-32b-think
Task	F1 $(\uparrow)$	Rec $(\uparrow)$	Cons $(\uparrow)$	$\Delta$ F1	$\Delta$ Rec	$\Delta$ Cons	Rel	MC-R	$\Delta$ F1	$\Delta$ Rec	$\Delta$ Cons	Rel	MC-R
bdd-oia	$0.58$	$0.57$	$1.00$	–	–	–	–	–	–	–	–	–	–
bdd-oia-2	$0.74$	$0.74$	$1.00$	$-0.08$	$-0.08$	$+0.00$	$\parallel$	$1.00$	–	–	–	–	–
cebab	$0.47$	$0.46$	$1.00$	–	–	–	–	–	–	–	–	–	–
chx	$0.54$	$0.52$	$1.00$	$-0.27$	$-0.16$	$+0.00$	$\Rightarrow$	$0.94$	$-0.54$	$-0.52$	$-0.35$	$\parallel$	$1.00$
cifar10	$0.87$	$0.87$	$1.00$	$-0.55$	$-0.47$	$+0.00$	$\parallel$	$3.38$	$-0.07$	$-0.07$	$+0.00$	$\Leftarrow$	$19.25$

Appendix

Table 25: With less-detailed prompts, generated formulas still match expert-provided ones on most tasks, but non-equivalent formulas degrade downstream SPL performance. Formulas are generated with CPMpy + CoT from the non-detailed prompt. We report mean

\Delta

F1 /

\Delta

Recall ( Rec )/

\Delta

consistency ( Cons ) relative to the ground-truth ( G-T ) formula; standard deviations across

5

seeds are omitted (see below for the full results). Rel denotes the relation between predicted and ground-truth formulas: equal (

=

), strict (

\Rightarrow

), permissive (

\Leftarrow

), or incomparable (

\parallel

), indicating whether the predicted formula satisfying assignments are equal to, a subset of, a superset of, or neither; unknown marks the two kand-logic formulas, for which the exact comparison, which is based on model counting, did not terminate. MC-R measures the ratio of satisfying assignments of the predicted formula to that of the ground-truth formula. Consistency drops below that of G-T only for incomparable or unknown formulas, which allow predictions the ground truth rejects. Interestingly, this does not happen for strict or permissive formulas. Missing cells indicate that the formula is either missing or was not executable (see Table 29 for details).

Task	Consistency $(\uparrow)$	Accuracy $(\uparrow)$	Precision $(\uparrow)$	Recall $(\uparrow)$	F1 $(\uparrow)$	Rel	MC-R
bdd-oia-2	$1.00\pm 0.00$	$0.70\pm 0.01$	$0.71\pm 0.00$	$0.66\pm 0.02$	$0.67\pm 0.02$	$\parallel$	$1.00$
chx	$1.00\pm 0.00$	$0.42\pm 0.03$	$0.27\pm 0.07$	$0.36\pm 0.01$	$0.26\pm 0.03$	$\Rightarrow$	$0.94$
cifar10	$1.00\pm 0.00$	$0.82\pm 0.00$	$0.29\pm 0.01$	$0.40\pm 0.01$	$0.32\pm 0.01$	$\parallel$	$3.38$
cifar100	$1.00\pm 0.00$	$0.99\pm 0.00$	$0.25\pm 0.00$	$0.32\pm 0.01$	$0.27\pm 0.01$	$=$	$1.00$
cle4evr	$1.00\pm 0.00$	$1.00\pm 0.00$	$0.99\pm 0.01$	$0.99\pm 0.01$	$0.99\pm 0.01$	$=$	$1.00$
fashion	$1.00\pm 0.00$	$0.98\pm 0.00$	$0.92\pm 0.01$	$0.92\pm 0.01$	$0.92\pm 0.01$	$=$	$1.00$

Appendix

Table 26: SPL results for non detailed prompt using gpt-oss-120b formulas . The table reports consistency, accuracy, precision, F1, Rel , and MC-R . Mean

\pm

std over 5 seeds.

Task	Consistency $(\uparrow)$	Accuracy $(\uparrow)$	Precision $(\uparrow)$	Recall $(\uparrow)$	F1 $(\uparrow)$	Rel	MC-R
chx	$0.65\pm 0.08$	$0.00\pm 0.00$	$0.00\pm 0.00$	$0.00\pm 0.00$	$0.00\pm 0.00$	$\parallel$	$1.00$
cifar10	$1.00\pm 0.00$	$0.94\pm 0.00$	$0.81\pm 0.01$	$0.80\pm 0.01$	$0.80\pm 0.01$	$\Leftarrow$	$19.25$
cifar100	$1.00\pm 0.00$	$0.99\pm 0.00$	$0.25\pm 0.01$	$0.31\pm 0.01$	$0.26\pm 0.01$	$=$	$1.00$
cle4evr	$1.00\pm 0.00$	$0.99\pm 0.01$	$0.99\pm 0.02$	$0.99\pm 0.02$	$0.99\pm 0.02$	$=$	$1.00$
fashion	$1.00\pm 0.00$	$0.98\pm 0.00$	$0.92\pm 0.00$	$0.92\pm 0.01$	$0.91\pm 0.01$	$=$	$1.00$
kand-logic-2	$1.00\pm 0.00$	$0.70\pm 0.00$	$0.56\pm 0.01$	$0.55\pm 0.00$	$0.54\pm 0.00$	$\Rightarrow$	$0.02$

Appendix

Table 27: SPL results for non detailed prompt using olmo-32b-think formulas. The table reports consistency, accuracy, precision, F1, Rel , and MC-R . Mean

\pm

std over 5 seeds.

Task	Consistency $(\uparrow)$	Accuracy $(\uparrow)$	Precision $(\uparrow)$	Recall $(\uparrow)$	F1 $(\uparrow)$	Rel	MC-R
cifar10	$1.00\pm 0.00$	$0.94\pm 0.00$	$0.82\pm 0.00$	$0.81\pm 0.01$	$0.81\pm 0.01$	$\Leftarrow$	$19.62$
cifar100	$1.00\pm 0.00$	$0.99\pm 0.00$	$0.25\pm 0.00$	$0.32\pm 0.01$	$0.27\pm 0.00$	$=$	$1.00$
cle4evr	$1.00\pm 0.00$	$1.00\pm 0.00$	$1.00\pm 0.00$	$1.00\pm 0.00$	$1.00\pm 0.00$	$=$	$1.00$
fashion	$1.00\pm 0.00$	$0.98\pm 0.00$	$0.92\pm 0.00$	$0.92\pm 0.00$	$0.91\pm 0.00$	$=$	$1.00$
kand-logic	$0.84\pm 0.07$	$0.62\pm 0.00$	$0.47\pm 0.01$	$0.44\pm 0.00$	$0.41\pm 0.01$	unknown	–
kand-logic-2	$0.85\pm 0.04$	$0.72\pm 0.01$	$0.61\pm 0.01$	$0.58\pm 0.02$	$0.57\pm 0.02$	$\parallel$	$0.19$

Appendix

Table 28: SPL results for non detailed prompt using qwen3-8b formulas. The table reports consistency, accuracy, precision, F1, Rel , and MC-R . Mean

\pm

std over 5 seeds.

Model	Task	Category	Reason ( CPMpy + CoT , non-detailed prompt)
gpt-oss-120b	bdd-oia	formula degenerate	5 of 25 task variables are missing
gpt-oss-120b	cebab	no formula produced	no CNF generated
olmo3-32b-think	bdd-oia	formula degenerate	6 of 25 task variables are missing
olmo3-32b-think	bdd-oia-2	formula degenerate	1 of 11 task variables is missing
olmo3-32b-think	warcraft	formula degenerate	UNSAT (0 models)
olmo3-32b-think	cebab	no formula produced	no CNF generated

Appendix

Table 29: Missing results in Table 25 , CPMpy + CoT with non-detailed prompts.

	Unconstrained			G-T					gpt-oss-120b
Task	F1 $(\uparrow)$	Rec $(\uparrow)$	Cons $(\uparrow)$	$\Delta$ F1	$\Delta$ Rec	$\Delta$ Cons	Rel	MC-R	$\Delta$ F1	$\Delta$ Rec	$\Delta$ Cons	Rel	MC-R
bdd-oia	$0.58$	$0.58$	$0.90$	$-0.00$	$+0.01$	$+0.02$	$=$	$1.00$	$+0.01$	$+0.02$	$+0.01$	$=$	$1.00$
bdd-oia-2	$0.73$	$0.71$	$0.92$	$-0.00$	$+0.00$	$+0.02$	$=$	$1.00$	$+0.00$	$+0.01$	$+0.00$	$=$	$1.00$
cebab	$0.46$	$0.46$	$0.63$	$+0.00$	$+0.00$	$+0.13$	$=$	$1.00$	$+0.01$	$+0.01$	$+0.17$	$=$	$1.00$
chx	$0.57$	$0.53$	$0.91$	$-0.00$	$+0.00$	$+0.07$	$=$	$1.00$	$-0.02$	$-0.02$	$+0.05$	$=$	$1.00$
cifar10	$0.87$	$0.86$	$0.94$	$-0.02$	$-0.01$	$+0.05$	$=$	$1.00$	$-0.02$	$-0.01$	$+0.05$	$=$	$1.00$

Appendix

Table 30: Downstream SL performance using generated formulas, when available, is comparable to that of expert-provided formulas on auto-nesy-bench . Semantic loss mainly improves consistency in almost all cases compared with an unconstrained baseline. The top table reports SL with the ground-truth ( G-T ) and gpt-oss-120b formulas, the bottom one with the olmo3-32b-think and qwen3-8b formulas against the unconstrained baseline. In both, the first group (Unconstrained) is the same backbone and classifier trained without the semantic loss, for which we report F1, Recall ( Rec ) and consistency ( Cons , the fraction of test predictions that satisfy the ground-truth formula); every other group reports

\Delta

F1 /

\Delta

Rec /

\Delta

Cons of SL relative to Unconstrained (positive is better). Standard deviations across

5

seeds are omitted (

\leq 0.02

for F1 and Rec on all tasks except sudoku , warcraft , mn-mul-bin and chx ); the full results, with standard deviations and all metrics, are attached below for reference. Rel denotes the relationship between the predicted and ground-truth formulas: equal (

=

), strict (

\Rightarrow

), permissive (

\Leftarrow

), or incomparable (

\parallel

), indicating whether the predicted formula satisfying assignments are equal to, a subset of, a superset of, or neither relative to the ground truth. MC-R measures the ratio of the number of satisfying assignments of the predicted formula to that of the ground-truth formula. Missing cells indicate the errors in the formula generation, formatting or during inference. Details about the missing results is provided in Table 24 .

Task	Consistency $(\uparrow)$	Accuracy $(\uparrow)$	Precision $(\uparrow)$	Recall $(\uparrow)$	F1 $(\uparrow)$
bdd-oia	$0.90\pm 0.00$	$0.78\pm 0.00$	$0.59\pm 0.01$	$0.58\pm 0.01$	$0.58\pm 0.00$
bdd-oia-2	$0.92\pm 0.00$	$0.75\pm 0.00$	$0.76\pm 0.00$	$0.71\pm 0.01$	$0.73\pm 0.01$
cebab	$0.63\pm 0.03$	$0.64\pm 0.01$	$0.48\pm 0.01$	$0.46\pm 0.02$	$0.46\pm 0.01$
chx	$0.91\pm 0.01$	$0.69\pm 0.01$	$0.68\pm 0.04$	$0.53\pm 0.02$	$0.57\pm 0.02$
cifar10	$0.94\pm 0.00$	$0.96\pm 0.00$	$0.89\pm 0.00$	$0.86\pm 0.00$	$0.87\pm 0.00$
cifar100	$0.63\pm 0.00$	$0.99\pm 0.00$	$0.66\pm 0.00$	$0.45\pm 0.01$	$0.52\pm 0.00$

Appendix

Table 31: Unconstrained model . The table reports consistency, accuracy, precision and F1. Mean

\pm

std over 5 seeds.

Task	Consistency $(\uparrow)$	Accuracy $(\uparrow)$	Precision $(\uparrow)$	Recall $(\uparrow)$	F1 $(\uparrow)$	Rel	MC-R
bdd-oia	$0.92\pm 0.00$	$0.78\pm 0.00$	$0.59\pm 0.01$	$0.58\pm 0.01$	$0.58\pm 0.00$	$=$	$1.00$
bdd-oia-2	$0.94\pm 0.01$	$0.75\pm 0.01$	$0.75\pm 0.01$	$0.71\pm 0.01$	$0.73\pm 0.01$	$=$	$1.00$
cebab	$0.77\pm 0.02$	$0.64\pm 0.01$	$0.48\pm 0.01$	$0.47\pm 0.02$	$0.47\pm 0.01$	$=$	$1.00$
chx	$0.97\pm 0.01$	$0.69\pm 0.01$	$0.68\pm 0.02$	$0.54\pm 0.03$	$0.57\pm 0.03$	$=$	$1.00$
cifar10	$0.99\pm 0.00$	$0.95\pm 0.00$	$0.86\pm 0.00$	$0.84\pm 0.01$	$0.85\pm 0.00$	$=$	$1.00$
cifar100	$0.70\pm 0.00$	$0.99\pm 0.00$	$0.64\pm 0.00$	$0.47\pm 0.00$	$0.53\pm 0.00$	$=$	$1.00$

Appendix

Table 32: SL logical consistency and downstream metrics with the Ground-Truth formula . The table reports consistency, accuracy, precision, F1, Rel , and MC-R . Mean

\pm

std over 5 seeds. Rel and MC-R are trivially

=

1.00

Task	Consistency $(\uparrow)$	Accuracy $(\uparrow)$	Precision $(\uparrow)$	Recall $(\uparrow)$	F1 $(\uparrow)$	Rel	MC-R
bdd-oia	$0.91\pm 0.01$	$0.78\pm 0.00$	$0.59\pm 0.00$	$0.60\pm 0.01$	$0.59\pm 0.01$	$=$	$1.00$
bdd-oia-2	$0.92\pm 0.01$	$0.75\pm 0.00$	$0.75\pm 0.00$	$0.72\pm 0.01$	$0.73\pm 0.00$	$=$	$1.00$
cebab	$0.80\pm 0.02$	$0.64\pm 0.01$	$0.48\pm 0.01$	$0.47\pm 0.02$	$0.47\pm 0.01$	$=$	$1.00$
chx	$0.96\pm 0.01$	$0.68\pm 0.01$	$0.65\pm 0.04$	$0.52\pm 0.01$	$0.55\pm 0.01$	$=$	$1.00$
cifar10	$0.99\pm 0.00$	$0.95\pm 0.00$	$0.86\pm 0.00$	$0.85\pm 0.01$	$0.85\pm 0.01$	$=$	$1.00$
cifar100	$0.72\pm 0.01$	$0.99\pm 0.00$	$0.62\pm 0.00$	$0.47\pm 0.00$	$0.53\pm 0.00$	$=$	$1.00$

Appendix

Table 33: SL logical consistency and exact LLM-formula-vs-oracle relationship for the gpt-oss-120b formulas . The table reports consistency, accuracy, precision, F1, Rel , and MC-R . Mean

\pm

std over 5 seeds.

Task	Consistency $(\uparrow)$	Accuracy $(\uparrow)$	Precision $(\uparrow)$	Recall $(\uparrow)$	F1 $(\uparrow)$	Rel	MC-R
bdd-oia-2	$0.94\pm 0.00$	$0.75\pm 0.00$	$0.75\pm 0.00$	$0.71\pm 0.01$	$0.73\pm 0.00$	$=$	$1.00$
cebab	$0.74\pm 0.02$	$0.66\pm 0.01$	$0.49\pm 0.01$	$0.48\pm 0.02$	$0.48\pm 0.02$	$=$	$1.00$
cifar10	$0.99\pm 0.00$	$0.95\pm 0.00$	$0.86\pm 0.01$	$0.85\pm 0.00$	$0.85\pm 0.01$	$=$	$1.00$
cifar100	$0.72\pm 0.02$	$0.99\pm 0.00$	$0.61\pm 0.01$	$0.47\pm 0.01$	$0.52\pm 0.01$	$=$	$1.00$
cle4evr	$1.00\pm 0.00$	$1.00\pm 0.00$	$1.00\pm 0.00$	$1.00\pm 0.00$	$1.00\pm 0.00$	$=$	$1.00$
fashion	$1.00\pm 0.00$	$0.98\pm 0.00$	$0.92\pm 0.00$	$0.92\pm 0.00$	$0.92\pm 0.00$	$=$	$1.00$

Appendix

Table 34: SL logical consistency and exact LLM-formula-vs-oracle relationship for the olmo3-32b-think formulas . The table reports consistency, accuracy, precision, F1, Rel , and MC-R . Mean

\pm

std over 5 seeds.

Task	Consistency $(\uparrow)$	Accuracy $(\uparrow)$	Precision $(\uparrow)$	Recall $(\uparrow)$	F1 $(\uparrow)$	Rel	MC-R
bdd-oia	$0.94\pm 0.01$	$0.78\pm 0.00$	$0.59\pm 0.01$	$0.60\pm 0.01$	$0.59\pm 0.00$	$=$	$1.00$
cifar10	$0.99\pm 0.00$	$0.96\pm 0.00$	$0.87\pm 0.00$	$0.86\pm 0.00$	$0.86\pm 0.00$	$=$	$1.00$
cifar100	$0.73\pm 0.00$	$0.99\pm 0.00$	$0.63\pm 0.00$	$0.49\pm 0.00$	$0.54\pm 0.00$	$=$	$1.00$
cle4evr	$1.00\pm 0.00$	$1.00\pm 0.00$	$1.00\pm 0.00$	$1.00\pm 0.00$	$1.00\pm 0.00$	$=$	$1.00$
fashion	$1.00\pm 0.00$	$0.98\pm 0.00$	$0.92\pm 0.00$	$0.92\pm 0.00$	$0.92\pm 0.00$	$=$	$1.00$
kand-logic-2	$0.42\pm 0.15$	$0.83\pm 0.01$	$0.76\pm 0.01$	$0.75\pm 0.01$	$0.75\pm 0.01$	$\Rightarrow$	$0.02$

Appendix

Table 35: SL logical consistency and exact LLM-formula-vs-oracle relationship for the qwen3-8b formulas . The table reports consistency, accuracy, precision, F1, Rel , and MC-R . Mean

\pm

std over 5 seeds.

	Unconstrained			G-T					gpt-oss-120b
Task	F1 $(\uparrow)$	Rec $(\uparrow)$	Cons $(\uparrow)$	$\Delta$ F1	$\Delta$ Rec	$\Delta$ Cons	Rel	MC-R	$\Delta$ F1	$\Delta$ Rec	$\Delta$ Cons	Rel	MC-R
bdd-oia	$0.58$	$0.58$	$0.90$	$-0.00$	$+0.01$	$+0.02$	$=$	$1.00$	–	–	–	–	–
bdd-oia-2	$0.73$	$0.71$	$0.92$	$-0.00$	$+0.00$	$+0.02$	$=$	$1.00$	$-0.01$	$-0.02$	$-0.02$	$\parallel$	$1.00$
cebab	$0.46$	$0.46$	$0.63$	$+0.00$	$+0.00$	$+0.13$	$=$	$1.00$	–	–	–	–	–
chx	$0.57$	$0.53$	$0.91$	$-0.00$	$+0.00$	$+0.07$	$=$	$1.00$	$-0.21$	$-0.14$	$-0.17$	$\Rightarrow$	$0.94$
cifar10	$0.87$	$0.86$	$0.94$	$-0.02$	$-0.01$	$+0.05$	$=$	$1.00$	$-0.20$	$-0.17$	$-0.22$	$\parallel$	$3.38$

Appendix

Table 36: With non-detailed prompts, SL benefits from correct formulas, while non-equivalent constraints degrade logical consistency. Formulas are generated with CPMpy + CoT from non-detailed prompts; the setup is identical to Table 30 . The top table reports SL with the ground-truth ( G-T ) and gpt-oss-120b formulas, the bottom one with the olmo3-32b-think and qwen3-8b generated formulas. For the Unconstrained we report F1, Recall ( Rec ) and consistency ( Cons , the fraction of predictions that satisfy the ground-truth formula); every other method reports

\Delta

F1 /

\Delta

Rec /

\Delta

Cons of SL relative to Unconstrained . Standard deviations across

5

seeds are omitted. Full results are reported in Appendix I . Rel denotes the relationship between the predicted and ground-truth formulas: equal (

=

), strict (

\Rightarrow

), permissive (

\Leftarrow

), or incomparable (

\parallel

), indicating whether the predicted formula satisfying assignments are equal to, a subset of, a superset of, or neither relative to the ground truth; unknown indicates cases where the model count did not terminate. MC-R measures the ratio of the number of satisfying assignments of the predicted formula to that of the ground-truth formula. Missing cells indicate a degenerate or no formula, as for SPL (see Table 29 for the full explanation).

Task	Consistency $(\uparrow)$	Accuracy $(\uparrow)$	Precision $(\uparrow)$	Recall $(\uparrow)$	F1 $(\uparrow)$	Rel	MC-R
chx	$0.86\pm 0.10$	$0.43\pm 0.01$	$0.30\pm 0.11$	$0.26\pm 0.01$	$0.16\pm 0.02$	–	–
cifar10	$0.96\pm 0.00$	$0.96\pm 0.00$	$0.87\pm 0.00$	$0.87\pm 0.00$	$0.87\pm 0.00$	$\Leftarrow$	$19.62$
cifar100	$0.73\pm 0.00$	$0.99\pm 0.00$	$0.63\pm 0.00$	$0.49\pm 0.00$	$0.54\pm 0.00$	$=$	$1.00$
cle4evr	$1.00\pm 0.00$	$1.00\pm 0.00$	$1.00\pm 0.00$	$1.00\pm 0.00$	$1.00\pm 0.00$	$=$	$1.00$
fashion	$0.99\pm 0.00$	$0.98\pm 0.00$	$0.92\pm 0.00$	$0.91\pm 0.00$	$0.92\pm 0.00$	$=$	$1.00$
kand-logic	$0.17\pm 0.02$	$0.80\pm 0.01$	$0.75\pm 0.01$	$0.70\pm 0.01$	$0.70\pm 0.01$	unknown	–

Appendix

Table 37: SL results with qwen3-8b generated formulas using CPMpy output, CoT and detailed prompt . The table reports consistency, accuracy, precision, F1, Rel , and MC-R . Mean

\pm

std over 5 seeds.

Task	Consistency $(\uparrow)$	Accuracy $(\uparrow)$	Precision $(\uparrow)$	Recall $(\uparrow)$	F1 $(\uparrow)$	Rel	MC-R
chx	$0.02\pm 0.01$	$0.53\pm 0.02$	$0.62\pm 0.02$	$0.53\pm 0.01$	$0.48\pm 0.01$	$\parallel$	$1.00$
cifar10	$0.97\pm 0.00$	$0.96\pm 0.00$	$0.87\pm 0.00$	$0.86\pm 0.01$	$0.86\pm 0.01$	$\Leftarrow$	$19.25$
cifar100	$0.72\pm 0.01$	$0.99\pm 0.00$	$0.61\pm 0.01$	$0.47\pm 0.00$	$0.52\pm 0.00$	$=$	$1.00$
cle4evr	$1.00\pm 0.00$	$1.00\pm 0.00$	$1.00\pm 0.00$	$1.00\pm 0.00$	$1.00\pm 0.00$	$=$	$1.00$
fashion	$1.00\pm 0.00$	$0.98\pm 0.00$	$0.92\pm 0.00$	$0.92\pm 0.00$	$0.92\pm 0.00$	$=$	$1.00$
kand-logic-2	$0.36\pm 0.01$	$0.81\pm 0.00$	$0.72\pm 0.01$	$0.69\pm 0.01$	$0.70\pm 0.01$	$\Rightarrow$	$0.02$

Appendix

Table 38: SL results with olmo-32b-think generated formulas using CPMpy output, CoT and detailed prompt . The table reports consistency, accuracy, precision, F1, Rel , and MC-R . Mean

\pm

std over 5 seeds.

Task	Consistency $(\uparrow)$	Accuracy $(\uparrow)$	Precision $(\uparrow)$	Recall $(\uparrow)$	F1 $(\uparrow)$	Rel	MC-R
bdd-oia-simple	$0.91\pm 0.02$	$0.74\pm 0.00$	$0.75\pm 0.00$	$0.69\pm 0.01$	$0.72\pm 0.00$	$\parallel$	$1.00$
chx	$0.74\pm 0.10$	$0.45\pm 0.02$	$0.48\pm 0.11$	$0.39\pm 0.02$	$0.36\pm 0.03$	$\Rightarrow$	$0.94$
cifar10	$0.73\pm 0.09$	$0.91\pm 0.01$	$0.83\pm 0.02$	$0.68\pm 0.01$	$0.67\pm 0.02$	$\parallel$	$3.38$
cifar100	$0.72\pm 0.01$	$0.99\pm 0.00$	$0.62\pm 0.00$	$0.48\pm 0.00$	$0.53\pm 0.00$	$=$	$1.00$
cle4evr	$0.99\pm 0.02$	$0.99\pm 0.02$	$0.99\pm 0.02$	$0.99\pm 0.03$	$0.99\pm 0.03$	$=$	$1.00$
fashion-	$1.00\pm 0.00$	$0.98\pm 0.00$	$0.92\pm 0.00$	$0.92\pm 0.00$	$0.92\pm 0.00$	$=$	$1.00$

Appendix

Table 39: SL results with gpt-oss-120b generated formulas using CPMpy output, CoT and detailed prompt . The table reports consistency, accuracy, precision, F1, Rel , and MC-R . Mean

\pm

std over 5 seeds.

Explore similar work

Neuro-Symbolic Synergy for World Modeling
Feb 11, 2026Hongyu Zhao, Siyu Zhou, Haolin Yang +2Neuro-Symbolic Framework LLM Reasoning Strategies
Department of Computer Science University of Maryland College Park, MD 20742, USA · Faculty of Engineering and IT Australian AI Institute University of Technology Sydney Sydney, Australia · Department of Statistics University of Chicago Chicago, IL 60637, USA +2
EM-NeSy: Expectation Maximization for Neurosymbolic Learning
Jun 12, 2026Annegret Seibt, Luc De Raedt, Giuseppe MarraNeuro-Symbolic Framework Expectation-Maximization
Department of Computer Science KU Leuven
LLM-Flax : Generalizable Robotic Task Planning via Neuro-Symbolic Approaches with Large Language Models
Apr 29, 2026Seongmin Kim, Daegyu LeeLarge Language Model Planning Classical Planning
Department of Physical AI Engineering, Jeonbuk National University(JBNU) · Faculty of Department of Advanced Defense Technology and Industry, Jeonbuk National University(JBNU)

Feb 11, 2026, cs.CLJ/K move · Enter open · S save

Neuro-Symbolic Synergy for World Modeling

Hongyu Zhao, Siyu Zhou, Haolin Yang, Zengyi Qin+1

Department of Computer Science University of Maryland College Park, MD 20742, USA · Faculty of Engineering and IT Australian AI Institute University of Technology Sydney Sydney, Australia · Department of Statistics University of Chicago Chicago, IL 60637, USA+2

Neuro-Symbolic Framework LLM Reasoning Strategies World Models Reasoning Skills Prior Knowledge Integration

Open paper AskPDF arXiv

Large language models (LLMs) exhibit strong general-purpose reasoning capabilities, yet they frequently hallucinate when used as world models (WMs), where strict compliance with deterministic transition rules--particularly in corner cases--is essential. In contrast, Symbolic WMs provide logical consistency but lack semantic expressivity. To bridge this gap, we propose Neuro-Symbolic Synergy (NeSyS), a framework that integrates the probabilistic semantic priors of LLMs with executable symbolic rules to achieve both expressivity and robustness. NeSyS alternates training between the two models using trajectories inadequately explained by the other. Unlike rule-based prompting, the symbolic WM contributes candidate-level scores through log-linear reranking, without requiring the LLM to interpret rule text. Rule-guided sampling prioritizes transitions that are weakly covered by symbolic rules, using 35--60% of the training pairs while outperforming full-data supervised fine-tuning in five of six settings. Experiments on ScienceWorld, WebShop, and PlanCraft demonstrate consistent gains in WM prediction accuracy and data efficiency; one-step lookahead on open-ended WebShop also improves agent reward. Our models, rules, and code are available at https://github.com/tianyi-lab/NeSyS.

Abstract

Explore similar work

Neuro-Symbolic Synergy for World Modeling

EM-NeSy: Expectation Maximization for Neurosymbolic Learning

LLM-Flax : Generalizable Robotic Task Planning via Neuro-Symbolic Approaches with Large Language Models