Translating Federated Learning Algorithms in Python into CSP Processes Using ChatGPT

Ilija Basicevic; Marko Popovic; Miodrag Djukic; Miroslav Popovic

REVIEW 3 major objections 5 minor 15 references

Translating Federated Learning Algorithms in Python into CSP Processes Using ChatGPT

T0 review · 3 major / 5 minor · reviewed 2026-08-07 · deepseek-v4-flash

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

Pith's one-line read A prompt-driven process translates Python federated learning algorithms into CSP processes verified by the PAT model checker.

desk verdict A useful, honest case study of LLM-assisted Python-to-CSP# translation that is undermined by a printed translation rule contradicting its own outputs. read the letter →

arxiv 2506.07173 v2 pith:35XARGOT submitted 2025-06-08 cs.AI

Miroslav Popovic , Marko Popovic , Miodrag Djukic , Ilija Basicevic This is my paper

classification cs.AI

keywords federatedlearningCSPCSP#modelcheckingChatGPTformalverificationPythonprocessalgebra

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 claims that the previously manual step of translating Python federated learning algorithms into process-algebra models can be automated with ChatGPT-4o. The proposed translation process iterates between giving ChatGPT a minimal context that explains the testbed's message-passing API and its mapping to CSP# channels, letting it produce CSP# code, and checking that code with the model checker PAT for deadlock-freedom, reachability of termination, and liveness. The claim is validated on two generic algorithms: a centralized server/client federated learning algorithm, which translated on the first attempt, and a decentralized algorithm with two message phases, which required four iterations and six manual error corrections. If the process holds, formal verification of federated orchestration protocols becomes accessible to developers who write plain Python, without a separate rewriting step or specialized CSP expertise.

What carries the argument

The central mechanism is the MPAPI translation table embedded in the prompt. CSP# is the dialect of CSP supported by the model checker PAT; the table maps the four Python messaging calls sendMsg, rcvMsg, broadcastMsg, and rcvMsgs onto channel send and receive events and recursive process definitions. The same table dictates that multi-field messages become dot-separated compound channel messages and that Python list buffers translate to channels. This translation table is load-bearing because PAT verifies only the generated CSP# model; the mapping is what connects the verified model back to the original Python source.

What would settle it

A concrete falsifier is to take a Python federated learning algorithm with a deliberately inserted communication bug, such as one client that never calls sendMsg, and run the full prompt-to-CSP# process; if the generated CSP# model still passes PAT's deadlock and liveness assertions, the translation rules do not preserve the Python control flow.

Watch

Extended reading notes

Core claim

On its own terms, the paper's discovery is that a small, hand-written translation rulebook is enough to make ChatGPT-4o produce CSP# models that pass exhaustive model checking. The rulebook fixes the bridge: sendMsg(address, msg) becomes nodeChannels[nodeId]!msg, rcvMsg() becomes nodeChannels[nodeId]?msg, messages with several fields become dot-separated compound channel events, broadcastMsg and rcvMsgs become tail-recursive processes, and Python list buffers used as FIFO queues become channels whose append and pop(0) are send and receive. Under this mapping, ChatGPT-4o generated the final CSP# processes for the centralized federated learning algorithm in the first iteration and for the decentralized algorithm in the fourth iteration after manual corrections, and PAT validated deadlock-freedom as well as the termination and liveness assertions on both. The paper treats this as evidence that the orchestration protocols of the generic centralized and decentralized federated learning algorithms are correct and that the translation bottleneck can be removed.

Load-bearing premise

The load-bearing premise is that the prompt's translation rules, which turn sendMsg and rcvMsg into channel events and list buffers into channels, faithfully capture what the Python testbed's messaging API actually does, because PAT checks the generated model and not the Python source.

Editorial extensions

If this is right

The centralized and decentralized generic federated learning orchestration protocols are PAT-verified as deadlock-free and as reaching termination, for the modeled configurations of three nodes and three iterations.
Translation of federated learning algorithms into CSP no longer requires first rewriting the code into a restricted actor model; the original Python code can be the direct input to the process.
ChatGPT's own feedback on the most and least useful parts of the prompt gives a practical way to shrink contexts and reduce the cost of LLM-assisted translation.
Human correction remains part of the process: every syntax and logical error in the tested cases was found and fixed by people, so the method currently reduces rather than removes human effort.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

