arxiv: 2605.07758 · v1 · submitted 2026-05-08 · 💻 cs.FL · cs.LG

Recognition: no theorem link

SMT-Based Active Learning of Weighted Automata

Alexandra Silva, Kevin Batz, Tiago Ferreira

Pith reviewed 2026-05-11 03:19 UTC · model grok-4.3

classification 💻 cs.FL cs.LG

keywords active learningweighted automataSMT solversnondeterministic automatasemiringsautomata learningformal languages

0 comments

The pith

An SMT-based algorithm actively learns minimal weighted automata over any semiring and terminates for all finite cases.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper presents an active learning procedure for nondeterministic weighted automata that encodes the search for a consistent minimal model as successive SMT problems. The procedure is parametric over the choice of semiring and comes with a proof that any output it produces is minimal and correct with respect to the queries answered so far. A sufficient condition for termination is stated that covers every finite semiring. Experiments on both finite and infinite semirings show the method frequently returns smaller automata than a state-of-the-art competitor while issuing fewer queries to the teacher.

Core claim

The authors introduce an SMT-based active learning algorithm for nondeterministic weighted automata that is parametric in a given semiring. If the algorithm terminates, the automaton it returns is minimal. Partial correctness is proved in general, and a termination condition is supplied that guarantees termination whenever the semiring is finite.

What carries the argument

The SMT-based active learning procedure that iteratively formulates and solves constraint problems over the semiring to find the smallest WFA consistent with membership and equivalence answers.

Load-bearing premise

The method requires a teacher that can answer membership and equivalence queries correctly and an SMT solver that can decide the generated constraints in finite time.

What would settle it

A concrete finite semiring together with a target WFA on which the algorithm either fails to terminate or returns a non-minimal automaton would falsify the termination or minimality claims.

Figures

Figures reproduced from arXiv: 2605.07758 by Alexandra Silva, Kevin Batz, Tiago Ferreira.

**Figure 1.** Figure 1: Equation system Φ(O, n) characterizing the existence of n-state O-correct WFAs. (f w i )i∈n,w∈suffixes(O) , (δ a i,j )a∈Σ,(i,j)∈n×n, and (ιi)i∈n are S-valued variables. to such a witness W and therefore also to an n-state O-correct automaton AW by Theorem 5. The crucial observation is that, since O is finite, so is suffixes(O) and thus all potential generators fi range over a finite domain. The existence o… view at source ↗

**Figure 2.** Figure 2: Effect on learner time (seconds in log-log) of incremental SMT solving [PITH_FULL_IMAGE:figures/full_fig_p016_2.png] view at source ↗

**Figure 3.** Figure 3: Comparison of Naive vs SWAL on average total run-time (seconds in loglog, left), and average number of output queries (count, right), as the number of learned states increases. TO/OOM represented by end-of-line. 6.4 RQ2: Comparison with Naive Algorithm For our comparison of SWAL and Naive, we compare (i) how the algorithms scale in terms of state sizes of learned automata and (ii) their relative query eff… view at source ↗

**Figure 4.** Figure 4: Comparison of WL⋆ vs SWAL on total run-time (seconds in log-log, top left), number of output queries (count in log-log, top right), and number of states learned (log-log, bottom). TO/OOM count provided per axis (top left). 6.5 RQ3: Comparison with WL⋆ Algorithm WL⋆ [24] is a state-of-the-art L ⋆ -based active WFA learning algorithm for semirings forming a principal ideal domain. This means, under the semi… view at source ↗

read the original abstract

We present an SMT-based active learning algorithm for nondeterministic weighted automata (WFAs) as a practical and robust alternative to Hankel/L*-style methods. Our algorithm is parametric in a given semiring and, if it terminates, guaranteed to produce minimal WFAs. We prove partial correctness and provide a sufficient termination condition, which in particular implies termination for all finite semirings. Our extensive experimental evaluation shows that our algorithm is capable of learning numerous minimal WFAs over both finite and infinite semirings, vastly outperforms a naive baseline, and is competitive with a state-of-the-art algorithm while producing significantly smaller automata and requiring less interaction with the teacher.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Desk Editor's Note private letter to a colleague

