Keyboard shortcuts

Press ← or → to navigate between chapters

Press S or / to search in the book

Press ? to show this help

Press Esc to hide this help

Large language models for chemistry robotics

(authored by agents unless marked 🧑) Tag: yoshikawa2023large, paper

verifier-assisted generation

CLAIRify turns a natural-language experiment into XDL, then repeatedly checks and repairs the generated program. The paper states: “CLAIRify generates XDL with an automated iterative prompting between a generator and a verifier.” (Section 3.1, p. 1062). Apply it by (1) provide the XDL description, action list, parameter rules, and user instruction to a generator; (2) run the candidate through an XML parser and rule checker; (3) if errors exist, append the prior XDL and concise errors to the original prompt; (4) regenerate; (5) stop at an error-free candidate or timeout (the evaluation uses a limit of 10 iterations, Section 4.1.2, p. 1068). The paper describes the loop as follows: “The generated code is passed through the verifier, and if no errors are generated, then the code is syntactically correct.” (Section 3.1.1, p. 1062). The verifier checks XML syntax, permitted action tags and parameters, mandatory properties, optional-property correctness, and definitions of hardware and reagents. It reports errors but does not suggest repairs: “The role of the verifier is limited to pointing out the errors, and it does not propose how to fix them.” (Section 3.1.2, p. 1064) The paper ablates the feedback message on a 10-experiment Chem-RnD validation set (Table 4, p. 1076): success was 0% for the previous XDL plus a generic “not correct” string, 30% for the last error list alone, 50% for the cumulative error list alone, and 100% for the previous XDL plus the last error list. Without any XDL description in the prompt, the LLM produced no valid XDL for any of those 10 experiments (Section 4.3.1, p. 1075).

Inference: in Verus, use an ordinary Rust generator plus a parser and a verified boundary checker; represent accepted structure with Rust types, and use requires and ensures on a verification function. The loop itself is runtime orchestration, while Verus proves that a parsed plan satisfies structural predicates. Do not claim the LLM semantics are proved: the paper proves syntax and necessary static conditions only. Evidence is 105/108 successful plans on Chem-RnD and 42/42 on Chem-EDU for CLAIRify (Table 1, p. 1069), against 92/108 and 0/42 for the SynthReader baseline; the generator was text-davinci-003, Chem-RnD used only protocols under 1000 characters, and the denominators are experiments, not proofs. Average generation took 33 ± 3 seconds per iteration and two calls for one interface example (Section 3.1.4, p. 1064). Assumptions include a timeout, a supplied resource list, and a verifier that knows only rule-level conditions.

resource constraints and task-motion planning

The prompt may include available hardware and reagents; the verifier rejects undeclared resources. If no list is supplied, the implementation assumes all resources exist (Section 3.1.3, p. 1064). The accepted XDL is parsed into objects, goals, and initial conditions. Algorithm 2 (with its description in the same section) says to parse XDL, perceive the scene, reject failed preconditions, solve each goal with optimistic PDDLStream instantiation, test stream feasibility, append the plan, and update the scene (Section 3.2, p. 1065). Streams sample continuous objects such as feasible grasping poses and collision-free motion, while a classical planner such as Fast Downward searches logical actions (Section 3.2.1, p. 1065). Inference: a Verus version can specify state transitions and prove that each action preserves invariants; continuous collision and kinematics remain trusted solver/controller results unless separately modeled.

constrained motion and closed-loop refinement

To prevent spills, the paper constrains end-effector orientation and uses projection-based sampling. Algorithm 3 samples q, repeatedly computes δq = J†(q)F(q), projects until the constraint tolerance is met, and invokes a path planner (Section 3.2.2, p. 1066). It adds an eighth degree of freedom (a revolute joint before the gripper) to a 7-DoF Franka arm. The Introduction (p. 1059) reports 97% constrained-planning success for the 8-DoF arm versus 84% for 7-DoF; Table 5 (Section 4.4.2, p. 1077) shows these are Scenario 1 (single step) planning rates, while Scenario 2 (two steps) gives 84% versus 70%. Each scenario ran 50 trials with random seeding of the IK solver, with end-effector pitch and roll limited to 0.1 rad (Section 4.4.2, p. 1076). Perception re-estimates the object pose just before grasping (Section 3.2.1, p. 1065); the task plan can also repeat a step until feedback reaches a condition such as “adding acid until pH reaches 7” (Section 3.2.1, p. 1066). The paper states it “empirically observed no spillage as long as orientation constraints are satisfied” (Section 3.2.2, p. 1066). Inference: Verus can prove bounded state-update and goal predicates, but not physical no-spill behavior without a trusted dynamics model. The paper reports 8.1% and 8.8% relative pouring errors for water and salt versus 81.4% and 24.1% for a PD-control baseline (Introduction, p. 1059; Section 4.4.1, p. 1076); each percentage is a material-specific average relative error from the paper’s pouring experiments, not a formal guarantee.

what is proved, trusted, and useful for VL

The paper says the rule-based verifier cannot do semantic checking: “semantic understanding is beyond the ability of a rule-based system”, so the LLM-based generator fixes the errors (Section 3.1.2, p. 1064). The paper also admits (Section 5, p. 1077): “Although the generated plans were syntactically correct and satisfied the constraints, they contained errors.” Inference: the rule checker establishes syntactic validity and necessary executability conditions; PDDLStream establishes sampled-plan feasibility; robot sensors, kinematics, LLM output, OpenAI service, and physical execution remain trusted. Inference: this is a moderate threat to agent-written verified Rust only when agents confuse checker acceptance with functional correctness; a Verus contract should state the intended safety property and separately validate generated code. Inference: existing work already supplies a generate-check-regenerate pattern and benchmark denominators; VL should reuse that architecture rather than redo prompt-loop basics.

techniques for the catalog

  • verifier-assisted iterative prompting: regenerate a structured program using concise checker errors until valid or timed out
  • resource-aware static checking: reject actions whose hardware or reagents are absent from the declared environment
  • stream-based task-motion planning: combine logical planning with sampled continuous feasibility checks
  • projection-based constrained planning: project sampled configurations onto equality constraints before path search
  • perception-driven refinement: refresh object state before grasping and repeat conditional tasks using feedback Checked 2026-10-18 against the full paper by a Claude agent (mid-paper quote: “The results show that the shaping function contributed to reducing the overshooting compared to PD control pouring.”): read the whole paper text and checked every quotation, section and page reference, the Table 1, 2, 4 and 5 numbers, the 33 ± 3 s timing, the 97%/84% and pouring error figures, and the algorithm steps; changed section 3.1.1 for the second quote, the 97% vs 84% context (Scenario 1, Table 5), the page of the pH 7 repetition, the verifier-semantics sentence, added the Table 4 ablation, baseline numbers, and Inference labels; did not check the cited external papers or the Verus mapping, which is the study’s own inference, or figures beyond their captions. Link is the DOI printed in the paper text.

Last edited: