Verification Learning: Make Unsupervised Neuro-Symbolic System Feasible
Authors: Lin-Han Jia
Wen-Chao Hu
Jie-Jing Shao
Lan-Zhe Guo
Yu-Feng Li
Venue: ICML 2025 poster (2025)
Keywords: Neural Symbolic Learning
Primary area: general_machine_learning->unsupervised_and_semisupervised_learning

Abstract: The current Neuro-Symbolic (NeSy) Learning paradigm suffers from an over-reliance on labeled data, so if we completely disregard labels, it leads to less symbol information, a larger solution space, and more shortcuts—issues that current Nesy systems cannot resolve. This paper introduces a novel learning paradigm, Verification Learning (VL), which addresses this challenge by transforming the label-based reasoning process in Nesy into a label-free verification process. VL achieves excellent learning results solely by relying on unlabeled data and a function that verifies whether the current predictions conform to the rules. We formalize this problem as a Constraint Optimization Problem (COP) and propose a Dynamic Combinatorial Sorting (DCS) algorithm that accelerates the solution by reducing verification attempts, effectively lowering computational costs and introduce a prior alignment method to address potential shortcuts. Our theoretical analysis points out which tasks in Nesy systems can be completed without labels and explains why rules can replace infinite labels for some tasks, while for others the rules have no effect. We validate the proposed framework through several fully unsupervised tasks including addition, sort, match, and chess, each showing significant performance and efficiency improvements.

Lan-Zhe Verification Learning:
Make Unsupervised Neuro-Symbolic System Feasible
Lin-Han Jia
Wen-Chao Hu"
Jie-Jing Shao
Lan-Zhe Guo Yu-Feng Li
Abstract
experience-based responses to simple tasks, while System 2 (deliberative processing) engages slow, knowledge-intent intensive reasoning for complex ones. This cognitive architecture mir- rors the dichotomy in artificial intelligence (AI) between data-driven and rule-driven learning paradigms. In the past, rule-driven symbolic learning systems were less favored compared data-driven neural learning systems due to their high maintenance and search costs. However, with the continuous iteration of neural network models, they still per- form poorly on reasoning tasks. Consequently, an increasing number of research efforts are now focused on Nesy systems capable of integrating data-driven and rule-driven methods.
The current Neuro-Symbolic (NeSy) Learning paradigm suffers from an over-reliance on la- beled data, so if we completely disregard labels, it leads to less symbol information, a larger so- lution space, and more shortcuts-issues that cur- rent Nesy systems cannot resolve. This paper in- troduces novel learning paradigm, Verification Learning (VL), which addresses this challenge by transforming the label-based reasoning process in Nesy into a label-free verification process. VL achieves excellent learning results solely by rely- ing on unlabeled data and function that verifies whether the current predictions conform to the rules. We formalize this problem Constraint Optimization Problem (COP) and propose Dy- namic Combinatorial Sorting (DCS) algorithm that accelerates the solution by reducing verifica- tion attempts, effectively lowering computational costs and introduce a prior aligmment method to address potential shortcuts. Our theoretical analy- sis points out which tasks in Nesy systems can be completed without labels and explains why rules can replace infinite labels for some tasks, while for others the rules have no effect. We validate the proposed framework through several fully un- supervised tasks including addition, sort, match, and chess, each showing significant performance and efficiency improvements.
In the Nesy paradigm, a machine learning model f estab- lishes mapping between inputs X and symbolic represen- tations S, i.e., S = S(X). Then, using a knowledge base K B and S, to infer the label Y, i.e., KB, S } Y. S is unknown and needs to be predicted based on both X and Y, ensuring consistency between the learning and reason- ing processes. While the goal to leverage knowledge to reduce reliance on labeled data, the real-world application of Nesy remains limited. For simple tasks, good results can be achieved without a symbolic system. For complex tasks, the required data grows exponentially but most current Nesy algorithms still require labels Y of the same scale as the in- put data X which are expensive to acquire. Therefore, there is an urgent need to develop unsupervised Nesy systems.
The difficulty in bridging the gap between supervised Nesy and unsupervised Nesy remains significant which can be seen in Figure 1. Firstly, the unsupervised paradigm lacks critical information compared to the supervised paradigm. Much of the performance improvement seen in current Nesy al algorithms comes from label leakage (Chang et al., 2020). For example, in the common task of handwritten digit ad- dition (Manhaeve et al., 2018), providing labels Y for the equations Ø
1. Introduction
Human cognition operates through a dual-system frame- work:
System (intuitive processing) enables rapid,
+ a = 0) and + = 18) effectively leaks the symbolic labels and 9, further propagated to other labels, essentially supervising the learning of X di- rectly. Secondly, the lack of labels drastically increases the search space for problem-solving, For example. transform- ing the problem changes the search space from 102 to 10 and when labels are available, one can further restrict the search to solutions
'National Key Laboratory for Novel Software Technology, Nanjing University, Nanjing, China "School of Artificial Intelli- gence, Nanjing University, Nanjing, China "School of Intelligence Science and Technology, Nanjing University. Nanjing, China. Cor- respondence to: Yu- Yu-Feng Guo <guolz@ @ mwj.aannu.duucn......
9 + 9
18) to +
&
Proceedings of the 4nnd International Conference Machine Learning. Vancouver, Canada. PMLR 267, 2025. Copyright 2025 by the author(s).

---

Verification Learning: Make Unsupervised Neuro-Symbolic System Feasible
where y = 18. Finally, the absence of labels leads a sig- nificant increase in the shorteuts problem in Nesy tasks. For example, in the equation
learning process corresponds Constraint Optimization Problem (COP), where the objective is to find the solution that maximizes the optimization score among all feasible solutions that satisfy the constraints. If the verification of solutions requires exhaustively traversing the entire solution space, this becomes computationally expensive. However, if we can sort the solutions in the solution space accord- ing to their scores and verify them in order dynamically, we can ensure that the first valid solution we verify is the optimal one. Initially, this sorting process had exponential complexity, but we introduced an algorithm called Dynamic Combinatorial Sorting (DCS), which is an extension of (Jia et al., 2025). This algorithm maintains a heap structure with low computational overhead, dynamically tracking the solution with the highest optimization goal value among unverified solutions. By doing so, we guarantee that the first valid solution we verify is the optimal one, thus reducing the COP problem's complexity to a similar level as the CSP. Initially, we implemented DCS under the assumption of independence and later extended it to handle some cases where independence does not hold but monotonicity holds, making it still applicable. This reveals that, Nesy, mono- tonicity is a more relaxed yet crucial property compared to independence.
1 + o 17). the only shortcut every other
is (8 + 9 = 17), while for equation that satisfies the addition rule like (0 + 0 = 00) forms shortcut.
Input
Imput
X
4
x
X
Knowlecige Base
Knowlodge Base
Less information Larger symbol space More shortcuts
Supervised Neuro Symbolic System
Unsupervised Neuro Symbolic System
Output S,
Output 5,
5
S;
5
S,
Figure 1. This example illustrates the differences between unsuper- vised and supervised neuro-symbolic systems in the addition task. It highlights that unsupervised neuro-symbolic systems exhibit broader applicability but also pose greater lcarning challenges.
Additionally, we propose a distribution alignment method to mitigate the severe shortcut and collapse problems caused by the excessive number of feasible solutions in the unsu- pervised setting. By leveraging the natural distribution of symbolic systems, this algorithm adjusts the output distribu- tion of the machine learning model, providing the necessary self-correction capability during training.
Due to the aforementioned issues, applying previous ap- proaches for unsupervised Nesy is largely infeasible. To address these problems, we propose a new paradigm called Verification Learning (VL). In the VL paradigm, the model's entire learning process (illustrated in Figure 2) can be com- pleted using only unlabeled data and knowledge-base based verification function. In the unsupervised setting, where a knowledge module cannot perform reasoning starting from the label Y. we instead replace the reasoning process with a constraint satisfaction verification on S drawn from the solution space. Using satisfiability verification instead of logical reasoning not only resolves the problem of a lack of starting points, but also bypasses challenges inherent in logical reasoning, such as incompleteness, infinite recursion, and high computational complexity. Additionally, this ap- proach is not tied to a specific logical form, allowing more general verification functions to replace the complex logic programming. Moreover, because it does not depend on label Y, the VL paradigm supports test time corrections, ensuring that the solutions output by the model conform to the specified constraints.
We also established an effective theoretical framework for unsupervised Nesy, proving that if the model's output sym- bolic distribution aligns with the natural distribution, the worst-case performance of unsupervised Nesy depends on the number of single-point orbits after performing the sym- metry group decomposition of the rule base. The average performance is determined by the size of each orbit corre- sponding to symbols. This theory also reveals that if two symbols are not completely equivalent in their role within the knowledge base, they can be distinguished under suffi- cient unlabeled data and optimization ultimately.
We conducted experiments on four rule-based tasks with- out labels, and made groundbreaking progress. We were able to: identify the numbers in addition expressions based solely on the addition rule (Manhaeve et al., 2018); rec- ognize numbers in ordered sequences based solely on the sort rule (Winters et al., 2022); identify characters in strings based solely on the string match rule (Dai et al., 2019); and identify chess pieces on chessboard based solely on the chess rule. The experimental results demonstrate the outstanding performance and efficiency of the VL paradigm.
In the problen-solving process, our goal is to identify the symbolic labels that maximize the alignment between the knowledge base and the machine learning predictions. VL's
2

---

Verification Learning: Make Unsupervised Neuro-Symbolic System Feasible
Candidate Symbol
Unlabeled Samples
Machine Learning Model
Combinations Dynamically
Knowledge-Base Based Verification Function
Ranked Based on Scores
Falsc
$
False
X2
$2
V KB
$
False
S4
True
The first combination that passes verification is used as supervision update the model.
Figure 2. This example illustrates how verification lcarning can complete the entire model training process using only unlabeled data and knowledge-based verification function.
2. Related Works
doku problems (Chang et al., 2020), where the model could directly determine symbolic labels S without relying on the input X, instead using only the labels Y. After eliminating this leakage, SATNet's performance completely failed, even dropping to 0%. We've found that this phenomenon is widespread in Nesy tasks. This reveals a situation in many tasks where the answer can be obtained without learning, significantly lowering the task's ' difficulty and failing to accurately reflect the system's 's ability to inte- grate the two components.
2.1. Neuro-Symbolic Learning
Research on Nesy can generally be classified into three types (Yu et al., 2023): Reasoning to learning, which fo- cuses on constructing network architectures (Mao et al., 2019) or loss functions based on rules, emphasizing the mapping from X S; Learning to reasoning, where learn- ing methods are employed to identify reasoning paths (Mao et al., 2019) accelerate the search process (Wang et al., 2018), focusing on the reasoning from S to Y; Learning- reasoning: which emphasizes the interaction between the two components and where S is unknown and needs to be obtained based on both X and Y, ensuring consistency between the learning and reasoning processes (Xu et al., 2018; Stammer et al., 2023; Petersen et al., 2021). Deep- Problog introduces probabilistic reasoning by incorporating probabilities predicted by neural networks into Prolog pro- grams (Manhaeve et al., 2018), while DeepStochlog, based on DeepProlog, uses Stochastic Definite Clause Grammars for stochastic reasoning (Winters et al., 2022). NeurASP, on the other hand, uses Answer Set Programming as the knowledge hase (Yang et al., 2023). Among the above meth- ods, all tend toward probabilistic reasoning. In contrast, abductive learning (ABL), as an important branch, is dedi- cated to inferring a definite symbol S from Y. ensuring that S aligns with the neural network's predictions (Dai et al., 2019; Huang et al., 2021; 2020; He et al., 2024; Shao et al., 2025; Jia al., 2025; Hu et al.. 2025b). Ground ABL pre- processes Ground Truth knowledge base based on ABL to avoid using Prolog search (Cai et al., 2021), while A3BL calculations for different candidate symbols S (He et al., 2024).
digit recognition
For the optimization problem of Nesy solving, it often in- volves search problems with exponential complexity. Cur- rently, there are some works that optimize this, such as us- ing gradient-free optimization algorithms (Yu et al., 2016), predicting error locations (Morishita et al., 2023), and de- signing reward-basee search methods using reinforcement learning algorithms (Hu et al., 2025a; Li et al., 2020). How- ever, these optimization algorithms cannot guarantee that the solution found is globally optimal.
Additionally, Nesy faces the issue of shorteuts (Yang et al., 2024; He et al., 2024). Many studies have highlighted that knowledge bases may have multiple satisfying solutions, but fail to accurately pinpoint the target one. However, few works have provided viable solutions address this problem.
Recently, van Krieken et al. (2024) explores the issue of independence in Nesy, pointing out that current Nesy frame- works rely on the assumption of independence. However, in reality, symbols do not satisfy independence always.
computes loss based on confidence-weigee
2.2. Constraint Optimization Problem (COP)
A CSP is defined as a triplet (Variable, Domain, Constraint), where "Variable" refers to a set of decision variables, each with possible values from the set "Domain," " and "Con-
The concept of label leakage was first introduced in the context of SATNet (Wang et al., 2019) solving visual Su-
3

