Pith. sign in

REVIEW 3 major objections 6 minor 58 references

Syntropy steers language models with multiparty session types so they generate deadlock-free protocol refinements at 95–99% validity.

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 · grok-4.5

2026-07-31 21:59 UTC pith:ZJELEPT7

load-bearing objection Solid first synthesis pipeline for async multiparty subtypes; headline validity is intentionally checker-backed, which is a design choice more than a hidden flaw. the 3 major comments →

arxiv 2607.27964 v1 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 generationsession 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.

Distributed systems break when components communicate in the wrong order; even small protocol changes can create deadlocks. This paper claims that large language models can systematically invent safe protocol refinements if generation is guided by multiparty session types and checked against asynchronous subtyping. The authors build Syntropy: models are fine-tuned on session-type pairs, then decode under a two-level monitor that prunes impossible prefixes and verifies finished candidates. Across five open models the method keeps syntactic correctness high and lifts semantic validity into the mid-to-high nineties, while still producing structurally varied refinements rather than copies of the original. A reader who maintains microservices or concurrent code cares because the work turns an undecidable, error-prone manual task into a reproducible synthesis pipeline that preserves deadlock freedom by construction.

Core claim

Syntropy shows that embedding asynchronous multiparty subtyping constraints into LLM generation—via LoRA fine-tuning on (supertype, subtype) pairs plus two-level monitoring—yields protocol refinements accepted as valid subtypes at 95.6%–99.5% rates while retaining high syntactic correctness and non-trivial diversity across multiple open models.

What carries the argument

Two-level constrained generation: Level 1 is a cheap per-token derivative feasibility check on partial session trees that prunes impossible beams; Level 2 is a widening-based fixpoint SimCheck that accepts only complete candidates sound under asynchronous multiparty subtyping.

Load-bearing premise

Validity is scored by a sound but incomplete subtyping checker that also shaped most of the training labels, so the reported percentages are lower bounds and large or borderline protocols may be systematically filtered out.

What would settle it

Run an independent, more complete asynchronous-subtyping decision procedure (or exhaustive human audit) on the accepted outputs for the 100 held-out supertypes; if a substantial fraction of ‘valid’ subtypes are rejected, or if identity subtypes of large protocols that the checker currently discards prove unsafe when substituted, the central validity claim fails.

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

If this is right

  • Protocol evolution in distributed systems can be assisted by automatically proposing deadlock-free local-type alternatives instead of hand-written refinements.
  • Open 7B–32B code models, once fine-tuned and monitored this way, can match or exceed frontier models on coverage of protocol specifications while remaining locally deployable.
  • The same two-level monitor pattern can be reused for other behavioural guarantees that admit a sound (even incomplete) tree or automaton checker.
  • Training data scale saturates around ~9,500 pairs, so further gains must come from better constraints or diversity incentives rather than more labelled subtypes alone.

Where Pith is reading between the lines

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

  • If the incomplete checker is the bottleneck, pairing Syntropy with a complete binary-session checker or interactive theorem prover could raise true semantic coverage on large recursive protocols.
  • The same prefix-derivative idea may transfer to synthesising refinements of choreographies or temporal-logic contracts where partial traces already decide unsatisfiability.
  • Persistent bias toward variance over reordering suggests that decoding objectives that explicitly reward anticipation depth could unlock more of the asynchronous refinement space.

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 presents Syntropy, a framework that combines LoRA fine-tuning of open LLMs with MPST-guided prompting and a two-level constrained decoding procedure (token-level derivative feasibility plus a widening-based fixpoint SimCheck adapted from Bocchi et al.) to synthesise asynchronous multiparty subtypes of a given session type. The goal is automatic protocol refinement that preserves communication safety and deadlock freedom. Evaluation on literature-derived and synthetic supertypes across five open models reports 95.4%–98.1% syntactic validity and 95.6%–99.5% semantic validity under monitoring, with ablations on prompting, fine-tuning, monitoring, and data scale, plus a coverage comparison against two frontier models.

Significance. Automatic synthesis of asynchronous multiparty subtypes is genuinely hard: AMS is undecidable, and prior work supplies checkers rather than generators. Coupling LLMs with a sound AMS monitor is a natural and previously unexplored bridge between generative models and session-type refinement. The multi-model evaluation, component ablations, data-scale sweep, transformation-category breakdown, and public artifacts (code, models, data) are real strengths and make the empirical claims inspectable. If the framing of guarantees is tightened to match the incomplete oracle, the work is a solid contribution at the SE/formal-methods interface and a useful template for verifier-in-the-loop protocol synthesis.

