I really think this gets at the heart of the distinction between language as it pertains to how we connect with others and language that records our observations of the world and its history.
I think the ideal mode for engaging with LLMs should be as interactive encyclopedias. They are excellent at rewarding curiosity when someone passionate about learning sits in the driver seat of this kind of tool. There is something to be said about the benefits of _active_ learning over _passive_ instruction.
Nonetheless, it's impossible to consistently discern fact from fiction when in the form of narrative. As such hallucinations are the key counterexample for why we can't have a world where LLMs can be effective instructors. Because it's one thing to be exposed to the structure of a narrative, and to read it as grammar, but you don't ever know how to _feel_ about these structures until you become tuned to another human being.
Perfectly safe. I would argue that it is the safest of the three, the least invasive both in terms of its design and in terms of privacy.
The open source model of development has encouraged the correct incentives for people to become active in identifying and fixing possible exploits in a global, communal effort.
Every server on the cloud has (by a large margin) chosen Linux as the OS to trust specifically for this reason.
The bindings are set and have a monadic interface, but there's some abstractions that still need refining/iterating: mostly I want to be able to formalize keyboard input and eventually build a tactic framework for zero-knowledge proofs.
I've been iterating on sodium bindings in Lean4 for about four months, and now that I've gotten to Ristretto255 I can see why the author is excited about its potential. Ristretto is a tightly designed API that allows me to build arbitrary polynomials on Curve25519 and I've been having a blast tinkering and experimenting with it! If the author by chance reads this, just want to say thank you for your work!
I've been writing [libsodium](https://doc.libsodium.org/) bindings in Lean4 and have ended up using `native_decide` quite liberally, mostly as a convenience. Can any Lean devs provide a more thorough interrogation of this? Should I go back and try to scrub its usage out of my library? Logically it seems consistent with what I'm trying to do with Lean4's FFI (i.e. you really do need to explicitly trust the Lean kernel since I'm adding nontrivial computation using a foreign cryptography library) but I'm curious if this isn't necessary and whether Lean devs would push back on its use.
I'm of the opinion that formalization is the biggest bottleneck of current generation LLMs. However, I don't think that this necessarily suggests that LLMs don't benefit from formal methods. Given existing abstractions, Lean4's exceptional tooling allows for more efficient iteration with LLMs and requires less human supervision since Lean's language server provides specific and actionable feedback whenever the LLM makes a mistake. I've also noticed that LLMs can reason about code written in Lean4 far more effectively than in Python, despite Python having orders of magnitude more training data than Lean.
Nonetheless, I concur that LLMs don't yet know how to translate a request stated in a prompt to a complete Lean4 interpretation. My practice so far has usually required me to first choose an existing reference file that is similar to my desired goals, and use this reference as "inspiration" for how the LLM should go about formalization.
As a playwright, I've certainly thought about AI impacting the art. In fact, it was the very eloquence of chatgpt's output that initiated all of this mania in the first place: not only was chatgpt able to explain to me gauge theory with surprising accuracy, it was able to do so using perfect Elizabethan english—exactly as I had instructed it to.
There is a missing ingredient that LLMs lack, however. They lack insight. Writing is made engaging by the promise of insight teased in its setups, the depths that are dug through its payoffs, and the revelations found in its conclusion. It requires solving an abstract sudoku puzzle where each sentence builds on something prior and, critically, advances an agenda toward an emotional conclusion. This is the rhetoric inherent to all storytelling, but just as in a good political speech or debate, everything hinges on the quality of the central thesis—the key insight that LLMs do not come equipped to provide on their own.
This is hard. Insight is hard. And an AI supporter would gladly tell you "yes! this is where prompting becomes art!" And perhaps there is merit to this, or at least there is merit insofar as Sam Altman's dreams of AI producing novel insights remain unfulfilled. This condition notwithstanding, what merit exactly do these supporters have? Has prompting become an art the same way that it has become engineering? It would seem AlphaWrite would like to say so.
But let's look at this rubric and evaluate for ourselves what else AlphaWrite would like to say:
```python
# Fallback to a basic rubric if file not found
return """Creative writing evaluation should consider:
1. Creativity and Originality (25%) - Unique ideas, fresh perspectives, innovative storytelling
2. Writing Quality (25%) - Grammar, style, flow, vocabulary, sentence structure
3. Engagement (20%) - How compelling and interesting the piece is to read
4. Character Development (15%) - Believable, well-developed characters with clear motivations
5. Plot Structure (15%) - Logical progression, pacing, resolution of conflicts"""
```
It's certainly just a default, and I mean no bad faith in using this for rhetorical effect, but this default also acts as a template, and it happens to be informative to my point. Insight, genuine insight, is hard because it is contingent on one's audience and one's shared experiences with them. It isn't enough to check boxes. Might I ask what makes for a better story: a narrative about a well developed princess who provides fresh perspectives on antiquated themes, or a narrative about a well developed stock broker who provides fresh perspectives on contemporary themes? The output fails to find its audience no matter what your rubric is.
And here lies the dilemma regarding the idea that prompts are an art: they are not. The prompts are not art by the simple fact that nobody will read them. What is read is what all that is communicated and any discerning audience will be alienated by anything generated by something as ambiguous as a English teacher's grading rubric.
I write because I want to communicate my insights to an audience who I believe would be influenced by them. I may be early in my career, but this is why I do it. The degree of influence I shall have measures the degree of "art" I shall attain. Not by whether or not I clear the minimum bar of literacy.