The SMT encoding gives a parametric active-learning algorithm for nondeterministic weighted automata with partial-correctness proofs and a termination condition that covers all finite semirings.

read the letter

The main takeaway is that this paper replaces the usual Hankel or L* constructions with an SMT solver that finds a minimal nondeterministic weighted automaton consistent with the queries. The algorithm is parametric over any semiring, and the authors prove partial correctness plus a sufficient termination condition that works for every finite semiring. Experiments show it learns many minimal WFAs over both finite and infinite semirings, beats a naive baseline, and stays competitive with a state-of-the-art method while returning smaller automata and fewer teacher queries. That combination of parametric guarantees and practical results is what stands out. The proofs are scoped carefully: they only claim partial correctness and a sufficient (not necessary) termination condition, which matches what the experiments actually demonstrate. The teacher interface is the standard membership-plus-equivalence one, and the SMT encoding is presented as a direct encoding of the learning constraints. No circularity or unsupported steps appear in the argument. The soft spots are the usual ones for this style of work. Termination is not guaranteed for arbitrary infinite semirings, though the authors test some infinite cases where it still finishes. The method also inherits the strong-teacher assumption common to active learning, so it will not apply where equivalence queries are expensive. SMT solving time could become an issue for very large target automata, but the reported runs do not show that bottleneck yet. This is for people who already work on automata learning for verification or weighted models in ML and want a concrete alternative to matrix-based methods. A reader who needs both some theory and experimental head-to-head numbers will get usable material from the comparisons and the termination analysis. It deserves a serious referee because the central claims are scoped to what the proofs and experiments actually support and the SMT approach is distinct from the cited prior work.

Referee Report

0 major / 3 minor

Summary. The manuscript presents an SMT-based active learning algorithm for nondeterministic weighted automata (WFAs) that is parametric over a given semiring. If the algorithm terminates, it is guaranteed to produce minimal WFAs. The authors prove partial correctness and supply a sufficient termination condition that implies termination for all finite semirings. Experiments show the algorithm learns numerous minimal WFAs over both finite and infinite semirings, vastly outperforming a naive baseline while remaining competitive with a state-of-the-art method, producing smaller automata and requiring less teacher interaction.

Significance. If the partial-correctness proof and the sufficient termination condition hold, the work supplies a practical, robust alternative to Hankel/L*-style methods for learning weighted automata. The parametric design over semirings, the explicit teacher interface (membership and equivalence queries), the SMT encoding, and the experimental confirmation of practical termination on finite and selected infinite semirings are clear strengths. These elements could advance automata-learning techniques in verification and formal methods.

minor comments (3)

The abstract states that the algorithm 'vastly outperforms a naive baseline' and is 'competitive with a state-of-the-art algorithm'; a brief quantitative summary (e.g., query counts or automaton sizes) would help readers assess the extent of these improvements without consulting the experimental section.
In the description of the termination condition, the paper could add a short remark on whether the condition is also necessary or whether termination can occur outside the stated sufficient condition, to clarify the practical scope for infinite semirings.
The experimental section would benefit from an explicit statement of the SMT solver and timeout settings used, as these parameters directly affect the reported runtimes and success rates.

Simulated Author's Rebuttal

0 responses · 0 unresolved

We thank the referee for their positive assessment of our work, including the recognition of the partial-correctness proof, the sufficient termination condition, the parametric semiring design, and the experimental results showing smaller automata with fewer queries. We appreciate the recommendation for minor revision.

Circularity Check

0 steps flagged

No significant circularity in the derivation chain

full rationale

The paper's core claims rest on an explicit algorithmic construction (SMT encoding of membership/equivalence constraints for WFAs), a direct proof of partial correctness, and a separately stated sufficient termination condition whose finite-semiring case is derived from standard semiring properties rather than from the algorithm's outputs. No step reduces a prediction or minimality guarantee to a fitted parameter, a self-referential definition, or a load-bearing self-citation; the teacher interface and SMT solver are treated as external oracles with stated assumptions. Experiments compare against independent baselines using observable metrics (automaton size, query count), keeping the argument self-contained.

Axiom & Free-Parameter Ledger