The same iterate-prompt-check-correct loop should transfer to other Python-to-formal-model translations, such as TLA+, mCRL2, or Promela, since nothing in the method is specific to CSP# except the translation table.
The paper verifies only small configurations with three nodes and three iterations; scaling to larger systems would likely strain PAT's state-space limits, so abstraction or symbolic techniques would be needed, which the paper does not address.
A stronger validation would compare message traces of the generated CSP# model against traces of the original Python algorithm under the same schedules, testing whether the translation preserves communication behavior and not just termination.

Share X Bluesky LinkedIn Reddit HN

Editorial analysis

A structured set of objections, weighed in public.

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

Desk Editor's Note

read the letter

Colleague,

Here's the short version: the paper shows ChatGPT-4o, with a human in the loop, can translate two PTB-FLA Python functions into CSP# models that pass PAT deadlock-freedom and termination checks. That is a real, modest result. The prompts and feedback questionnaires are included, which is helpful for anyone trying to reproduce or extend the workflow.

What's worth credit: the authors document the syntax and logic errors ChatGPT made and the manual fixes needed. They are honest in the conclusion that humans must correct all errors. For a short conference paper, that is a fair amount of transparency.

The soft spots, in order of seriousness. First, the printed translation rules in Table I are inconsistent with the validated outputs. The rule says sendMsg(address, msg) becomes nodeChannels[nodeId]!msg, which would send to the sender's own channel. But Table II's client uses nodeChannels[FlSrvId]!ldata, and Table IV uses nodeChannels[msgSrcAdr]! and DrainBuffer forwards to msgSrcAdr. So either the rule is a typo in the paper or ChatGPT silently corrected it. The paper never explains this. This is not a trivial nit: the rule is the load-bearing bridge between Python semantics and CSP#. PAT verifies the CSP# model, not the translation. If the rule is wrong, the verification says nothing about the Python code. The paper needs to fix the table or state explicitly that ChatGPT was given the correct rule.

Second, there are no PAT scripts, logs, or the exact ChatGPT conversation history, so the claims are not independently reproducible. Third, the 'minimality of context' is based on ChatGPT's self-reported feedback, which isn't a real measure.

The stress-test note is right about the inconsistency. I'd still send this to a serious referee, because the core experiment is coherent and the issue is correctable. The paper is for people working on LLM-assisted formal verification or using PTB-FLA. It does not change FL or formal methods, but it's a useful data point. I would not cite it in my own work until the mapping issue is resolved.

Recommendation: send it to peer review with a request that the authors fix the translation-rule table and provide artifacts.

Referee Report

3 major / 5 minor

Summary. The paper presents an iterative, ChatGPT-based translation process that takes Python implementations of two generic federated learning algorithms from the PTB-FLA framework and produces CSP# models for verification with the PAT model checker. The process consists of building a context prompt with MPAPI translation rules, asking ChatGPT to generate the CSP# code, and then iteratively fixing errors until PAT validates the model. The authors report successful translation for both a centralized and a decentralized FL algorithm, with PAT checks for deadlock freedom, reachability of a termination flag, and a liveness property. They also ask ChatGPT to rate the difficulty and to identify the most and least useful parts of the prompt, which they use as an estimate of context minimality.

Significance. If the approach works as claimed, it is a useful case study in using LLMs to reduce the manual effort of formalizing distributed orchestration protocols. The paper contributes concrete prompts, final CSP# process definitions, and an honest account of the manual corrections required. The central evidence, however, is weaker than the abstract suggests: PAT verifies properties of the generated CSP# model, but the paper does not demonstrate that this model faithfully corresponds to the original Python behavior. Moreover, the published translation rule for sendMsg is internally inconsistent with the reported outputs. The two case studies are still valuable as empirical data points, and the limitations section is candid about the need for human correction. The main claims need to be sharpened and the translation rules corrected before the paper can be accepted.

major comments (3)

