Technical Summary: U-Define: Designing User Workflows for Hard and Soft Constraints in LLM-Based Planning

1. Problem Statement

While Large Language Models (LLMs) have lowered the barrier for end-user task planning, their "black-box" nature introduces significant reliability issues. LLMs often produce inconsistent plans, fail to enforce strict requirements, and generate outputs with confident but erroneous reasoning. Existing verification approaches, such as external critics or formal verification, often rely on rigid, pre-engineered templates or domain-specific specifications that limit flexibility. Conversely, purely soft constraint approaches (e.g., numeric weights or flexible preferences) are often difficult for users to interpret and fail to guarantee critical safety or logical rules.

The core challenge addressed by this work is designing an interaction workflow that allows users to reliably express and balance hard constraints (rules that must never be violated) and soft constraints (preferences reflecting flexibility) within LLM-based planning, without requiring users to learn formal specification languages or rely on rigid templates.

2. Methodology and System Design

The authors propose U-Define, a system that operationalizes a workflow where users define constraints in natural language, categorize them by strictness, and receive verification results tailored to each constraint type. The system extends prior work (VeriPlan) by removing template dependencies and introducing a hybrid verification architecture.

System Architecture

U-Define structures the planning process into three stages:

1. Definition Stage:

   • Input: Users input constraints in natural language and categorize them as either Hard or Soft.
   • Rule Translator: A specialized LLM agent (fine-tuned on LLaMA 7B using the NL2LTL dataset) translates user-defined hard constraints into Linear Temporal Logic (LTL) properties.
   • PRISM Conversion: The LTL properties are further translated into the PRISM modeling language, a format required for probabilistic model checking.
   • Validation: The system converts the formal rules back into natural language for user verification before proceeding.

2. Verification Stage:

   • Plan Generation: An LLM Planner generates candidate plans based on the user's task prompt and constraints.
   • Hard Constraint Verification: The generated plan is converted into PRISM format. A formal Model Checker (using PRISM and Stormpy) exhaustively explores the plan's state space to verify adherence to the LTL rules. It returns a binary validity result and a list of specific violated rules.
   • Soft Constraint Verification: An LLM-as-Judge agent evaluates the plan against soft constraints. It provides a 1–5 star rating and a natural language explanation regarding the degree of alignment with user preferences.

3. Feedback Stage:

   • Users review the ranked plans (prioritized by hard constraint violations) and verification outputs.
   • Users can iteratively refine constraints, adjust the strictness of rules, or modify the prompt. The system regenerates the plan and re-verifies it, creating a closed feedback loop.

Technical Implementation

• LLM Agents: Most agents use GPT-4. The Rule Translator uses a fine-tuned LLaMA 7B model.
• Formal Verification: Utilizes PRISM and Stormpy for model checking.
• Evaluation: The system was evaluated through a component-level technical evaluation (measuring translation accuracy) and two user studies.

3. Key Contributions

Technical Contributions

• Automated Translation Pipeline: An automated pipeline that translates natural language hard constraints into formal verification artifacts (LTL and PRISM) using LLMs, eliminating the need for pre-engineered domain templates.
• Hybrid Verification Mechanism: A system that applies distinct verification methods based on constraint type: formal model checking for hard constraints (guaranteeing correctness) and LLM-as-judge evaluation for soft constraints (assessing preference alignment).

System Contributions

• U-Define Interface: A user interface that allows simultaneous definition of hard and soft constraints, visualizing them via a mind-map layout, and presenting differentiated verification feedback (violation lists vs. star ratings).

Empirical Contributions

• User Studies: Two studies were conducted:
  1. Study 1 (General Users): A within-subjects ablation study with 12 participants across three scenarios (vacation, wedding, recipe planning).
  2. Study 2 (Domain Experts): A study with 6 experts from diverse fields (education, construction, finance) performing professional planning tasks.
• Findings:
  • Perceived Value: The full system (C1) significantly outperformed ablated conditions (Soft-only, Hard-only, None) in perceived usefulness, satisfaction, and performance.
  • Distinct Roles: Users perceived hard and soft constraints as serving complementary roles: hard constraints provided a non-negotiable foundation, while soft constraints allowed for customization.
  • Rigidity vs. Flexibility: Hard-only conditions led to fewer iterations but lower satisfaction due to rigidity and latency. Soft-only conditions encouraged exploration but suffered from unreliable explanations and verification gaps.
  • Expert Challenges: Experts valued the system for managing strict rules but faced "context overhead" in recalling and inputting numerous constraints. They also noted that some professional constraints (numeric limits, calendar logic) exceeded the expressiveness of LTL.

4. Results and Significance

Technical Performance

• LTL Translation: The fine-tuned LLM achieved an average Levenshtein similarity of 83.12% against human-generated ground truth. Errors were primarily predicate-level (e.g., token mismatches) rather than logical operator errors.
• PRISM Conversion: The PRISM plan conversion achieved 97.4% similarity, with errors also occurring at the predicate level.

User Experience and Design Implications

The paper claims that U-Define successfully bridges the gap between the reliability of deterministic verification and the flexibility of generative AI. Key design implications derived from the results include:

1. Support for Mixed Constraints: Systems should allow users to explicitly distinguish between hard and soft constraints to balance reliability and personalization.
2. Actionable Explanations: Explanations for hard constraints should explicitly list violated rules rather than providing generic scalar ratings, which users found confusing for soft constraints.
3. Context Management: Future systems must assist users in reducing the cognitive overhead of constraint input (e.g., via templates, reusable profiles, or external tool integration), a critical need identified by domain experts.
4. Verification Coverage: Systems should transparently indicate when a user's constraint cannot be fully verified by the formal engine (e.g., numeric constraints) and treat those parts as heuristic checks.

Significance

The paper argues that effective planning support requires giving users control over how constraints are expressed and enforced. By placing the authority to define constraint strictness in the hands of the user and pairing it with appropriate verification mechanisms, U-Define demonstrates that it is possible to create planning systems that are both dependable (through formal verification of critical rules) and adaptable (through flexible preference handling). This approach addresses the limitations of purely template-based verification and purely generative planning, offering a pathway for more reliable human-AI collaboration in complex, real-world scenarios.