Pith. sign in

REVIEW 3 major objections 5 minor 1 cited by

Generative Agents for Multi-Agent Autoformalization of Interaction Scenarios

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

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

Pith's one-line read LLM agents convert game prose into verified code at ~77% accuracy

desk verdict Solid incremental framework for autoformalizing 2x2 game descriptions, but the headline semantic accuracy overstates fidelity for non-numeric scenarios because it mixes exact payoff matching with weak constraint checks. read the letter →

arxiv 2412.08805 v3 pith:AKO37EJQ submitted 2024-12-11 cs.AI

Agnieszka Mensfelt , Kostas Stathis , Vince Trencsenyi This is my paper · ORCID
classification cs.AI
keywords autoformalizationlargelanguagemodelsmulti-agentsimulationgametheorylogicprogrammingProloggeneralplayingsemanticvalidation
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

GAMA, the framework presented here, aims to turn plain-English descriptions of strategic interactions into executable, formally validated game programs, so that multi-agent simulations can be built without hand-coding game rules. The paper tests this on 110 descriptions of five classic 2×2 simultaneous-move games, with and without numerical payoffs, and on descriptions of five gameplay strategies. The headline result is that the LLM-driven pipeline produces syntactically valid Prolog in 100% of cases (Claude 3.5 Sonnet) or 99.82% (GPT-4o), with average semantic correctness of 76.5% and 77% respectively; when exact payoff values are given, semantic correctness rises to 86% for both models. If this holds, scenario authors can write a situation in prose and receive a working, tournament-ready simulation module, with the LLM acting only as translator rather than as an in-game decision-maker.

What carries the argument

The load-bearing mechanism is the GAMA agent architecture: an LLM autoformalizer coupled to a Prolog solver and a three-stage validator. The solver represents games in a light GDL-style dialect of the Situation Calculus: game-independent rules (game/2, holds/2, finally/2) define legal play, while game-specific predicates (initial/1, legal/2, effect/3, abnormal/3, payoff/4, and a select/4 predicate for strategies) encode each game. The autoformalizer receives one-shot examples of these predicates for the Prisoner's Dilemma and tit-for-tat, generates code for a new scenario, and self-corrects using error lines returned by the solver, up to five attempts. Syntactically valid programs then enter tournament play to expose runtime faults, and finally are judged semantically: exact payoff-match when ground truth is available, otherwise constraint-based checking against the target game's payoff relations. This pipeline is what turns fallible LLM output into verified logic programs.

What would settle it

Show that a generated matrix can satisfy a game's payoff constraints yet contradict the natural-language scenario (for example, a Prisoner's Dilemma matrix with the 'cooperate' and 'defect' payoffs swapped, or a Matching Pennies matrix where both players win on the same outcome); if such a matrix is produced and scored semantically correct by GAMA's constraint check, the claimed 76.5%/77% semantic accuracy overstates fidelity to the input text, and a human-annotation study on the 55 non-numeric outputs would reveal the size of the gap.

Watch

Extended reading notes

Core claim

The paper's central claim is that autoformalization—using LLMs to translate natural language into a formal language—can be made reliable enough to produce reasoning modules for simulation agents, provided the translation is wrapped in a three-level validation pipeline. Working with 2×2 simultaneous-move games (Prisoner's Dilemma, Hawk-Dove, Stag Hunt, Battle of the Sexes, Matching Pennies), GAMA prompts an LLM with one worked Prisoner's Dilemma example, lets it emit game-specific Prolog predicates, then checks syntax with a solver, checks runtime behaviour by having the agent play tournaments against clones, and checks semantics by comparing tournament outcomes to target payoffs or, when no ground truth exists, by verifying the generated payoff matrix satisfies the defining payoff inequalities of the intended game. The reported outcome is near-perfect syntax, runtime correctness between 79% and 91%, and semantic correctness of 86% for scenarios with explicit numbers versus 67–68% for scenarios where payoffs must be inferred from prose.

Load-bearing premise

For the 55 scenarios without numerical payoffs, semantic correctness is measured by checking that the generated payoff matrix satisfies the target game's payoff inequalities (such as T > R > P > S for the Prisoner's Dilemma), not by checking that the matrix actually matches the scenario's story; a matrix that passes the inequality check while mislabelling or misvaluing the scenario's actions would still be scored correct.

Editorial extensions