[Section III, Table I (and analogously Table III)] The stated translation rule for sendMsg is erroneous as printed. Table I says: 'the call sendMsg(address, msg) translates to nodeChannels[nodeId]!msg', which sends to the sender's own channel and ignores the address parameter. The same problem appears in the broadcastMsg example, which loops over all nodes except the sender rather than over the addresses argument. Yet the PAT-validated outputs in Tables II and IV correctly use nodeChannels[FlSrvId]!ldata and nodeChannels[msgSrcAdr]!..., respectively, so the reported outputs contradict the stated rule. Since these translation rules are the core of the 'context' contribution, the paper must either correct the rule (e.g., to nodeChannels[address]!msg) and explain why ChatGPT's outputs diverged from it, or the claim that PAT verifies the Python-to-CSP# translation is unsupported. This is not a cosmetic issue: a reader following the published rule would generate a different, non-equivalent CSP# model.
[Section III.B/III.C and Abstract] The experimental validation checks only deadlock-freedom, reachability of the terminated flag, and the liveness property []<> Terminated of the generated CSP# model. It does not check that the model is behaviorally equivalent to the original Python function. The abstract's claim of 'successful translation (verified by the model checker PAT)' therefore overstates what PAT establishes. The paper should either supply an explicit correspondence argument between the Python MPAPI semantics and the generated CSP# channels and processes, or rephrase the claim to 'the generated CSP# model satisfies the specified properties.' Without such a mapping, PAT success does not certify that the Python algorithms were translated correctly.
[Section II step (4) and Section IV] The paper's own conclusion states that 'humans must manually correct all the errors made by ChatGPT,' and Section II explicitly includes a manual-modification step. In the decentralized case, the authors report that finding two logical errors required significant effort, including analysis of PAT log files and simulation traces. In this light, the abstract and introduction characterize the process as 'automated translation' too strongly. The process is ChatGPT-assisted, semi-automated translation. The wording should be adjusted throughout, and the amount and kind of human intervention should be stated in the abstract, because it materially affects what the method contributes.

minor comments (5)

[Section III, Table I] The table uses the term '#CSP' in several places; this should be 'CSP#' for consistency with the rest of the paper.
[Section III.B, Table II] The parenthetical explanation says the syntax error was corrected 'by replacing ";" for "->"' but the preceding sentence says ChatGPT used '->' instead of ';'. The wording should be reversed: '->' was replaced by ';'.
[Section III.C, Table IV] The comment for Syntax error 4, Correction 2 says 'parameter ldata was missing, so it was added before the parameter count,' but the actual corrected line in Table IV shows 'DrainBuffer(nodeId, iterNo, ldata, call(ccount, dataFromClients1[nodeId]))'. It would be clearer to state that the parameter was added to both the definition and the call sites.
[Section II and III] The minimality of the context is estimated from ChatGPT's self-reported feedback (difficulty rating and redundant parts). This is a subjective measure, not an independent evaluation. The paper should explicitly acknowledge that the minimality claim is based on the LLM's own report and is not verified by an external metric.
[Section III] No PAT scripts, configuration files, or verification logs are provided. The paper would be substantially easier to reproduce and check if the complete runnable CSP# models, together with the exact PAT commands and outputs, were included in an appendix or a public repository.

Circularity Check

0 steps flagged · score 0.0 of 10

No significant circularity: external PAT checks and self-contained prompts; self-citations are scaffolding; flagged translation-rule inconsistency is a correctness gap, not a circular reduction.

full rationale

