Pith. sign in

REVIEW 3 major objections 6 minor 58 references

Syntropy shows that an LLM can generate deadlock-free protocol refinements when every output token is checked against multiparty session types.

Reviewed by Pith at T0; open to challenge. T0 means a machine referee read the full paper against a public rubric. the ladder, T0–T4 →

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗

T0 review · deepseek-v4-flash

2026-08-04 03:15 UTC pith:ZJELEPT7

load-bearing objection The case for Syntropy is real, but the headline validity numbers contradict the paper's own algorithm; the evaluation needs a major rework before the result can be trusted. the 3 major comments →

arxiv 2607.27964 v2 pith:ZJELEPT7 submitted 2026-07-30 cs.SE cs.AI

Specification-Guided Synthesis of Deadlock-Free Communication Protocol Refinements with Large Language Models

Yang Li , Ping Hou , Nobuko Yoshida This is my paper
classification cs.SE cs.AI
keywords formal specificationslarge language modelsprotocol refinementbehavioural correctnessconstrained generationmultiparty session typesasynchronous subtypingdeadlock freedom
verification ladder T0 review T1 audit T2 compute T3 formal T4 reserved

The pith

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

Communication protocols evolve, but a small change such as reordering two messages can silently introduce a deadlock. This paper argues that protocol refinement can be formalised as asynchronous multiparty subtyping, and that a large language model can be taught and constrained to generate such refinements automatically. The framework, Syntropy, encodes a protocol as a session tree, fine-tunes an open-weight LLM on valid refinement patterns, and runs a two-level monitor that prunes infeasible prefixes token by token and verifies completed candidates with a full subtyping check. The paper reports 95.6–99.5% semantic validity across several open-weight language models while keeping syntactic correctness above 95% and producing structurally distinct refinements. A sympathetic reader would care because this points toward LLM-generated code with behavioural guarantees rather than merely plausible syntax.

Core claim

On the paper's own terms, the discovery is that an LLM can be turned into a reliable generator of protocol refinements if the subtyping relation is pushed into the generation loop. Given a supertype session type, Syntropy fine-tunes the model on six structure-preserving transformations — identity, recursion unfold, input reordering, output reordering, input contravariance, and output covariance — then, during decoding, a derivative-based feasibility check rejects any prefix that cannot be completed to a valid subtype, and a widening-based fixpoint checker accepts only completed candidates that are genuine asynchronous subtypes. The result is that accepted outputs are safe replacements: they

What carries the argument

The central object is the asynchronous multiparty subtyping relation, which says when one session type can safely replace another under FIFO communication. Syntropy represents each protocol as a session tree, encodes the six subtyping rules as prompt guidance, and couples a LoRA-fine-tuned LLM with two monitors: Level 1 performs a token-level derivative feasibility check on the partial session tree, pruning prefixes that cannot lead to a valid subtype; Level 2 runs a widening-based fixpoint subtype checker on each completed tree. Level 1 is a cheap over-approximation that preserves all potentially valid candidates, and Level 2 is a sound-but-incomplete conservative filter that guarantees acc

Load-bearing premise

The whole guarantee rests on the automated checker that approves each refinement being sound — it must never accept a protocol substitution that could in fact introduce a deadlock — and on its size limit (roughly 701 grammar units) not excluding the protocols people actually need.

What would settle it

Feed Syntropy a supertype larger than 701 grammar units: if even the identity refinement is rejected by the checker, the framework cannot refine the protocols at the top of its claimed range. Alternatively, take an accepted refinement, substitute it into a running MPST implementation of the federated-learning protocol, and exercise all message orderings; a single deadlock would show the checker is not sound and the validity figure is not a guarantee.

Watch this falsifier — get emailed when new claim-graph text bears on it.

If this is right

  • Accepted refinements are genuine asynchronous subtypes, so substituting them into an MPST-typed system preserves communication safety and deadlock freedom.
  • Semantic validity jumps from roughly 49–66% with direct generation to 96–99.5% with two-level monitoring, isolating monitoring as the decisive component.
  • The framework generalises across model families: five different open-weight models all land in the 95.4–98.1% syntactic and 95.6–99.5% semantic validity ranges.
  • Fine-tuning saturates at about 9,500 training pairs, so the approach is reproducible with moderate compute and predictable cost.
  • Out-of-the-box frontier models cover only 4–18% of the test supertypes, while every fine-tuned model covers 100%, indicating that specification-guided fine-tuning, not raw model scale, is what buys coverage.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • The two-level pattern — cheap per-token over-approximation plus an expensive sound final check — transfers naturally to other synthesis tasks with undecidable or semi-decidable validation, such as temporal-logic or contract synthesis.
  • The paper's own limitation statement means the reported validity does not yet apply to very large protocols; the 701-grammar-unit ceiling suggests a compositional or modular refinement strategy as the next step.
  • The model's preference for variance over reordering transformations hints that generation difficulty is uneven; rebalancing training data or adding reordering-specific rewards could steer outputs toward richer structural changes.
  • One testable extension: use Syntropy to generate batches of guaranteed-safe protocol variants as regression suites for existing session-type toolchains, turning the verifier into a diversity generator.

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

3 major / 6 minor

Summary. The paper introduces Syntropy, a framework for synthesizing refinements (subtypes) of multiparty session types using fine-tuned LLMs with two-level monitoring. It fine-tunes several open-weight code LLMs via LoRA on (supertype, subtype) pairs, using transformation rules (Identity, RefA, RefB, RefIn, RefOut, Unfold) as structured guidance, and then constrains generation with a token-level derivative feasibility check and a final sound-but-incomplete subtyping checker (SimCheck). Evaluations on literature-derived and synthetic datasets report 95.4–98.1% syntactic validity and 95.6–99.5% semantic validity across five LLMs, plus ablations, data-scale studies, and a comparison with frontier models on coverage.

Significance. If the validity results are correct, Syntropy is a noteworthy integration of formal session-type theory with LLM constrained decoding: it demonstrates that specification-guided generation plus a verifier can yield high-quality, diverse protocol refinements, with a public artifact and reproducible training/evaluation pipeline. The paper's honesty about checker incompleteness and size limitations, its multi-model ablations, and its comparison with frontier LLMs are strengths. However, the central validity claim is currently undermined by a metric inconsistency that must be resolved before the contribution can be assessed.

major comments (3)
  1. [§3.2.2 (Algorithm 1) and §4.1.3 / Table 3] Algorithm 1 adds a candidate to the output set Ω only when SimCheck returns true at EOS (lines 12-13). The semantic validity metric in §4.1.3 is defined as the proportion of syntactically valid outputs accepted by the same [6] checker. Therefore, for the 'With Monitoring' condition, semantic validity evaluated on the actual output set must be 100%. Table 3 reports values 95.6–99.5%, and Tables 5-6 report several acceptance rates below 100% (e.g., 87.1%, 92.2%, 94.6%). This is a direct internal contradiction. Either the evaluation denominator includes syntactically valid candidates that were rejected by Level 2 and are not in Ω, or the metric is computed on a different, unspecified set. The headline statement 'Syntropy achieves 95.6%-99.5% validity' needs to be redefined and recomputed with a clearly stated evaluation set.
  2. [§4.1.3 and §3.2.2] Even if the denominator issue is fixed, the semantic validity metric is circular: the system's Level 2 acceptance filter and the evaluation metric use the same checker. Thus the reported semantic validity is essentially a property of the filter, not an independent measure of the LLM's ability to generate semantically correct refinements. The paper should separate generator quality from end-to-end filtered output: for example, report raw LLM validity before Level 2 (as in the 'No Monitoring' condition) and state explicitly that the filtered output is valid by construction whenever the checker is sound. This distinction is essential for interpreting the ablation in Figure 9 and the RQ1 answers.
  3. [§4.1.1 / §2] The paper acknowledges that the checker of [6] is sound but incomplete and that it cannot handle protocols above roughly 701 grammar units, so even identity subtypes may be rejected. Since this checker is both the guarantee mechanism for deadlock freedom and the evaluation oracle, the paper's central guarantee is conditional on the soundness of [6]. This is acceptable if stated prominently, but the abstract and conclusion currently phrase the guarantee unconditionally. Please add an explicit caveat in the abstract/conclusion and, ideally, report how many test supertypes fall within the checker's size limit, so readers can judge the practical scope of the framework.
minor comments (6)
  1. [Algorithm 1] The pseudocode is ambiguous: the 'else' on line 14 appears to attach to the SimCheck 'if', adding rejected EOS candidates to C, but then line 16 sets Beams←Top_k(C), which could reselect candidates that have already reached EOS. Please clarify the control flow, especially how C is reset across decoding steps.
  2. [§4.1.3] Semantic validity is described as a lower bound because the checker is incomplete, but Tables 3, 5, and 6 report these values as plain percentages without a footnote. Add a note that all semantic-validity figures are lower bounds relative to the true subtype relation.
  3. [References] References [53] and [54] appear to be the same paper (NL2CTL) with identical titles and overlapping metadata, likely a duplication. Please consolidate.
  4. [Figure 4] The figure contains typos ('Traing Data', 'Subtying Rules') and some labels are very small. Please fix and increase readability.
  5. [§4.2.1] The statement 'each supertype yields approximately 5 subtypes per rule' is unclear about whether this is per generation call or averaged over the test set. Please clarify the denominator.
  6. [§4.7] The frontier-model comparison uses coverage as the key metric, but the gap in coverage (18% and 4% vs. 100%) is reported without confidence intervals or error bars. At minimum, state the number of supertypes in the test set (100) and the variance across repeated runs.

Circularity Check

1 steps flagged

Semantic validity is defined and computed with the same SimCheck predicate that Algorithm 1 uses to select the output set, so the headline validity is forced by construction; the reported sub-100% numbers are inconsistent with this and cannot describe the constrained outputs.

specific steps
  1. self definitional [Algorithm 1, Level 2 (lines 12-13, §3.2.2); Semantic Validity metric (2), §4.1.3; Table 3]
    "if SimCheck(T f,T S) then Ω←Ω∪{seq′} ... Semantic Validity. The proportion of syntactically valid subtypes accepted by the subtyping checker in [6], used as a proxy for semantic correctness."

    Ω is defined as exactly the set of candidates for which SimCheck returns true, while semantic validity is defined as the fraction of outputs accepted by that same checker. Therefore, applied to Syntropy-Gen's output, semantic validity is not an empirical property of the LLM's refinements; it is the Level-2 acceptance predicate restated. It equals 100% on Ω by construction. The reported 95.6–99.5% values in Table 3 are also inconsistent with this: if the metric were computed on the final output set it would be 100%, and if it were computed on the pre-filter pool it would not measure the constrained system. Either way, the headline 'validity' reduces to the filter rather than being predicted from the generation model.