major comments (3)
  1. [§4.1.3, Table 3, Abstract, Algorithm 1] §4.1.3, Table 3, and the abstract state 95.6%–99.5% “validity,” but semantic validity is defined as acceptance by the sound-but-incomplete checker of Bocchi et al. [6] (SimCheck in Algorithm 1, Level 2). The paper correctly notes incompleteness and size cutoffs in §4.1.1 and §4.6, yet the headline claim and abstract do not present these rates as lower bounds on true AMS, nor quantify how often Level-1-feasible complete candidates are rejected by Level 2 or refused for size. Because accepted outputs are valid by construction whenever Level 2 accepts, the central empirical claim should be restated as high acceptance into [6]’s sound fragment under beam search, with explicit lower-bound language in the abstract and §4.2.
  2. [§4.1.1 Dataset Construction] §4.1.1 constructs synthetic and enriched literature training pairs with a heuristic “inspired by” the same asynchronous subtyping algorithm and filters them with the same checker (99.13% / 97.97% acceptance). Combined with test-time SimCheck, this couples the learned distribution to the oracle’s accepted fragment. The ablations show that monitoring and fine-tuning both matter, but they do not separate “learning AMS structure” from “steering into patterns the checker already accepts.” A load-bearing clarification is needed: either a held-out analysis (e.g., manual or alternative-tool inspection of samples near the checker’s blind spots / size threshold), or a clearly scoped claim that Syntropy targets the decidable fragment checked by [6], not full AMS.
  3. [§4.2–§4.5, Fig. 7, Table 6] Diversity and “non-trivial refinements” are supported mainly by rule histograms (Fig. 7–8), branch/message averages (Table 3–4), and two hand-chosen structural cases (Table 6). There is no baseline that applies the same Level-1/Level-2 monitors without a fine-tuned LLM (e.g., grammar-constrained or heuristic search over the transformation rules in Table 1), nor a measure of distinctness up to α-renaming/trivial unfold. Without that, it remains unclear how much of the reported coverage and diversity is due to the LLM versus the formal search envelope. A modest baseline or a normalised uniqueness metric on the test set would make the synthesis claim proportionate to the evidence.
minor comments (6)
  1. [Abstract, §1] Abstract and Introduction use “guaranteed behavioural correctness” without immediately qualifying that guarantees hold for Level-2-accepted outputs under a sound incomplete procedure. Align wording with §3.2.2’s conservative-checker discussion.
  2. [§2 Motivation] Fig. 1–3 motivation (federated learning) is helpful, but the evaluation never returns to end-to-end multiparty composition (global type / relative deadlock freedom of a full system after substituting a refined local type). A short discussion of what local AMS guarantees for the system would help non-MPST readers.
  3. [§4.7] §4.7 compares frontier models under the “same prompts” and default decoding. Briefly note that the BNF-style session-type encoding and transformation vocabulary were co-designed with fine-tuning, so low coverage may partly reflect format mismatch rather than pure capability.
  4. [Table 1, §1–§2] Table 1 “Subtying” → “Subtyping”; occasional spacing issues (“Ensuringbehavioural”, “enforcs”, “MPSTfurther”). A pass for compound-word spacing and typos would help.
  5. [§3.2.2, §4.2.2] Report beam size k used in the main tables and whether temperature scaling for CodeLlama (T=1.2) was applied only for diversity plots or also for Table 3 validity numbers.
  6. [Data Availability Statement] Data availability DOIs are welcome; ensure the anonymous Zenodo links in the camera-ready point to the final non-anonymous release and pin checker [6] version/commit used for all reported rates.

Circularity Check

2 steps flagged

Monitored semantic validity is nearly tautological (Ω only retains SimCheck accepts), and training pairs are filtered by the same external AMS checker used at test time; synthesis content is otherwise non-circular.

specific steps
  1. self definitional [§3.2.2 Algorithm 1 lines 11–13; §4.1.3 metric (2); Table 3 “With Monitoring” Sem.%]
    "if SimCheck(Tf, TS) then Ω ← Ω ∪ {seq′} ... Semantic Validity. The proportion of syntactically valid subtypes accepted by the subtyping checker in [6], used as a proxy for semantic correctness. ... With Monitoring ... Sem.(%) ... 99.2 / 99.5 / 95.7 / 96.4 / 95.6"

    Under constrained generation, membership in the reported output set Ω is defined by passing SimCheck (the [6] checker). Semantic validity is defined as the same acceptance predicate. For the monitored pipeline, high Sem.% is therefore true largely by construction of the retention rule, not by an independent test of whether retained strings are AMS subtypes. (Residual sub-100% figures do not remove the definitional alignment of metric and filter.)

  2. fitted input called prediction [§4.1.1 Subtype Generation and Validation; training set description]
    "For synthetic supertypes, subtypes are generated through a heuristic procedure inspired by an asynchronous subtyping algorithm [6] and validated using its checker. ... additional subtypes are generated using the same procedure and validated accordingly. Validation results show that 99.13% of subtypes from literature-derived supertypes ... and 97.97% from synthetic supertypes are accepted."

    Supervised targets are not independent AMS ground truth; they are samples already accepted (or produced under) the same incomplete oracle later used as Level-2 and as the semantic-validity metric. The model is trained to imitate that oracle’s accepted fragment, then scored on how often monitored outputs land in that fragment—statistically coupled train/label/test labeling, analogous to fitting a labeling function and calling agreement a prediction. This biases diversity and headline validity toward [6]’s decidable subset without proving completeness on subtypes [6] rejects.

