Create and curate a TLA+ Dataset for LLM Training and Evaluation

[lemmy]

This issue proposes the creation of a TLA+ dataset and benchmark suite based on logic puzzles and existing community modules. The goal is to enable consistent evaluation of LLMs on TLA+-related tasks and facilitate broader adoption of formal methods in AI-assisted development.

📌 Motivation

There is growing interest in evaluating language models on formal specification tasks. TLA+ lacks a dataset to test model performance. Having such a dataset would support:

• Objective (or at least consistent) comparison of LLM performance on TLA+ tasks.
• Enhanced support for tools like Aider, Codex CLI in formal language contexts.
• A reference point for developers and researchers choosing the best tool/model for TLA+-related workflows.

🧩 Proposal Components

1. Logic Puzzles as Benchmarks

Logic puzzles like Die Hard, River Crossing, etc., could form the basis of a benchmark dataset. These puzzles:

• Are well known and have abundant prose descriptions available online.
• Require converting informal problem descriptions into formal specs.
• Frequently test a model’s ability to find counterexamples, a key TLA+ skill.
• Early results at https://www.youtube.com/watch?v=dZv0ykx5aGo&list=PLWLcqZLzY8u8C4dz41PglOOXncqr0c0du

2. TLA+ Dataset

• Create a dataset of problem statements (ideally in natural language), and their corresponding TLA+ specifications.
• CommunityModules, Examples, and other open-source TLA+ specs could serve as seeds for this dataset.
• Could follow the structure of existing coding problem repositories (e.g., Exercism, LeetCode) adapted for formal methods.

3. Benchmarking Framework

• Design scripts or tooling to run LLMs against the TLA+ dataset.
• Measure performance in terms of spec correctness, ability to catch errors (via TLC), and model explanation quality.
• Optionally, support community-submitted results for model comparisons.

🚀 Next Steps

• Identify and gather initial problem set (e.g., 5–10 logic puzzles).
• Draft initial problem statements and reference specs.
• Define benchmark evaluation criteria.
• Explore automation/tooling for running LLMs against the benchmark.

Related: FM-5

[lemmy]

Initial set of puzzles and infrastructure at https://github.com/tlaplus/TLAiBench

[granular-storage]

Hi,
thank you for pushing this issue.
Would be very useful to perhaps "link" this project with maintaining the examples repo and build over them while maintaining examples.
I am also thinking that one "problem" can have multiple solutions, some better in being more general but perhaps harder for beginners while also larger in state space. (the LLM part could be separated in another issue as the competence is orthogonal)

Eg, https://github.com/tlaplus/Examples/blob/master/specifications/MissionariesAndCannibals/MissionariesAndCannibals.tla
I can create another spec, although less elegant. (created with Gemini2.5 including documentation)

MissionariesAndCannibals.pdf

-------------------------- MODULE MissionariesAndCannibals --------------------------
(***************************************************************************)
(* This module specifies a solution to the Missionaries and Cannibals      *)
(* problem using integer-based state variables.                            *)
(***************************************************************************)

EXTENDS Integers  \* Imports standard integer arithmetic operators (+, -, >=, etc.).

(***************************************************************************)
(*                              VARIABLES                                  *)
(* These are the variables that define the state of the system at any      *)
(* given time.                                                             *)
(***************************************************************************)
VARIABLES
    m,  \* Represents the number of missionaries on the STARTING bank.
    c,  \* Represents the number of cannibals on the STARTING bank.
    b   \* Represents the location of the boat.
        \*  1 means the boat is at the STARTING bank.
        \* -1 means the boat is at the DESTINATION bank.