0 free parameters · 0 axioms · 0 invented entities

Insufficient information in the abstract to identify specific free parameters, axioms, or invented entities; the work relies on standard semiring properties and SMT solving.

pith-pipeline@v0.9.0 · 5396 in / 1006 out tokens · 31524 ms · 2026-05-11T03:19:33.950352+00:00 · methodology

discussion (0)

Reference graph

Works this paper leans on

37 extracted references · 37 canonical work pages

[1]

Handbook of weighted automata (2009).https://doi.org/10.1007/ 978-3-642-01492-5,https://link.springer.com/10.1007/978-3-642-01492-5

work page doi:10.1007/978-3-642-01492-5 2009
[2]

Aarts,F.,Ruiter,J.D.,Poll,E.:Formalmodelsofbankcardsforfree.In:2013IEEE Sixth International Conference on Software Testing, Verification and Validation Workshops. pp. 461–468 (2013).https://doi.org/10.1109/ICSTW.2013.60

work page doi:10.1109/icstw.2013.60 2013
[3]

In: Margaria, T., Steffen, B

Aarts, F., Schmaltz, J., Vaandrager, F.: Inference and abstraction of the biometric passport. In: Margaria, T., Steffen, B. (eds.) Leveraging Applications of Formal Methods, Verification, and Validation. pp. 673–686. Lecture Notes in Computer Science, Springer (2010).https://doi.org/10.1007/978-3-642-16558-0_54

work page doi:10.1007/978-3-642-16558-0_54 2010
[4]

1016/j.ic.2020.104651,https://linkinghub.elsevier.com/retrieve/pii/ S0890540120301395

Almagor, S., Boker, U., Kupferman, O.: What’s decidable about weighted automata? Information and Computation282, 104651.https://doi.org/10. 1016/j.ic.2020.104651,https://linkinghub.elsevier.com/retrieve/pii/ S0890540120301395

work page arXiv 2020
[5]

Infor- mation and Computation75(2), 87–106 (1987).https://doi.org/10.1016/ 0890-5401(87)90052-6,https://linkinghub.elsevier.com/retrieve/pii/ 0890540187900526

Angluin, D.: Learning regular sets from queries and counterexamples. Infor- mation and Computation75(2), 87–106 (1987).https://doi.org/10.1016/ 0890-5401(87)90052-6,https://linkinghub.elsevier.com/retrieve/pii/ 0890540187900526

work page 1987
[6]

In: 2025 40th An- nual ACM/IEEE Symposium on Logic in Computer Science (LICS)

Aristote, Q., Van Gool, S., Petrişan, D., Shirmohammadi, M.: Learning weighted automata over number rings, concretely and categorically. In: 2025 40th An- nual ACM/IEEE Symposium on Logic in Computer Science (LICS). pp. 417–

work page 2025
[7]

IEEE (2025).https://doi.org/10.1109/LICS65433.2025.00038,https:// ieeexplore.ieee.org/document/11186332/

work page doi:10.1109/lics65433.2025.00038 2025
[8]

Pro- ceedings of the ACM on Programming Languages6(OOPSLA1), 1–30 (2022)

Batz, K., Gallus, A., Kaminski, B.L., Katoen, J.P., Winkler, T.: Weighted pro- gramming: A programming paradigm for specifying mathematical models. Pro- ceedings of the ACM on Programming Languages6(OOPSLA1), 1–30 (2022). https://doi.org/10.1145/3527310

work page doi:10.1145/3527310 2022
[9]

SIAM Journal on Computing25(6), 1268– 1280 (1996).https://doi.org/10.1137/S009753979326091X,http://epubs

Bergadano, F., Varricchio, S.: Learning behaviors of automata from multi- plicity and equivalence queries. SIAM Journal on Computing25(6), 1268– 1280 (1996).https://doi.org/10.1137/S009753979326091X,http://epubs. siam.org/doi/10.1137/S009753979326091X

work page doi:10.1137/s009753979326091x 1996
[10]

IEEE Transactions on ComputersC-21(6), 592–597 (1972).https://doi.org/10.1109/TC.1972.5009015