The derivation chain is: (1) the authors write a prompt that embeds MPAPI-to-CSP# translation rules and a CSP# skeleton with properties; (2) ChatGPT fills in the process definitions; (3) humans correct syntax and logic errors; (4) PAT checks deadlock-freedom and termination. Nothing in this chain defines the output in terms of the property being proved, nor fits a parameter to a target and then re-predicts it. PAT is an external checker, and the generated CSP# code is not an input to the prompt, so the central claim of successful translation verified by PAT has independent empirical content. The many same-author citations ([2]-[7]) are motivational and scaffolding; the current validation does not rest on [6] or [7] for its correctness. The ChatGPT questionnaire used to estimate context minimality is self-reported, making that estimate weak, but that is an evidentiary weakness rather than a circular argument. I explicitly flag two correctness concerns that do not rise to circularity: the printed rule in Table I ('the call sendMsg (address, msg) translates to nodeChannels [nodeId]!msg') is inconsistent with the PAT-validated outputs in Tables II and IV, which use nodeChannels[FlSrvId]!ldata and nodeChannels[msgSrcAdr]!..., respectively; and the conclusion admits 'humans must manually correct all the errors made by ChatGPT.' These mean PAT verifies properties of the final model, not the fidelity of the stated translation rule or the autonomy of the pipeline, but neither is an Eq. X = Eq. Y reduction. Therefore no circular step is established.

Assumptions & free parameters 0 free parameters · 4 assumptions · 0 invented entities

No free parameters are fitted; the ChatGPT hyperparameters are fixed defaults. The paper's central claim rests on the fidelity of prompt-level translation rules and on PAT properties being the right ones. No new physical or mathematical entities are introduced.

assumptions (4)

domain assumption The MPAPI translation rules in the prompt preserve Python semantics (sendMsg, rcvMsg, broadcastMsg, rcvMsgs, list buffers map to channels and recursion).
PAT verifies the translated CSP# model, not the Python code. If the mapping is unfaithful, verification does not transfer to the original algorithm. Location: Section III, Table I context.
domain assumption Deadlock freedom and termination are sufficient to establish the claimed safety and liveness of the FL algorithms.
The abstract claims safety and liveness verification, but the stated properties are only deadlockfree and reaches or eventually Terminated. No explicit safety invariant is defined. Location: Tables I and IV.
domain assumption fl_centralized and fl_decentralized represent the PTB-FLA generic algorithms.
The experimental validation uses exactly two functions from the authors' own framework, with no argument that other algorithms in the framework are similar. Location: Section III.
standard math PAT is a sound model checker for CSP#.
The paper treats PAT's validation as authoritative; this is a standard tooling assumption. Location: Section II, step 3.

how reviews work

0 comments

Cite this review

Pith. "Pith review of Translating Federated Learning Algorithms in Python into CSP Processes Using ChatGPT." pith.science (2026). https://pith.science/paper/35XARGOT

@misc{pith2026250607173,
  author       = {Pith},
  title        = {Pith review of: Translating Federated Learning Algorithms in Python into CSP Processes Using ChatGPT},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/35XARGOT}},
  note         = {Machine review of arXiv:2506.07173}
}

read the original abstract

The Python Testbed for Federated Learning Algorithms is a simple Python FL framework that is easy to use by ML&AI developers who do not need to be professional programmers and is also amenable to LLMs. In the previous research, generic federated learning algorithms provided by this framework were manually translated into the CSP processes and algorithms' safety and liveness properties were automatically verified by the model checker PAT. In this paper, a simple translation process is introduced wherein the ChatGPT is used to automate the translation of the mentioned federated learning algorithms in Python into the corresponding CSP processes. Within the process, the minimality of the used context is estimated based on the feedback from ChatGPT. The proposed translation process was experimentally validated by successful translation (verified by the model checker PAT) of both generic centralized and decentralized federated learning algorithms.

Discussion (0). Sign in to comment.

Reference graph

Works this paper leans on

15 extracted references · 10 canonical work pages

[1]

Accessed: 10.01.2025 [Online]

TaRDIS: Trustworthy And Resilient Decentralised Intelligence For Edge Systems . Accessed: 10.01.2025 [Online]. Available: https://www.project-tardis.eu/

work page 2025
[2]

A Simple Python Testbed for Federated Learning Algorithms,

M. Popovic, M. Popovic, I. Kastelan, M. Djukic, and S. Ghilezan, “A Simple Python Testbed for Federated Learning Algorithms,” in Proc. of the 2023 Zooming Innovation in Consumer Technologies Conference, pp. 148 -153, 2023. DOI: 10.1109/ZINC58345.2023.10173859

work page arXiv 2023
[3]

A Federated Learning Algorithms Development Paradigm,