full rationale

The central circularity is metric/filter identity: the paper evaluates 'semantic validity' using the same SimCheck oracle that defines the accepted output set in Algorithm 1. This makes the headline validity tautological for the constrained system and, as reported, internally inconsistent. The other load-bearing ingredients are not circular: the AMS formalism [22] is published external work (and formalized in Rocq [18]); the checker [6] is not authored by the present authors and is an external, sound-but-incomplete oracle; self-citations such as [7,15] are benchmark sources only. The deadlock-freedom guarantee is inherited from the subtyping theorem plus the checker's soundness, which is a threat to validity, not circularity. The paper also contains independent content (syntactic validity, transformation diversity, no-monitoring baseline, frontier-model comparison), so the circularity is partial rather than total.

Axiom & Free-Parameter Ledger

3 free parameters · 5 axioms · 0 invented entities

The central claims rest on the soundness of an external checker (from [6]) for both filtering and evaluation, plus the authors' own prior theory ([22]) for the refinement semantics. The transformation-rule prompt is an ad hoc generative prior. No new physical or theoretical entities are introduced.

free parameters (3)
  • loss weight for auxiliary fields (labels, n_subtypes) = 0.2
    Hand-chosen in §3.1 to deprioritize weak supervision signals; affects what the model learns and thus generation diversity/validity.
  • temperature for stochastic beam search = 1.2
    Applied for CodeLlama-7B in §4.2.2 to restore transformation diversity; other models use default. Hand-tuned, not swept.
  • beam size k
    Algorithm 1 parameterizes beam search on k but the paper never states the value used in experiments; load-bearing for diversity and validity.
axioms (5)
  • domain assumption The asynchronous subtyping checker from [6] is sound (accepted ⇒ valid subtype) and its acceptance is the correct ground truth for semantic validity.
    Used both as the system's Level 2 filter (§3.2.2) and as the evaluation metric (§4.1.3). If the checker is unsound, the central validity claims fail.
  • domain assumption Asynchronous multiparty subtyping (AMS) from [22] preserves deadlock freedom and communication safety; a subtype can safely replace its supertype.
    This is the theoretical foundation (§2). The paper relies on it, but it is cited prior work by the authors' group.
  • ad hoc to paper The transformation rules in Table 1 (Identity, Unfold, RefA, RefB, RefIn, RefOut) instantiate the subtyping rules R1, R2, C1, C2 and form a sufficient basis for generating a representative subtype space.
    The prompt conditions the LLM on these rules (§3.1); if the set is not representative, diversity and coverage claims are weaker.
  • domain assumption The Level 1 Feasible predicate is an over-approximation that prunes no prefix extendable to a valid subtype.
    Stated in §3.2.2 without proof; if wrong, valid refinements are lost, harming coverage/diversity.
  • standard math Asynchronous subtyping is undecidable in general, so any complete decision procedure is impossible; a sound-but-incomplete checker is the right oracle.
    From [8,27]; motivates the checker-based design. Not controversial.

pith-pipeline@v1.3.0-alltime-deepseek · 22581 in / 17548 out tokens · 670435 ms · 2026-08-04T03:15:53.700385+00:00 · methodology

0 comments
read the original abstract

Ensuring behavioural correctness in communication protocols is a central challenge in distributed software systems, as subtle inconsistencies can lead to deadlocks. In such settings, protocol refinement - the safe substitution of a protocol that preserves correctness and compatibility with other components - is essential. Large language models (LLMs) have demonstrated strong capabilities in code generation and program synthesis, yet lack mechanisms to reliably produce outputs with correct behaviour. Formal specification approaches, such as multiparty session types (MPST), offer rigorous guarantees, including deadlock freedom, but provide limited support for automatically constructing protocol refinements. In this paper, we present Syntropy, a framework for synthesising protocol refinements guided by MPST specifications and LLMs. It incorporates refinement constraints directly into the generation process, ensuring the generated variants satisfy these guarantees. Our comprehensive evaluation indicates that Syntropy achieves 95.6%-99.5% validity while maintaining high syntactic correctness, and produces diverse, non-trivial refinements across multiple LLMs.

Figures

Figures reproduced from arXiv: 2607.27964 by Nobuko Yoshida, Ping Hou, Yang Li.