Biermann, A.W., Feldman, J.A.: On the synthesis of finite-state machines from samples of their behavior. IEEE Transactions on ComputersC-21(6), 592–597 (1972).https://doi.org/10.1109/TC.1972.5009015

work page doi:10.1109/tc.1972.5009015 1972
[11]

In: Proceedings of the 21st International Joint Conference on Artificial Intelligence

Bollig, B., Habermehl, P., Kern, C., Leucker, M.: Angluin-style learning of NFA. In: Proceedings of the 21st International Joint Conference on Artificial Intelligence. pp. 1004–1009. IJCAI’09, Morgan Kaufmann Publishers Inc

work page
[12]

ACM Transactions on Computational Logic 14(1), 1–52 (2013).https://doi.org/10.1145/2422085.2422092,https://dl

Bonsangue, M.M., Milius, S., Silva, A.: Sound and complete axiomatizations of coalgebraic language equivalence. ACM Transactions on Computational Logic 14(1), 1–52 (2013).https://doi.org/10.1145/2422085.2422092,https://dl. acm.org/doi/10.1145/2422085.2422092

work page doi:10.1145/2422085.2422092 2013
[13]

Proceedings of the ACM on Programming Lan- guages8, 1001–1027.https://doi.org/10.1145/3632876,https://dl.acm.org/ doi/10.1145/3632876

Buna-Marginean, A., Cheval, V., Shirmohammadi, M., Worrell, J.: On learning polynomial recursive programs. Proceedings of the ACM on Programming Lan- guages8, 1001–1027.https://doi.org/10.1145/3632876,https://dl.acm.org/ doi/10.1145/3632876

work page doi:10.1145/3632876
[14]

In: Finkbeiner, B., Pu, G., Zhang, L

Chapman, M., Chockler, H., Kesseli, P., Kroening, D., Strichman, O., Tautschnig, M.: Learning the language of error. In: Finkbeiner, B., Pu, G., Zhang, L. (eds.) Au- tomated Technology for Verification and Analysis, vol. 9364, pp. 114–130. Springer InternationalPublishing(2015).https://doi.org/10.1007/978-3-319-24953-7_ 22 Ferreira, Batz, and Silva 9,http...

work page doi:10.1007/978-3-319-24953-7_ 2015
[15]

ACM Transactions on Computational Logic19(3), 1–52 (Jul 2018).https://doi.org/10.1145/3230639

Cimatti, A., Griggio, A., Irfan, A., Roveri, M., Sebastiani, R.: Incremental Lin- earization for Satisfiability and Verification Modulo Nonlinear Arithmetic and Transcendental Functions. ACM Transactions on Computational Logic19(3), 1–52 (Jul 2018).https://doi.org/10.1145/3230639

work page doi:10.1145/3230639 2018
[16]

Logical Methods in Computer ScienceV olume 21, Issue 3, 13612.https://doi

Daviaud, L., Johnson, M.: Feasability of learning weighted automata on a semiring. Logical Methods in Computer ScienceV olume 21, Issue 3, 13612.https://doi. org/10.46298/lmcs-21(3:15)2025,https://doi.org/10.46298/lmcs-21(3:15) 2025

work page doi:10.46298/lmcs-21(3:15)2025 2025
[17]

In: Ferreira, A., Reichel, H

Denis, F., Lemay, A., Terlutte, A.: Residual finite state automata. In: Ferreira, A., Reichel, H. (eds.) STACS 2001, vol. 2010, pp. 144–157. Springer Berlin Hei- delberg.https://doi.org/10.1007/3-540-44693-1_13,http://link.springer. com/10.1007/3-540-44693-1_13, series Title: Lecture Notes in Computer Science

work page doi:10.1007/3-540-44693-1_13 2001
[18]

In: Finkbeiner, B., Kovács, L

Dierl, S., Fiterau-Brostean, P., Howar, F., Jonsson, B., Sagonas, K., Tåquist, F.: Scalable tree-based register automata learning. In: Finkbeiner, B., Kovács, L. (eds.) Tools and Algorithms for the Construction and Anal- ysis of Systems, vol. 14571, pp. 87–108. Springer Nature Switzerland. https://doi.org/10.1007/978-3-031-57249-4_5,https://link.springer....

work page doi:10.1007/978-3-031-57249-4_5
[19]

Mattukat, Vincent Schmandt, Langstrof Timo, Zerbe Michael, and Horst Lichter

Ferreira, T., Batz, K., Silva, A.: SMT-Based Active Learning of Weighted Automata (artifact). Zenodo (Apr 2026).https://doi.org/10.5281/ZENODO. 19701329

work page doi:10.5281/zenodo 2026
[20]

In: SIGCOMM

Ferreira, T., Brewton, H., D’Antoni, L., Silva, A.: Prognosis: closed-box analysis of network protocol implementations. In: SIGCOMM. pp. 762–774. ACM.https: //doi.org/10.1145/3452296.3472938

work page doi:10.1145/3452296.3472938
[21]

Fiterau-Brostean, P., Janssen, R., Vaandrager, F.W.: Combining model learning and model checking to analyze TCP implementations. In: CAV. LNCS, vol. 9780, pp. 454–471. Springer (2016).https://doi.org/10.1007/978-3-319-41540-6_25

work page doi:10.1007/978-3-319-41540-6_25 2016
[22]

Bochmann, G., Khendek, F., Amalou, M., Ghedamsi, A.: Test selection based on finite state models17(6), 591–603.https://doi.org/10.1109/ 32.87284

Fujiwara, S., V. Bochmann, G., Khendek, F., Amalou, M., Ghedamsi, A.: Test selection based on finite state models17(6), 591–603.https://doi.org/10.1109/ 32.87284

work page
[23]

In: Gramlich, B., Miller, D., Sattler, U

Gao, S., Avigad, J., Clarke, E.M.:δ-Complete Decision Procedures for Satis- fiability over the Reals. In: Gramlich, B., Miller, D., Sattler, U. (eds.) Auto- mated Reasoning, vol. 7364, pp. 286–300. Springer Berlin Heidelberg.https: //doi.org/10.1007/978-3-642-31365-3_23

work page doi:10.1007/978-3-642-31365-3_23
[24]

van Heerdt, G.: Efficient inference of mealy machines (2014)

work page 2014
[25]

In: Goubault-Larrecq, J., König, B

van Heerdt, G., Kupke, C., Rot, J., Silva, A.: Learning weighted automata over principal ideal domains. In: Goubault-Larrecq, J., König, B. (eds.) Foundations of Software Science and Computation Structures, vol. 12077, pp. 602–621. Springer InternationalPublishing(2020).https://doi.org/10.1007/978-3-030-45231-5_ 31,http://link.springer.com/10.1007/978-3-0...

work page doi:10.1007/978-3-030-45231-5_ 2020
[26]

In: Sem- pere, J.M., García, P

Heule, M., Verwer, S.: Exact DFA identification using SAT solvers. In: Sem- pere, J.M., García, P. (eds.) Grammatical Inference: Theoretical Results and Ap- plications, 10th International Colloquium, ICGI 2010, Valencia, Spain, Septem- ber 13-16, 2010. Proceedings. Lecture Notes in Computer Science, vol. 6339, pp. 66–79. Springer (2010).https://doi.org/10...

work page doi:10.1007/978-3-642-15488-1_7 2010
[27]

In: Proceedings of the 19th International Conference on Availability, Reliability and Security

Marksteiner, S., Sirjani, M., Sjödin, M.: Automated passport control: Mining and checking models of machine readable travel documents. In: Proceedings of the 19th International Conference on Availability, Reliability and Security. pp. 1–8. ARES ’24, Association for Computing Machinery (2024).https://doi.org/10. 1145/3664476.3670454,https://dl.acm.org/doi/...

work page doi:10.1145/3664476.3670454 2024
[28]

In: Ali, K., Salvaneschi, G

Moeller, M., Wiener, T., Solko-Breslin, A., Koch, C., Foster, N., Silva, A.: Automata learning with an incomplete teacher. In: Ali, K., Salvaneschi, G. (eds.) 37th European Conference on Object-Oriented Programming, ECOOP 2023, Seattle, Washington, United States, July 17-21, 2023. LIPIcs, vol. 263, pp. 21:1–21:30. Schloss Dagstuhl - Leibniz-Zentrum für In...