If this is right

  • Non-programmers can produce executable, validated game modules by writing scenario descriptions in ordinary language, lowering the entry barrier to multi-agent simulation.
  • Simulation-time reasoning no longer depends on the LLM: once a game is autoformalized, the Prolog solver takes over, so LLM hallucinations and arithmetic errors do not affect actual play.
  • Autoformalized games can directly host strategy tournaments; the paper's round-robin experiment ranks best-response as the strongest strategy on average across the five games.
  • Gameplay strategies themselves can be autoformalized from prose: GPT-4o reached 100% semantic correctness on all five tested strategies, and Claude 3.5 Sonnet on four of five.
  • The validation pipeline extends to structurally similar games (e.g., rock-paper-scissors, sequential Prisoner's Dilemma), with broader generalization left for future work.

Reading between the lines

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

  • A human-evaluation study on the 55 constraint-checked scenarios would probably find that the true semantic accuracy is lower than the reported 67–68%, because payoff-inequality checks cannot detect matrices that satisfy the ordering but misrepresent which action is which or swap story roles.
  • The largest gains from adding runtime and semantic feedback into the autoformalization loop would likely come in Matching Pennies with non-numeric payoffs (30.2–34.2% semantic accuracy), whose failures stem from descriptions that state winners without stating that the other player loses.
  • The agent-template-plus-solver-trace pattern is portable: the same architecture could target temporal logics, planning domains, or normative rules, since the contribution is the validation pipeline rather than Prolog specifically.
  • The format-translation framing suggests a general recipe for safe LLM-generated code: keep the LLM out of the execution loop and force every generated artifact through a checker with a narrow, well-defined notion of correctness.
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.

Referee Report

3 major / 5 minor

Summary. The paper introduces GAMA, a framework that uses LLM-based agents to autoformalize natural-language descriptions of 2x2 simultaneous-move games and gameplay strategies into executable logic programs (Prolog-like predicates). The framework consists of a game module, a strategy module, and a three-level validation pipeline: syntactic validation via a solver, runtime validation via tournament simulation, and semantic validation using exact target payoffs when ground truth is available or game-type constraint checking otherwise. The empirical evaluation covers 110 scenarios across five game types with Claude 3.5 Sonnet and GPT-4o, reporting 100% syntactic correctness, 76.5%/77% semantic correctness, and high accuracy for autoformalized strategies. The paper also demonstrates an Axelrod-style tournament using the autoformalized game rules and strategies.

Significance. If the reported results are valid, GAMA is a useful step toward reducing the manual effort of building multi-agent simulations, and the three-level validation pipeline is a practical contribution. The authors provide open-source code and evaluation logs, which supports reproducibility. However, the headline semantic accuracy is a composite of two very different validation standards: the numeric-description half uses exact payoff matching, while the non-numeric half uses only game-type constraint checking. The latter does not measure whether the generated matrix matches the described scenario, so the headline number overstates the fidelity of autoformalization. The strategy autoformalization accuracy also rests on a relatively weak equivalence test. These issues do not invalidate the framework, but they should be addressed before the empirical claims can be taken at face value.

major comments (3)
  1. [Sections 3.4, 4.4, Table 6] The semantic correctness metric for non-numeric descriptions checks only whether the generated payoff matrix satisfies the ordering constraints of the intended game type (e.g., T > R > P > S for Prisoner's Dilemma, as in valid_pd_payoffs in Section 3.5.4), not whether the action names and payoff values correspond to the content of the natural-language description. Because the one-shot prompt already contains a complete PD program, a model can copy or slightly adapt those payoff values for any non-numeric PD scenario and pass the check without grounding the description's specifics. The abstract's 76.5%/77% semantic accuracy is an unweighted average of the 86% exact-match numeric score and the 67%/68% constraint-based non-numeric score, so it inherits this weakness. Please report the numeric and non-numeric semantic accuracies separately, and either rename the constraint-based metric (e.g., 'structure correctness') or add a human-annotated semantic evaluation on the non-numeric subset.
  2. [Section 4.2 vs Table 3] The dataset composition is arithmetically inconsistent. Section 4.2 states that for both variants there are 5 common-metaphor scenarios per game (5 x 5 = 25) plus 50 alternative-metaphor scenarios (10 per game), which totals 75 per variant, not the 55 per variant used in Table 3 and not the 110 total stated in the abstract. This discrepancy affects the denominators of all reported percentages. Please clarify the exact number of scenarios per variant and correct either the text or the table.
  3. [Sections 4.6 and 5.3] The semantic validation of autoformalized strategies compares only the total payoff over four rounds against a single clone opponent (anti-tit-for-tat) to a target payoff. Total payoff equality is a necessary but not sufficient condition for strategy equivalence; different strategies can yield the same aggregate payoff against one fixed opponent in a short horizon. The claim of high semantic accuracy for strategies therefore needs either a more discriminative test (e.g., multiple opponents, longer horizons, or per-round move comparison) or an explicit discussion of this limitation.
minor comments (5)
  1. [Table 3] Table 3 lists Rounds = 10 for Experiment 4, while Section 4.6 states that the strategy autoformalization played four rounds against a clone; please correct this inconsistency.
  2. [Section 3.2] The text refers to 'Listing 1' as an overview of the autoformalization module, but no listing appears in the manuscript; please include the listing or remove the reference.
  3. [Section 2.3] The sentence 'GDL focused on information games only' should probably read 'perfect-information games' to match standard terminology.
  4. [Section 3.4] The definition of semantic correctness as 'correspondence between the generated code and the input natural language description' is not what the constraint-based validation actually measures; please align the terminology with the validation method.
  5. [Figure 2] The heatmap's row and column ordering is not explained in the caption, and the small labels make the figure hard to read; please add an explanation and increase the font size.

Circularity Check

0 steps flagged · score 2.0 of 10

No load-bearing circularity: the headline results rest on re-run experiments with exact payoff checks for numeric scenarios, while the main caveats are self-authored benchmarks and a weak constraint-based semantic check for non-numeric scenarios, which are validity limitations rather than derivation-circularity.

full rationale

No step in the paper's derivation chain reduces by construction to a fitted parameter, a self-citation, or a definition of the target result. For numeric descriptions (Exp. 1), semantic correctness is checked by comparing generated payoffs to exact target values (Sections 3.4 and 4.3), and for strategy autoformalization (Exp. 4) it is checked against target payoffs plus manual inspection for the random strategy. The central empirical claim therefore retains independent content, e.g., the 86% exact payoff matching on the 55 numeric scenarios. Two caveats explain the modest score. First, the evaluation benchmark and the core autoformalization module originate in the authors' prior work [23], so the evaluation is not externally grounded; however, the current paper re-runs the pipeline and does not cite [23] as proof of the reported accuracy, so this is self-referential provenance rather than load-bearing circularity. Second, for non-numeric game descriptions (Exp. 2, Section 4.4), semantic correctness is assessed by checking whether the generated payoff matrix satisfies the type-level constraints from Section 2.1 instead of comparing the matrix content to the natural language description. This weakens the construct validity of the 67%/68% non-numeric semantic scores and of the headline averages, but it is a measurement-validity limitation, not an equivalence between the framework's output and its input by construction. No circular step is exhibited, so no step is listed.

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

The central claim rests on the correctness of the Prolog solver, the accuracy of the dataset labels, and the adequacy of constraint-based semantic validation for non-numeric scenarios. Experimental hyperparameters such as temperature, max attempts, and rounds are chosen by hand and affect the reported percentages, but none are fitted to data. No new physical or formal entities are postulated.

free parameters (3)
  • temperature = 1
    LLM sampling temperature chosen by hand; high randomness affects reproducibility of the reported correctness rates.
  • max_attempts = 5
    Maximum number of self-correction attempts before labeling a scenario syntactically incorrect; directly influences reported syntactic correctness.
  • rounds = 4 (Experiments 1, 2, 4) and 10 (Experiment 3)
    Tournament length chosen by hand; affects payoff totals used for semantic validation and strategy rankings.
assumptions (4)
  • domain assumption The Prolog solver correctly implements the game-theoretic semantics described in Section 3.5.
    Section 3.5 claims an encoding of Situation Calculus and GDL-like predicates; any bug in the solver would transfer to all reported correctness percentages.
  • domain assumption The 110-scenario dataset's game labels and target payoffs are correct.
    Section 4.2 describes an improved version of the dataset from [23]; no inter-annotator agreement or external benchmark is provided.
  • ad hoc to paper For non-numeric descriptions, satisfying the game-type payoff constraints is treated as semantic correctness.
    Section 4.4 adopts constraint checking as a proxy for exact semantics because ground truth payoffs are unavailable; this weakens the semantic correctness measurement.
  • domain assumption A single one-shot example is sufficient to guide correct formalization of all five games and six strategies.
    Sections 3.2 and 4.6 rely on one-shot prompting; the paper acknowledges performance degrades for strategies most divergent from the example.

how reviews work

0 comments
Cite this review

Pith. "Pith review of Generative Agents for Multi-Agent Autoformalization of Interaction Scenarios." pith.science (2026). https://pith.science/paper/AKO37EJQ

@misc{pith2026241208805,
  author       = {Pith},
  title        = {Pith review of: Generative Agents for Multi-Agent Autoformalization of Interaction Scenarios},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/AKO37EJQ}},
  note         = {Machine review of arXiv:2412.08805}
}
read the original abstract

