NeSy25 in Santa Cruz, and a Mario Kart run over HWY17

Trip 8 to 10 September 2025 · Written up 10 September 2025 · Last expanded 29 September 2026

The first thing I put up from Santa Cruz was not about the conference at all, it was northern Monterey Bay seen from the town, and I did not have a single word worth adding to it.

I was in town for NeSy25, the neurosymbolic AI conference, in September 2025. I missed the first day, the other two were packed, and it then took me a month to find the time to organize my notes into anything I would stand behind, which is roughly my rate for a field I am new to.

HWY17 is like playing Mario Kart

I left town during that same window anyway. Google Gemini/Cloud were running the Imagination in Action shindig over at Moffet Place, and Project NANDA: The Internet of AI Agents got me in (I had no business being there at all, since I was in California for NeSy, and I still owe them one).

Getting a ride out of Santa Cruz was nuts. HWY17 is like playing Mario Kart, and the price of that particular lap was Neal Stephenson, who I missed completely. What I got instead was an eclectic mix of technologists, VCs, artists and generally interesting people, which is not the room you walk into at an academic conference.

Make models reason, and show their work

Back at NeSy, the core idea is old enough to count as classical: combine neural representations with formal structure (logic, programs, constraints, ontologies) and you buy back data efficiency, controllability and verifiability. What struck me was the emphasis running through the talks, the posters and the industry sessions alike, which was to make models reason and make them show their work.

That second half is the part that pays my bills, since a great many of my client conversations come down to interpreting machine operations post-mortem, after the system has run and somebody senior wants to know why.

Five areas carried most of the weight. The first was LLMs with structure, where instead of treating reasoning as more tokens, sessions showed models augmented with finite-state and programlike controllers, typed memory and schema-aware retrieval, all of it aimed at predictable deduction as opposed to prompt sorcery. The second was verification in the loop, where proof obligations, constraint checks and solver feedback are moving out of after-the-fact audit and into training and inference as first-class steps. The third was knowledge graphs and ontologies, anchoring retrieval and explanation in curated schemas so an answer can be traced to known terms and relations, and disputed when it cannot be.

The fourth was trust, safety and evaluation, where out-of-distribution and length generalization work sat alongside practical robustness discussion, timely given how hard the field is pushing on reasoning models trained with RL. The fifth was early industry integration, with demos in automotive, enterprise data and scientific discovery, which is to say the domains where being wrong costs real money.

On the final day the organizers said outright that the industry side of this is still relatively early, which I appreciated hearing from the podium (as opposed to reading it in a retrospective three years from now).

Reasoning models and SOX compliance

My read, which nobody quite said out loud, is that this relatively classical field is converging with GenAI LLM methodology because the rest of the field walked into the same wall from the other side, and not because neurosymbolic methods won the argument.

The shift across 2025 has been away from bigger context windows and towards structured cognition: RL-trained reasoning LLMs, solver-augmented pipelines, and symbolic checks closing the loop on hallucinations and tool misuse. The NeSy agenda of explicit state, verifiable steps and interpretable memory fits that shift almost too neatly. Business people have started talking about reasoning models the way they used to talk about SOX compliance!

That got a laugh out of me when I wrote it down, and then it stopped being funny. Sarbanes-Oxley never made a single company honest; what it did was force records that could be checked and put a named executive’s signature on them, and an industry of controls and attestation grew up around that one requirement. Verification in the loop is the same move pointed at a model, i.e. instead of asking the system to be right, ask it to leave a trace somebody can check.

The question I carried back over the hill is that if proof obligations and constraint checks really are becoming first-class steps, somebody has to sign them, and it is not clear who.

One postscript. This was apparently the odd year the conference ran in the US instead of Europe, which makes me selfish about wanting it back. Walking around UC-Santa Cruz feels like a Tolkien Elven town, and I would take that Mario Kart run over HWY17 again for another two days of it.

Photographs

Links

The NeSy25 program and proceedings, the earlier years of proceedings I said I still need to read properly before judging the velocity of all this, and the Imagination in Action listing for the Moffet Place event. To be added.

Open entry
This page is not finished, and is not meant to be. I add photographs, people and links as I dig them out, so it keeps growing after publication. Why the whole site works this way is on the colophon.