Symbolic Reasoning

TL;DR for operators A model that is highly reliable at applying one explicit rule transition is not necessarily reliable at executing an entire procedure built from those transitions. In Reasoning Capabilities of Large Language Models. Lessons Learned from General Game Playing1, the strongest evaluated model, Gemini 2.5 Pro, achieves 95.6% exact success on one-step next-state generation. At five dependent state transitions, exact success falls to 73.4%. When the model must also choose actions during those five steps, it falls again to 65.3%. ...

TL;DR for operators A synthetic reasoning trace can end with the correct answer and still contain intermediate steps you would not want a model to imitate. ORACLE1 addresses that data-quality problem by checking reasoning one step at a time: it uses a symbolic reasoning engine when a step can be formalized, and LLM-based correctness and feasibility judgments when it cannot. ...

When Solvers Guess Smarter: Teaching SMT to Think in Functions Timeouts are where formal verification quietly loses its glamour. A team writes a specification. A solver receives the formula. Everyone expects the machine to answer a clean question: is this system safe, satisfiable, contradictory, or not? Then the solver thinks. And thinks. And returns nothing useful before the clock runs out. ...

TL;DR for operators SymbolicThought1 is a useful reminder that relationship extraction is not a vibes problem. It is a graph problem wearing a language-model costume. The paper proposes a human-in-the-loop system for extracting character relationships from narrative text. The pipeline lets an LLM propose characters and relations, then applies symbolic rules to infer missing edges, detect contradictions, retrieve supporting evidence, and ask humans to confirm or correct what matters. That is the important mechanism: the LLM is not trusted as a final judge. It is treated as a noisy extractor inside a controlled annotation workflow. ...