Figure 1
Figure 1. Figure 1: Federated learning protocol p? updp q? updq m! std p? . . . . . . wtd p? . . . . . . (a) Session tree Ta for 𝑇a q? updq p? updp m! std q? . . . . . . wtd q? . . . . . . (b) Session tree T ′ a for 𝑇 ′ a [PITH_FULL_IMAGE:figures/full_fig_p002_1.png] view at source ↗
Figure 3
Figure 3. Figure 3: FSMs for role a We evaluate Syntropy on two datasets, comprising protocols derived from the literature and synthetic benchmarks, using multi￾ple LLMs of varying sizes: three 7B code models, a general-purpose 7B model, and a 32B model. Syntropy attains 95.6%–99.5% va￾lidity across all models, while maintaining strong syntactic cor￾rectness (95.4%–98.1%). Furthermore, it produces multiple distinct refinement… view at source ↗
Figure 4
Figure 4. Figure 4: Overview of Syntropy to deadlock. This highlights the challenge of designing correct re￾finements and motivates the application of formal specifications to ensure the rigorous synthesis of protocol refinements that preserve communication properties. MPST and Asynchronous Subtyping. Multiparty Session Types (MPST) [24, 44] provide a framework for specifying and verifying communication protocols. In MPST, th… view at source ↗
Figure 5
Figure 5. Figure 5: Training dynamics across LLMs 0 1 2 3 4 Training Tokens ×10 6 0 1 2 3 4 5 Training Loss 0.121 2.7 4.2 (a) Training Loss vs Tokens (Window size 5) 0 1 2 3 4 Training Tokens ×10 6 0.6 0.8 1 2 4 Gradient Norm (log scale) 0.121 2.7 4.2 (b) Gradient Norm vs Tokens (Window size 5) 0 1 2 3 4 Training Tokens ×10 6 0.0 0.5 1.0 1.5 2.0 Learning Rate ×10 4 0.121 2.7 4.2 (c) Learning Rate vs Tokens 602 9500 10800 [PI… view at source ↗
Figure 7
Figure 7. Figure 7: Transformation distribution across LLMs 0 2500 5000 7500 10000 12500 15000 17500 20000 Transformation Count 1320 705 2956 12328 2517 797 237 925 924 1495 2465 264 432 393 458 458 982 1909 139 2480 245 362 768 1371 261 1834 576 601 1052 2577 153 2969 263 427 701 1701 216 1977 w/o w/ 0 w/o w/ 602 w/o w/ 9500 w/o w/ 10800 Rules RefA RefB RefIn RefOut Identity Unfold (a) Transformation distribution across data… view at source ↗
Figure 9
Figure 9. Figure 9: Ablation results across metrics on Qwen2.5-Coder-7B Fig. 8a and Fig. 8b. Additional metrics and computational costs are reported in [PITH_FULL_IMAGE:figures/full_fig_p009_9.png] view at source ↗

Review history (2 revisions) →

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Reference graph

Works this paper leans on

58 extracted references · 11 linked inside Pith

  1. [1]

    Agrawal, Aditya Kanade, Navin Goyal, Shuvendu K

    Lakshya A. Agrawal, Aditya Kanade, Navin Goyal, Shuvendu K. Lahiri, and Sriram K. Rajamani. 2023. Monitor-Guided Decoding of Code LMs with Static Analysis of Repository Context. InAdvances in Neural Information Processing Systems 36: Annual Conference on Neural Information Processing Systems 2023, NeurIPS 2023, New Orleans, LA, USA, December 10 - 16, 2023...

    2023

  2. [2]

    Nye, Maarten Bosma, Henryk Michalewski, David Dohan, Ellen Jiang, Carrie J

    Jacob Austin, Augustus Odena, Maxwell I. Nye, Maarten Bosma, Henryk Michalewski, David Dohan, Ellen Jiang, Carrie J. Cai, Michael Terry, Quoc V. Le, and Charles Sutton. 2021. Program Synthesis with Large Language Models. CoRRabs/2108.07732 (2021). arXiv:2108.07732 https://arxiv.org/abs/2108.07732

    Pith/arXiv arXiv 2021

  3. [3]

    Luca Beurer-Kellner, Marc Fischer, and Martin T. Vechev. 2023. Prompting Is Programming: A Query Language for Large Language Models.Proc. ACM Program. Lang.7, PLDI (2023), 1946–1969. doi:10.1145/3591300

    doi:10.1145/3591300 2023

  4. [4]

    Luca Beurer-Kellner, Marc Fischer, and Martin T. Vechev. 2024. Guiding LLMs The Right Way: Fast, Non-Invasive Constrained Generation. InForty-first Inter- national Conference on Machine Learning, ICML 2024, Vienna, Austria, July 21-27, 2024 (Proceedings of Machine Learning Research, Vol. 235), Ruslan Salakhutdi- nov, Zico Kolter, Katherine A. Heller, Adri...

    2024

  5. [5]

    Laura Bocchi, Andy King, and Maurizio Murgia. 2024. Asynchronous Subtyping by Trace Relaxation. InTools and Algorithms for the Construction and Analysis of Systems - 30th International Conference, TACAS 2024, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2024, Luxembourg City, Luxembourg, April 6-11, 2024, Procee...

    doi:10.1007/978-3-0 2024

  6. [6]

    Laura Bocchi, Andy King, Maurizio Murgia, and Simon Thompson. 2025. Abstract Subtyping for Asynchronous Multiparty Sessions. In36th International Confer- ence on Concurrency Theory, CONCUR 2025, Aarhus, Denmark, August 26-29, 2025 (LIPIcs, Vol. 348), Patricia Bouyer and Jaco van de Pol (Eds.). Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 10:1–10:19....

    doi:10.4230/lipics.concur.2025 2025

  7. [7]

    Mario Bravetti, Marco Carbone, Julien Lange, Nobuko Yoshida, and Gianluigi Zavattaro. 2019. A Sound Algorithm for Asynchronous Session Subtyping. In 30th International Conference on Concurrency Theory, CONCUR 2019, Amsterdam, The Netherlands, August 27-30, 2019 (LIPIcs, Vol. 140), Wan J. Fokkink and Rob van Glabbeek (Eds.). Schloss Dagstuhl - Leibniz-Zent...

    doi:10.4230/lipics.concur.2019.38 2019

  8. [8]

    Mario Bravetti, Marco Carbone, and Gianluigi Zavattaro. 2017. Undecidability of asynchronous session subtyping.Inf. Comput.256 (2017), 300–320. doi:10.1016/J. IC.2017.07.010

    doi:10.1016/j 2017

  9. [9]

    Mark Chen, Jerry Tworek, Heewoo Jun, Qiming Yuan, Henrique Pondé de Oliveira Pinto, Jared Kaplan, Harri Edwards, Yuri Burda, Nicholas Joseph, Greg Brockman, Alex Ray, Raul Puri, Gretchen Krueger, Michael Petrov, Heidy Khlaaf, Girish Sastry, Pamela Mishkin, Brooke Chan, Scott Gray, Nick Ryder, Mikhail Pavlov, Alethea Power, Lukasz Kaiser, Mohammad Bavarian...

    Pith/arXiv arXiv 2021

  10. [10]

    Tzu-Chun Chen, Mariangiola Dezani-Ciancaglini, and Nobuko Yoshida. 2024. On the Preciseness of Subtyping in Session Types: 10 Years Later. InProceedings of the 26th International Symposium on Principles and Practice of Declarative Programming, PPDP 2024, Milano, Italy, September 9-11, 2024, Alessandro Bruni, Alberto Momigliano, Matteo Pradella, Matteo Ros...

    arXiv 2024

  11. [11]

    Tzu-Chun Chen, Mariangiola Dezani-Ciancaglini, Alceste Scalas, and Nobuko Yoshida. 2017. On the Preciseness of Subtyping in Session Types.Logical Methods in Computer Science13, 2 (2017). doi:10.23638/LMCS-13(2:12)2017

    doi:10.23638/lmcs-13(2:12)2017 2017

  12. [12]

    Yongchao Chen, Rujul Gandhi, Yang Zhang, and Chuchu Fan. 2023. NL2TL: Trans- forming Natural Languages to Temporal Logics using Large Language Models. InProceedings of the 2023 Conference on Empirical Methods in Natural Language Processing, Houda Bouamor, Juan Pino, and Kalika Bali (Eds.). Association for Computational Linguistics, Singapore, 15880–15903....

    doi:10.18653/v1/2023.emnlp- 2023

  13. [13]

    Bharath Chintagunta, Namit Katariya, Xavier Amatriain, and Anitha Kannan

  14. [14]

    Matthias Cosler, Christopher Hahn, Daniel Mendoza, Frederik Schmitt, and Caroline Trippel. 2023. nl2spec: Interactively Translating Unstructured Natural Language to Temporal Logics with Large Language Models. InComputer Aided Verification - 35th International Conference, CA V 2023, Paris, France, July 17- 22, 2023, Proceedings, Part II (Lecture Notes in C...

    doi:10.1007/978-3-031- 2023

  15. [15]

    Zak Cutner, Nobuko Yoshida, and Martin Vassor. 2022. Deadlock-free asynchro- nous message reordering in rust with multiparty session types. InPPoPP ’22: 27th ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming, Seoul, Republic of Korea, April 2 - 6, 2022, Jaejin Lee, Kunal Agrawal, and Michael F. Spear (Eds.). ACM, 246–261. doi:10.114...

    arXiv 2022

  16. [16]

    DeepSeek-AI. 2026. DeepSeek-V4: Towards Highly Efficient Million-Token Con- text Intelligence. arXiv:2606.19348 https://arxiv.org/abs/2606.19348

    arXiv 2026

  17. [17]

    Nicola Dragoni, Saverio Giallorenzo, Alberto Lluch-Lafuente, Manuel Mazzara, Fabrizio Montesi, Ruslan Mustafin, and Larisa Safina. 2017. Microservices: Yester- day, Today, and Tomorrow. InPresent and Ulterior Software Engineering, Manuel Mazzara and Bertrand Meyer (Eds.). Springer, 195–216. doi:10.1007/978-3-319- 67425-4_12

    doi:10.1007/978-3-319- 2017

  18. [18]

    Burak Ekici and Nobuko Yoshida. 2026. Formalising Asynchronous Session Subtyping.ACM Trans. Comput. Logic27, 3, Article 18 (June 2026), 45 pages. doi:10.1145/3815176

    doi:10.1145/3815176 2026

  19. [19]

    Francesco Fuggitti and Tathagata Chakraborti. 2023. NL2LTL - a Python Package for Converting Natural Language (NL) Instructions to Linear Temporal Logic (LTL) Formulas. InThirty-Seventh AAAI Conference on Artificial Intelligence, AAAI 2023, Thirty-Fifth Conference on Innovative Applications of Artificial Intelligence, IAAI 2023, Thirteenth Symposium on Ed...

    2023

  20. [20]

    Saibo Geng, Martin Josifoski, Maxime Peyrard, and Robert West. 2023. Grammar- Constrained Decoding for Structured NLP Tasks without Finetuning. InProceed- ings of the 2023 Conference on Empirical Methods in Natural Language Process- ing, EMNLP 2023, Singapore, December 6-10, 2023, Houda Bouamor, Juan Pino, and Kalika Bali (Eds.). Association for Computati...

    doi:10.18653/v1/2023.emnlp-main.674 2023

  21. [21]

    Silvia Ghilezan, Svetlana Jaksic, Jovanka Pantovic, Alceste Scalas, and Nobuko Yoshida. 2019. Precise subtyping for synchronous multiparty sessions.J. Log. Algebraic Methods Program.104 (2019), 127–173. doi:10.1016/J.JLAMP.2018.12.002

    doi:10.1016/j.jlamp.2018.12.002 2019

  22. [22]

    Silvia Ghilezan, Jovanka Pantović, Ivan Prokić, Alceste Scalas, and Nobuko Yoshida. 2023. Precise Subtyping for Asynchronous Multiparty Sessions.ACM Transactions on Computational LogicVolume 24, Issue 2, 14 (2023), 1–73. doi:10. 1145/3568422

    2023

  23. [23]

    Kohei Honda, Vasco Thudichum Vasconcelos, and Makoto Kubo. 1998. Lan- guage Primitives and Type Discipline for Structured Communication-Based Programming. InESOP. doi:10.1007/BFb0053567

    doi:10.1007/bfb0053567 1998

  24. [24]

    Kohei Honda, Nobuko Yoshida, and Marco Carbone. 2016. Multiparty Asynchro- nous Session Types.J. ACM63, 1, Article 9 (2016). doi:10.1145/2827695

    doi:10.1145/2827695 2016

  25. [25]

    Binyuan Hui, Jian Yang, Zeyu Cui, Jiaxi Yang, Dayiheng Liu, Lei Zhang, Tianyu Liu, Jiajun Zhang, Bowen Yu, Keming Lu, Kai Dang, Yang Fan, Yichang Zhang, An Yang, Rui Men, Fei Huang, Bo Zheng, Yibo Miao, Shanghaoran Quan, Yunlong Feng, Xingzhang Ren, Xuancheng Ren, Jingren Zhou, and Junyang Lin. 2024. Qwen2.5-Coder Technical Report. arXiv:2409.12186 [cs.CL...

    Pith/arXiv arXiv 2024

  26. [26]

    Brendan McMahan, Brendan Avent, Aurélien Bellet, Mehdi Bennis, Arjun Nitin Bhagoji, Kallista A

    Peter Kairouz, H. Brendan McMahan, Brendan Avent, Aurélien Bellet, Mehdi Bennis, Arjun Nitin Bhagoji, Kallista A. Bonawitz, Zachary Charles, Graham Cormode, Rachel Cummings, Rafael G. L. D’Oliveira, Hubert Eichner, Salim El Rouayheb, David Evans, Josh Gardner, Zachary Garrett, Adrià Gascón, Badih Ghazi, Phillip B. Gibbons, Marco Gruteser, Zaïd Harchaoui, ...

    2021

  27. [27]

    Julien Lange and Nobuko Yoshida. 2017. On the Undecidability of Asynchronous Session Subtyping. InFoundations of Software Science and Computation Structures - 20th International Conference, FOSSACS 2017, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2017, Uppsala, Sweden, April 22-29, 2017, Proceedings (Lecture N...

    doi:10.1007/978-3-662- 2017

  28. [28]

    Edward A. Lee. 2008. Cyber Physical Systems: Design Challenges. In2008 11th IEEE International Symposium on Object and Component-Oriented Real-Time Distributed Computing (ISORC). 363–369. doi:10.1109/ISORC.2008.25

    doi:10.1109/isorc.2008.25 2008

  29. [29]

    Raymond Li, Loubna Ben Allal, Yangtian Zi, Niklas Muennighoff, Denis Kocetkov, Chenghao Mou, Marc Marone, Christopher Akiki, Jia Li, Jenny Chim, Qian Liu, Evgenii Zheltonozhskii, Terry Yue Zhuo, Thomas Wang, Olivier Dehaene, Mishig Davaadorj, Joel Lamy-Poirier, João Monteiro, Oleh Shliazhko, Nicolas Gontier, Nicholas Meade, Armel Zebaze, Ming-Ho Yee, Loge...

  30. [30]

    Xiaohan Lin, Qingxing Cao, Yinya Huang, Haiming Wang, Jianqiao Lu, Zhengying Liu, Linqi Song, and Xiaodan Liang. 2024. FVEL: Interactive Formal Verification Environment with Large Language Models via Theorem Proving. In Advances in Neural Information Processing Systems 38: Annual Conference on Neu- ral Information Processing Systems 2024, NeurIPS 2024, Va...

    2024

  31. [31]

    Zhi Ma, Cheng Wen, Zhexin Su, Xiao Liang, Cong Tian, Shengchao Qin, and Mengfei Yang. 2025. Bridging Natural Language and Formal Specification- Automated Translation of Software Requirements to LTL via Hierarchical Se- mantics Decomposition Using LLMs. In40th IEEE/ACM International Conference on Automated Software Engineering, ASE 2025, Seoul, Korea, Repu...

    arXiv 2025

  32. [32]

    Wooldridge, and Philip Torr

    Samuele Marro, Emanuele La Malfa, Jesse Wright, Guohao Li, Nigel Shadbolt, Michael J. Wooldridge, and Philip Torr. 2024. A Scalable Communication Pro- tocol for Networks of Large Language Models.CoRRabs/2410.11905 (2024). arXiv:2410.11905 doi:10.48550/ARXIV.2410.11905

    Pith/arXiv arXiv doi:10.48550/arxiv.2410.11905 2024

  33. [33]

    Daniel Melcer, Nathan Fulton, Sanjay Krishna Gouda, and Haifeng Qian

  34. [34]

    Daniel Mendoza, Christopher Hahn, and Caroline Trippel. 2024. Translating Natural Language to Temporal Logics with Large Language Models and Model Checkers. InFormal Methods in Computer-Aided Design, FMCAD 2024, Prague, Czech Republic, October 15-18, 2024, Nina Narodytska and Philipp Rümmer (Eds.). IEEE, 1–11. doi:10.34727/2024/ISBN.978-3-85448-065-5_17

    doi:10.34727/2024/isbn.978-3-85448-065-5_17 2024

  35. [35]

    Niels Mündler, Jingxuan He, Hao Wang, Koushik Sen, Dawn Song, and Martin T. Vechev. 2025. Type-Constrained Code Generation with Language Models.Proc. ACM Program. Lang.9, PLDI (2025), 601–626. doi:10.1145/3729274

    doi:10.1145/3729274 2025

  36. [36]

    Shaan Nagy, Timothy Zhou, Nadia Polikarpova, and Loris D’Antoni. 2026. Chop- Chop: A Programmable Framework for Semantically Constraining the Output of Language Models.Proc. ACM Program. Lang.10, POPL (2026), 1905–1932. doi:10.1145/3776708

    doi:10.1145/3776708 2026

  37. [37]

    OpenAI. 2026. Introducing GPT-5.5. https://openai.com/index/introducing-gpt- 5-5/. Accessed: June 2026

    2026

  38. [38]

    Kanghee Park, Timothy Zhou, and Loris D’Antoni. 2025. Flexible and Efficient Grammar-Constrained Decoding. arXiv:2502.05111 [cs.CL] https://arxiv.org/ abs/2502.05111

    Pith/arXiv arXiv 2025

  39. [39]

    Plummer, Zhaoran Wang, and Hongxia Yang

    Chau Pham, Boyi Liu, Yingxiang Yang, Zhengyu Chen, Tianyi Liu, Jianbo Yuan, Bryan A. Plummer, Zhaoran Wang, and Hongxia Yang. 2024. Let Models Speak Ciphers: Multiagent Debate through Embeddings. InThe Twelfth International Conference on Learning Representations, ICLR 2024, Vienna, Austria, May 7-11,

    2024

  40. [40]

    Gabriel Poesia, Alex Polozov, Vu Le, Ashish Tiwari, Gustavo Soares, Christopher Meek, and Sumit Gulwani. 2022. Synchromesh: Reliable Code Generation from Pre-trained Language Models. InThe Tenth International Conference on Learning Representations, ICLR 2022, Virtual Event, April 25-29, 2022. OpenReview.net. https://openreview.net/forum?id=KmtVD97J43e

    2022

  41. [41]

    Sunil Prakash. 2026. LDP: An Identity-Aware Protocol for Multi-Agent LLM Systems. arXiv:2603.08852 [cs.AI] https://arxiv.org/abs/2603.08852

    arXiv 2026

  42. [42]

    Qwen, :, An Yang, Baosong Yang, Beichen Zhang, Binyuan Hui, Bo Zheng, Bowen Yu, Chengyuan Li, Dayiheng Liu, Fei Huang, Haoran Wei, Huan Lin, Jian Yang, Jianhong Tu, Jianwei Zhang, Jianxin Yang, Jiaxi Yang, Jingren Zhou, Junyang Lin, Kai Dang, Keming Lu, Keqin Bao, Kexin Yang, Le Yu, Mei Li, Mingfeng Xue, Pei Zhang, Qin Zhu, Rui Men, Runji Lin, Tianhao Li,...

    Pith/arXiv arXiv 2025

  43. [43]

    https://openreview.net/forum?id=sehRvaIPQQ

    OpenReview.net. https://openreview.net/forum?id=sehRvaIPQQ

  44. [44]

    Alceste Scalas and Nobuko Yoshida. 2019. Less is More: Multiparty Session Types Revisited.Proc. ACM Program. Lang.3, POPL, Article 30 (Jan. 2019), 29 pages. doi:10.1145/3290343

    doi:10.1145/3290343 2019

  45. [45]

    Deshmukh, and Yiannis Kantaros

    David Smith Sundarsingh, Jun Wang, Jyotirmoy V. Deshmukh, and Yiannis Kantaros. 2026. ConformalNL2LTL: Translating Natural Language Instruc- tions into Temporal Logic Formulas with Conformal Correctness Guarantees. arXiv:2504.21022 [cs.CL] https://arxiv.org/abs/2504.21022

    arXiv 2026

  46. [46]

    Tadahiro Taniguchi, Ryo Ueda, Tomoaki Nakamura, Masahiro Suzuki, and Akira Taniguchi. 2025. Generative Emergent Communication: Large Language Model is a Collective World Model.CoRRabs/2501.00226 (2025). arXiv:2501.00226 doi:10.48550/ARXIV.2501.00226

    Pith/arXiv arXiv doi:10.48550/arxiv.2501.00226 2025

  47. [47]

    Baptiste Rozière, Jonas Gehring, Fabian Gloeckle, Sten Sootla, Itai Gat, Xi- aoqing Ellen Tan, Yossi Adi, Jingyu Liu, Tal Remez, Jérémy Rapin, Artyom Kozhevnikov, Ivan Evtimov, Joanna Bitton, Manish Bhatt, Cristian Canton- Ferrer, Aaron Grattafiori, Wenhan Xiong, Alexandre Défossez, Jade Copet, Faisal Azhar, Hugo Touvron, Louis Martin, Nicolas Usunier, Th...

    Pith/arXiv arXiv doi:10.48550/arxiv.2308.12950 2023

  48. [48]

    Ashish Vaswani, Noam Shazeer, Niki Parmar, Jakob Uszkoreit, Llion Jones, Aidan N Gomez, Ł ukasz Kaiser, and Illia Polosukhin. 2017. Attention is All you Need. InAdvances in Neural Information Processing Systems, I. Guyon, U. Von Luxburg, S. Bengio, H. Wallach, R. Fergus, S. Vishwanathan, and R. Garnett (Eds.), Vol. 30. Curran Associates, Inc. https://proc...

    2017

  49. [49]

    Saurous, and Yoon Kim

    Bailin Wang, Zi Wang, Xuezhi Wang, Yuan Cao, Rif A. Saurous, and Yoon Kim. 2023. Grammar Prompting for Domain-Specific Language Genera- tion with Large Language Models. InAdvances in Neural Information Pro- cessing Systems 36: Annual Conference on Neural Information Processing Sys- tems 2023, NeurIPS 2023, New Orleans, LA, USA, December 10 - 16, 2023, Ali...

    2023

  50. [50]

    Zhongyi Wang, Tengjie Lin, Mingshuai Chen, Mingqi Yang, Haokun Li, Xiao Yi, Shengchao Qin, and Jianwei Yin. 2025. Preguss: It Analyzes, It Specifies, It Verifies. arXiv:2508.14532 [cs.SE] https://arxiv.org/abs/2508.14532

    Pith/arXiv arXiv 2025

  51. [51]

    Shubham Ugare, Tarun Suresh, Hangoo Kang, Sasa Misailovic, and Gagandeep Singh. 2025. SynCode: LLM Generation with Grammar Augmentation.Transac- tions on Machine Learning Research2025 (2025). https://openreview.net/forum? id=HiUZtgAPoH

    2025

  52. [52]

    Nobuko Yoshida. 2024. Programming Language Implementations with Multiparty Session Types. InActive Object Languages: Current Research Trends, Frank S. de Boer, Ferruccio Damiani, Reiner Hähnle, Einar Broch Johnsen, and Eduard Kamburjan (Eds.). Lecture Notes in Computer Science, Vol. 14360. Springer, 147–165. doi:10.1007/978-3-031-51060-1_6

    doi:10.1007/978-3-031-51060-1_6 2024

  53. [53]

    Mengyan Zhao, Ran Tao, Yanhong Huang, Jianqi Shi, Shengchao Qin, and Yang Yang. 2024. NL2CTL: Automatic Generation of Formal Requirements Specifica- tions via Large Language Models. InFormal Methods and Software Engineering: 25th International Conference on Formal Engineering Methods, ICFEM 2024, Hi- roshima, Japan, December 2–6, 2024, Proceedings(Hiroshi...

    doi:10.1007/978-981-96-0617-7_1 2024

  54. [54]

    Mengyan Zhao, Ran Tao, Yanhong Huang, Jianqi Shi, Shengchao Qin, and Yang Yang. 2024. NL2CTL: Automatic Generation of Formal Requirements Specifi- cations via Large Language Models. InFormal Methods and Software Engineer- ing - 25th International Conference on Formal Engineering Methods, ICFEM 2024, Hiroshima, Japan, December 2-6, 2024, Proceedings (Lectu...

    doi:10.1007/978-9 2024

  55. [55]

    Willard and Rémi Louf

    Brandon T. Willard and Rémi Louf. 2023. Efficient Guided Generation for Large Language Models. arXiv:2307.09702 [cs.CL] https://arxiv.org/abs/2307.09702

    Pith/arXiv arXiv 2023

  56. [2021]

    InProceedings of the 6th Machine Learning for Healthcare Conference (Proceedings of Machine Learning Research, Vol

    Medically Aware GPT-3 as a Data Generator for Medical Dialogue Sum- marization. InProceedings of the 6th Machine Learning for Healthcare Conference (Proceedings of Machine Learning Research, Vol. 149), Ken Jung, Serena Yeung, Mark Sendak, Michael Sjoding, and Rajesh Ranganath (Eds.). PMLR, 354–372. https://proceedings.mlr.press/v149/chintagunta21a.html

  57. [2023]

    StarCoder: may the source be with you!Trans. Mach. Learn. Res.2023 (2023). https://openreview.net/forum?id=KoFOg41haE

    2023

  58. [2024]

    arXiv:2402.17988 [cs.PL] https://arxiv.org/abs/2402.17988

    Constrained Decoding for Fill-in-the-Middle Code Language Mod- els via Efficient Left and Right Quotienting of Context-Sensitive Grammars. arXiv:2402.17988 [cs.PL] https://arxiv.org/abs/2402.17988

    Pith/arXiv arXiv