(***************************************************************************)
(* `vars` is a tuple of all state variables. It's used in the `Spec`       *)
(* definition to assert that any state change must be described by `Next`. *)
(***************************************************************************)
vars == <<m, c, b>>

(***************************************************************************)
(*                              CONSTANTS                                  *)
(* These are fixed values for a specific instance of the problem.          *)
(***************************************************************************)
CONSTANTS TotalMissionaries, TotalCannibals

(***************************************************************************)
(* The `ASSUME` statement provides concrete values for the constants.      *)
(* This is primarily for the TLC model checker.                            *)
(***************************************************************************)
ASSUME TotalMissionaries = 3 /\ TotalCannibals = 3

(***************************************************************************)
(* `Init` is the Initial State Predicate. It defines the state of the      *)
(* system at the very beginning of an execution.                           *)
(***************************************************************************)
Init ==
    /\ m = TotalMissionaries  \* All missionaries (3) are on the start bank.
    /\ c = TotalCannibals      \* All cannibals (3) are on the start bank.
    /\ b = 1                  \* The boat starts at the start bank.

(***************************************************************************)
(* `IsSafe(miss, can)` defines the core rule of the puzzle for a single    *)
(* river bank. It is TRUE if the configuration is safe.                    *)
(***************************************************************************)
IsSafe(miss, can) ==
    \/ miss = 0        \* It's safe if there are no missionaries on the bank, or
    \/ miss >= can     \* It's safe if missionaries are not outnumbered by cannibals.

(***************************************************************************)
(* `StateIsSafe` is a state constraint (an invariant) that must be true in *)
(* every reachable state. It applies the `IsSafe` rule to both banks.      *)
(***************************************************************************)
StateIsSafe ==
    /\ IsSafe(m, c)  \* The start bank must be safe.
    /\ IsSafe(TotalMissionaries - m, TotalCannibals - c) \* The destination bank must be safe.
        \* The number of people on the destination bank is the total minus those on the start bank.

(***************************************************************************)
(* `Move(m_boat, c_boat)` defines the logic of a single boat trip.         *)
(* It's a predicate that is true if moving `m_boat` missionaries and       *)
(* `c_boat` cannibals is a valid action from the current state.            *)
(***************************************************************************)
Move(m_boat, c_boat) ==
    LET
        \* `LET` defines local aliases for complex expressions to improve readability.
        people_in_boat == m_boat + c_boat
        \* These calculate the state of the start bank AFTER the move.
        \* The `b` variable cleverly handles direction:
        \* - If b=1 (start->dest), people are subtracted from the start bank count.
        \* - If b=-1 (dest->start), people are added back to the start bank count (m - (-1 * m_boat)).
        m_next == m - (b * m_boat)
        c_next == c - (b * c_boat)
    IN
        \* This is a conjunction of all rules for a valid move.
        /\ people_in_boat \in {1, 2}  \* The boat must carry 1 or 2 people.
        /\ m_boat >= 0 /\ c_boat >= 0  \* The number of people moved cannot be negative.

        \* This checks if there are enough people on the correct bank to make the move.
        /\ IF b = 1
           THEN /\ m >= m_boat /\ c >= c_boat  \* If at start bank, check start bank counts.
           ELSE /\ (TotalMissionaries - m) >= m_boat  \* If at dest bank, check dest bank counts.
                /\ (TotalCannibals - c) >= c_boat

        \* This is the crucial safety check for the resulting state.
        /\ IsSafe(m_next, c_next)
        /\ IsSafe(TotalMissionaries - m_next, TotalCannibals - c_next)

        \* This section defines the variable values in the next state (`'`).
        /\ m' = m_next
        /\ c' = c_next
        /\ b' = -b  \* The boat's location flips.

(***************************************************************************)
(* `Next` is the Next-State Relation. It defines all possible transitions  *)
(* from one state to the next.                                             *)
(***************************************************************************)
Next ==
    \* A next state exists if there is (`\E`) some combination of missionaries
    \* and cannibals to move (`m_moved`, `c_moved`) such that the `Move`
    \* predicate is true for that combination.
    \E m_moved \in 0..2, c_moved \in 0..2:
        Move(m_moved, c_moved)

(***************************************************************************)
(* `Spec` is the main formula describing the system's behavior.            *)
(***************************************************************************)
Spec == Init /\ [][Next]_vars
    \* A behavior is valid if:
    \* - It starts in a state satisfying `Init`.
    \* - AND (`/\`)
    \* - For all steps (`[]`), the step must satisfy `Next` or leave `vars` unchanged.

(***************************************************************************)
(* `SolutionFound` defines the goal state. This is NOT an invariant. It is *)
(* the state we want to reach. The model checker is used to find a path to *)
(* a state where this predicate is true.                                   *)
(***************************************************************************)
SolutionFound ==
    /\ m = 0  \* No missionaries are left on the start bank.
    /\ c = 0  \* No cannibals are left on the start bank.

=============================================================================

[lemmy]

I am also thinking that one "problem" can have multiple solutions, some better in being more general but perhaps harder for beginners while also larger in state space. (the LLM part could be separated in another issue as the competence is orthogonal)

There is precedence for that. There are two solutions to the Tower of Hanoi problem: https://github.com/tlaplus/Examples/tree/master/specifications/tower_of_hanoi