Pith. sign in

REVIEW 3 minor 37 references

SMT-Based Active Learning of Weighted Automata

T0 review · 0 major / 3 minor · reviewed 2026-05-11 · grok-4.3

Challenge this review Download PDF Read on arXiv ↗ Review JSON

Pith's one-line read An SMT-based algorithm actively learns minimal weighted automata over any semiring and terminates for all finite cases.

desk verdict 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 →

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

Tiago Ferreira , Kevin Batz , Alexandra Silva This is my paper · ORCID
classification cs.FLcs.LG
keywords activelearningweightedautomataSMTsolversnondeterministicsemiringsformallanguages
verification ladder T0 review T1 audit T2 compute T3 formal

The pith

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

The reading

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.

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.

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.

Watch

Extended reading notes

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.

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.

Share X Bluesky LinkedIn Reddit HN

Signed reviews

No signed human review yet.

Request a human review

A listed scientist reviews the paper for a fee and the review publishes here regardless of verdict. See the reviewers or get listed.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit.

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)
  1. 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.
  2. 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.
  3. 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 · score 0.0 of 10

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.

Assumptions & free parameters 0 free parameters · 0 assumptions · 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.

how reviews work

0 comments
Cite this review

Pith. "Pith review of SMT-Based Active Learning of Weighted Automata." pith.science (2026). https://pith.science/paper/2605.07758

@misc{pith2026260507758,
  author       = {Pith},
  title        = {Pith review of: SMT-Based Active Learning of Weighted Automata},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/2605.07758}},
  note         = {Machine review of arXiv:2605.07758}
}
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.

Figures

Figures reproduced from arXiv: 2605.07758 by the authors.

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 of suitable… 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 log￾log, 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 effi￾ciency, … view at source ↗
Figures from the paper (1 more)
Figure 4
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…

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

37 extracted references · 37 canonical work pages

  1. [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. [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. [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. [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. [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. [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. [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. [8]

    ACM Program

    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

Show all 37 references
  1. [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

    1996 doi

  2. [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

    1972 doi

  3. [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

  4. [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

    2013 doi

  5. [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

    doi

  6. [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...

    2015 doi

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

    2018 doi

  8. [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

    2025 doi

  9. [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: ...

    2001 doi

  10. [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...

    doi

  11. [19]

    Zenodo (Apr 2026).https://doi.org/10.5281/ZENODO

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

    2026 doi

  12. [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

    doi

  13. [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

    2016 doi

  14. [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

  15. [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

    doi

  16. [24]

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

    2014

  17. [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:...

    2020 doi

  18. [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 Not...

    2010 doi

  19. [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 M...

    2024 doi

  20. [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, 2...

    2023 doi

  21. [29]

    In: Ramakrishnan, C.R., Rehof, J

    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

    doi

  22. [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 Publi...

  23. [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

    2001 doi

  24. [32]

    In: Proceedings of the 2024 Conference on Empirical Methods in Natural Language Processing

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

    2024 doi

  25. [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....

    1999 doi

  26. [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

    2026 doi

  27. [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/1159119...

    doi

  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

  29. [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

    2017 doi

Pith tools

Reviewed May 11, 2026 · model on record in the stance chip above.