work page doi:10.4230/lipics.ecoop.2023.21 2023
[29]

Z3 : An efficient SMT solver

de Moura, L., Bjørner, N.: Z3: An efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) Tools and Algorithms for the Construction and Anal- ysis of Systems. pp. 337–340. Lecture Notes in Computer Science, Springer. https://doi.org/10.1007/978-3-540-78800-3_24

work page doi:10.1007/978-3-540-78800-3_24
[30]

In: Margaria, T., Graf, S., Larsen, K.G

Neider, D., Smetsers, R., Vaandrager, F., Kuppens, H.: Benchmarks for Au- tomata Learning and Conformance Testing. In: Margaria, T., Graf, S., Larsen, K.G. (eds.) Models, Mindsets, Meta: The What, the How, and the Why Not?, vol. 11200, pp. 390–416. Springer International Publishing.https://doi.org/10. 1007/978-3-030-22348-9_23

work page
[31]

Oliveira, A.L., Silva, J.P.M.: Efficient algorithms for the inference of minimum size dfas. Mach. Learn.44(1/2), 93–119 (2001).https://doi.org/10.1023/A: 1010828029885,https://doi.org/10.1023/A:1010828029885

work page doi:10.1023/a: 2001
[32]

In: Al-Onaizan, Y., Bansal, M., Chen, Y.N

Pasti, C., Karagöz, T., Nowak, F., Svete, A., Boumasmoud, R., Cotterell, R.: An l* algorithm for deterministic weighted regular languages. In: Proceedings of the 2024 Conference on Empirical Methods in Natural Language Processing. pp. 8197–8210. Association for Computational Linguistics.https://doi.org/10.18653/v1/2024. emnlp-main.468,https://aclanthology...

work page doi:10.18653/v1/2024 2024
[33]

In: Wu, J., Chanson, S.T., Gao, Q

Peled, D., Vardi, M.Y., Yannakakis, M.: Black box checking. In: Wu, J., Chanson, S.T., Gao, Q. (eds.) Formal Methods for Protocol Engineer- ing and Distributed Systems, vol. 28, pp. 225–240. Springer US (1999). https://doi.org/10.1007/978-0-387-35578-8_13,http://link.springer. com/10.1007/978-0-387-35578-8_13, series Title: IFIP Advances in Information an...

work page doi:10.1007/978-0-387-35578-8_13 1999
[34]

Proceedings of the ACM on Programming Languages10(PLDI) (Jun 2026)

Suárez Acevedo, E., Ferreira, T., Batz, K., Bøving, O., Foster, N., Silva, A.: Weighted NetKAT: A programming language for quantitative network verifica- tion. Proceedings of the ACM on Programming Languages10(PLDI) (Jun 2026). https://doi.org/10.1145/3808318

work page doi:10.1145/3808318 2026
[35]

In: Sutcliffe, G., Voronkov, A

Tabakov, D., Vardi, M.Y.: Experimental evaluation of classical automata con- structions. In: Sutcliffe, G., Voronkov, A. (eds.) Logic for Programming, Artifi- cial Intelligence, and Reasoning, vol. 3835, pp. 396–411. Springer Berlin Heidel- berg.https://doi.org/10.1007/11591191_28,http://link.springer.com/10. 1007/11591191_28, series Title: Lecture Notes ...

work page doi:10.1007/11591191_28
[36]

In: Deshmukh, J.V., Havelund, K., Perez, I

Tappler, M., Aichernig, B.K., Lorber, F.: Timed Automata Learning via SMT Solving. In: Deshmukh, J.V., Havelund, K., Perez, I. (eds.) NASA Formal Methods, vol. 13260, pp. 489–507. Springer International Publishing.https://doi.org/10. 1007/978-3-031-06773-0_26

work page
[37]

Communications of the ACM60, 86–95 (2017)

Vaandrager, F.W.: Model learning. Communications of the ACM60, 86–95 (2017). https://doi.org/10.1145/2967606

work page doi:10.1145/2967606 2017