M. Popovic, M. Popovic, I. Kastelan, M. Djukic, and I. Basicevic, “A Federated Learning Algorithms Development Paradigm,” in: J. Kofron, T. Margaria, C. Seceleanu (eds.) Engineering of Computer- Based Systems, LNCS, Springer, Cham, vol. 14390, pp. 26 –41,

work page
[4]

Developing Elementary Federated Learning Algorithms Leveraging the ChatGPT,

M. Popovic, M. Popovic, I. Kastelan, M. Djukic, I. Basicevic, “Developing Elementary Federated Learning Algorithms Leveraging the ChatGPT,” in Proc. 31st IEEE Telecommunications Forum, pp. 1 -4, 2023. DOI: 10.1109/TELFOR59449.2023.10372714

work page arXiv 2023
[5]

PTB-FLA Development Paradigm Adaptation for ChatGPT,

M. Popovic, M. Popovic, I. Kastelan, M. Djukic, I. Basicevic, “PTB-FLA Development Paradigm Adaptation for ChatGPT,” Computer Science and Information Systems, vol. 21, no. 4, pp. 1269-1292, 2024. DOI: 10.2298/CSIS231224036P

work page doi:10.2298/csis231224036p 2024
[6]

Correct orchestration of Federated Learning generic algorithms: formalisation and verification in CSP,

I. Prokić, S. Ghilezan, S. Kašterović, M. Popovic, M. Popovic, I. Kaštelan, “Correct orchestration of Federated Learning generic algorithms: formalisation and verification in CSP,” in: J. Kofron, T. Margaria, C. Seceleanu (eds.) Engineering of Computer -Based Systems, LNCS, Springer, Cham, vol. 14390, pp. 274 -288, 2024. DOI: 10.1007/978-3-031-49252-5_25

work page doi:10.1007/978-3-031-49252-5_25 2024
[7]

Correct orchestration of Federated Learning generic algorithms: Python translation t o CSP and verification by PAT,

M. Djukic, I. Prokić, M. Popovic, S. Ghilezan, M. Popovic, S. Prokić, “Correct orchestration of Federated Learning generic algorithms: Python translation t o CSP and verification by PAT,” , International Journal on Software Tools for Technology Transfer (STTT), in press (should apper in Q1 2025)

work page 2025
[8]

Accessed: 20.01.2025 [Online]

Number of ChatGPT Users ( Jan 2025) by Fabio Duarte . Accessed: 20.01.2025 [Online]. Available: https://explodingtopics.com/blog/chatgpt-users

work page 2025

Show all 15 references

[9]

GPT-4 Technical Report,

OpenAI, “GPT-4 Technical Report,” arXiv:2303.08774v6, 2024

2024 arXiv
[10]

Sparks of artificial general intelligence: Early experiments with GPT-4,

S. Bubeck, V. Chandrasekaran, R. Eldan, J. Gehrke, E. Horvitz, E. Kamar, P. Lee, Y.T. Lee, Y. Li, S. Lundberg, H. Nori, H. Palangi, M.T. Ribeiro, Y. Zhang , “Sparks of artificial general intelligence: Early experiments with GPT-4,” arXiv:2303.12712v5, 2023

2023 arXiv
[11]

HuggingGPT: Solving AI Tasks with ChatGPT and its Friends in Hugging Face ,

Y. Shen, K. Song, X. Tan, D. Li, W. Lu, Y. Zhuang, “HuggingGPT: Solving AI Tasks with ChatGPT and its Friends in Hugging Face ,” arXiv:2303.17580v4, 2024

2024 arXiv
[12]

Large Language Models Empowered Autonomous Edge AI for Connected Intelligence,

Y. Shen, J. Shao, X. Zhang, Z. Lin, H. Pan, D. Li, J. Zhang, K.B. Letaief, “Large Language Models Empowered Autonomous Edge AI for Connected Intelligence, ” in IEEE Communications Magazine, vol. 62, no. 10, pp. 140 -146, October 2024, DOI: 10.1109/MCOM.001.2300550

2024 doi
[13]

PAT: Towards Flexible Verification under Fairness ,