---

Verification Learning: Make Unsupervised Neuro-Symbolic System Feasible
straint" is the rules that must be satisfied by these variables. A COP is represented as (Variable, Domain, Constraint, Ob- jective), and it seeks to find a feasible solution that optimizes an objective function defined over the variables (Fioretto et al., 2018). In a minimization problem, a solution S E COP(V ariable, Domain, Constraint, Objective) if and only if S ε CSP(V CV (VriiVarable, Domain, Constraint),
Here, score(S") represents the probability or weight asso- ciated with S' and the definition of the score varies across different approaches. In DeepProblog and DeepStochlog. the score is the product of the rule probabilities along the reasoning path. In ABI., the score corresponds to the con- sistency distance between f f(X) and S", while in A3BL, it reflects the confidence in g(
Domain, Constraind),
and AT Objective(S) I Objective(T) (Mulamba et al., 2020).
In real-world scenarios. Y generally does not exist and is more often part of the unknown symbolic sequence S. Therefore, in unsupervised Nesy, we must avoid relying on Y as starting point for reasoning. Instead, candidates(S) is directly determined by the knowledge base BB, i.e., K B F candidates(S). This introduces several challenges: 1. It prevents label leakage of Y into S; significantly increases the space of S; 3. More importantly, it leads to overabundance of candidates(S) because of extreme shortcuts, making the process of traversing and scoring all candidate solutions extremely difficult.
3. From Supervised Reasoning to Unsupervised Verification
In the classical Nesy paradigm, the perception module contains learning function that establishes mapping between input X and symbols S. Here, S is a sym- bolic sequence of length 4, i.e., S = [$1...., st]. where 8t E C = fci...., } and s; ~ P. with & representing the size of the symbol space and P representing the natural distribution of the symbols. The entire symbolic sequence space is represented as S = C². The input X may corre- spond to sequence of inputs [æi...., xr]] that match the meaning of the symbols in S, where x; E IR,, and d is the dimensionality of z;. The global input space is X' = Rd4.
In unsupervised settings, the original reasoning process KB }= candidates(S) and the subsequent traversal of candidates(S) to compute scores and select the best so- lution or a weighted sum become computationally pro- hibitive. In practical applications, this makes the system no longer deployable. Therefore, we convert the paradigm of KB + candidates(S) into process of generating new solutions S' and validating whether the current pre- dicted symbolic sequence S' belongs to condidates(S)) Specifically, if S" KB } True, then we can prove that S' E candidates(S).
The perception module f(S[X) E F maps inputs to the symbol space. Here, f corresponds to the conditional distri- bution of the intermediate concepts given the input, where f is in the hypothesis space F C X + S. Additionally, we define ( to represent the model's predicted probability distribution in the symbol space.
This verification paradigm is simpler and more aligned with real-world scenarios for several reasons: 1. It is suitable for unsupervised settings and does not require a known start- ing point Y for reasoning, which also enables verification to support test time corrections when reasoning cannot; 2. Verification does not rely on a complete knowledge base. According to the incompleteness theorem, most real-world symbolic systems (even simple arithmetic systems) are in- complete, meaning there are many true propositions without provable reasoning paths but can be validated as true; 3. Verification guarantees the process is halting, whereas rea- soning cannot guarantee this due to recursions; 4. The computational complexity of validation is typically much lower than that of reasoning. Many NP problems can be val- idated in polynomial time, but finding solution cannot be done yet within polynomial time; 5. Verification is generally more convenient and general at the programming level. It only requires a function VxB S + (True, False), which can replace the entire knowledge base. It is not limited to propositional logic or first-order logic and does not require constructing a search process like in Prolog.
The reasoning module contains a knowledge base K B. From the input symbolic sequence S, we can infer a label Y E y, i.e., K, F Y. Furthermore, us- ing Y and KB, a set of possible candidate solutions for S can also be inferred inversely, i.e., KB,Y Y + condidates(S)
(Si....,5 (a where the ground truth S is guaranteed to be in candidates(S). For any S; E candidates {S). it is shortcut to S.
In the training process of a Nesy system, the input dataset Xtrain [(X1, Yi).... (Xn, Yx)] learns to maintain con- sistency between input and output by learning intermediate symbolic sequences S. We denote the loss function used as L, Methods like DeepProblog, DeepStochlog, and similar approaches minimize the following:
min S'Ecandidatex(S)
Score(S')- (oore(")-L(((X))..)))) L()(
(1)
Alternatively approaches like ABL minimize:
min ((f(X), Sopt)
JEF
With this approach, we bypass the complex processes in- volved with candidates(S). Moreover, due to the exces-
s.t. Sopt = arg st E(andidatea)
max
Score(S')

---

Verification Learning: Make Unsupervised Neuro-Symbolic System Feasible
sive shorteuts in unsupervised settings, methods like Deep- Problog, which find all candidate solutions and weight them, are no longer applicable. Instead, we adopt strategy sim- ilar to ABL, where we select only the highest so- lutions. Our goal now shifts to finding the highest-scoring solution that can be verified, i.c., solving the COP problem COP(S,S, VKB, Score). In the following, we will explore how to solve the COP problem with minimal cost.
is changed to si,j+1, the score for that position score( will change to score(St.+1)), which updates the global score (core(S) by a factor of U; = score((t.3) resents the minimal cost of changing symbol 8i. For the current unverified assignment S, we select the next assign- ment by sorting the successors based on the smallest cost v and iteratively update the assignments. Hence, each as- signment has most I successors, and the successors are ordered. We denote these successors as Suc(S).
score(sL.+1) where v rep-
4. Solve COP by Dynamic Combinatorial Sorting
Under the property of independence, while the greedy rule does not hold (i.e., the (i + 1)ss assignment S is not necessarily the successor of the ith assignment S,), it is always true that S4+1 is successor of one of the preceding assignments. Formally, for any i E k", there exists 1 S S such that S.41 E Suc(S,).
Score) Solving the optimization problem COP(S, S, VKB, Score) requires to find the solution that satisfies the VKB con- straint and has the highest score. Following conventional methods, we would need to verify all possible assignments in the feasible set to determine which solution satisfies the constraint and has the highest score. This exponential time complexity approach is not feasible. Therefore, we propose a strategy that validates solutions in descending order of score in S. By doing so, we ensure that the first solution validated by VK successfully is the optimal one.
Theorem 4.1. When the Score satisfies independence, i.e, Score(S) = -Ta, score(sp), for any >> 1, there exists 0 j<j i, 0 < S 1, < ki such that modifying 8p from the original symbol Sp.q sp.a+1 results in sy, and Suc(S;)p = ($1....,$p-1: Spt, Sptl....,. 81) E Suc(S,)- Furthermore, there does not exist any S' E S such that S' & S,-1) and (core(S") > Score(Suc(S)))) Therefore, S, = Sud(S)
Given that S = [s1...., si] consists of symbols, and con- sidering the global feasible set as a combination of multiple variables, this problem is known as the combinatorial sort- ing problem. Since the size of the feasible set k using classical sorting algorithms would be computationally infea- sible. However, when the score satisfies certain properties, We can infer the (i + 1),, ranked solution based on the top i known solutions. In this way, we only need to know the highest-scoring solution to sequentially derive all other solu- tions, without having to enumerate and sort all of them. This significantly reduces the computational complexity while ensuring that the verification order remains strict, guarantee- ing the global optimality of the COP solution.
This crucial property allows us to maintain a heap structure dynamically, where we track the successors of each verified assignment, keyed by the maximum successor score. This enables us quickly find the assignment with the highest score among all unverified successors of the first assign- ments, ensuring that the assignment ranked i + 1 is selected.
Next, the following process can be used to dynamically find the next assignment to be validated:
1. For i = 1, we select the nighest-scoring assignment for each position in S1, and derive the successors Suc(Si), which are then placed in the heap.
First, we discuss the scenario where the score satisfies in- dependence (van Krieken et al., 2024), and present a com- binatorial sorting solution. We then extend the solution to cases where independence is not satisfied but monotonicity is, which provides more relaxed conditions. This highlights that monotonicity is more crucial property for Nesy tasks, and problems that satisfy monotonicity are just easy to solve as those that satisfy independence.
2. For i > 1, we select the highest-scoring successor from the heap, i.e., the one with the maximum suc- cessor score Sj. and then select the highest-scoring assignment from Suc(S)) to form S,. We then derive the successors Suc(S:). which are then placed in the heap. The successor assignments of Sj are updated to Suc(S,) {S.). and if non-empty, they are placed back in the heap.
4.1. Independent Case
In the case where the score has independence, Score(S)= Il,es score(s;), where score(s;) represents the score of an individual symbol in the symbol combination S, such as the commonly used confidence g(X))... Under the inde- pendence assumption, we sort all possible values for each symbol 5;. This ensures that for each position, the assign- ment with the highest score is selected, When a symbol st.j
By following this process, we ensure that the assignments are verified in strict score order, guaranteeing that the first solution to pass the verification is the optimal solu- tion for the COP problem. If the first valid solution is ranked K, the complexity of maintaining the heap struc- ture is O(K log K), and the total complexity becomes O(K (log K log + k)).
5

---

Verification Learning: Make Unsupervised Neuro-Symbolic System Feasible
4.2. Non-Independent Case
sible. In such cases, strategies like reinforcement learning or other sampling-based methods can be used estimate Score(S). However, these methods no longer guarantee strict order, and thus, cannot ensure the optimal solution to the COP problem.
The selection of the Score function can vary, and affects the performance of VL. Using more diverse optimization objectives often leads to violations of the independence as- sumption. For instance, the consistency score Score(S) =
[i [(X): in (Dai al., 2019) distance cannot be expressed as an independent score.
5. Mitigate Shortcut Problem by Distribution Alignment
We examined whether DCS remains applicable in broader contexts. We found that the fundamental reason for DCS success lies in Theorem 4.1: the + 1-th assignment comes from one of the previous i assignments by modifying only one symbol. If this condition is violated, it means that at least one position has had change in priority between different symbols, thus affecting the global score (core(S). As a sufficient condition, we can guarantee that if the priority between different symbols at the same position satisfies a fixed total ordering. DCS will always find the optimal solution to the COP problem.
After setting up the framework, we can begin learning using unsupervised data and the verification procedure. However, there are significant challenges unsupervised scenarios, particularly due to the shortcut problem. Additionally, dur- ing the initialization phase of the neural network, the predic- tions are often highly biased, leading to situation where the network explores only a few symbols. For example, in an addition task, if all symbols are predicted as 0 (i.c., 0 + 0 = 00), it can pass the verification and also minimize the loss in the learning task to zero in the addition task.
Theorem 4.2. When the Score satisfies monotonicity, i.e.,
To address this, we propose distribution alignment strategy. By aligning the model's output symbol distribution with the natural distribution P of the symbols, we can significantly mitigate this issue. In cases where the natural distribution is unknown, we can use a uniform distribution as a prior. During the initial phase, this ensures that the output distri- bution is spread out. In later stages, even after removing the influence of the prior distribution, the model's output distribution will eventually concentrate on the distribution consistent with the training data. The specific adjustment process is to directly modify the probabilities output by the model to:
for any 0- < p I I and any 0 < q < k, there does not exist a S' such that modifying Sp from Sp.q to sp.++1 results in Sy', and Suc(S"),
(81;.... ........-11p---. ;p-11 ;pth:1 81) E Suc(S'), satisfying Score(Suu(SS )p) > (C))e(("),, then
any i 1, there exists O- < j < i, 0 < P S results in Suc(S,)p = "51....,sp-1.1 Sp
si) E Suc(S,).
Furthermore, there does not exist any S E S such that S' & Si-1) and Score(S')= > Score(Suc((S))) Therefore, S, Su.
Proposition 4.3. Clearly, the satisfaction of independence by Score is a sufficient but not necessary condition for Score to satisfy monotonicity.
1. Po, 9(X)ss g (()):s
(3)
For the consistency distance, symbol s; matches the pre- dicted value f(X); at position i is given higher priority, while the priorities for other symbols remain the same. This satisfies the monotonicity property. Therefore, even with consistency score, combinatorial sorting can still be applied successfully. Furthermore, if we combine multiple Score functions that satisfy monotonicity (e.g., first prioritize the assignments with the highest consistency, then select the ones with the highest confidence), DSC can still achieve the optimal solution the COP problem.
Σx-1 9())
6. Theoretical Study on When Knowledge Can Assist Unsupervised Learning
We performed a theoretical analysis of VL which relies solely on unlabeled data and verification function. The theoretical results demonstrate the upper bounds that Nesy can achieve under the condition of distribution alignment, without requiring supervision. We further analyzed which tasks can be solved without labels and which cannot.
It is worth noting that when monotonicity is not satisfied, even obtaining the top-ranked solution requires exhaustively searching the entire solution space with exponential com- plexity. Therefore, the following theorem holds.
In fact, the theoretical analysis of unsupervised learning can be divided into two parts. The first component is the knowledge-inducee error, which reflects the system's ability to establish correspondence between the categories identi- fied by the learner and the labels of the symbols. The second part is the data-induced error, which reflects the system's 's ability to group samples belonging to the same category together. Together, these two factors determine the upper bound of the generalization error in unsupervised learning.
Theorem 4.4. The monotonicity of the score function is a sufficient and necessary condition for the COP problem to admit a general algorithm with sub-exponential complexity.
If even monotonicity is violated, solving for the optimal (core(S) without traversing all solutions becomes impos-
6

---

Verification Learning: Make Unsupervised Neuro-Symbolic System Feasible
VL effectively addresses both of these issues, with the two modules working together to promote each other's success.
system unless the symbols correspond to the correct values. Thus, all symbols in the addition task are fixed points, and the upper bound error is additionn 0%. This means that with enough data and model improve- ments, we can achieve good results.
6.1. Knowledge-Inducee Error in VL
VL can make the predicted results align with the rule base. So our primary goal is to explore the gap between main- taining consistency with the rule base and being able to distinguish between symbols. This gap is determined by the symmetry of the function VK on the symbol set.
3. Chess Task: is also important to consider cases where a one-way inclusion (not a bijection) occurs. For exam- ple, in a chessboard scenario, a Queen can move along diagonal and straight lines, a Rook along straight lines, and Bishop along diagonals. This leads to situations where Rook or Bishop could be mapped as Queen. In such cases, the task becomes unsolvable because it lacks the necessary bijections. However, the presence of natural distribution P helps correct this issue by ensuring that, the model can distinguish Rooks and Bishops from Queens. So Rchees = 0%. Thus, the dis- tribution P extends the domain of solvable problems, enabling the model to handle more complex tasks that would otherwise be unsolvable.
Let's start with a symbol set S = {s1,...,,5h sk,, and define its symmetry group, (ym(S), which consists of all possible permutations of the set. Any permutation E Sym(S) is bijection ø: S - S. We define G as the symmetry group of the verification function VKB, i.e., the subgroup of Sym(() (S) that keeps the results of VKB invariant. Specifically, for all 5 E S and σ E G. let (S) = (8()))s, have (SB(S) = (SS).
We perform an orbit decomposition of the symmetry group G for the function VKB- For each symbol 8,, its orbit is defined as Os, {s(ss G), which represents all the equivalence symbols that can be reached by applying the symmetries of G to s4-
6.2.
Error in VL
Once the error induced by the task is determined, combining it with the error introduced by the learning process allows us to obtain the upper bound on the generalization error. In unsupervised learning, since it is not possible to distinguish between the symbols in the same orbit, the empirical error should be minimized by selecting the permutation in the symmetry group G. We define R(f) as the current minimal symmetrie permutation empirical error.
If the orbit O., of symbol 8; is a singleton (i.e., Os, = {s; }), then &; is a fixed point of VKB- Therefore, by the orbit decomposition, we can identify the set of fixed points of the verification function VK Fix Os
{s:})-
The musk-induced upper bound error is given by the sum of probabilities of the symbols
that are not fixed points, i.e.,
ΣI(s, T(se & Pi. ,SSS
(4)
R(f) min oEG
Σ xxx)+0(8)) XEX
(6)
The average error is determined by the sum of the ratio of the symbol probabilities to the sizes of their orbits:
By minimizing the permutation error and the task-induced emorr, we can derive the performance bounds for VL in solving unsupervised neural-symbolic learning tasks.
Ps
(5)
1
Theorem 6.1. For any function f E F, if i is a a p-Lipschitz continuous loss function, Rn is the Rademacher complexity for a sample size of n, Riosk is the current task- induced upper bound on error, and R(f)) is the current minimal symmetric permutation empirical error, then the empirical error R(f)) for the prediction of the current symbol set by f satisfies, with at least probability 1 1- ō:
BEES
This error, caused by the task itself, cannot be compensated by data, making it fundamental limitation that cannot be addressed through knowledge verification. To better understand these concepts, consider the following examples:
1. Sudoku Task: In the Sudoku task, any permutation of numbers still satisfies the constraints. This means that all permutations of symbols in Sudoku do not alter the knowledge base. Consequently, the upper bound on task-induced error for Sudoku is Hap = 100%, meaning that regardless of data size or model performance, the fully unsupervised Sudoku task could still have a 0% accuracy.
l2g(2/8) 2n
R() S 2p +3
+
pap
Prask
(7)
7. Experiments
To validate the effectiveness of the framework we proposed, we conducted experiments on 4 unsupervised tasks. These experiments were primarily extensions of previously super- vised Nesy tasks. For all tasks, we used LeNet as the basic
2. Addition Task: In the addition task, no permutation of symbols (such as numbers) can still satisfy the addition
7

---

Verification Learning: Make Unsupervised Neuro-Symbolic System Feasible
Table I. The comparison of symbol recognition accuracy on the Addition dataset.
Method
4
5
8
Deepproblog
53.53
40.42
33.67
29.86
27.51
25.46
23.63
22.52
21.47
DeepStochlog
56.21
44.43
39.06
36.02
34.02
31.14
27.74
24.38
21.24
Se
53.66
36.07
28.39
29.77
14.63
23.25
23.61
22.51
7.63
Ground ABL
42.50
42.00
98.25
26.00
30.25
25.25
25.75
24.00
20.25
A3BL
46.16
99.50
38.00
26.00
30.25
24.50
25.75
24.00
20.25
VL 100.00
41.38
99.50
99.80
99.65
99.19
70.70
98.73
98.28
V
100.00
49.83
100.00
100.00
100.00
100.00
69.20
99.95
100.00
vLg 100.00
99.88
99.75
100.00
99.75
99.00
99.25
97.75
48.80
VITTC
100.00
100.00
100.00
100.00
100.00
99.95
100.00
100.00
51.40
network architecture (denoted as f) for symbol recognition from X to S, with a learning rate of 0.001 and Adam opti- mizer for optimization. Due to the fact that many algorithms train extremely slowly, in order to conduct a performance comparison with them as comprehensively as possible, we set a unified number of epochs to 10. All experiments were completed on 4 A800 GPUs. The comparison methods in- clude Deepproblog, Deepstochlog, NeurASP, Ground ABL, and A3BL. For algorithms that are only suitable for su- pervised learning, we used [True, False], i.e., whether the result matches the knowledge base, as the label for the new tasks to enable comparison. Additionally, we compared the performance of four versions of the algorithm in ablation experiments, including Score settings under the inde- pendent and non-independent hypotheses represented by VL and VL y. to explore the impact of optimization tar- get settings on VL. Under the independent hypothesis, the Score setting used the neural network model's 's confidence, while under the non-independent hypothesis, the Score used combination of consistency and confidence. Furthermore, we compared the impact of using test time correction in both cases and used the tag TTC to indicate them. Our knowledge base is in the form of verification function, and the program was written in simple Python code. During the experiments, NeurASP experienced severe timeouts (no results returned after over 300 hours), and Deepstochlog en- countered memory issues (the table size limit swi-prolog was set 10)2). In the experimental results, these issues were indicated by TLE (Time Limit Exceeded) and MLE (Memory Limit Exceeded), respectively.
Table comparison symbol recognition accuracy on the
Sort dataset.
Method
4
5
6
Deepproblog
96.65
97.12
95.93
39.36
45.97
DeepStochlog
84.27
81.72
77.28
MLE
MLE
NeurASP
5.03
8.95
TLE
TLE
TLE
Ground ABL
10.20
20.22
24.19
29.73
39.35
A3BL
29.75
69.43
49.28
49.61
97.28
VL
77.50
77.20
96.67
68.86
98.23
VLTTC
78.75
76.40
99.67
69.00
99.89
VLy 97.00
98.76
97.97
98.20
98.71
VLTTC 99.25
99.66
99.67
99.78
99.90
Table The comparison symbol recognition accuracy on the
Match dataset.
Method
6
7
8
10
Deepproblog
16.72
14.30
12.33
11.03
10.25
DeepStochlog
16.68
14.28
12.70
26.17
MLE
NeurASP
18.82
14.02
12.20
8.68
TLE
Ground ABL
16.68
14.28
12.35
11.03
10.02
A3BL
16.68
14.28
12.35
11.03
10.02
VL
65.95
42.50
73.97
97.38
96.67
VLTTC
68.20
44.63
72.33
99.85
99.67
VLG 66.27
73.25
98.22
70.35
97.08
VLTTC
68.08
75.72
99.97
81.00
99.68
Table The comparison symbol recognition accuracy on the
Chess dataset.
Method
2
3
4
5
6
7.1. Addition
Deepproblog
49.46
33.10
25.08
49.46
15.66
NeurASP
53.66
36.07
23.93
19.07
18.82
The experiment the Addition task is extension of the addition experiment from Deepproblog, where the answer part was modified to be the input number images. To verify its generalizability, we tested all addition bases between binary and decimal numbers. The results demonstrated the effectiveness of VI. on this task, and showed that with only the addition rule, the model could learn classify all
Ground ABL
49.90
67.65
75.70
70.55
33.95
A3BL
100.00
99.80
75.95
38.30
34.35
VL
100.00
99.90
98.00
95.70
95.15
VLTTC
100.00
99.90
92.55
91.30
92.55
VL
100.00
99.90
98.00
95.70
95.15
VLTTC
100.00
99.90
92.55
91.30
92.55
8

---

Verification Learning: Make Unsupervised Neuro-Symbolic System Feasible
Table 5. The comparison of time consumption on the Addition dataset.
Method
2
3
4
5
6
7
8
9
10
Deepproblog
2778.45
9118.23
15281.67
21273.89
23988.50
30621.92
33400.69
38804.44
42391.21
DeepStochlog
1289.68
454.59
984.16
1251.83
1636.27
1583.25
2168.25
2743.55
3097.91
Ne
1133.23
1475.02
2407.18
2354.81
4169.20
7648.07
13483.66
23013.77
38526.15
Ground ABL
135.05
140.47
141.60
133.90
86.68
131.38
160.69
126.84
123.05
A3BL
187.25
183.92
200.41
203.90
202.73
161.57
184.81
185.87
190.74
VL1 112.04
114.80
111.79
111.94
111.36
109.58
106.66
112.81
116.26
VL
110.48
101.17
80.32
91.05
80.79
111.18
112.27
82.16
118.36
numbers. The results are showed in Table 1.
7.5. Time Consumption
In addition to its excellent performance, VI also demon- strates exceptional time efficiency. We conducted a runtime comparison on the addition dataset, with time measured in seconds. The results show that VI. even outperforms Ground ABL., which has preprocessing of the knowledge base. This is because VL finds the optimal solution with far fewer verification steps. Compared with the training time of some methods that increases rapidly as the symbol space expands, the growth rate of VL's training time relatively slow. The results showed in Table 5.
7.2. Sort
The Sort task is an extension of the sort task from Deep- problog, where digit recognition performed based on an ordered sequence of images. The only knowledge in the knowledge base is the ordering of the numbers. The ex- periments demonstrated that the model, relying solely on the ordering, could successfully perform recognition for all digits. In the experiments, we tested ordered sequences with lengths ranging from 4 to 8, and the results confirmed the effectiveness of VL under the sorting rule. The results are showed in Table 2.
8. Conclusion
7.3. Match
This research explores the feasibility of unsupervised Nesy system from both theoretical and practical perspectives. We demonstrate the necessity of developing unsupervised Nesy systems through practical cases, while highlighting three major challenges: reduced symbolic information availability, expanded solution space, and more prevalent shortcut issues.
The Match task an extension of the anbnen task from Deepstochlog. The task involves character recognition based on fixed model strings in unsupervised setting. The original task only matched the character set a"b"c", but we increased the task difficulty by extending it to situations not limited to three character sets, with n being variable. We conducted experiments with character categories ranging from to 10 and validated the effectiveness of VL in the character matching task. The results are showed in Table
We propose verification learning framework that trans- forms traditional symbolic reasoning starting from super- vision signal Y into a verification paradigm independent of Y. This framework is formalized as a Constraint Opti- mization Problem, for which we prove that can be solved with sub-expone uub-exponential complexity under the condition of in- dependence and the more general condition of monotonicity. We propose a corresponding dynamic combinatorial sorting algorithm for this problem. We also address the exponential growth of shortcuts through distribution alignment.
7.4. Chess
The Chess task comes from (Dai et al., 2019), which is an extension of the 8- Queens problem. In the Chess task, there six types of pieces: the bishop moves diagonally any number of squares, the king moves one square in any direc- tion, the knight moves in an L-shape, the pawn moves one square diagonally forward, the queen moves any number of squares along straight line or diagonally, and the rook moves any number of squares along a straight line. We identify the type of piece based on the changes in the chess- board configuration. Experiments were conducted with 2 to 6 types of chess pieces, with the piece types dynamically added based on the lexicographical order of the piece names. The results are showed in Table 4.
The theoretical foundation establishes the problem types addressable by VL using group theory, accompanied by gen- eralization error analysis. Experimental validation across four unsupervised learning tasks demonstrates breakthrough progress from infeasible to feasible solutions.
Future work will focus on developing more sophisticated VL frameworks for complex tasks and exploring applications in broader unlabeled data scenarios.

---

Verification Learning: Make Unsupervised Neuro-Symbolic System Feasible
Acknowledgements
Huang, Y.-X., Dai, w.-z., Cai, L.-W., Muggleton, S. H., and Jiang, Y. Fast abductive learning by similarity- based con- sistency optimization. In Advances in Neural Information Processing Systems, pp. 26574 -65844, 2021.
This research was supported by the Key Program Jiangsu Science Foundation (BK20243012), Leading-edgee Technol- ogy Program of Jiangsu Science Foundation (BK20232003) and the Fundamental Research Funds for the Central Uni- versities (0221 14380023).
Jia, L.-H., Han, S.-Y., Guo, L.-Z., Zhou, Z., Li, Z.-L., Li, Y.F.,, and Zhou, Z.-H. A smooth transition be- tween induction and deduction: Fast abductive learning based on probabilistic symbol perception. arXiv preprint arXiv:2502. 129129992.1999, 2025.
Impact Statement
This paper presents work whose goal to advance the field of Machine Learning. There are many potential societal consequences of our work, none which feel must be specifically highlighted here.
Li, Q. Huang, S., Hong, Y., Chen, Y., Wu, Y. N., and Zhu, S.-C. Closed loop neural-symbolic learning via integrat- ing neural perception, grammar parsing, and symbolic reasoning. In Proceedings of the 37th International Con- ference on Machine Learning, pp. 5884-888488 2020.
References
Manhaeve, R., Dumancic, S., Kimmig, A., Demeester, T., and De Raedt, L. Deepproblog: Neural probabilistic logic programming. In Advances in Neural Information Processing Systems, pp. 3753-3763, 2018.
Cai, L.-W.. Dai, W.-Z.,, Huang, Y.-.., Li, Y., Muggleton, S. H., and Jiang, Y. Abductive learning with ground knowledge base. In Proceedings of the 30th Interna- tional Joint Conference on Artificial Intelligence, pp- 1815-1821, 2021.
Mao, J., Gan, C., Kohli, P., Tenenbaum, J. B., and Wu, J. The neuro-symbolic concept learner: Interpreting scenes, words, and sentences from natural supervision. In Pro- ceedings of the 7th International Conference on Learning Representations, 2019.
Chang, O., Flokas, L., Lipson, H., and Spranger, M. As- sessing satnet's ability to solve the symbol grounding problem. Advances in Neural Information Processing 2020.
Systems, pp.
Morishita, T., Morio, G., Yamaguchi, A., and Sogawa, Y. Learning deductive reasoning from synthetic corpus based on formal logic. In Proceedings of the 40th Inter- national Conference Machine Learning, pp. 25254- 25274, 2023.
Dai, W.-Z.,, Xu, Q., Yu, Y., and Zhou, Z.-H. Bridging ma- chine learning and logical reasoning by abductive learn- ing. In Advances in Neural Information Processing Sys- tems, pp. 2811-82188 1-222, 2019.
Fioretto, F., Pontelli, E., and Yeoh, W. Distributed con- straint optimization problems and applications: A survey. Journal of Artificial Intelligence Research, 61:623-696 2018.
Mulamba, M., Mandi, J., Canoy, R., and Guns, T. Hybrid classification and reasoning for image-based constraint solving. In Proceedings of the International Conference on Integration of Constraint Programming, Artificial In- telligence, and Operations Research, pp. 364-380, 2020.
He, H.-Y., Sun, H., Xie, Z., and Li, M. Ambiguity-aware abductive learning. In Proceedings of the 41st Inter- national Conference on Machine Learning, pp. 18019- 18042, 2024.
Petersen, F., Borgelt, C., Kuehne, H., and Deussen, O. Learning with algorithmic supervision via continuous relaxations. Advances in Neural Information Processing Systems, 34:16520-16531, 2021.
Hu, W.-C., Dai, W.-Z., Jiang, Y., and Zhou, Z.HH. Efficient rectification of neuro-symbolic reasoning inconsistencies by abductive reflection. In Proceedings of the 39th AAAI Conference on Artificial Intelligence, 2025a.
Shao, J.-J., Hao, H.-R., Yang, X.-W. and Li, Y.-F. Learning for long-horizon planning via neuro-symbolic abductive imitation. Proceedings of the 31stACM SIGKDD Confer- ence on Knowledge Discovery and Data Mining, 2025.
Hu, W.-C., Li, Q.JJ, Jia, L.-H., Ge, C., Li, Y.F.. Jiang, Y., and Zhou, Z.-H. Curriculum abductive learning. arXiv preprint arXiv:2505.1 /2275, 2025b.
Stammer, W., Friedrich, F., Steinmann, D., Brack, M., Shindo, H.,, and Kersting, K. Learning by self-explaining. arXiv preprint arXiv:2309.088 08395, 2023.
Huang, Y.-.,, Dai, W.-Z., Yang, J., Cai, L.-W., Cheng, S., Huang, R., Li, Y.FF, and Zhou, Z.HH. Semi-supervised abductive learning and its application to theft judicial sentencing. In Preceedings of the 20th International Conference on Data Mining, pp. 1070-1075, 2020.
van Krieken, E., Minervini, P., Ponti, E., and Vergari, A. On the independence assumption in neurosymbolic learning. Proceedings of the 41st International Conference on Machine Learning, pp. 49078 49097, 2024.
10

---

Verification Learning: Make Unsupervised Neuro-Symbolic System Feasible
Wang, P.-W., Donti, P., Wilder, B., and Kolter, Z. Satnet: Bridging deep learning and logical reasoning using differentiable satisfiability solver. In Proceedings of the 36th International Conference on Machine Learning, PP. 6545-6554, 2019.
Wang, X., Ye, Y., and Gupta, A. Zero-shot recognition via semantic embeddings and knowledge graphs. In Proceed- ings of the IEEE/CVF Conference on Computer Vision and Puttern Recognition, pp. 6857-6866, 2018.
Winters, T., Marra, G., Manhaeve, R., and De Raedt, L. Deepstochlog: Neural stochastic logic programming. In Proceedings of the 34th AAAI Conference on Artificial Intelligence, pp. 10090-10100, 2022.
Xu, Zhang, Z., Friedman, T., Liang, Y., and Broeck, G. A semantic loss function for deep learning with symbolic knowledge. In Proceedings of the 35th International Conference on Machine Learning, pp. 5502-5511, 2018.
Yang, X.-W., Wei, W.-D., Shao, J.-J., Y.-F, and Zhou, Z.- H. Analysis for abductive learning and neural-syman symbolic reasoning shortcuts. In Proceedings of the 41st Inter- national Conference on Machine Learning, pp. 56524- 56541, 2024.
Yang, Z.., Ishay, A., and Lee, J. Neurasp: Embracing neural networks into answer set programming. Proceedings of the 29th International Joint Conference on Artificial Intelligence, pp. 1765-1762, 2023.
Yu, D., Yang, B., Liu, D., Wang, H., and Pan, S. A survey neural-symbolic learning systems. Neural Networks, 166:105-1266 126, 2023.
Yu, Y., Qian, H., and Hu, Y.Q. Derivative-free optimization via classification. In Proceedings of the 32th AAAI Con- ference Artificial Intelligence, pp. 2286-2292, 2016.

---

Verification Learning: Make Unsupervised Neuro-Symbolic System Feasible
A. Proof of Theorems
A.I. Proof of Theorem 4.1
We can use proof by contradiction. Suppose there exists a score-ranked St at position such that St & (SI..... St-1). and there does not exist < < <, < 1,0 < q < & such that modifying the symbol Sp. at position p of S to Sp,tt gives Suc(S})p with Score(Suc(S)) (S) 2 Score(S,)- Then for any j there are least two positions Pa and ps where the symbols Sp..tar Sp. of 5c at positions Pa and ps and the symbols Sp.:ga3' Spo.qus of S at these positions satisfy Gai 2 Qaj + 1, qbi Obj + 1; or there is at least one position Pa where the symbol Sparau of S; and Spanes of Sj satisfy qai 2 quj + 2.
For the first case, there must exist 1 < < i such that modifying the symbol at position Pa (similarly for pb) of Sy to Spanag+1 gives p.. Since qoi 2 Qai + 1, qbi Qbj and for any other position & {a, bJ. qei 2 gejs and since score is a sorted probability, we have:
score(Spa.u.a) scorelpas 4as + 1), score(Sm..u)) score(pb; (b)); score(Spera)) score(pes tos)
By the independence assumption, Score(S) = IT score(pi.q:).. so:
Score(Suc(S))uu 2 Score(S;)
which leads contradiction, thus the assumption is invalid.
For the second case, there must exist 1 < j < i such that modifying the symbol position Pa of Sy to Spa gives Suc(S,)p.. Since Qai Qaj + and for any other position c + a, qci 2 9ej. we have:
score(Spa.ne 2 score(Pas los + 1), score(Sp.aad score(po:
Thus:
Score(Suc(S))un Score(Si)
leading to contradiction, the assumption is invalid. Therefore, Theorem 4.1 is proved.
A.2. Proof of Theorem 4.2
The proof process is the same that of Theorem 4.1. Due to the satisfaction of the monotonicity assumption, for any 0 <<p < and any 0 g < k. there does not exist S' such that modifying 8p from Sp, sp,9+1 yields Suc(S"), (s1,..., 8p-1, 1p.....,pp-1,533 Sy', Sp+1....,88) 81) E Suc(S") satisfying Score(Suc(S")) > Score(S"). It can be seen that for any q' > q. modifying Sp from Sp.q to Sp.a' to obtain Sy also cannot satisfy Score(Suc(S5)) > Score(S").
Thus, for the first case, where qas 2 Yaf + 1, qbi > 4bj. and for any other position e & {a, b). 9ιi 2 9ej. it can similarly be proven that Score(Suc(S))... )..) 2 Score(S.) holds, leading to a contradiction and invalidating the assumption.
For the second case, where qai > Qaj + and for any other position c A a, qoi 2 9oj. can similarly be proven that Score(Suc(S))p.) 2 Score(S,) holds, leading to contradiction and invalidating the assumption.
Therefore, Theorem 4.2 is proved.
A.3. Proof of Theorem 4.4
The sufficiency can be proved according Theorem 4.2.
When the monotonicity condition is not satisfied, even if we find the top-ranked Sj by Score, we still need to calculate the scores of all S' E S. It is impossible to find the maximum solution without exhaustive traversal, and even more impossible to infer the ish largest solution from the first - 1 ranked solutions. Thus, the necessity is proved.
A.4. Proof of Theorem 6.1
First, consider the clustering ability of the function f. We define the clustering error as the error rate between the labels assigned to samples under the optimal label assignment strategy after clustering and the true labels. According to the Rademacher complexity theory, for any function f E and a p-Lipschitz continuous loss function L., under the action of
12

---

Verification Learning: Make Unsupervised Neuro-Symbolic System Feasible
samples, the generalization error Ronale (f) under the optimal label assignment strategy be determined by the empirical error rate R(f) and the model space complexity R. (F), that is, with probability least 6, it holds that:
(2/()
Rirrall (f) S R(f) 2 + 3V
2n
Due the indistinguishability of symbols in the system, the between the label assignment strategy and the optimal label assignment strategy differs by most Rask- The system's 's generalization enror R(f) is determined by the generalization error Romalee under the optimal label assignment strategy and the maximum difference R between the actual label assignment strategy and the optimal one, i.e.,
R()+ S Roraele (f) + Ruck
Finally, it can be concluded that with probability at least - 5:
log(2/8)
R() < R() 2p + +3/
+ R
2n
B. The Programs of All of the Verification Function
Addition def cigite_to_nunber (aillsss)
number = for d in digits: number == num aum_classes
number d return number
def number_to_digits (number, digit_size, 2 digits=[]
for i in range (digit_size): digits. (numerénnm_clasee,,
number//=num_ee
return digits[::-1]
def V KB (nums, num souuuddiiits._i num_classes))
numsl, nums2, nums 3=nums :num_digits]] nums nums [num_ [nun_digits+2:
return (digits_te salissst___uuutt number (numsl, num num_
wwwpuuaaasssssnmcllaaaeeee classsssss
+ higits__o__umbbe (nums2, num pun_claasse-mmmmcccsss --\ digits_to to to__uberr_reerrrrr (nums3, num cl classes=num (
Sort
def V_XB (nums):
1=len (nums)
for in range (1-1):
if nums [_+]] <=nums [_::
return False
return True
Match
def V V_KB (nums) 1=len (nums)
13

---

Verification Learning: Make Unsupervised Neuro-Symbolic System Feasible
count-None
cur_count=0
for in range :
if >0 and nums [_] <nums <nums[_11] [-1]]
return False
elif _>0 and nums [_>numms [_-1]:
if count is None:
count=cur_count elif count!=cur_count:
return False cur_count=0
cur cur_count+-1
return count is None or cur_count==count
Chess
def attack (type, x1, yl, x2, ; if type 0:
return bishop bishop_attack attack (xl, yl, x2, y2)
elif type == 1:
return king_attack (x1, yl, x2, y2)
elif type == 2:
return knight_attack attack (xl, yl, x2, y2)
elif type == 3:
return pawn_attacke (x1, yi, x2, y2)
elif type 4:
return queen_attaoe (xl, yl, x2, y2)
elif type == 5:
return rook_attack (x1, yl, x2, y2)
return False
def king_attack (xi, yl, x2, y2)
King moves one step any direction return abs(x1 x2) <= and abs (yl y2) <= 1
def queen_ yl, x2, y2): # Queen moves straight or diagonal return self.straight_atee self delf.diaggnall attck (xl, yl, x2, y2)
(x1, yl, x2, y2) or \
def rook_attack (x1, yl, x2, y2): # Rook moves straight return self. (x1, yl, x2, y2)
def bishop_at (xl, yl, x2, :2):
# Bishop moves diagonally return self. ditdaallllllaa (x1, yl, x2, y2)
def knight_attack (x1, yl, x2, y2):
# Knight moves in "L" shape
return (abs (x1 - x2) = 2 and abs (y1 y2) == 1) or (abs (xl x2) -- 1 and abs (yl - y2) -- 2)
def pawn_attacks (x1, yl, x2, y2): Pawn attacks diagonally (assuming it's a white pawn)
14

---

Verification Learning: Make Unsupervised Neuro-Symbolic System Feasible
return abs (x1 x2) and y2 yl
def straight_attack (x1, yl, x2, y2)
# Moves straight: either same row or same column return x1 = x2 or y = y2
def diagonal_attack (xl, yl, x2, y2)
# Diagonal move: difference between and y is the same return abs (x1 x2) abs (yl y2)
def V_KB (type, pos):
1-len (type)
for i in range (1):
for in range :
if attack (type [i], pos [i] [0], pos[i] [1], pos [j] [0], , pos [i] (1])
return True
return False
All of the code open-sourced on the github http:///tttooooomoiriiiiiiaallae
15


Reviews:
[{"review_id": "WsefJTzS89", "reviewer": "Reviewer_NuWZ", "summary": "This paper presents a new framework in unsupervised NeSy, excelling in theory and experiments.  And the new framework shows excellent performance across diverse tasks. However, there are several weaknesses that need to be addressed to enhance the quality of the paper. The authors should provide further explanations for the experiment and refine the language clarity.", "questions": "", "limitations": "", "rating": 2, "confidence": null, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "Dear reviewer NuWZ:\n\nThank you for valuable comments.\n\n**Regarding Weakness 1:**  \nAbout the language, you are absolutely correct. \"KL\" should be corrected to \"VL\"; this was a typographical error. Thank you for pointing it out.  \nAbout the formulas, we have provided more detailed explanations for all of them. If anything remains unclear, please feel free to point it out:  \n- **Equations (1) and (2)** summarize the training methods of previous label-based neuro-symbolic learning algorithms. Equation (1) generalizes the training method of algorithms like DeepProbLog, which utilize all candidate solutions for training. Equation (2) generalizes the training method of algorithms like ABL, which select the highest-scoring candidate solution from the search results for training.  \n- **Equation (3)** describes the process of aligning the predicted probabilities from the neural network with the prior distribution of symbols, which helps prevent the network's predictions from collapsing into trivial solutions. For example, the addition rule is still satisfied even when the neural network predicts all symbols as 0. \n- **Equations (4) and (5)** describe the upper bound and mean error caused by the task itself in unsupervised neuro-symbolic systems. Equation (4) states that the error upper bound is equal to the sum of the distributions of all non-fixed-point symbols in the symbolic system, where a fixed point refers to symbols whose functions cannot be replaced in the system. Equation (5) states that the mean error is equal to the sum of the ratios between the distribution of each symbol and the number of its orbits, where the number of orbits represents how many other symbols can replace the function of a given symbol.  \n- **Equation (6)** describes the empirical error caused by training a neural network in an unsupervised manner. Since the training error in unsupervised learning should be determined by its clustering error, the minimum error under all label assignments should be considered.  \n- **Equation (7)** describes the upper-bound generalization error of an unsupervised neuro-symbolic system. This error is jointly determined by the training error, the complexity of the model space, and the task-specific error upper bound.\n\n**Regarding Weakness 2:**  \nThe observed performance variation is due to the early termination of the neural network training process before full convergence. To ensure an objective comparison, we maintained consistent hyperparameters across all methods and experimental settings. Specifically, we fixed the number of training epochs for all algorithms to 10 across different bases.  \nIn the particular setting you pointed out, while the accuracy was 51.40% at the 10th epoch, it exceeded 90% by the 13th epoch:  \n|Epoch|10|11|12|13|14|15|  \n|-|-|-|-|-|-|-|  \n|$VL_{\\not\\perp}$|48.80|57.05|67.88|90.85|92.83|94.28|  \n|$VL_{\\not\\perp}^{TTC} $ |51.40|63.05|78.13|97.38|98.85|98.95|  \n\nThis indicates that the algorithm did not fail; rather, due to the expanded symbolic space, the neural network requires more training. We did not adopt a higher number of epochs because this would cause DeepProbLog and NeurASP to exceed the time limit (300 hours).\n\n**Regarding Weakness 3:**  \nIn Section 3 of the original paper, we analyzed why methods such as DeepProbLog and NeurASP fail when reasoning without label Y, and why the VL paradigm remains effective even without relying on Y. Here, we further expand this analysis by incorporating specific tasks.  \nThe fundamental reason why DeepProbLog, NeurASP and etc. fail in unsupervised tasks is that they lack the ability to precisely identify the correct symbolic label S from a vast set of candidate symbolic labels candidates(S).  \n- In supervised tasks, |candidates(S)| is relatively small, making this issue less severe.  \n- In unsupervised tasks, |candidates(S)| is significantly larger, amplifying the problem and ultimately leading to algorithm failure.   \n\nFor example, in an **addition task**:  \n- With supervision, the KB consists of addition rules. Given an equation like **Image1+Image2=Y**, when Y=0, we get candidates(S) = \\{(0,0)\\}; when Y=1, candidates(S) = \\{(0,1), (1,0)\\}, and so on. The average of |candidates(S)| is only **4.91**, indicating a relatively low level of imprecision.  \n- Without supervision, where no Y is provided, given **Image1+Image2=Image3 Image4**, the KB alone must infer: candidates(S)=\\{(0,0,0,0),...,(9,9,1,8)\\}. Here, |candidates(S)| reaches **100**, making it infeasible for DeepProbLog and NeurASP to identify the correct symbolic label S efficiently. The overwhelming number of imprecise labels leads to training failure.\n\nIn contrast, VL has a significant advantage in efficiently identifying the precise symbolic label S from candidates(S). VL excels even when |candidates(S)| is large because it leverages the proposed combinatorial ranking algorithm, which efficiently and precisely selects the optimal symbolic label S that adheres to the rules.", "claims_and_evidence": "Yes", "methods_and_evaluation_criteria": "Yes", "theoretical_claims": "N/A", "experimental_designs_or_analyses": "Yes", "relation_to_broader_scientific_literature": "enhance the trustworthy of model", "essential_references_not_discussed": "Yes", "other_strengths_and_weaknesses": "weakness：\n1. The language is occasionally unclear, e.g., \"KL paradigm\" in the introduction should likely be \"VL paradigm\" . Additionally, some equations are lack sufficient explanation.\n2. Table 1 shows significant performance fluctuations in the addition task (e.g., $V L_L^{TTC}$ drops to 51.40% at base 10), but no explanation is provided.\n3. Although the experiments compare against DeepProblog, NeurASP, etc., the authors don't sufficiently discuss the limitations of these methods in unsupervised settings and why VL significantly outperforms them in specific tasks (e.g., 100% accuracy in addition), lacking in-depth qualitative analysis.\n\n\nStrength:\n1. The VL paradigm, by replacing reasoning with verification, eliminates the reliance on labels, filling a gap in unsupervised NeSy research. \n2. The DCS algorithm reduces the complexity of COP from exponential to near-CSP levels, significantly improving computational efficiency. Time consumption data in Table 2 further validates its superiority.\n3. The paper validates VL across four diverse tasks (addition, sorting, matching, chess), spanning simple arithmetic to complex rule-based scenarios. The results show excellent performance across tasks.", "other_comments_or_suggestions": "No", "questions_for_authors": "See the strengths and weaknesses", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "extra_scores": {}}, {"review_id": "npX6Yen1PX", "reviewer": "Reviewer_3PLJ", "summary": "The paper introduces verification learning, a neuro-symbolic paradigm to overcome reliance on labeled data by converting traditional symbolic reasoning into a label-free verification process. VL frames the learning task as a constraint optimization problem and leverages a dynamic Combinatorial sorting algorithm to efficiently find optimal solutions. A distribution alignment method is also introduced to mitigate shortcut issues common in unsupervised settings. Experiments demonstrate the efficacy of VL across various tasks, including addition, sorting, matching, and chess.", "questions": "", "limitations": "", "rating": 3, "confidence": null, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "Dear reviewer 3PLJ:\n\nThank you for valuable comments.\n## Weakness 1, Suggestions 1 & 2\nFirst, we need to clarify that in Nesy, for more complex scenarios where monotonicity is not satisfied, **no algorithm can find the global optimal solution in sub-exponential time. Monotonicity is both a necessary and sufficient condition for solving it**.\n\nIn a Nesy problem, where there are **m symbols**, each with **n possible values**, the complexity of the solution space is **$O(n^m)$**. The goal is to find the optimal solution among them.  \n- If monotonicity holds, the DCS algorithm can solve the problem efficiently with extremely low complexity.  \n- If monotonicity does not hold, the only way to guarantee finding the optimal solution is by exhaustively searching the entire solution space, because even if **$n^m-1$** solutions have already been evaluated, there is no way to determine whether the last remaining solution is optimal.  \n\nExample 1: Independence Holds\nFor m = 2, n = 2 suppose:\n\nscore=[[0.4,0.6],[0.7,0.3]]\n\nScore(s₁=v₁,s₂=v₁)=0.28  \nScore(s₁=v₁,s₂=v₂)=0.12  \nScore(s₁=v₂,s₂=v₁)=0.42  \nScore(s₁=v₂,s₂=v₂)=0.18  \n\nExample 2: Monotonicity Holds\n\nScore(s₁=v₁,s₂=v₁)=0.25  \nScore(s₁=v₁,s₂=v₂)=0.18  \nScore(s₁=v₂,s₂=v₁)=0.34  \nScore(s₁=v₂,s₂=v₂)=0.23  \nmonotonicity is satisfied:  \nScore(s₁=v₁,s₂=x)<Score(s₁=v₂,s₂=x)  \nScore(s₁=x,s₂=v₂)<Score(s₁=x,s₂=v₁)\n\nExample 3: Monotonicity Does Not Hold\n\nScore(s₁ = v₁,s₂= v₁)=0.23  \nScore(s₁ = v₁,s₂ = v₂)=0.25  \nScore(s₁ = v₂,s₂ = v₁)=0.34  \nScore(s₁ = v₂,s₂ = v₂)=0.18  \nHere, fixing one symbol’s value leads to inconsistent ranking of the other symbol’s scores, meaning monotonicity is violated. In this case, there is no alternative to brute-force enumeration to guarantee finding the optimal solution. \n## Weakness 2\nOur theory is actually applicable.  It demonstrates that in many real-world scenarios—such as **traffic control, industrial anomaly detection, and circuit analysis**—it is entirely feasible to replace all labels with rules for learning.\nOur theory also highlights that the key to replacing labels with rules lies in ensuring that different symbols within the rule system possess irreplaceability. For instance, in autonomous driving tasks, the rule **\"Red and green lights cannot be on simultaneously\"** cannot distinguish between them. However, the rule **\"Stop at red, go at green\"** effectively differentiates them. This insight is valuable for **selecting meaningful rules** when constructing a knowledge base.\n## Weakness 3 & Question 3\nThe primary role of distribution alignment is to initialize the neural network’s predictive distribution, preventing it from falling into trivial solutions.\nAccording to Bayes' theorem, the posterior probability learned by the model can inherently correct biased priors. When the true natural distribution is unknown, a uniform distribution can be used as the prior to ensure a sufficiently diverse initialization. This allows the model to fully utilize all available knowledge and gradually converge to the true distribution.\nBelow is a comparison between using a uniform prior for alignment and no alignment on an imbalanced addition dataset:\n|Method|2|3|4|5|6|7|8|9|10|\n|-|-|-|-|-|-|-|-|-|-|\n|No prior|46.60|32.68|29.58|29.60|27.00|35.08|24.13|28.43|31.43|\n|Inexact prior|100.00|100.00|99.95|100.00|58.50|99.90|59.23|49.43|43.45|\n\n## Weakness 4\nOur algorithm is practical as it only requires writing a verification function, significantly simplifying the complexity of knowledge compared to others.\nFurthermore, when dealing with a large amount of unlabeled data, writing a verification program is more cost-effective than manually labeling. VL can achieve 92.02% based on the autonomous driving rule set Road-R.\n\n## Question 1\nAs the size of the symbol space increases, VL exhibits a low growth in runtime. In Table 2, we compare the runtime as the number of symbol categories increases from 2 to 10, where VL's runtime only increases from 112.04 to 116.26, whereas the runtimes of DeepProbLog increase by a factor of 20.\nThis efficiency is due to our sorting algorithm, which ensures that the first solution passing verification is the optimal one. The time complexity is O(K(logK+mlogm+nlogn)), where the constant K represents the position of the first verified solution.\n\n## Question 2\nWe conducted experiments to validate the robustness. In our tests, the verification function returns the correct validation result with probability p, and we gradually decrease p from 100% down to 50%(completely random).\nOur findings indicate that the algorithm's performance only experiences a significant decline when predictions approach complete randomness. As long as the probability of returning correct results is higher than that of returning incorrect results, VL can largely mitigate the impact of errors, demonstrating a strong fault tolerance.\n|p|100|95|90|85|80|75|70|65|60|55|50\n|-|-|-|-|-|-|-|-|-|-|-|-|\n|Acc|98.28|97.58|97.24|94.19|95.02|94.72|93.99|93.55|92.58|83.34|53.58|", "claims_and_evidence": "Yes", "methods_and_evaluation_criteria": "Yes", "theoretical_claims": "Yes", "experimental_designs_or_analyses": "Yes", "relation_to_broader_scientific_literature": "This work provides practical and theoretical foundations for unsupervised learning without labelled data.", "essential_references_not_discussed": "No", "other_strengths_and_weaknesses": "Strengths:\n1. The proposed verification learning paradigm is innovative. It clearly addresses critical bottlenecks in existing neuro-symbolic frameworks by eliminating the need for labeled data.\n2. The paper provides theoretical analyses that clarify task solvability conditions and generalization bounds.\n3. Experiments across diverse tasks demonstrate performance improvements and data efficiency.\n\nWeaknesses:\n1. The assumption of monotonicity, although relaxed compared to independence, still limits the generalizability of the proposed DCS algorithm to more complex, non-monotonic scenarios.\n2. The theoretical framework, while insightful, may be overly idealized, and the translation of these theoretical insights to complex real-world scenarios may not be straightforward.\n3. The complexity of the distribution alignment strategy may not be trivial in tasks with highly imbalanced or unknown natural symbol distributions.\n4. In general, this method requires substantial domain knowledge, which may be impractical in many real-world scenarios.", "other_comments_or_suggestions": "1. Clarify explicitly the conditions under which monotonicity fails. Provide a simple example scenario.\n2. The readability of certain theoretical sections (especially Sections 4.1 and 4.2) could be improved by using concrete examples to illustrate key concepts clearly.", "questions_for_authors": "1. Can the DCS algorithm handle tasks with high-dimensional symbol spaces or extensive solution spaces without significant computational overhead?\n2. In practice, how sensitive is VL to incorrect or noisy verification functions, and how might such imperfections affect learning performance?\n3. Could distribution alignment be adapted or automated for scenarios where the natural distribution is not unknown?", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "extra_scores": {}}, {"review_id": "utOU4h3hva", "reviewer": "Reviewer_Vjyz", "summary": "In this work, the authors introduce a novel learning paradigm called Verification Learning (VL) to address the problem of learning without labels in neuro-symbolic models. VL corresponds to flipping the standard label-based reasoning [S,KB |= Y] into predicting a set of possible candidate solutions leveraging the knowledge base and the labels [KB,Y |= candidates(S)], and eventually remove the labels from the picture, to infer the set of candidates directly from the knowledge base [KB |= candidates(S)]. Since directly inferring the correct candidate assignment from the set of candidate symbols is computationally prohibitive (would require enumerating all the possible candidates, infeasible in practical scenarios) the author resorts to a generation-validation strategy. To be competitive, this verification approach exploits the assumption that the generated candidates can be sorted according to some scores (that matches the fitness of the candidates), allowing the exploration of the candidate space in an efficient manner using a heap structure. The authors show that this is possible not only when the score factorizes over the symbols (independent assumption, Th. 4.1) but also in the more relaxed constraint where the score satisfies monotonicity (Th. 4.2). The authors also introduce a distribution alignment with some prior to avoid shortcut solutions. Finally, the authors include a theoretical analysis on the upper bounds on accuracy that VL can achieve and experimental results on 4 tasks: addition, sort, match, chess.\n\n## update after rebuttal\nI acknowledge and appreciate the efforts made by the authors, and I have carefully reviewed their responses. The additional experimental results on the Road-R dataset, the ablation on the distribution alignment, the additional baselines introduced for other reviewers (Hybrid, ABL-zoopt, REFL, PSP), and the empirical quantification of the benefits of sorting algorithms increased my confidence in the value of this work. I also want to thank the authors for addressing my questions and some of the weaknesses highlighted in the initial review. Even if I agree with Reviewer W1W6 on the fact that the work still requires further improvement, I am raising my score in light of the new experimental results and explanations added during the rebuttal.", "questions": "", "limitations": "", "rating": 3, "confidence": null, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "Dear Reviewer Vjyz:\n\nThank you for valuable comments.\n### Regarding the Benefits of Sorting Algorithms\nWe supplement this comparison with the time consumption of the naïve sorting method. As the space grows exponentially, the time required by the naïve method increases tenfold, while DCS remains stable.\n|Algorithm|2|3|4|5|6|7|8|9|10|\n|-|-|-|-|-|-|-|-|-|-|\n|VL|112|114|111|111 |111|109|106|112|116|\n|Naive|114|127|173|213|239|394|573|641|1254|\n\n### Regarding Monotonicity\nWhen monotonicity is not satisfied, it can be proven that no algorithm with a complexity lower than exponential can find the optimal solution. Fortunately, the optimization objectives in current Nesy frameworks almost satisfy monotonicity.\n\n1.Metrics that satisfy independence\nAn example is the Confidence Score, defined as:\n$Confidence(S)=\\prod_{i=1}^{m} confidence(x_i)_{s_i}$\n\n2.Metrics that do not satisfy independence but still satisfy monotonicity.\n$Consistency(S)=\\sum_{i=1}^{m}\\left[ f(x_i)=s_i\\right]$\n\n3.Combinations of Metrics\nAny metric formed by adding, multiplying (with positive values), or concatenating also retains monotonicity. For example, the two-dimensional tuple: $(Consistency(S), Confidence(S))$ remains a monotonicity-preserving metric.\n### Regarding Practical Applications\nIn applications, VL can be applied in various scenarios. In autonomous driving, a vehicle can automatically recognize pedestrians, traffic lights, and crosswalks in an image using only the traffic rules. In circuit fault analysis, VL can identify faulty components based solely on input circuit diagrams and electrical rules.\nWe further validated VL in real-world scenarios by conducting experiments on the Road-R autonomous driving dataset with driving rules.\n|Method|4|5|6|7|8|9|\n|-|-|-|-|-|-|-|\n|Deepporblog|6.24|16.91|20.31|7.46|12.57|11.50\n|Deepstochlog|5.98|19.12|MLE|MLE|MLE|MLE|\n|NeurASP|27.30|22.34|6.12|TLE|TLE|MLE|\n|ABL|86.58|58.01|44.93|28.15|19.50|5.18|\n|WSABL|87.22|57.38|32.11|31.01|36.29|22.45|\n|$VL_{\\not\\perp}$|92.06|86.54|86.53|82.16|82.90|73.36|\n|$VL_{\\not\\perp}^{TTC}$|93.43|92.38|93.87|90.63|93.33|88.48|\n|$VL_{\\perp}$|92.06|87.84 |87.59|84.93|82.80|72.72|\n|$VL_{\\perp}^{TTC}$|93.43|92.40|92.93|90.86|91.90|82.24|\n### Regarding Ablation Study on Alignment\nWithout distribution alignment, unsupervised learning can effectively cluster similar samples together but struggles to associate them with the correct symbols.\n|Method|2|3|4|5|6|7|8|9|10|\n|-|-|-|-|-|-|-|-|-|-|\n|$VL_{\\not\\perp}^{noalign}$|46.25|100.00|34.5|29.6|27.00|25.25|21.83|24.13|21.42|\n|$VL_{\\not\\perp}$|100.00|99.88|99.75|100.00|99.75|99.00|99.25|97.75|48.80|\n|$VL_{\\perp}^{noalign}$|46.60|32.68|29.58|29.60|27.00|35.08|24.13|28.43|31.43|\n|$VL_{\\perp}$|100.00|41.38|99.50|99.80|99.65|99.19|70.70|98.73|98.28|\n\n### Regarding Experimental Designs or Analyses\nThe goal of this work is to train neural networks without any labels by utilizing verification functions. This enables the neural networks to accurately extract symbols from raw data. All accuracy values reported in this paper correspond to the accuracy of the neural network in symbol recognition. In Section 7, we introduce the general experimental setup. A LeNet backbone was employed in all cases, with training conducted for 10 epochs.\n\n### Regarding Question 1\nIn this paper, all the permutations we describe are global permutations applied to the entire symbol system. The permutation we aim to express is holistic (in a 9x9 grid) and refers to symbol permutations on the entire Sudoku board. For example, by permuting all the 1s in the 9x9 grid to 2s, 2s to 3s, ..., and 9s to 1s, this global permutation will cause corresponding changes in each row, column, and 3x3 grid, but will not violate any of the constraints on any of them. For example, in a vision Sudoku task with 81 unlabeled images, a completely unsupervised approach would fail to prevent the images from being interpreted as permuted labels. Due to the possibility of all labels being permuted, the error bound caused by the Sudoku task itself can reach 100%.\n\n### Regarding Question 2\nIn Nesy, machine learning models such as neural networks play a role in recognizing abstract symbols from raw data. Our work is no different in this regard, and our ultimate goal is to complete the neural network training process using only a verification function as the knowledge base.\nThe pipeline described in this paper can be summarized as follows:\n1. A set of samples $X=[x_1,\\dots,x_m]$ is input into the network f.\n2. The neural network outputs probability predictions for this set of samples g(X) and label predictions f(X).\n3. The probability predictions g(X) are then adjusted through distribution alignment to obtain $g_{align}(X)$.\n4. A Score is chosen as an optimization goal with monotonicity.\n5. The DCS is called to obtain the optimal result $Y^{val}$ validated by the verification function.\n6. The result $Y^{val}$ is used as supervision information, and the loss is computed by comparing it with g(X).", "claims_and_evidence": "The authors claim that VL can be a valid alternative to the standard label-based reasoning to learn symbols in neuro-symbolic models. This is supported by presenting (loose) theoretical upper bounds motivated by group theory and a limited set of empirical results on four different symbolic tasks (addition, sort, chess, and match). A second claim is that VL can reduce known issues of neuro-symbolic models, i.e., label leakage and shortcut learning, which comes by the definition of the methodology itself (labels are not used in the training process at all). The authors claim that the proposed sorting strategy gives an edge compared to a naive implementation that evaluates of all the possible symbol assignments. Clearly this is the case, but the advantage is not quantified experimentally. Also, while the argument about monotonicity as necessary condition to enable an efficient combinatorial sorting solution, it is not clear how often and for which score functions this condition would generally hold. Finally, the extent to which this methodology could be apply in real-world scenarios (for which collecting labels can be expensive) is not clear, as a complete verifier would be always needed to allow the generation-verification procedure. Adding an outlook on how this methodology could scale to more complex scenarios could help.", "methods_and_evaluation_criteria": "The proposed benchmark are valid choices to evaluate the claims, even if slightly simplistic. This does not represent a major issue, since it is in line with the datasets used to benchmark standard NeSy models. The proposed methodology is principled and, to the best of my knowledge, is original compared to previous works.", "theoretical_claims": "The authors propose three main theoretical contributions in the paper:\n-\tA proof that, when the symbols satisfy the independence assumption, the exploration of the candidates can be performed efficiently “exploding” a limited number of successors for each candidate and guiding the search using a heap structure [Th 4.1].\n-\tA proof that independence is a sufficient but not necessary condition. On the other hand, the relax constraint of monotonicity of the scoring function is a more relaxed but necessary condition [Th 4.2].\n-\tTheoretical bounds on which problem types are addressable by the VL framework using group theory [Section 6].\nThe first two are correct, I did not check carefully the third.", "experimental_designs_or_analyses": "The methodology of the experiments is not sufficiently clear and could benefit from some more careful rewriting. For instance, it is not clear what the accuracies reported in the table represent, how exactly is the model trained, how the baseline models compare to the proposed VL framework in terms of size/supervision/etc. Moreover, some of the novelties introduced in this work are not really ablated in the experimental analysis. For instance, there is no quantification of the computational benefit of the efficient combinatorial sorting solution and no ablation of the distribution alignment technique introduced in Section 5 (which also comes out a bit of nowhere).", "relation_to_broader_scientific_literature": "This work is mainly related to works on label leakage (Chang 2020) and shortcut learning (Yang 2024, He 2024) as a potential solution to these problems (labels are completely removed from the learning process, hence no leakage or shortcut is possible)", "essential_references_not_discussed": "I am not aware of essential references related but not discussed in the manuscript.", "other_strengths_and_weaknesses": "A major strength of this paper is the originality of the idea, which is interesting and allowed by a series of non-trivial steps, e.g. the efficient combinatorial sorting to speed up the COP. However, the presentation of the material could be greatly improved. I believe the manuscript still needs to be ironed in many parts, the notation needs to be simplified in some sections, and less background knowledge must be given for granted in others. Some examples:\n-\tThe examples in the 3rd paragraph of the introduction are not well introduced and it is borderline impossible to understand them without referring to the original papers. More in general, I think that giving for granted a lot of background knowledge is an issue underlying many parts of the text, which undermines its accessibility and utility for the community in general. \n-\tSometimes the notation is heavy, overlapping, and confounding. For instance, take the paragraph in Line 206 left column: on its own the concept it’s rather straightforward, but the imprecise notation (S_{i+1}\\in S_j, while it should be S_{i+1}\\in Suc(S_j)) considerably complicates the understanding of it. \n-\tIt is not explained in the manuscript what are the test time corrections (TTC) mentioned in the results section. \n-\tTables are very poorly commented and could benefit from more explicative captions or more detailed descriptions in the main text. Right now, they are not self-contained, and one should go through the entire result section to understand what the different columns represent. The tables do not report which metric is used in the corresponding experiments.", "other_comments_or_suggestions": "-\tIn Line 45, page 1 you use a comma to “tie” together the two symbols, while in Line 51 you use a plus symbol (not clear if this is intentional or not).\n-\tKL in Line 70 of page 2 left column pops out of nowhere.\n-\tThe references should be revised, as some are missing quite important fields (e.g. Yang et al. He et al., and van Krieken et al are all missing the year).\n-\tThe last sentence of the paragraph, line 126 left column, does not sound correct.\n-\tLine 133, page 3 right column there is a comma instead of a full stop.\n-\tLines 174—195 inconsistent use of ; and .", "questions_for_authors": "-\tIn the 1st example of section 6, you state that the error upper bound for Sudoku is 100%, because any permutation of numbers within a row, column or grid satisfies the constraints within them. However, these permutations would not satisfy the constraints of other entities (e.g., permuting within a row would still guarantee the satisfaction within itself, but would most likely result in breaking the constraints of other columns/grids). Why are these not taken in account?\n-\tWhere is the L (learning) in VL? What is effectively trained in your setup? This should be really clarified in the manuscript, which right now is missing a clear outline of the proposed system and training pipeline.", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "extra_scores": {}}, {"review_id": "d06dZ8pGye", "reviewer": "Reviewer_W1W6", "summary": "This paper introduces a novel learning paradigm, named verification learning, which transform the label-based reasoning process in neuro-symbolic into a label-free verification process. It achieves good learning results solely by relying on unlabeled data and a function that verifies whether the current prediction conform to the rules. The theoretical analysis points out which tasks in neuro-symbolic systems can be completed without labels and explains why rules can replace infinite labels.", "questions": "", "limitations": "", "rating": 2, "confidence": null, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "Dear Reviewer W1W6:\n\nThank you for valuable comments.\n### Regarding Question 1 and Weaknesses 1:\nMethodological Innovations:\n1. Explored fully unsupervised Nesy algorithms and provided a systematic solution.\n2. Proposed a universal approach for finding globally optimal solutions to Nesy search problems solvable in sub-exponential time.\n3. Demonstrated that in the Nesy domain, a single validation function can replace an entire complex knowledge base.\n4. Shifted the paradigm from inference to validation, expanding the symbolic space complexity that can be solved.\n\nTheoretical Innovations:\n1. Proved that when a symbolic system is sufficiently differentiated, rules can theoretically replace all labels. This is equivalent to proving that rule-based clustering alone can achieve classification.  \n2. Demonstrated that monotonicity is a necessary and sufficient condition Nesy to achieve a globally optimal solution in sub-exponential time.\n3. Established that the irreplaceability of symbols within a system is a necessary condition for their correct recognition.\n\n### Regarding Question 2:\nRegarding Formula (1):\nIn Formula (1), we have generalized various algorithms, such as deepproblog and others, to highlight the commonality in their form. Therefore, the Score does not refer to any specific score. I outline the differences in the Score chosen by different algorithms for comparison.\n- In deepproblog and deepstochlog, $Score(S)=\\prod_{i=1}^{|path|} p(path_i)$ where path refers to the path leading to S derived from the root.\n- In ABL, $Score(S)=\\sum_{i=1}^{m}[f(x_i)==s_i]$ known as the Consistency, which represents the number of symbols in S that align with the predictions.\n- In WSABL, $Score(S)=\\prod_{i=1}^{m} confidence(x_i)_{s_i}$ known as the Confidence, which represents the probability that predicts.\n- In VL. In the independent mode, we use the Confidence. In the non-independent mode, Score(S)=(Consistency(S), Confidence(S)). This means seeking the solution with the highest consistency and, the one with the highest confidence among them.\n\nRegarding Proofs\n\nFor Theorem 4.1, we use proof by contradiction. Suppose for the i-th largest solution i>1, there is no 0<j<i such that i=suc(j). Then, there must exist some l where i=suc(l) and score(l)>score(i). Since no 0<j<i satisfies i=suc(j), it follows that l>i, contradicting score(l) >score(i). Thus for any i>1, there must exist 0<j< i such that i=suc(j).\n\nThe proof for Theorem 4.2 follows the same reasoning as Theorem 4.1.\n\nFor Proposition 4.3, if S is independent in terms of Score, then Score(S) is the product of individual scores. This ensures that reordering any subset does not affect the relative ranking of scores, making independence a sufficient condition for monotonicity.\n\nFor Theorem 6.1, let $\\hat{R}(f)$ be the empirical loss of the best permutation for clustering. The difference between its empirical and generalization error is bounded by \n$2\\rho \\mathcal{R}_n(F)+3 \\sqrt{\\frac{\\log(2/\\delta)}{2n}}$.\n\nThe difference between the optimal and true permutation is given by $R^{up}_{task}$.\n### Regarding Weaknesses 2 and Question 3:\nWe expanded the experiments by adding 4 new comparison methods. These include 2 classic methods, Hybrid and ABL-zoopt, where Hybrid is an algorithm for solving the CSP problems using neural networks, and ABL-zoopt is a classic method based on gradient-free optimization. Additionally, we included 2 recent methods, REFL and PSP. REFL accelerates the inference process using the Reflection mechanism which is the best paper at AAAI 25. PSP is the latest algorithm that combines probabilistic symbolic perception with symbolic context.\n|Method|2|3|4|5|6|7|8|9|10|\n|-|-|-|-|-|-|-|-|-|-|\n|Hybrid|53.75|40.85|38.73|35.48|28.38|30.48|24.13|21.83|21.43|\n|ABL-Zoopt|100.00|44.50|99.55|70.33|40.15 |25.25|26.43|48.25|48.03|\n|REFL|99.98|42.60|64.80|99.43|99.05|62.78|57.57|62.93|49.08|\n|PSP|99.88|45.58|64.75|99.03 |75.38|67.58|63.30|98.23 |97.38|\n|VL|100.00|49.83|100.00|100.00|100.00|100.00|69.20|99.95|100.00|\n\nAdditionally, we have included more evaluation metrics. In addition to the accuracy in symbol recognition, we have also included classic metrics such as Recall, Precision, F1 Score, and ROC-AUC. Furthermore, we have added the Global Accuracy metric, which describes the probability that the network provides the correct answer for all symbols in a given set. It is used to reflect the algorithm's ability to find the precise solution.\n|Method|Accuracy|Recall|Precision|F1|ROC-AUC|Global Accuracy|\n|-|-|-|-|-|-|-|\n|Deepporblog |21.41|2.14|10.00|3.53|50.00|0.75|\n|Deepstochlog|12.50|1.25|10.00|2.22|47.60|0.00|\n|NeurASP|7.44|1.23|9.96|1.55|49.41|0.00|\n|ABL|21.43|2.14|10.00|3.53|50.00|1.50|\n|WSABL|21.47| 21.47|10.00|3.54|50.73|0.98|\n|Hybrid|21.43|2.14|10.00|3.53|50.00|1.50|\n|ABL-Zoopt|48.03|22.27|27.23|24.75|81.23|5.20|\n|REFL|49.09| 27.29|30.93|29.91|78.30|10.90|\n|PSP|97.38| 97.09|96.54| 96.77|99.92|89.80|\n|VL|99.95|99.93|99.94|99.93|99.98|99.90|", "claims_and_evidence": "Yes.", "methods_and_evaluation_criteria": "Yes.", "theoretical_claims": "Yes.", "experimental_designs_or_analyses": "Yes.", "relation_to_broader_scientific_literature": "Neuro-Symbolic Learning, Constraint optimization Problem.", "essential_references_not_discussed": "No.", "other_strengths_and_weaknesses": "**Strength**: \\\n(1) The idea and motivation is clear state. The writing is good and the method pipeline is easy to follow. \\\n(2) This paper provides a comprehensive theoretical foundation for the proposed method. \n\n**Weaknesses**: \\\n(1) The novelty of the proposed method requires further elaboration and discussion. \\\n(2) The experiments is somewhat weak and necessitates further expansion and refinement to ensure robustness and comprehensiveness.", "other_comments_or_suggestions": "See questions below.", "questions_for_authors": "(1) The proposed method seems simple, and I concern about the novelty. I recognize the significance of a label-free neuro-symbolic framework and the urgency of developing corresponding solutions. While I appreciate the idea and motivation behind this paper, I remain interested in how other reviewers evaluate its novelty. Could the authors provide a more detailed explanation of the proposed method's novelty from both algorithmic and theoretical perspectives? \\\n(2) The algorithm description requires further refinement, as I believe many details are omitted and not adequately explained in the supplementary materials. For example, what is the precise definition of the score in Equation 1? Additionally, are there brief proofs provided for the theorems and propositions presented in the paper? \\\n (3) The experiments are weak incomplete; additional evaluation metrics and baselines are necessary to facilitate more comprehensive comparisons.", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "extra_scores": {}}]

Author rebuttal:

Meta-review: he paper presents a Verification Learning (VL) that enables unsupervised neuro-symbolic (NeSy) systems to function effectively without reliance on labeled data. Traditional NeSy approaches depend heavily on labeled datasets, and removing labels often leads to challenges such as reduced symbolic information, an expanded solution space, and the emergence of shortcut solutions. VL addresses these issues by transforming the label-based reasoning process into a label-free verification process. In this framework, learning is guided solely by a verification function that checks whether the model's predictions adhere to predefined rules. Overall, the reviews are mixed, 2x weak reject and 2x weak accept, resulting in a borderline paper. The two negative reviews are rather short, and I have downweighted them. Still as pointed out in the reviews, the presentation has to be improved. More importantly, the paper should be discussed the work on learning by self-explaining, see e.g. 

Wolfgang Stammer, Felix Friedrich, David Steinmann, Manuel Brack, Hikaru Shindo, Kristian Kersting. Learning by Self-Explaining. Transactions on Machine Learning Research (TMLR), 2024

as well as on the semtantic loss

Jingyi Xu, Zilu Zhang, Tal Friedman, Yitao Liang, Guy Van den Broeck: A Semantic Loss Function for Deep Learning with Symbolic Knowledge. ICML 2018: 5498-5507

and algorithmic supervision such as 

Felix Petersen, Christian Borgelt, Hilde Kuehne, Oliver Deussen: Learning with Algorithmic Supervision via Continuous Relaxations. NeurIPS 2021: 16520-16531

Nevertheless, the idea of validation is interesting.
Decision: Accept (poster)