full rationale

Syntropy’s load-bearing correctness claim is not a first-principles derivation of asynchronous multiparty subtyping; it is LLM proposal plus an external sound (incomplete) checker from Bocchi et al. [6]. That is standard verifier-in-the-loop synthesis, not self-definition of AMS. Two mild circularity-adjacent facts remain. (1) With two-level monitoring, Algorithm 1 adds a completed candidate to Ω only if SimCheck(Tf, TS) holds, while “semantic validity” is defined as acceptance by that same checker—so the headline 95.6–99.5% figures for the monitored pipeline largely measure that the filter is applied, not an independent discovery of AMS. (2) Synthetic and enriched literature training pairs were themselves produced by a heuristic “inspired by” [6] and retained only when that checker accepted them (99.13% / 97.97%), so the model is steered into [6]’s accepted fragment and evaluated inside it. Neither step is author-self-citation of a uniqueness theorem, fitted physical parameters renamed as predictions, or renaming of a known empirical law. Ablations still show non-trivial content: without monitoring, semantic validity falls to ~60%, and diversity/coverage claims are separate from the tautological filter. Score 3 reflects metric-by-construction and same-oracle train/test coupling without collapsing the central engineering claim.

Axiom & Free-Parameter Ledger

5 free parameters · 5 axioms · 2 invented entities

The central empirical claim rests on standard LLM fine-tuning practice, the existing sound-but-incomplete AMS theory/checkers, and engineering choices (beam size, LoRA rank, weighted loss, data mixture). No new physical entities are postulated; the main substantive assumptions are that checker acceptance is a useful proxy for semantic validity and that the curated/synthetic subtype distribution is representative enough for the reported generalisation.

free parameters (5)
  • LoRA rank / alpha / dropout = 64 / 32 / 0.05
    Rank 64, α=32, dropout 0.05 chosen as training configuration; affects capacity and what patterns are learned.
  • Weighted token loss (subtype vs auxiliary) = 1.0 / 0.2
    Weights 1.0 on subtype tokens and 0.2 on labels/counts are hand-chosen weak-supervision knobs.
  • Beam size k and top-2k expansion = beam k; expand top-2k
    Search width directly controls which candidates reach Level-2 checking and reported diversity.
  • Training mixture size and balance across rules = 10800 pairs (100 lit-derived + 604 synthetic supertypes in train)
    704 supertypes / 10800 pairs with approximate balance over Identity/RefA/RefB/RefIn/RefOut/Unfold; composition is a design choice that shapes measured validity and diversity.
  • Stochastic beam temperature for CodeLlama = T=1.2
    T=1.2 introduced so CodeLlama produces RefA/RefB diversity under default settings it lacked.
axioms (5)
  • domain assumption Asynchronous multiparty subtyping (AMS) as defined by Ghilezan et al. is a sound characterisation of deadlock-freedom-preserving protocol refinement.
    Invoked throughout §§2–3 as the semantic target of synthesis; taken from cited theory.
  • domain assumption The derivative/widening checker of Bocchi et al. [6] is sound (accepted ⇒ true subtype) though incomplete.
    Level-2 SimCheck and the semantic-validity metric rest on this; paper states incompleteness and size limits explicitly.
  • domain assumption Session types may be faithfully encoded in the linearised BNF-style syntax (REC_X_OPEN/CLOSE, lbrace/rbrace) without changing AMS semantics.
    §3.1 claims the adaptation preserves semantics while aiding sequence modelling.
  • domain assumption Standard transformer next-token prediction with LoRA can learn structure-preserving subtype transformations from paired examples.
    Background assumption of Syntropy-Train; not proved, supported empirically.
  • ad hoc to paper Beam search plus Level-1 feasible-prefix over-approximation preserves all potentially valid completions that the beam would otherwise explore.
    Design justification in §3.2.2; relative to non-exhaustive beam search and infinite subtype space.
invented entities (2)
  • Syntropy two-level monitor (Level-1 derivative Feasible + Level-2 widening SimCheck integrated into LLM decoding) independent evidence
    purpose: Filter tokens and final candidates so generation stays inside AMS constraints while retaining diversity.
    Engineering assembly of prior subtyping machinery into constrained decoding; not a new mathematical object, but the paper’s main procedural contribution.
  • Heuristic transformation labels (Identity, RefA, RefB, RefIn, RefOut, Unfold) as weak supervision no independent evidence
    purpose: Condition the model on named AMS-allowed moves and analyse diversity.
    Labels are auxiliary and acknowledged as non-canonical when multiple rules apply; used for training signals and reporting.

pith-pipeline@v1.2.0-daily-grok45 · 28249 in / 3635 out tokens · 63995 ms · 2026-07-31T21:59:16.186646+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 ↗

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 · 6 canonical work pages

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

    work page 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...

    work page 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

    work page 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

    work page 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

    work page 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...

    work page 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