5 ms·
Show HN: I'm 6 months late, but I made a Natural Language theorem prover
- ArnavAgrawal03 2y agoLast year, I built a theorem prover in Ocaml for propositional logic: https://github.com/ArnavAgrawal03/ProveML https://github.com/ArnavAgrawal03/ProveML. After the release of structured outputs, I thought it would be fun to see if we could turn natural language into propositional logic statements and use the theorem prover to answer queries more deterministically. In my limited testing, this actually works really well! I feel there's a lot of potential in employing LLMs as a "frontend" for more deterministic backends (such as theorem provers). Would love to hear your thoughts - would you use something like this if deployed to production with wider support and nice APIs? I'm also interested in thinking of this as an alternative to regular RAG or knowledge graphs - though using a resolution-refutation based theorem prover would make retrieval a lot more expensive
- deleted 2y ago[deleted]
- doormatt 2y agoYour OpenAI Key is still visible in the commit history.
- ArnavAgrawal03 2y agoyep it's been defunct for a while now tho - so no point removing it