Multi-agent simulations are versatile tools for exploring interactions among natural and artificial agents, but their development typically demands domain expertise and manual effort. This work introduces the Generative Agents for Multi-Agent Autoformalization (GAMA) framework, which automates the formalization of interaction scenarios in simulations using agents augmented with large language models (LLMs). To demonstrate the application of GAMA, we use natural language descriptions of game-theoretic scenarios representing social interactions, and we autoformalize them into executable logic programs defining game rules, with syntactic correctness enforced through a solver-based validation. To ensure runtime validity, an iterative, tournament-based procedure tests the generated rules and strategies, followed by exact semantic validation when ground truth outcomes are available. In experiments with 110 natural language descriptions across five 2x2 simultaneous-move games, GAMA achieves 100% syntactic and 76.5% semantic correctness with Claude 3.5 Sonnet, and 99.82% syntactic and 77% semantic correctness with GPT-4o. The framework also shows high semantic accuracy in autoformalizing agents' strategies.

Figures

Figures reproduced from arXiv: 2412.08805 by the authors.

Figure 1
Figure 1. Overview of the GAMA framework. Dashed lines indicate optional control flows. Games and strategies can be specified either through predefined rules or natural language descriptions, or optionally by loading a predefined agent. Semantic validation is performed when ground truth outcomes are available. The Validator may employ a formal solver. external environment, manages game history (including each agent’s moves, o… view at source ↗
Figure 2
Figure 2. Normalized total payoff for each strategy by game. Rows are ordered by the strategies with the highest average total payoff, and columns are arranged similarly based on the games. The total payoff for the winning strategy in each game is highlighted in white [PITH_FULL_IMAGE:figures/full_fig_p006_2.png] view at source ↗

Discussion (0). Continue with ORCID to comment.

Forward citations

Cited by 1 Pith paper

Reviewed papers in the Pith corpus that reference this work. Sorted by Pith novelty score. Full citation record

  1. Game Theory Meets Large Language Models: A Systematic Survey with Taxonomy and New Frontiers

    cs.AI 2025-02 conditional novelty 5.0 of 10

    A taxonomy-based survey of bidirectional game theory and LLM research, spanning evaluation, alignment, economic competition, and LLM-driven game solving.

Reference graph

Works this paper leans on

40 extracted references · 20 canonical work pages · cited by 1 Pith paper

  1. [1]

    Achiam, S

    J. Achiam, S. Adler, S. Agarwal, et al. GPT-4 technical report. arXiv preprint arXiv:2303.08774, 2023

    arXiv 2023

  2. [2]

    Akata, L

    E. Akata, L. Schulz, J. Coda-Forno, et al. Playing repeated games with large language models. arXiv preprint arXiv:2305.16867, 2023

    arXiv 2023

  3. [3]

    Claude 3.5, 2024

    Anthropic. Claude 3.5, 2024. URL https://www.anthropic.com/news/ claude-3-5-sonnet

    work page 2024

  4. [4]

    Axelrod and W

    R. Axelrod and W. D. Hamilton. The evolution of cooperation. science, 211(4489):1390–1396, 1981

    work page 1981

  5. [5]

    Y . Chen, R. Gandhi, Y . Zhang, and C. Fan. Nl2tl: Transforming natural languages to temporal logics using large language models. In Proceed- ings of the 2023 Conference on Empirical Methods in Natural Language Processing, pages 15880–15903, 2023

    work page 2023

  6. [6]

    Cosler, C

    M. Cosler, C. Hahn, D. Mendoza, F. Schmitt, and C. Trippel. nl2spec: interactively translating unstructured natural language to temporal log- ics with large language models. In International Conference on Com- puter Aided Verification, pages 383–396. Springer, 2023

    work page 2023

  7. [7]

    C. Fan, J. Chen, Y . Jin, and H. He. Can large language models serve as rational players in game theory? a systematic analysis. arXiv preprint arXiv:2312.05488, 2023

    arXiv 2023

  8. [8]

    J. Feng, R. Xu, J. Hao, H. Sharma, Y . Shen, D. Zhao, and W. Chen. Lan- guage models can be logical solvers. arXiv preprint arXiv:2311.06158, 2023

    arXiv 2023

Show all 40 references
  1. [9]

    M. R. Genesereth, N. Love, and B. Pell. General game playing: Overview of the AAAI competition. AI Mag., 26(2):62–72, 2005

    2005

  2. [10]

    G. D. Giacomo, Y . Lespérance, and A. R. Pearce. Situation calculus based programs for representing and reasoning about game structures. In F. Lin, U. Sattler, and M. Truszczynski, editors,Principles of Knowl- edge Representation and Reasoning: Proceedings of the Twelfth Inter...

    2010

  3. [11]

    R. Gibbons. A Primer in Game Theory . Pearson Education Limited, Harlow, Essex, United Kingdom, 1992

    1992

  4. [12]

    Gillioz, J

    A. Gillioz, J. Casas, E. Mugellini, and O. A. Khaled. Overview of the transformer-based models for nlp tasks. In 2020 15th Conference on Computer Science and Information Systems (FedCSIS), pages 179–183,

    2020

  5. [13]

    Z. Gou, Z. Shao, Y . Gong, et al. Critic: Large language mod- els can self-correct with tool-interactive critiquing. arXiv preprint arXiv:2305.11738, 2024

    2024 arXiv

  6. [14]

    F. Guo. GPT agents in game theory experiments. arXiv preprint arXiv:2305.05516, 2023

    2023 arXiv

  7. [15]

    He-Yueya, G

    J. He-Yueya, G. Poesia, R. E. Wang, and N. D. Goodman. Solving math word problems by combining language models with symbolic solvers. arXiv preprint arXiv:2304.09102, 2023

    2023 arXiv

  8. [16]

    Imani, L

    S. Imani, L. Du, and H. Shrivastava. Mathprompter: Mathematical rea- soning using large language models. arXiv preprint arXiv:2303.05398, 2023

    2023 arXiv

  9. [17]

    A. Q. Jiang, S. Welleck, J. P. Zhou, W. Li, J. Liu, M. Jamnik, T. Lacroix, Y . Wu, and G. Lample. Draft, sketch, and prove: Guiding formal the- orem provers with informal proofs. arXiv preprint arXiv:2210.12283, 2022

    2022 arXiv

  10. [18]

    Lesperance, G

    Y . Lesperance, G. De Giacomo, M. Rostamigiv, and S. M. Khan. Ab- straction of situation calculus concurrent game structures. Proceedings of the AAAI Conference on Artificial Intelligence , 38(9):10624–10634, Mar. 2024. doi: 10.1609/aaai.v38i9.28933. URL https://ojs.aaai.org/ ...

    2024 doi

  11. [19]

    Lorè and B

    N. Lorè and B. Heydari. Strategic behavior of large language models: Game structure vs. contextual framing. arXiv preprint arXiv:2309.05898, 2023

    2023 arXiv

  12. [20]

    N. Love, T. Hinrichs, D. Haley, E. Schkufza, and M. Genesereth. Gen- eral Game Playing: Game Description Language Specification. Techni- cal Report LG–2006–01, Stanford University, 2006

    2006

  13. [21]

    Madaan, N

    A. Madaan, N. Tandon, P. Gupta, et al. Self-refine: Iterative refinement with self-feedback. arXiv preprint arXiv:2303.17651, 2023

    2023 arXiv

  14. [22]

    McCarthy and P

    J. McCarthy and P. Hayes. Some philosophical problems from the standpoint of artificial intelligence. In B. L. Webber and N. J. Nils- son, editors, Readings in Artificial Intelligence, pages 431–450. Morgan Kaufmann, 1981

    1981

  15. [23]

    Mensfelt, K

    A. Mensfelt, K. Stathis, and V . Tencsenyi. Autoformalization of Game Descriptions using Large Language Models. In 1st International Work- shop on Next-Generation Language Models for Knowledge Representa- tion and Reasoning, Hanoi, Vietnam, 2024. URL https://arxiv.org/abs/ 2409.12300

    2024 arXiv

  16. [24]

    OpenAI. GPT-4o. https://openai.com/index/hello-gpt-4o/, 2024. URL https://openai.com/index/hello-gpt-4o/. Accessed: 25/07/2024

    2024

  17. [25]

    Osborne and A

    M. Osborne and A. Rubinstein. A Course in Game Theory . The MIT Press, 1994

    1994

  18. [26]

    L. Pan, A. Albalak, X. Wang, and W. Wang. Logic-lm: Empowering large language models with symbolic solvers for faithful logical rea- soning. In Findings of the Association for Computational Linguistics: EMNLP 2023, pages 3806–3824, 2023

    2023

  19. [27]

    X. Qiu, T. Sun, Y . Xu, Y . Shao, N. Dai, and X. Huang. Pre-trained mod- els for natural language processing: A survey.Science China Technolog- ical Sciences, 63:1872–1897, 2020. doi: 10.1007/s11431-020-1647-3

    2020 doi

  20. [28]

    Rasmusen

    E. Rasmusen. Games and information an introduction to game theory. Blackwell, 2006

    2006

  21. [29]

    Renze and E

    M. Renze and E. Guven. Self-reflection in llm agents: Effects on problem-solving performance. arXiv preprint arXiv:2405.06682, 2024

    2024 arXiv

  22. [30]

    R. B. Scherl and H. J. Levesque. Knowledge, action, and the frame problem. Artif. Intell. , 144(1-2):1–39, 2003. doi: 10.1016/S0004-3702(02)00365-X. URL https://doi.org/10.1016/ S0004-3702(02)00365-X

    2003 doi

  23. [31]

    Schiffel and M

    S. Schiffel and M. Thielscher. Reasoning about general games de- scribed in gdl-ii. Proceedings of the AAAI Conference on Artificial Intelligence, 25(1):846–851, Aug. 2011. doi: 10.1609/aaai.v25i1.7944

    2011 doi

  24. [32]

    Shinn, F

    N. Shinn, F. Cassano, E. Berman, et al. Reflexion: Language agents with verbal reinforcement learning. arXiv preprint arXiv:2303.11366, 2023

    2023 arXiv

  25. [33]

    Thielscher

    M. Thielscher. A general game description language for incomplete information games. In Proceedings of the Twenty-Fourth AAAI Confer- ence on Artificial Intelligence , AAAI’10, page 994–999. AAAI Press, 2010

    2010

  26. [34]

    Thielscher

    M. Thielscher. The general game playing description language is uni- versal. In T. Walsh, editor, IJCAI 2011, Proceedings of the 22nd Inter- national Joint Conference on Artificial Intelligence, Barcelona, Catalo- nia, Spain, July 16-22, 2011, pages 1107–1112. IJCAI/AAAI, 2011

    2011

  27. [35]

    Wang and Y

    Y . Wang and Y . Zhao. Rupbench: Benchmarking reasoning under per- turbations for robustness evaluation in large language models. arXiv preprint arXiv:2406.11020, 2024

    2024 arXiv

  28. [36]

    Wielemaker, T

    J. Wielemaker, T. Schrijvers, M. Triska, and T. Lager. Swi-prolog. The- ory and Practice of Logic Programming, 12(1-2):67–96, 2012

    2012

  29. [37]

    Y . Wu, A. Q. Jiang, W. Li, M. Rabe, C. Staats, M. Jamnik, and C. Szegedy. Autoformalization with large language models. Advances in Neural Information Processing Systems, 35:32353–32368, 2022

    2022

  30. [38]

    Z. Yang, A. Ishay, and J. Lee. Coupling large language models with logic programming for robust and general reasoning from text. arXiv preprint arXiv:2307.07696, 2023

    2023 arXiv

  31. [39]

    W. X. Zhao, K. Zhou, J. Li, et al. A survey of large language models. arXiv preprint arXiv:2303.18223, 2023

    2023 arXiv

  32. [2020]

    doi: 10.15439/2020F20

    doi

Pith tools

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