J. Sun, Y. Liu, J.S. Dong, J. Pang , “PAT: Towards Flexible Verification under Fairness ,” in: A. Bouajjani, O. Maler (eds .) Computer Aided Verification, LNCS, Springer, Berlin, Heidelberg, Vol. 5643, pp. 709 -714, 2009 . DOI: 10.1007/978-3-642-02658- 4_59

2009 doi
[14]

IterGen: Iterative Structured LLM Generation,

S. Ugare, R. Gumaste, T. Suresh, G. Singh, S. Misailovic, “IterGen: Iterative Structured LLM Generation,” arXiv:2410.07295v1, 2024

2024 arXiv
[2024]

DOI: 10.1007/978-3-031-49252-5_4

doi

Pith tools

Reviewed August 7, 2026 · model on record in the stance chip above.

[1] [1]

Accessed: 10.01.2025 [Online]

TaRDIS: Trustworthy And Resilient Decentralised Intelligence For Edge Systems . Accessed: 10.01.2025 [Online]. Available: https://www.project-tardis.eu/

work page 2025

[2] [2]

A Simple Python Testbed for Federated Learning Algorithms,

M. Popovic, M. Popovic, I. Kastelan, M. Djukic, and S. Ghilezan, “A Simple Python Testbed for Federated Learning Algorithms,” in Proc. of the 2023 Zooming Innovation in Consumer Technologies Conference, pp. 148 -153, 2023. DOI: 10.1109/ZINC58345.2023.10173859

work page arXiv 2023

[3] [3]

A Federated Learning Algorithms Development Paradigm,

M. Popovic, M. Popovic, I. Kastelan, M. Djukic, and I. Basicevic, “A Federated Learning Algorithms Development Paradigm,” in: J. Kofron, T. Margaria, C. Seceleanu (eds.) Engineering of Computer- Based Systems, LNCS, Springer, Cham, vol. 14390, pp. 26 –41,

work page

[4] [4]

Developing Elementary Federated Learning Algorithms Leveraging the ChatGPT,

M. Popovic, M. Popovic, I. Kastelan, M. Djukic, I. Basicevic, “Developing Elementary Federated Learning Algorithms Leveraging the ChatGPT,” in Proc. 31st IEEE Telecommunications Forum, pp. 1 -4, 2023. DOI: 10.1109/TELFOR59449.2023.10372714

work page arXiv 2023

[5] [5]

PTB-FLA Development Paradigm Adaptation for ChatGPT,

M. Popovic, M. Popovic, I. Kastelan, M. Djukic, I. Basicevic, “PTB-FLA Development Paradigm Adaptation for ChatGPT,” Computer Science and Information Systems, vol. 21, no. 4, pp. 1269-1292, 2024. DOI: 10.2298/CSIS231224036P

work page doi:10.2298/csis231224036p 2024

[6] [6]

Correct orchestration of Federated Learning generic algorithms: formalisation and verification in CSP,

I. Prokić, S. Ghilezan, S. Kašterović, M. Popovic, M. Popovic, I. Kaštelan, “Correct orchestration of Federated Learning generic algorithms: formalisation and verification in CSP,” in: J. Kofron, T. Margaria, C. Seceleanu (eds.) Engineering of Computer -Based Systems, LNCS, Springer, Cham, vol. 14390, pp. 274 -288, 2024. DOI: 10.1007/978-3-031-49252-5_25

work page doi:10.1007/978-3-031-49252-5_25 2024

[7] [7]

Correct orchestration of Federated Learning generic algorithms: Python translation t o CSP and verification by PAT,

M. Djukic, I. Prokić, M. Popovic, S. Ghilezan, M. Popovic, S. Prokić, “Correct orchestration of Federated Learning generic algorithms: Python translation t o CSP and verification by PAT,” , International Journal on Software Tools for Technology Transfer (STTT), in press (should apper in Q1 2025)

work page 2025

[8] [8]

Accessed: 20.01.2025 [Online]

Number of ChatGPT Users ( Jan 2025) by Fabio Duarte . Accessed: 20.01.2025 [Online]. Available: https://explodingtopics.com/blog/chatgpt-users

work page 2025